more edits

diff --git a/src/Backend/cnfexpr.c b/src/Backend/cnfexpr.c
new file mode 100644 (file)
index 0000000..02fdeb1
--- /dev/null
+++ b/src/Backend/cnfexpr.c
@@ -0,0 +1,81 @@
+#include "cnfexpr.h"
+
+#define LITCAPACITY 4
+#define MERGESIZE 5
+
+static inline uint boundedSize(uint x) { return (x > MERGESIZE)?MERGESIZE:x; }
+
+LitVector * allocLitVector() {
+       LitVector *This=ourmalloc(sizeofLitVector);
+       initLitVector(This);
+       return This;
+}
+
+void initLitVector(LitVector *This) {
+       This->size=0;
+       This->capacity=LITCAPACITY;
+       This->literals=ourmalloc(This->capacity * sizeof(Literal));
+}
+
+void freeLitVector(LitVector *This) {
+       ourfree(This->literals);
+}
+
+void deleteLitVector(LitVector *This) {
+       freeLitVector(This);
+       ourfree(This);
+}
+
+void addLiteralLitVector(LitVector *This, Literal l) {
+       Literal labs = abs(l);
+       uint vec_size=This->size;
+       uint searchsize=boundedSize(vec_size);
+       uint i=0;
+       for (; i < searchsize; i++) {
+               Literal curr = This->literals[i];
+               Literals currabs = abs(curr);
+               if (currabs > labs)
+                       break;
+               if (currabs == labs) {
+                       if (curr == -l)
+                               size = 0; //either true or false now depending on whether this is a conj or disj
+                       return;
+               }
+               if ((++This->size) >= This->capacity) {
+                       This->capacity << = 1;
+                       This->literals=ourrealloc(This->capacity * sizeof(Literal));
+               }
+               
+               if (vec_size < MERGESIZE) {
+                       memmove(&This->literals[i+1], &This->literals[i], (vec_size-i) * sizeof(Literal));
+                       This->literals[i]=l;
+               } else {
+                       This->literals[vec_size]=l;
+               }
+       }
+}
+
+CNFExpr * allocCNFExprBool(bool isTrue) {
+       CNFExpr *This=ourmalloc(sizeof(CNFExpr));
+       this->litSize=0;
+       this->isTrue=isTrue;
+       allocInlineVectorLitVector(&This->clauses);
+       initLitVector(&This->singletons);
+       return This;
+}
+
+CNFExpr * allocCNFExprLiteral(Literal l) {
+       CNFExpr *This=ourmalloc(sizeof(CNFExpr));
+       this->litSize=1;
+       this->isTrue=false;
+       allocInlineVectorLitVector(&This->clauses);
+       initLitVector(&This->singletons);
+       addLiteralLitVector(This, l);
+       return This;
+}
+
+void deleteCNFExpr(CNFExpr *This) {
+       deleteVectorArray(&This->clauses);
+       freeLitVector(&This->singletons);
+       ourfree(This);
+}

diff --git a/src/Backend/cnfexpr.h b/src/Backend/cnfexpr.h
new file mode 100644 (file)
index 0000000..fcb75bd
--- /dev/null
+++ b/src/Backend/cnfexpr.h
@@ -0,0 +1,32 @@
+#ifndef CNFEXPR_H
+#define CNFEXPR_H
+#include "classlist.h"
+#include "vector.h"
+
+typedef int Literal;
+
+
+struct LitVector {
+       uint size;
+       uint capacity;
+       Literal *literals;
+};
+typedef CNFClause CNFClause;
+
+VectorDef(LitVector, LitVector *)
+
+struct CNFExpr {
+       uint litSize;
+       bool isTrue;
+       VectorLitVector clauses;
+       LitVector singletons;
+};
+
+typedef CNFExpr CNFExpr;
+
+bool alwaysTrueCNF(CNFExpr * This);
+bool alwaysFalseCNF(CNFExpr * This);
+uint getLitSizeCNF(CNFExpr * This);
+void clearCNF(CNFExpr *This, bool isTrue);
+uint getClauseSizeCNF(CNFExpr * This);
+#endif

diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h
index e1b21d36f69f4ea5ec45ebb646a39b3024e4b16a..0d254c83d5ff56d3d2fd25214c0ae53ee8e11871 100644 (file)
--- a/src/Backend/constraint.h
+++ b/src/Backend/constraint.h
@@ -44,6 +44,7 @@ Constraint * cloneConstraint(Constraint * c);
 static inline void setNegConstraint(Constraint * This, Constraint *c) {This->neg=c;}
 Constraint *negateConstraint(Constraint * c);
 
+
 extern Constraint ctrue;
 extern Constraint cfalse;
 
@@ -51,4 +52,6 @@ Constraint * generateBinaryConstraint(uint numvars, Constraint ** vars, uint val
 Constraint * generateLTConstraint(uint numvars, Constraint ** vars, uint value);
 Constraint * generateEquivNVConstraint(uint numvars, Constraint **var1, Constraint **var2);
 Constraint * generateEquivConstraint(Constraint *var1, Constraint *var2);
+
+
 #endif

diff --git a/src/Backend/inc_solver.c b/src/Backend/inc_solver.c
index 5e1ed548ab31e487d958bc1fb293c840ffc0533b..b9cc549fdbf30dc3fa408b008d8f24ec63db8ade 100644 (file)
--- a/src/Backend/inc_solver.c
+++ b/src/Backend/inc_solver.c
@@ -42,6 +42,15 @@ void addClauseLiteral(IncrementalSolver * This, int literal) {
        }
 }
 
+void addArrayClauseLiteral(IncrementalSolver * This, uint numliterals, int * literals) {
+       for(uint i=0;i<numliterals; i++) {
+               This->buffer[This->offset++]=literals[i];
+               if (This->offset==IS_BUFFERSIZE) {
+                       flushBufferSolver(This);
+               }
+       }
+}
+
 void finishedClauses(IncrementalSolver * This) {
        addClauseLiteral(This, 0);
 }

diff --git a/src/Backend/inc_solver.h b/src/Backend/inc_solver.h
index 15e5def4ccd8c498f7bca94694bf3b01938205bb..9b3e2ab55cc61f6ee503bcd81288e66974a5e538 100644 (file)
--- a/src/Backend/inc_solver.h
+++ b/src/Backend/inc_solver.h
@@ -31,6 +31,7 @@ struct IncrementalSolver {
 IncrementalSolver * allocIncrementalSolver();
 void deleteIncrementalSolver(IncrementalSolver * This);
 void addClauseLiteral(IncrementalSolver * This, int literal);
+void addArrayClauseLiteral(IncrementalSolver * This, uint numliterals, int * literals);
 void finishedClauses(IncrementalSolver * This);
 void freeze(IncrementalSolver * This, int variable);
 int solve(IncrementalSolver * This);

diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c
index c24475427558b2a192a74b2cea549d0c4730d7e8..4a3719b9faa10093a0d42d69d47cb8f35dc4e541 100644 (file)
--- a/src/Backend/nodeedge.c
+++ b/src/Backend/nodeedge.c
@@ -1,6 +1,9 @@
 #include "nodeedge.h"
 #include <string.h>
 #include <stdlib.h>
+#include "inc_solver.h"
+
+/** Code ported from C++ BAT implementation of NICE-SAT */
 
 VectorImpl(Edge, Edge, 16)
 
@@ -56,6 +59,8 @@ Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashcode) {
        memcpy(n->edges, edges, sizeof(Edge)*numEdges);
        n->flags.type=type;
        n->flags.wasExpanded=0;
+       n->flags.cnfVisitedDown=0;
+       n->flags.cnfVisitedUp=0;
        n->numEdges=numEdges;
        n->hashCode=hashcode;
        n->intAnnot[0]=0;n->intAnnot[1]=0;
@@ -339,3 +344,344 @@ void countConstraint(CNF *cnf, VectorEdge *stack, Edge e) {
                }
        }
 }
+
+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)) {
+               root = (Edge) { (Node *) nroot->ptrAnnot[isNegEdge(root)]};
+       }
+       
+       if (edgeIsConst(root)) {
+               if (isNegEdge(root)) {
+                       //trivally unsat
+                       Edge newvar=constraintNewVar(cnf);
+                       Literal var=getEdgeVar(newvar);
+                       Literal clause[] = {var, -var, 0};
+                       addArrayClauseLiteral(cnf->solver, 3, clause);
+                       return;
+               } else {
+                       //trivially true
+                       return;
+               }
+       } else if (edgeIsVarConst(root)) {
+               Literal clause[] = { getEdgeVar(root), 0};
+               addArrayClauseLiteral(cnf->solver, 2, 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);
+                       pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]});
+                       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)];
+       if (isProxy(cnfExp)) {
+               //solver.add(getProxy(cnfExp))
+       } else if (backtrackLit) {
+               //solver.add(introProxy(solver, root, cnfExp, isNegEdge(root)));
+       } else {
+               //solver.add(*cnfExp);
+       }
+
+       if (!((intptr_t) cnfExp & 1)) {
+               //free rootExp
+               nroot->ptrAnnot[isNegEdge(root)] = NULL;
+       }
+}
+
+//DONE
+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);
+       //delete exp; //FIXME
+  
+       n->ptrAnnot[isNeg] = (void*) ((intptr_t) (l << 1) | 1);
+       
+       return l;
+}
+
+//DONE
+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
+       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);
+       }
+}
+
+
+//DONE
+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), 0};
+                               addArrayClauseLiteral(cnf->solver, 2, clause);
+                       } else {
+                               Literal clause[] = {-getProxy(dest), 0};
+                               addArrayClauseLiteral(cnf->solver, 2, clause);
+                       }
+                       
+                       dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
+               } else {
+                       clearCNF(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 = exp->singletons()[0];
+               delete exp;
+               n->ptrAnnot[sign] = (void*) ((intptr_t) (l << 1) | 1);
+       } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || e->isVarForced())) {
+               introProxy(solver, e, exp, sign);
+       } else {
+               n->ptrAnnot[sign] = exp;
+       }
+}
+
+void constrainCNF(CNF * cnf, Literal l, CNFExpr *exp) {
+       if (alwaysTrueCNF(exp)) {
+               return;
+       } else if (alwaysFalseCNF(expr)) {
+               Literal clause[] = {-l, 0};
+               addArrayClauseLiteral(cnf->solver, 2, clause);
+               return;
+       }
+       //FIXME
+       
+}
+
+void outputCNF(CNF *cnf, CNFExpr *exp) {
+       
+}
+
+CNFExpr* fillArgs(CNF *cnf, Edge e, bool isNeg, Edge * largestEdge, VectorEdge * args) {
+       args.clear();
+
+       *largestEdge = (void*) NULL;
+       CnfExp* largest = NULL;
+       int i = e->size();
+       while (i != 0) {
+               Edge arg = (*e)[--i]; arg.negateIf(isNeg);
+               
+               if (arg.isVar()) {
+                       args.push(arg);
+                       continue;
+               }
+               
+               if (arg->op() == NodeOp_Ite || arg->op() == NodeOp_Iff) {
+                       arg = arg->ptrAnnot(arg.isNeg());
+               }
+    
+               if (arg->intAnnot(arg.isNeg()) == 1) {
+                       CnfExp* argExp = (CnfExp*) arg->ptrAnnot(arg.isNeg());
+                       if (!isProxy(argExp)) {
+                               if (largest == NULL) {
+                                       largest = argExp;
+                                       largestEdge = arg;
+                                       continue;
+                               } else if (argExp->litSize > largest->litSize) {
+                                       args.push(largestEdge);
+                                       largest = argExp;
+                                       largestEdge = arg;
+                                       continue;
+                               }
+                       }
+               }
+               args.push(arg);
+       }
+       
+       if (largest != NULL) {
+               largestEdge->ptrAnnot(largestEdge.isNeg()) = NULL;
+       }
+       
+       return largest;
+}
+
+
+CNFExpr * produceConjunction(CNF * cnf, Edge e) {
+       Edge largestEdge;
+       CnfExp* accum = fillArgs(e, false, largestEdge);
+       if (accum == NULL) accum = new CnfExp(true);
+       
+       int i = _args.size();
+       while (i != 0) {
+               Edge arg(_args[--i]);
+               if (arg.isVar()) {
+                       accum->conjoin(atomLit(arg));
+               } else {
+                       CnfExp* argExp = (CnfExp*) arg->ptrAnnot(arg.isNeg());
+      
+                       bool destroy = (--arg->intAnnot(arg.isNeg()) == 0);
+                       if (isProxy(argExp)) { // variable has been introduced
+                               accum->conjoin(getProxy(argExp));
+                       } else {
+                               accum->conjoin(argExp, destroy);
+                               if (destroy) arg->ptrAnnot(arg.isNeg()) = NULL;
+                       }
+               }
+       }
+       
+       return accum;
+}
+
+#define CLAUSE_MAX 3
+
+CNFExpr* produceDisjunction(CNF *cnf, Edge e) {
+       Edge largestEdge;
+       CNFExpr* accum = fillArgs(e, true, largestEdge);
+       if (accum == NULL)
+               accum = new CNFExpr(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 (accum->clauseSize() > CLAUSE_MAX)
+               accum = new CNFExpr(introProxy(solver, largestEdge, accum, largestEdge.isNeg()));
+       
+       int i = _args.size();
+       while (i != 0) {
+               Edge arg(_args[--i]);
+               if (arg.isVar()) {
+                       accum->disjoin(atomLit(arg));
+               } else {
+                       CNFExpr* argExp = (CNFExpr*) arg->ptrAnnot(arg.isNeg());
+                       
+                       bool destroy = (--arg->intAnnot(arg.isNeg()) == 0);
+                       if (isProxy(argExp)) { // variable has been introduced
+                               accum->disjoin(getProxy(argExp));
+                       } else if (argExp->litSize == 0) {
+                               accum->disjoin(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
+                               
+                               if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + aC + aL + aC)) {
+                                       accum->disjoin(introProxy(solver, arg, argExp, arg.isNeg()));
+                               } else {
+                                       accum->disjoin(argExp, destroy);
+                                       if (destroy) arg->ptrAnnot(arg.isNeg()) = NULL;
+                               }
+                       }
+               }
+       }
+  
+       return accum;
+}

diff --git a/src/Backend/nodeedge.h b/src/Backend/nodeedge.h
index e17bba659666d20b0967fcf80c4d1c84b3cc0f89..e515640354a06353483a85dcc7b147268bd6e9c3 100644 (file)
--- a/src/Backend/nodeedge.h
+++ b/src/Backend/nodeedge.h
@@ -31,6 +31,8 @@ typedef enum NodeType NodeType;
 struct NodeFlags {
        NodeType type:2;
        int wasExpanded:2;
+       int cnfVisitedDown:2;
+       int cnfVisitedUp:2;
 };
 
 typedef struct NodeFlags NodeFlags;
@@ -55,11 +57,15 @@ struct CNF {
        uint maxsize;
        bool enableMatching;
        Node ** node_array;
+       IncrementalSolver * solver;
        VectorEdge constraints;
 };
 
 typedef struct CNF CNF;
 
+struct CNFExpr;
+typedef struct CNFExpr CNFExpr;
+
 static inline bool getExpanded(Node *n, int isNegated) {
        return n->flags.wasExpanded & (1<<isNegated);
 }
@@ -89,6 +95,10 @@ static inline bool isNegEdge(Edge e) {
        return ((uintptr_t)e.node_ptr) & NEGATE_EDGE;
 }
 
+static inline bool isPosEdge(Edge e) {
+       return !(((uintptr_t)e.node_ptr) & NEGATE_EDGE);
+}
+
 static inline bool isNodeEdge(Edge e) {
        return !(((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT);
 }
@@ -142,6 +152,18 @@ static inline Edge constraintNegateIf(Edge e, bool negate) {
        return eret;
 }
 
+static inline Literal getEdgeVar(Edge e) {
+       int val = (int) (((uintptr_t) e.node_ptr) >> VAR_SHIFT);
+       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);
+}
 
 uint hashNode(NodeType type, uint numEdges, Edge * edges);
 Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashCode);
@@ -157,6 +179,10 @@ Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge);
 Edge constraintNewVar(CNF *cnf);
 void countPass(CNF *cnf);
 void countConstraint(CNF *cnf, VectorEdge * stack, Edge e);
+void convertPass(CNF *cnf, bool backtrackLit);
+void convertConstraint(CNF *cnf, VectorEdge *stack, Edge e, bool backtrackLit);
+void constrain(CNF * cnf, Literal l, CNFExpr *exp);
+void produceCNF(CNF * cnf, Edge e);
 
 
 Edge E_True={(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};