import choco.Problem;
import choco.Constraint;
import choco.Solver;
import choco.Solution;
import choco.ContradictionException;
import choco.integer.*;
import choco.integer.search.DecreasingDomain;
import choco.search.*;
import choco.search.AbstractGlobalSearchSolver;
import choco.search.AbstractGlobalSearchLimit;
import choco.integer.search.*;
import java.io.*;
import java.lang.*;
import java.util.*;

public class Max {	
   

    public static void main(String[] args) throws Exception,ContradictionException,FileNotFoundException,IOException {
	
	int noFiles = args.length;
	long ms1 = System.currentTimeMillis();
	Dict d = new Dict();
	Tree t1 = new Tree(args[0],d);
	Tree t2 = new Tree(args[1],d);

	Problem pb = new Problem();
	int m = d.size();

	UMatrix um = new UMatrix(m-1,pb,d,false);

	t1.softBreakUp(um);
	t2.softBreakUp(um);

	if (noFiles == 3){
	    MyIo fin = new MyIo(args[2]);
	    while (fin.hasMoreData()){
		String v = fin.getNextString();
		String w = fin.getNextString();
		String x = fin.getNextString();
		String y = fin.getNextString();
		um.predates(v,w,x,y);
	    }
	}

	// um.postTriples();

	IntDomainVar D[] = um.getOptVars();
	int n = um.numbConstraints();
	IntDomainVar nc = pb.makeBoundIntVar("number of constraints",0,n);
	
	pb.post(pb.eq(nc,pb.sum(D)));
	Solver s = pb.getSolver();
	s.setVarSelector(new VarOrder(D)); 
	s.setValIterator(new DecreasingDomain());

	long ms2 = System.currentTimeMillis();	
	//pb.maximize(nc,true);
	boolean solved = pb.solve(false);
	long ms3 = System.currentTimeMillis();

	if (solved){
	    Tree t3 = um.toTree();
	    System.out.println(t3);
	}
	else
	    System.out.println("();");
	
	ArrayList A = um.getTriples();
	for (int i=0;i<A.size();i++){
	    Triple t = (Triple)A.get(i);
	    IntDomainVar v = t.getVar();
	    if (v.getVal() == 0) System.out.println(t.look());
	}

	System.out.println("model: " + (ms2-ms1) + "ms   " + "solve: " + (ms3-ms2) + "ms" );
	AbstractGlobalSearchLimit S = (AbstractGlobalSearchLimit)s.getSearchSolver().limits.get(1);
	int nds = S.getNbTot();
	System.out.println("nodes: " + nds + " " + nc.pretty() + " n = " + n);
    }
}