edits
authorBrian Demsky <bdemsky@uci.edu>
Mon, 8 Jan 2018 23:44:47 +0000 (15:44 -0800)
committerBrian Demsky <bdemsky@uci.edu>
Mon, 8 Jan 2018 23:44:47 +0000 (15:44 -0800)
src/Backend/constraint.cc
src/Backend/constraint.h

index 386706d..390b831 100644 (file)
@@ -2,7 +2,6 @@
 #include <string.h>
 #include <stdlib.h>
 #include "inc_solver.h"
-#include "cnfexpr.h"
 #include "common.h"
 #include "qsort.h"
 /*
 VectorImpl(Edge, Edge, 16)
 Edge E_True = {(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};
 Edge E_False = {(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};
-Edge E_BOGUS = {(Node *)0x12345673};
+Edge E_BOGUS = {(Node *)0xffff5673};
 Edge E_NULL = {(Node *)NULL};
 
 
 CNF *createCNF() {
        CNF *cnf = (CNF *) ourmalloc(sizeof(CNF));
        cnf->varcount = 1;
-       cnf->capacity = DEFAULT_CNF_ARRAY_SIZE;
-       cnf->mask = cnf->capacity - 1;
-       cnf->node_array = (Node **) ourcalloc(1, sizeof(Node *) * cnf->capacity);
-       cnf->size = 0;
-       cnf->maxsize = (uint)(((double)cnf->capacity) * LOAD_FACTOR);
-       cnf->enableMatching = true;
-       initDefVectorEdge(&cnf->constraints);
-       initDefVectorEdge(&cnf->args);
        cnf->solver = allocIncrementalSolver();
        cnf->solveTime = 0;
        cnf->encodeTime = 0;
@@ -66,130 +57,29 @@ CNF *createCNF() {
 }
 
 void deleteCNF(CNF *cnf) {
-       for (uint i = 0; i < cnf->capacity; i++) {
-               Node *n = cnf->node_array[i];
-               if (n != NULL)
-                       ourfree(n);
-       }
-       deleteVectorArrayEdge(&cnf->constraints);
-       deleteVectorArrayEdge(&cnf->args);
        deleteIncrementalSolver(cnf->solver);
-       ourfree(cnf->node_array);
        ourfree(cnf);
 }
 
 void resetCNF(CNF *cnf) {
-       for (uint i = 0; i < cnf->capacity; i++) {
-               Node *n = cnf->node_array[i];
-               if (n != NULL)
-                       ourfree(n);
-       }
-       clearVectorEdge(&cnf->constraints);
-       clearVectorEdge(&cnf->args);
        resetSolver(cnf->solver);
-       memset(cnf->node_array, 0, sizeof(Node *) * cnf->capacity);
-
        cnf->varcount = 1;
-       cnf->size = 0;
-       cnf->enableMatching = true;
        cnf->solveTime = 0;
        cnf->encodeTime = 0;
 }
 
-void resizeCNF(CNF *cnf, uint newCapacity) {
-       Node **old_array = cnf->node_array;
-       Node **new_array = (Node **) ourcalloc(1, sizeof(Node *) * newCapacity);
-       uint oldCapacity = cnf->capacity;
-       uint newMask = newCapacity - 1;
-       for (uint i = 0; i < oldCapacity; i++) {
-               Node *n = old_array[i];
-               if (n == NULL)
-                       continue;
-               uint hashCode = n->hashCode;
-               uint newindex = hashCode & newMask;
-               for (;; newindex = (newindex + 1) & newMask) {
-                       if (new_array[newindex] == NULL) {
-                               new_array[newindex] = n;
-                               break;
-                       }
-               }
-       }
-       ourfree(old_array);
-       cnf->node_array = new_array;
-       cnf->capacity = newCapacity;
-       cnf->maxsize = (uint)(((double)cnf->capacity) * LOAD_FACTOR);
-       cnf->mask = newMask;
-}
-
-Node *allocNode(NodeType type, uint numEdges, Edge *edges, uint hashcode) {
+Node *allocNode(NodeType type, uint numEdges, Edge *edges) {
        Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
        memcpy(n->edges, edges, sizeof(Edge) * numEdges);
-       n->flags.type = type;
-       n->flags.wasExpanded = 0;
-       n->flags.cnfVisitedDown = 0;
-       n->flags.cnfVisitedUp = 0;
-       n->flags.varForced = 0;
        n->numEdges = numEdges;
-       n->hashCode = hashcode;
-       n->intAnnot[0] = 0;n->intAnnot[1] = 0;
-       n->ptrAnnot[0] = NULL;n->ptrAnnot[1] = NULL;
        return n;
 }
 
 Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge *edges) {
-       if (cnf->size > cnf->maxsize) {
-               resizeCNF(cnf, cnf->capacity << 1);
-       }
-       uint hashvalue = hashNode(type, numEdges, edges);
-       uint mask = cnf->mask;
-       uint index = hashvalue & mask;
-       Node **n_ptr;
-       for (;; index = (index + 1) & mask) {
-               n_ptr = &cnf->node_array[index];
-               if (*n_ptr != NULL) {
-                       if ((*n_ptr)->hashCode == hashvalue) {
-                               if (compareNodes(*n_ptr, type, numEdges, edges)) {
-                                       Edge e = {*n_ptr};
-                                       return e;
-                               }
-                       }
-               } else {
-                       break;
-               }
-       }
-       *n_ptr = allocNode(type, numEdges, edges, hashvalue);
-       cnf->size++;
-       Edge e = {*n_ptr};
+       Edge e = {allocNode(type, numEdges, edges)};
        return e;
 }
 
-uint hashNode(NodeType type, uint numEdges, Edge *edges) {
-       uint hash = type;
-       hash += hash << 10;
-       hash ^= hash >> 6;
-       for (uint i = 0; i < numEdges; i++) {
-               uint c = (uint) ((uintptr_t) edges[i].node_ptr);
-               hash += c;
-               hash += hash << 10;
-               hash += hash >> 6;
-       }
-       hash += hash << 3;
-       hash ^= hash >> 11;
-       hash += hash << 15;
-       return hash;
-}
-
-bool compareNodes(Node *node, NodeType type, uint numEdges, Edge *edges) {
-       if (node->flags.type != type || node->numEdges != numEdges)
-               return false;
-       Edge *nodeedges = node->edges;
-       for (uint i = 0; i < numEdges; i++) {
-               if (!equalsEdge(nodeedges[i], edges[i]))
-                       return false;
-       }
-       return true;
-}
-
 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges) {
        Edge edgearray[numEdges];
 
@@ -251,7 +141,7 @@ Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
        if (lowindex == 1)
                return edges[0];
 
-       if (cnf->enableMatching && lowindex == 2 &&
+       if (lowindex == 2 &&
                        isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
                        getNodeType(edges[0]) == NodeType_AND &&
                        getNodeType(edges[1]) == NodeType_AND &&
@@ -351,7 +241,7 @@ Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) {
 }
 
 void addConstraintCNF(CNF *cnf, Edge constraint) {
-       pushVectorEdge(&cnf->constraints, constraint);
+       //      pushVectorEdge(&cnf->constraints, constraint);
 #ifdef CONFIG_DEBUG
        model_print("****SATC_ADDING NEW Constraint*****\n");
        printCNF(constraint);
@@ -367,8 +257,6 @@ Edge constraintNewVar(CNF *cnf) {
 
 int solveCNF(CNF *cnf) {
        long long startTime = getTimeNano();
-       countPass(cnf);
-       convertPass(cnf, false);
        finishedClauses(cnf->solver);
        long long startSolve = getTimeNano();
        int result = solve(cnf->solver);
@@ -387,367 +275,6 @@ bool getValueCNF(CNF *cnf, Edge var) {
        return isneg ^ getValueSolver(cnf->solver, l);
 }
 
-void countPass(CNF *cnf) {
-       uint numConstraints = getSizeVectorEdge(&cnf->constraints);
-       VectorEdge *ve = allocDefVectorEdge();
-       for (uint i = 0; i < numConstraints; i++) {
-               countConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i));
-       }
-       deleteVectorEdge(ve);
-}
-
-void countConstraint(CNF *cnf, VectorEdge *stack, Edge eroot) {
-       //Skip constants and variables...
-       if (edgeIsVarConst(eroot))
-               return;
-
-       clearVectorEdge(stack);pushVectorEdge(stack, eroot);
-
-       bool isMatching = cnf->enableMatching;
-
-       while (getSizeVectorEdge(stack) != 0) {
-               Edge e = lastVectorEdge(stack); popVectorEdge(stack);
-               bool polarity = isNegEdge(e);
-               Node *n = getNodePtrFromEdge(e);
-               if (getExpanded(n,  polarity)) {
-                       if (n->flags.type == NodeType_IFF ||
-                                       n->flags.type == NodeType_ITE) {
-                               Edge pExp = {(Node *)n->ptrAnnot[polarity]};
-                               getNodePtrFromEdge(pExp)->intAnnot[0]++;
-                       } else {
-                               n->intAnnot[polarity]++;
-                       }
-               } else {
-                       setExpanded(n, polarity);
-
-                       if (n->flags.type == NodeType_ITE ||
-                                       n->flags.type == NodeType_IFF) {
-                               n->intAnnot[polarity] = 0;
-                               Edge cond = n->edges[0];
-                               Edge thenedge = n->edges[1];
-                               Edge elseedge = n->flags.type == NodeType_IFF ? constraintNegate(thenedge) : n->edges[2];
-                               thenedge = constraintNegateIf(thenedge, !polarity);
-                               elseedge = constraintNegateIf(elseedge, !polarity);
-                               thenedge = constraintAND2(cnf, cond, thenedge);
-                               cond = constraintNegate(cond);
-                               elseedge = constraintAND2(cnf, cond, elseedge);
-                               thenedge = constraintNegate(thenedge);
-                               elseedge = constraintNegate(elseedge);
-                               cnf->enableMatching = false;
-                               Edge succ1 = constraintAND2(cnf, thenedge, elseedge);
-                               n->ptrAnnot[polarity] = succ1.node_ptr;
-                               cnf->enableMatching = isMatching;
-                               pushVectorEdge(stack, succ1);
-                               if (getExpanded(n, !polarity)) {
-                                       Edge succ2 = {(Node *)n->ptrAnnot[!polarity]};
-                                       Node *n1 = getNodePtrFromEdge(succ1);
-                                       Node *n2 = getNodePtrFromEdge(succ2);
-                                       n1->ptrAnnot[0] = succ2.node_ptr;
-                                       n2->ptrAnnot[0] = succ1.node_ptr;
-                                       n1->ptrAnnot[1] = succ2.node_ptr;
-                                       n2->ptrAnnot[1] = succ1.node_ptr;
-                               }
-                       } else {
-                               n->intAnnot[polarity] = 1;
-                               for (uint i = 0; i < n->numEdges; i++) {
-                                       Edge succ = n->edges[i];
-                                       if (!edgeIsVarConst(succ)) {
-                                               succ = constraintNegateIf(succ, polarity);
-                                               pushVectorEdge(stack, succ);
-                                       }
-                               }
-                       }
-               }
-       }
-}
-
-void convertPass(CNF *cnf, bool backtrackLit) {
-       uint numConstraints = getSizeVectorEdge(&cnf->constraints);
-       VectorEdge *ve = allocDefVectorEdge();
-       for (uint i = 0; i < numConstraints; i++) {
-               convertConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i), backtrackLit);
-       }
-       deleteVectorEdge(ve);
-}
-
-void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit) {
-       Node *nroot = getNodePtrFromEdge(root);
-
-       if (isNodeEdge(root) && (nroot->flags.type == NodeType_ITE || nroot->flags.type == NodeType_IFF)) {
-               nroot = (Node *) nroot->ptrAnnot[isNegEdge(root)];
-               root = (Edge) { nroot };
-       }
-       if (edgeIsConst(root)) {
-               if (isNegEdge(root)) {
-                       //trivally unsat
-                       Edge newvar = constraintNewVar(cnf);
-                       Literal var = getEdgeVar(newvar);
-                       Literal clause[] = {var};
-                       addArrayClauseLiteral(cnf->solver, 1, clause);
-                       clause[0] = -var;
-                       addArrayClauseLiteral(cnf->solver, 1, clause);
-                       return;
-               } else {
-                       //trivially true
-                       return;
-               }
-       } else if (edgeIsVarConst(root)) {
-               Literal clause[] = { getEdgeVar(root)};
-               addArrayClauseLiteral(cnf->solver, 1, clause);
-               return;
-       }
-
-       clearVectorEdge(stack);pushVectorEdge(stack, root);
-       while (getSizeVectorEdge(stack) != 0) {
-               Edge e = lastVectorEdge(stack);
-               Node *n = getNodePtrFromEdge(e);
-
-               if (edgeIsVarConst(e)) {
-                       popVectorEdge(stack);
-                       continue;
-               } else if (n->flags.type == NodeType_ITE ||
-                                                        n->flags.type == NodeType_IFF) {
-                       popVectorEdge(stack);
-                       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) &&
-                               (!needNeg || n->flags.cnfVisitedUp & 2)) {
-                       popVectorEdge(stack);
-               } else if ((needPos && !(n->flags.cnfVisitedDown & 1)) ||
-                                                        (needNeg && !(n->flags.cnfVisitedDown & 2))) {
-                       if (needPos)
-                               n->flags.cnfVisitedDown |= 1;
-                       if (needNeg)
-                               n->flags.cnfVisitedDown |= 2;
-                       for (uint i = 0; i < n->numEdges; i++) {
-                               Edge arg = n->edges[i];
-                               arg = constraintNegateIf(arg, isNegEdge(e));
-                               pushVectorEdge(stack, arg);     //WARNING, THIS LOOKS LIKE A BUG IN THE ORIGINAL CODE
-                       }
-               } else {
-                       popVectorEdge(stack);
-                       produceCNF(cnf, e);
-               }
-       }
-       CNFExpr *cnfExp = (CNFExpr *) nroot->ptrAnnot[isNegEdge(root)];
-       ASSERT(cnfExp != NULL);
-       if (isProxy(cnfExp)) {
-               Literal l = getProxy(cnfExp);
-               Literal clause[] = {l};
-               addArrayClauseLiteral(cnf->solver, 1, clause);
-       } else if (backtrackLit) {
-               Literal l = introProxy(cnf, root, cnfExp, isNegEdge(root));
-               Literal clause[] = {l};
-               addArrayClauseLiteral(cnf->solver, 1, clause);
-       } else {
-               outputCNF(cnf, cnfExp);
-       }
-
-       if (!((intptr_t) cnfExp & 1)) {
-               deleteCNFExpr(cnfExp);
-               nroot->ptrAnnot[isNegEdge(root)] = NULL;
-       }
-}
-
-
-Literal introProxy(CNF *cnf, Edge e, CNFExpr *exp, bool isNeg) {
-       Literal l = 0;
-       Node *n = getNodePtrFromEdge(e);
-
-       if (n->flags.cnfVisitedUp & (1 << !isNeg)) {
-               CNFExpr *otherExp = (CNFExpr *) n->ptrAnnot[!isNeg];
-               if (isProxy(otherExp))
-                       l = -getProxy(otherExp);
-       } else {
-               Edge semNeg = {(Node *) n->ptrAnnot[isNeg]};
-               Node *nsemNeg = getNodePtrFromEdge(semNeg);
-               if (nsemNeg != NULL) {
-                       if (nsemNeg->flags.cnfVisitedUp & (1 << isNeg)) {
-                               CNFExpr *otherExp = (CNFExpr *) nsemNeg->ptrAnnot[isNeg];
-                               if (isProxy(otherExp))
-                                       l = -getProxy(otherExp);
-                       } else if (nsemNeg->flags.cnfVisitedUp & (1 << !isNeg)) {
-                               CNFExpr *otherExp = (CNFExpr *) nsemNeg->ptrAnnot[!isNeg];
-                               if (isProxy(otherExp))
-                                       l = getProxy(otherExp);
-                       }
-               }
-       }
-
-       if (l == 0) {
-               Edge newvar = constraintNewVar(cnf);
-               l = getEdgeVar(newvar);
-       }
-       // Output the constraints on the auxiliary variable
-       constrainCNF(cnf, l, exp);
-       deleteCNFExpr(exp);
-
-       n->ptrAnnot[isNeg] = (void *) ((intptr_t) (l << 1) | 1);
-
-       return l;
-}
-
-void produceCNF(CNF *cnf, Edge e) {
-       CNFExpr *expPos = NULL;
-       CNFExpr *expNeg = NULL;
-       Node *n = getNodePtrFromEdge(e);
-
-       if (n->intAnnot[0] > 0) {
-               expPos = produceConjunction(cnf, e);
-       }
-
-       if (n->intAnnot[1]  > 0) {
-               expNeg = produceDisjunction(cnf, e);
-       }
-
-       /// @todo Propagate constants across semantic negations (this can
-       /// be done similarly to the calls to propagate shown below).  The
-       /// trick here is that we need to figure out how to get the
-       /// semantic negation pointers, and ensure that they can have CNF
-       /// produced for them at the right point
-       ///
-       /// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false)
-
-       // propagate from positive to negative, negative to positive
-       if (!propagate(cnf, &expPos, expNeg, true))
-               propagate(cnf, &expNeg, expPos, true);
-
-       // The polarity heuristic entails visiting the discovery polarity first
-       if (isPosEdge(e)) {
-               saveCNF(cnf, expPos, e, false);
-               saveCNF(cnf, expNeg, e, true);
-       } else {
-               saveCNF(cnf, expNeg, e, true);
-               saveCNF(cnf, expPos, e, false);
-       }
-}
-
-bool propagate(CNF *cnf, CNFExpr **dest, CNFExpr *src, bool negate) {
-       if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
-               if (*dest == NULL) {
-                       *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
-               } else if (isProxy(*dest)) {
-                       bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
-                       if (alwaysTrue) {
-                               Literal clause[] = {getProxy(*dest)};
-                               addArrayClauseLiteral(cnf->solver, 1, clause);
-                       } else {
-                               Literal clause[] = {-getProxy(*dest)};
-                               addArrayClauseLiteral(cnf->solver, 1, clause);
-                       }
-
-                       *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
-               } else {
-                       clearCNFExpr(*dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
-               }
-               return true;
-       }
-       return false;
-}
-
-void saveCNF(CNF *cnf, CNFExpr *exp, Edge e, bool sign) {
-       Node *n = getNodePtrFromEdge(e);
-       n->flags.cnfVisitedUp |= (1 << sign);
-       if (exp == NULL || isProxy(exp)) return;
-
-       if (exp->litSize == 1) {
-               Literal l = getLiteralLitVector(&exp->singletons, 0);
-               deleteCNFExpr(exp);
-               n->ptrAnnot[sign] = (void *) ((((intptr_t) l) << 1) | 1);
-       } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) {
-               introProxy(cnf, e, exp, sign);
-       } else {
-               n->ptrAnnot[sign] = exp;
-       }
-}
-
-void constrainCNF(CNF *cnf, Literal lcond, CNFExpr *expr) {
-       if (alwaysTrueCNF(expr)) {
-               return;
-       } else if (alwaysFalseCNF(expr)) {
-               Literal clause[] = {-lcond};
-               addArrayClauseLiteral(cnf->solver, 1, clause);
-               return;
-       }
-
-       for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
-               Literal l = getLiteralLitVector(&expr->singletons,i);
-               Literal clause[] = {-lcond, l};
-               addArrayClauseLiteral(cnf->solver, 2, clause);
-       }
-       for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
-               LitVector *lv = getVectorLitVector(&expr->clauses,i);
-               addClauseLiteral(cnf->solver, -lcond);//Add first literal
-               addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals); //Add rest
-       }
-}
-
-void outputCNF(CNF *cnf, CNFExpr *expr) {
-       for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
-               Literal l = getLiteralLitVector(&expr->singletons,i);
-               Literal clause[] = {l};
-               addArrayClauseLiteral(cnf->solver, 1, clause);
-       }
-       for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
-               LitVector *lv = getVectorLitVector(&expr->clauses,i);
-               addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals);
-       }
-}
-
-CNFExpr *fillArgs(CNF *cnf, Edge e, bool isNeg, Edge *largestEdge) {
-       clearVectorEdge(&cnf->args);
-
-       *largestEdge = (Edge) {(Node *) NULL};
-       CNFExpr *largest = NULL;
-       Node *n = getNodePtrFromEdge(e);
-       int i = n->numEdges;
-       while (i != 0) {
-               Edge arg = n->edges[--i];
-               arg = constraintNegateIf(arg, isNeg);
-               Node *narg = getNodePtrFromEdge(arg);
-
-               if (edgeIsVarConst(arg)) {
-                       pushVectorEdge(&cnf->args, arg);
-                       continue;
-               }
-
-               if (narg->flags.type == NodeType_ITE || narg->flags.type == NodeType_IFF) {
-                       arg = (Edge) {(Node *) narg->ptrAnnot[isNegEdge(arg)]};
-               }
-
-               if (narg->intAnnot[isNegEdge(arg)] == 1) {
-                       CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
-                       if (!isProxy(argExp)) {
-                               if (largest == NULL) {
-                                       largest = argExp;
-                                       *largestEdge = arg;
-                                       continue;
-                               } else if (argExp->litSize > largest->litSize) {
-                                       pushVectorEdge(&cnf->args, *largestEdge);
-                                       largest = argExp;
-                                       *largestEdge = arg;
-                                       continue;
-                               }
-                       }
-               }
-               pushVectorEdge(&cnf->args, arg);
-       }
-
-       if (largest != NULL) {
-               Node *nlargestEdge = getNodePtrFromEdge(*largestEdge);
-               nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL;
-       }
-
-       return largest;
-}
-
 void printCNF(Edge e) {
        if (edgeIsVarConst(e)) {
                Literal l = getEdgeVar(e);
@@ -800,92 +327,6 @@ void printCNF(Edge e) {
        model_print(")");
 }
 
-CNFExpr *produceConjunction(CNF *cnf, Edge e) {
-       Edge largestEdge;
-
-       CNFExpr *accum = fillArgs(cnf, e, false, &largestEdge);
-       if (accum == NULL)
-               accum = allocCNFExprBool(true);
-
-       int i = getSizeVectorEdge(&cnf->args);
-       while (i != 0) {
-               Edge arg = getVectorEdge(&cnf->args, --i);
-               if (edgeIsVarConst(arg)) {
-                       conjoinCNFLit(accum, getEdgeVar(arg));
-               } else {
-                       Node *narg = getNodePtrFromEdge(arg);
-                       CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
-
-                       bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
-                       if (isProxy(argExp)) {// variable has been introduced
-                               conjoinCNFLit(accum, getProxy(argExp));
-                       } else {
-                               conjoinCNFExpr(accum, argExp, destroy);
-                               if (destroy)
-                                       narg->ptrAnnot[isNegEdge(arg)] = NULL;
-                       }
-               }
-       }
-
-       return accum;
-}
-
-#define CLAUSE_MAX 3
-
-CNFExpr *produceDisjunction(CNF *cnf, Edge e) {
-       Edge largestEdge;
-       CNFExpr *accum = fillArgs(cnf, e, true, &largestEdge);
-       if (accum == NULL)
-               accum = allocCNFExprBool(false);
-
-       // This is necessary to check to make sure that we don't start out
-       // with an accumulator that is "too large".
-
-       /// @todo Strictly speaking, introProxy doesn't *need* to free
-       /// memory, then this wouldn't have to reallocate CNFExpr
-
-       /// @todo When this call to introProxy is made, the semantic
-       /// negation pointer will have been destroyed.  Thus, it will not
-       /// be possible to use the correct proxy.  That should be fixed.
-
-       // at this point, we will either have NULL, or a destructible expression
-       if (getClauseSizeCNF(accum) > CLAUSE_MAX)
-               accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge)));
-
-       int i = getSizeVectorEdge(&cnf->args);
-       while (i != 0) {
-               Edge arg = getVectorEdge(&cnf->args, --i);
-               Node *narg = getNodePtrFromEdge(arg);
-               if (edgeIsVarConst(arg)) {
-                       disjoinCNFLit(accum, getEdgeVar(arg));
-               } else {
-                       CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
-
-                       bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
-                       if (isProxy(argExp)) {// variable has been introduced
-                               disjoinCNFLit(accum, getProxy(argExp));
-                       } else if (argExp->litSize == 0) {
-                               disjoinCNFExpr(accum, argExp, destroy);
-                       } else {
-                               // check to see if we should introduce a proxy
-                               int aL = accum->litSize;                        // lits in accum
-                               int eL = argExp->litSize;                       // lits in argument
-                               int aC = getClauseSizeCNF(accum);               // clauses in accum
-                               int eC = getClauseSizeCNF(argExp);      // clauses in argument
-                               //POSSIBLE BUG #2 (eL * aC +aL * eC > eL +aC +aL +aC)
-                               if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + eC + aL + aC)) {
-                                       disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg)));
-                               } else {
-                                       disjoinCNFExpr(accum, argExp, destroy);
-                                       if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
-                               }
-                       }
-               }
-       }
-
-       return accum;
-}
-
 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
        Edge carray[numvars];
        for (uint j = 0; j < numvars; j++) {
index 0683230..a48e5da 100644 (file)
@@ -30,59 +30,26 @@ enum NodeType {
 
 typedef enum NodeType NodeType;
 
-struct NodeFlags {
-       NodeType type : 2;
-       int varForced : 1;
-       int wasExpanded : 2;
-       int cnfVisitedDown : 2;
-       int cnfVisitedUp : 2;
-};
-
-typedef struct NodeFlags NodeFlags;
-
 struct Node {
-       NodeFlags flags;
        uint numEdges;
-       uint hashCode;
-       uint intAnnot[2];
-       void *ptrAnnot[2];
+       NodeType type;
        Edge edges[];
 };
 
-#define DEFAULT_CNF_ARRAY_SIZE 64
-#define LOAD_FACTOR 0.25
+typedef struct Node Node;
 
 struct CNF {
        uint varcount;
-       uint capacity;
-       uint size;
-       uint mask;
-       uint maxsize;
-       bool enableMatching;
-       Node **node_array;
        IncrementalSolver *solver;
-       VectorEdge constraints;
-       VectorEdge args;
        long long solveTime;
        long long encodeTime;
 };
 
 typedef struct CNF CNF;
 
-struct CNFExpr;
-typedef struct CNFExpr CNFExpr;
-
-static inline bool getExpanded(Node *n, int isNegated) {
-       return n->flags.wasExpanded & (1 << isNegated);
-}
-
-static inline void setExpanded(Node *n, int isNegated) {
-       n->flags.wasExpanded |= (1 << isNegated);
-}
-
 static inline Edge constraintNegate(Edge e) {
-       Edge enew = { (Node *) (((uintptr_t) e.node_ptr) ^ NEGATE_EDGE)};
-       return enew;
+       Edge eneg = { (Node *) (((uintptr_t) e.node_ptr) ^ NEGATE_EDGE)};
+       return eneg;
 }
 
 static inline bool sameNodeVarEdge(Edge e1, Edge e2) {
@@ -119,7 +86,7 @@ static inline Node *getNodePtrFromEdge(Edge e) {
 
 static inline NodeType getNodeType(Edge e) {
        Node *n = getNodePtrFromEdge(e);
-       return n->flags.type;
+       return n->type;
 }
 
 static inline bool equalsEdge(Edge e1, Edge e2) {
@@ -167,20 +134,12 @@ static inline Literal getEdgeVar(Edge e) {
        return isNegEdge(e) ? -val : val;
 }
 
-static inline bool isProxy(CNFExpr *expr) {
-       return (bool) (((intptr_t) expr) & 1);
-}
-
-static inline Literal getProxy(CNFExpr *expr) {
-       return (Literal) (((intptr_t) expr) >> 1);
-}
-
 CNF *createCNF();
 void deleteCNF(CNF *cnf);
 void resetCNF(CNF *cnf);
 
 uint hashNode(NodeType type, uint numEdges, Edge *edges);
-Node *allocNode(NodeType type, uint numEdges, Edge *edges, uint hashCode);
+Node *allocNode(NodeType type, uint numEdges, Edge *edges);
 bool compareNodes(Node *node, NodeType type, uint numEdges, Edge *edges);
 Edge create(CNF *cnf, NodeType type, uint numEdges, Edge *edges);
 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges);
@@ -199,17 +158,6 @@ int solveCNF(CNF *cnf);
 bool getValueCNF(CNF *cnf, Edge var);
 void printCNF(Edge e);
 
-void convertPass(CNF *cnf, bool backtrackLit);
-void convertConstraint(CNF *cnf, VectorEdge *stack, Edge e, bool backtrackLit);
-void constrainCNF(CNF *cnf, Literal l, CNFExpr *exp);
-void produceCNF(CNF *cnf, Edge e);
-CNFExpr *produceConjunction(CNF *cnf, Edge e);
-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 generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);
 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);