Commiting my local changes ...

[satune.git] / src / Backend / constraint.cc

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index b35b45602efb98e76f2739e5a9cdbd934e6bc06e..6425c58b6ab7ee554dca680369e4fb2ac338c614 100644 (file)
--- 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);
        }
 }