Bug fixes

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index c9a47f95df93338e6a824975a78915fe50c76572..207b327bf693182d4d06a7ded3b4849aa913b367 100644 (file)
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -23,7 +23,7 @@ public:
        BooleanValue boolVal;
        Vector<Boolean *> parents;
        virtual void updateParents() {}
-
+       
        CMEMALLOC;
 };
 

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index 8bcb1e9838ae010975f1b5defeddba059e43c7bc..f716ccec274ec786c2c6545888af26fb63cd2a3c 100644 (file)
--- a/src/Backend/constraint.cc
+++ b/src/Backend/constraint.cc
@@ -116,6 +116,21 @@ void freeEdgeRec(Edge e) {
        for(uint i=0; i < numEdges; i++) {
                freeEdgeRec(node->edges[i]);
        }
+       ourfree(node);
+}
+
+void freeEdge(Edge e) {
+       if (edgeIsVarConst(e))
+               return;
+       Node * node = getNodePtrFromEdge(e);
+       ourfree(node);
+}
+
+void freeEdgesRec(uint numEdges, Edge * earray) {
+       for(uint i=0; i < numEdges; i++) {
+               Edge e = earray[i];
+               freeEdgeRec(e);
+       }
 }
 
 void freeEdgeCNF(Edge e) {
@@ -238,8 +253,10 @@ Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
                return E_True;
        else if (remainSize == 1)
                return edges[initindex];
-       else if (equalsEdge(edges[initindex], E_False))
+       else if (equalsEdge(edges[initindex], E_False)) {
+               freeEdgesRec(numEdges, edges);
                return E_False;
+       }
 
        /** De-duplicate array */
        uint lowindex = 0;
@@ -249,7 +266,10 @@ Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
                Edge e1 = edges[lowindex];
                Edge e2 = edges[initindex];
                if (sameNodeVarEdge(e1, e2)) {
+                       ASSERT(!isNodeEdge(e1));
                        if (!sameSignEdge(e1, e2)) {
+                               freeEdgesRec(lowindex + 1, edges);
+                               freeEdgesRec(numEdges-initindex, &edges[initindex]);
                                return E_False;
                        }
                } else
@@ -269,13 +289,25 @@ Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
                Edge *e0edges = getEdgeArray(edges[0]);
                Edge *e1edges = getEdgeArray(edges[1]);
                if (sameNodeOppSign(e0edges[0], e1edges[0])) {
-                       return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
+                       Edge result=constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
+                       freeEdge(edges[0]);
+                       freeEdge(edges[1]);
+                       return result;
                } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
-                       return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
+                       Edge result=constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
+                       freeEdge(edges[0]);
+                       freeEdge(edges[1]);
+                       return result;
                } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
-                       return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
+                       Edge result=constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
+                       freeEdge(edges[0]);
+                       freeEdge(edges[1]);
+                       return result;
                } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
-                       return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
+                       Edge result=constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
+                       freeEdge(edges[0]);
+                       freeEdge(edges[1]);
+                       return result;
                }
        }
 
@@ -302,6 +334,8 @@ Edge constraintIFF(CNF *cnf, Edge left, Edge right) {
 
        Edge e;
        if (equalsEdge(lpos, rpos)) {
+               freeEdgeRec(left);
+               freeEdgeRec(right);
                e = E_True;
        } else if (ltEdge(lpos, rpos)) {
                Edge edges[] = {lpos, rpos};
@@ -331,16 +365,18 @@ Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) {
 
        Edge result;
        if (equalsEdge(cond, E_True)) {
+               freeEdgeRec(elseedge);
                result = thenedge;
        } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
                Edge array[] = {cond, elseedge};
                result = constraintOR(cnf,  2, array);
        } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
                result = constraintIMPLIES(cnf, cond, thenedge);
-       } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) {
+       } else if (equalsEdge(elseedge, E_False) || equalsEdge(cond, elseedge)) {
                Edge array[] = {cond, thenedge};
                result = constraintAND(cnf, 2, array);
        } else if (equalsEdge(thenedge, elseedge)) {
+               freeEdgeRec(cond);
                result = thenedge;
        } else if (sameNodeOppSign(thenedge, elseedge)) {
                if (ltEdge(cond, thenedge)) {
@@ -529,6 +565,37 @@ Edge simplifyCNF(CNF *cnf, Edge input) {
        }
 }
 
+void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar) {
+       Node * andNode = cnfform.node_ptr;
+       int orvar = getEdgeVar(eorvar);
+       ASSERT(orvar != 0);
+       uint numEdges = andNode->numEdges;
+       for(uint i=0; i < numEdges; i++) {
+               Edge e = andNode->edges[i];
+               if (edgeIsVarConst(e)) {
+                       int array[2] = {getEdgeVar(e), orvar};
+                       ASSERT(array[0] != 0);
+                       addArrayClauseLiteral(cnf->solver, 2, array);
+               } else {
+                       Node * clause = e.node_ptr;
+                       uint cnumEdges = clause->numEdges + 1;
+                       if (cnumEdges > cnf->asize) {
+                               cnf->asize = cnumEdges << 1;
+                               ourfree(cnf->array);
+                               cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
+                       }
+                       int * array = cnf->array;
+                       for(uint j=0; j < (cnumEdges - 1); j++) {
+                               array[j] = getEdgeVar(clause->edges[j]);
+                               ASSERT(array[j] != 0);
+                       }
+                       array[cnumEdges - 1] = orvar;
+                       addArrayClauseLiteral(cnf->solver, cnumEdges, array);
+               }
+       }
+}
+
+
 void outputCNF(CNF *cnf, Edge cnfform) {
        Node * andNode = cnfform.node_ptr;
        uint numEdges = andNode->numEdges;
@@ -556,23 +623,45 @@ void outputCNF(CNF *cnf, Edge cnfform) {
        }
 }
 
+void generateProxy(CNF *cnf, Edge expression, Edge proxy, Polarity p) {
+       if (P_TRUE || P_BOTHTRUEFALSE) {
+               // proxy => expression
+               Edge cnfexpr = simplifyCNF(cnf, expression);
+               freeEdgeRec(expression);
+               outputCNFOR(cnf, cnfexpr, constraintNegate(proxy));
+               freeEdgeCNF(cnfexpr);
+       }
+       if (P_FALSE || P_BOTHTRUEFALSE) {
+               // expression => proxy
+               Edge cnfnegexpr = simplifyCNF(cnf, constraintNegate(expression));
+               freeEdgeRec(expression);
+               outputCNFOR(cnf, cnfnegexpr, proxy);
+               freeEdgeCNF(cnfnegexpr);
+       }
+}
+
 void addConstraintCNF(CNF *cnf, Edge constraint) {
-       if (equalsEdge(constraint, E_True))
+       if (equalsEdge(constraint, E_True)) {
                return;
-       else if (equalsEdge(constraint, E_False)) {
+       } else if (equalsEdge(constraint, E_False)) {
                cnf->unsat = true;
                return;
        }
+       if (cnf->unsat) {
+               freeEdgeRec(constraint);
+               return;
+       }
 
-       Edge cnfform = simplifyCNF(cnf, constraint);
-       freeEdgeRec(constraint);
-       outputCNF(cnf, cnfform);
-       freeEdgeCNF(cnfform);
-#ifdef CONFIG_DEBUG
+#if 0
        model_print("****SATC_ADDING NEW Constraint*****\n");
        printCNF(constraint);
        model_print("\n******************************\n");
 #endif
+       
+       Edge cnfform = simplifyCNF(cnf, constraint);
+       freeEdgeRec(constraint);
+       outputCNF(cnf, cnfform);
+       freeEdgeCNF(cnfform);
 }
 
 Edge constraintNewVar(CNF *cnf) {

diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h
index 2dd6d8e3d8f18e39999e0580b83f464ebaef7b2f..adcd3f1836688b57841429c0b87473f5fc4dd6cb 100644 (file)
--- a/src/Backend/constraint.h
+++ b/src/Backend/constraint.h
@@ -176,6 +176,9 @@ void addEdgeToResizeNode(Node ** node, Edge e);
 void mergeFreeNodeToResizeNode(Node **node, Node * innode);
 void mergeNodeToResizeNode(Node **node, Node * innode);
 void freeEdgeRec(Edge e);
+void outputCNF(CNF *cnf, Edge cnfform);
+void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar);
+void generateProxy(CNF *cnf, Edge expression, Edge proxy, Polarity p);
 
 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);
 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index 44e3e63795103d06574a3aa645b6c2eb71a95bcd..b6e8da1f515741a35d7bd4302ceb11ec70212609 100644 (file)
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -68,7 +68,13 @@ Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) {
                model_print("Unhandled case in encodeConstraintSATEncoder %u", constraint->type);
                exit(-1);
        }
-       booledgeMap.put(constraint, result.node_ptr);
+       if (constraint->parents.getSize() > 1) {
+               Edge e = getNewVarSATEncoder();
+               generateProxy(cnf, result, e, constraint->polarity);
+               booledgeMap.put(constraint, e.node_ptr);
+               result = e;
+       }
+
        return c.isNegated() ? constraintNegate(result) : result;
 }
 
@@ -99,6 +105,7 @@ Edge SATEncoder::encodeLogicSATEncoder(BooleanLogic *constraint) {
        case SATC_NOT:
                return constraintNegate(array[0]);
        case SATC_IFF:
+               ASSERT(constraint->inputs.getSize() == 2);
                return constraintIFF(cnf, array[0], array[1]);
        case SATC_OR:
        case SATC_XOR:

diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc
index f4eda5240d69c401d2a47ec0cd0474199103c837..987f2022604e8184bead56219c6e7d5c44de883b 100644 (file)
--- a/src/Backend/satfuncopencoder.cc
+++ b/src/Backend/satfuncopencoder.cc
@@ -57,6 +57,7 @@ Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constra
                        }
                        Edge term = constraintAND(cnf, numDomains, carray);
                        pushVectorEdge(clauses, term);
+                       ASSERT(getSizeVectorEdge(clauses) > 0);
                }
 
                notfinished = false;
@@ -75,7 +76,6 @@ Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constra
                }
        }
        if (getSizeVectorEdge(clauses) == 0) {
-               clearVectorEdge(clauses);
                return E_False;
        }
        Edge cor = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));