edits

diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c
index be406eb946cd49a2cc06a32958f30f15c8377780..75a5dfbb486d322725c820dfaf2ef19ebdbc3103 100644 (file)
--- a/src/Backend/nodeedge.c
+++ b/src/Backend/nodeedge.c
@@ -306,8 +306,8 @@ void countConstraint(CNF *cnf, VectorEdge *stack, Edge e) {
                                n->intAnnot[polarity]++;
                        }
                } else {
-                       setExpanded(n, polarity); n->intAnnot[polarity]=1;
-                       
+                       setExpanded(n, polarity);
+
                        if (n->flags.type == NodeType_ITE||
                                        n->flags.type == NodeType_IFF) {
                                n->intAnnot[polarity]=0;
@@ -336,6 +336,7 @@ void countConstraint(CNF *cnf, VectorEdge *stack, Edge e) {
                                        n2->ptrAnnot[1]=succ1.node_ptr;
                                } 
                        } else {
+                               n->intAnnot[polarity]=1;
                                for (uint i=0;i<n->numEdges;i++) {
                                        Edge succ=n->edges[i];
                                        succ=constraintNegateIf(succ, polarity);
@@ -369,8 +370,10 @@ void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit
                        //trivally unsat
                        Edge newvar=constraintNewVar(cnf);
                        Literal var=getEdgeVar(newvar);
-                       Literal clause[] = {var, -var};
-                       addArrayClauseLiteral(cnf->solver, 2, clause);
+                       Literal clause[] = {var};
+                       addArrayClauseLiteral(cnf->solver, 1, clause);
+                       clause[0]=-var;
+                       addArrayClauseLiteral(cnf->solver, 1, clause);
                        return;
                } else {
                        //trivially true
@@ -393,18 +396,20 @@ void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit
                } else if (n->flags.type==NodeType_ITE ||
                                                         n->flags.type==NodeType_IFF) {
                        popVectorEdge(stack);
-                       pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]});
-                       pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[1]});
+                       if (n->ptrAnnot[0]!=NULL)
+                               pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]});
+                       if (n->ptrAnnot[1]!=NULL)
+                               pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[1]});
                        continue;
                }
 
                bool needPos = (n->intAnnot[0] > 0);
                bool needNeg = (n->intAnnot[1] > 0);
-               if ((!needPos || n->flags.cnfVisitedUp & 1) ||
+               if ((!needPos || n->flags.cnfVisitedUp & 1) &&
                                (!needNeg || n->flags.cnfVisitedUp & 2)) {
                        popVectorEdge(stack);
-               } else if ((needPos && !n->flags.cnfVisitedDown & 1) ||
-                                                        (needNeg && !n->flags.cnfVisitedDown & 2)) {
+               } else if ((needPos && !(n->flags.cnfVisitedDown & 1)) ||
+                                                        (needNeg && !(n->flags.cnfVisitedDown & 2))) {
                        if (needPos)
                                n->flags.cnfVisitedDown|=1;
                        if (needNeg)
@@ -421,15 +426,19 @@ void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit
        }
        CNFExpr * cnfExp = (CNFExpr *) nroot->ptrAnnot[isNegEdge(root)];
        if (isProxy(cnfExp)) {
-               //solver.add(getProxy(cnfExp))
+               Literal l=getProxy(cnfExp);
+               Literal clause[] = {l};
+               addArrayClauseLiteral(cnf->solver, 1, clause);
        } else if (backtrackLit) {
-               //solver.add(introProxy(solver, root, cnfExp, isNegEdge(root)));
+               Literal l=introProxy(cnf, root, cnfExp, isNegEdge(root));
+               Literal clause[] = {l};
+               addArrayClauseLiteral(cnf->solver, 1, clause);
        } else {
-               //solver.add(*cnfExp);
+               outputCNF(cnf, cnfExp);
        }
 
        if (!((intptr_t) cnfExp & 1)) {
-               //free rootExp
+               deleteCNFExpr(cnfExp);
                nroot->ptrAnnot[isNegEdge(root)] = NULL;
        }
 }
@@ -472,7 +481,6 @@ Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg) {
        return l;
 }
 
-//DONE
 void produceCNF(CNF * cnf, Edge e) {
        CNFExpr* expPos = NULL;
        CNFExpr* expNeg = NULL;

diff --git a/src/Backend/nodeedge.h b/src/Backend/nodeedge.h
index bc0eb5cec3fe55530147a09e55f064dd7be03373..7933bf8b57b70704764c0c953c594e4eaef36ed0 100644 (file)
--- a/src/Backend/nodeedge.h
+++ b/src/Backend/nodeedge.h
@@ -147,6 +147,10 @@ static inline bool edgeIsConst(Edge e) {
        return (((uintptr_t) e.node_ptr) & ~((uintptr_t)NEGATE_EDGE)) == EDGE_IS_VAR_CONSTANT;
 }
 
+static inline bool edgeIsNull(Edge e) {
+       return e.node_ptr == NULL;
+}
+
 static inline bool edgeIsVarConst(Edge e) {
        return ((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT;
 }
@@ -192,6 +196,8 @@ CNFExpr* produceDisjunction(CNF *cnf, Edge e);
 bool propagate(CNF *cnf, CNFExpr * dest, CNFExpr * src, bool negate);
 void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign);
 CNFExpr* fillArgs(CNF * cnf, Edge e, bool isNeg, Edge * largestEdge);
+Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg);
+void outputCNF(CNF *cnf, CNFExpr *expr);
 
 Edge E_True={(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};
 Edge E_False={(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};