//
// An example of using LCF.ifThen 
//
// If v1 = 2 then v2 > 4
// i.e. v1 = 2 -> v2 > 4
//
// NOTE: A -> B = ¬A v B
//
import java.io.*;
import java.util.*;
import org.chocosolver.solver.Model;
import org.chocosolver.solver.Solver;
import org.chocosolver.solver.variables.IntVar;
import org.chocosolver.solver.constraints.IIntConstraintFactory.*;
import org.chocosolver.solver.constraints.IReificationFactory.*;
import org.chocosolver.solver.constraints.Constraint;
import org.chocosolver.solver.search.strategy.Search;
import org.chocosolver.solver.exception.ContradictionException;

public class IFTHEN {
    
    public static void main(String args[]) throws ContradictionException {
	Model model = new Model("IFTHEN");
	Solver solver = model.getSolver();
	IntVar v1 = model.intVar("v1",0,6);
	IntVar v2 = model.intVar("v2",0,6);
	
	Constraint c1 = model.arithm(v1,"=",2);
	Constraint c2 = model.arithm(v2,">",4);
	
	model.ifThen(c1,c2); // NOTE: not posted

	//
	// NOTE: could have said ...
	// model.ifThen(model.arithm(v1,"=",v2),model.arithm(v2,">",4));
	//
	
	//System.out.println(c1 +" "+ c2);
	
	// model.arithm(v1,"<=",v2).post();

	//System.out.println(model);
	
	solver.propagate();
	System.out.println(v1 +" "+ v2);
      
	solver.setSearch(Search.inputOrderLBSearch(v1,v2));
	while(solver.solve())
	    System.out.println("["+v1.getValue() +" : "+ v2.getValue() +"]");
    }
}
//
// NOTE: needed the imports ...
// import org.chocosolver.solver.constraints.IReificationFactory.*;
// import org.chocosolver.solver.constraints.Constraint;
//