X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FBackend%2Fconstraint.cc;fp=src%2FBackend%2Fconstraint.cc;h=6425c58b6ab7ee554dca680369e4fb2ac338c614;hp=b35b45602efb98e76f2739e5a9cdbd934e6bc06e;hb=cb27924ba5a3ef99d44a1e0cbdd43906b2a28d61;hpb=7c07450f8c8a3878de97508054a1399aa6d761f1

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index b35b456..6425c58 100644
--- a/src/Backend/constraint.cc
+++ b/src/Backend/constraint.cc
@@ -575,6 +575,9 @@ Edge simplifyCNF(CNF *cnf, Edge input) {
 
 void addClause(CNF *cnf, uint numliterals, int *literals){
 	cnf->clausecount++;
+	for(uint i=0; i< numliterals; i++)
+		model_print("%d ", literals[i]);
+	model_print("\n");
 	addArrayClauseLiteral(cnf->solver, numliterals, literals);
 }
 
@@ -640,17 +643,23 @@ void generateProxy(CNF *cnf, Edge expression, Edge proxy, Polarity p) {
 	if (p == P_TRUE || p == P_BOTHTRUEFALSE) {
 		// proxy => expression
 		Edge cnfexpr = simplifyCNF(cnf, expression);
+		Edge cnfnegexpr = simplifyCNF(cnf, constraintNegate(expression));
 		if (p == P_TRUE)
 			freeEdgeRec(expression);
 		outputCNFOR(cnf, cnfexpr, constraintNegate(proxy));
+		outputCNFOR(cnf, cnfnegexpr, proxy);
 		freeEdgeCNF(cnfexpr);
+		freeEdgeCNF(cnfnegexpr);
 	}
 	if (p == P_FALSE || p == P_BOTHTRUEFALSE) {
 		// expression => proxy
 		Edge cnfnegexpr = simplifyCNF(cnf, constraintNegate(expression));
+		Edge cnfexpr = simplifyCNF(cnf, expression);
 		freeEdgeRec(expression);
 		outputCNFOR(cnf, cnfnegexpr, proxy);
+		outputCNFOR(cnf, cnfexpr, constraintNegate(proxy));
 		freeEdgeCNF(cnfnegexpr);
+		freeEdgeCNF(cnfexpr);
 	}
 }