edits

diff --git a/src/Backend/cnfexpr.c b/src/Backend/cnfexpr.c
index aebc546300c45a988296470d7af1a345d7a700d2..07d13fab559e3093390d5b93695a5ab7e76bcbb4 100644 (file)
--- a/src/Backend/cnfexpr.c
+++ b/src/Backend/cnfexpr.c
@@ -38,6 +38,8 @@ C port of CNF SAT Conversion Copyright Brian Demsky 2017.
 #define LITCAPACITY 4
 #define MERGESIZE 5
 
+VectorImpl(LitVector, LitVector *, 4)
+
 static inline uint boundedSize(uint x) { return (x > MERGESIZE)?MERGESIZE:x; }
 
 LitVector * allocLitVector() {
@@ -157,7 +159,7 @@ void conjoinCNFLit(CNFExpr *This, Literal l) {
        addLiteralLitVector(&This->singletons, l);
        uint newsize=getSizeLitVector(&This->singletons);
        if (newsize==0)
-               clearCNF(This, false); //We found a conflict
+               clearCNFExpr(This, false); //We found a conflict
        else
                This->litSize+=getSizeLitVector(&This->singletons);
 }
@@ -189,7 +191,7 @@ void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy) {
 void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
        if (expr->litSize==0) {
                if (!This->isTrue) {
-                       clearCNF(This, false);
+                       clearCNFExpr(This, false);
                }
                if (destroy) {
                        deleteCNFExpr(expr);
@@ -211,7 +213,7 @@ void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
                addLiteralLitVector(&This->singletons, l);
                if (getSizeLitVector(&This->singletons)==0) {
                        //Found conflict...
-                       clearCNF(This, false);
+                       clearCNFExpr(This, false);
                        if (destroy) {
                                deleteCNFExpr(expr);
                        }
@@ -341,7 +343,7 @@ void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
        /** Handle the special cases */
        if (expr->litSize == 0) {
                if (expr->isTrue) {
-                       clearCNF(This, true);
+                       clearCNFExpr(This, true);
                }
                if (destroy) {
                        deleteCNFExpr(expr);

diff --git a/src/Backend/cnfexpr.h b/src/Backend/cnfexpr.h
index d76914ac2398cb4b88296c64e45bf1a586e0c315..5f1f9077d93e21277ef13128e2d784dd539c5570 100644 (file)
--- a/src/Backend/cnfexpr.h
+++ b/src/Backend/cnfexpr.h
@@ -45,11 +45,10 @@ void deleteCNFExpr(CNFExpr *This);
 void clearCNFExpr(CNFExpr *This, bool isTrue);
 
 void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy);
-bool alwaysTrueCNF(CNFExpr * This);
-bool alwaysFalseCNF(CNFExpr * This);
-uint getLitSizeCNF(CNFExpr * This);
-void clearCNF(CNFExpr *This, bool isTrue);
-uint getClauseSizeCNF(CNFExpr * This);
+static inline bool alwaysTrueCNF(CNFExpr * This) {return (This->litSize==0) && This->isTrue;}
+static inline bool alwaysFalseCNF(CNFExpr * This) {return (This->litSize==0) && !This->isTrue;}
+static inline uint getLitSizeCNF(CNFExpr * This) {return This->litSize;}
+static inline uint getClauseSizeCNF(CNFExpr * This) {return getSizeLitVector(&This->singletons) + getSizeVectorLitVector(&This->clauses);}
 void conjoinCNFLit(CNFExpr *This, Literal l);
 void disjoinCNFLit(CNFExpr *This, Literal l);
 void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy);

diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c
index f31a098164cefe23d93795965477db7476357693..f836fff7a83f16e6245c80fdccaa98ad2c842d31 100644 (file)
--- a/src/Backend/nodeedge.c
+++ b/src/Backend/nodeedge.c
@@ -136,7 +136,7 @@ Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge * edges) {
 uint hashNode(NodeType type, uint numEdges, Edge * edges) {
        uint hashvalue=type ^ numEdges;
        for(uint i=0;i<numEdges;i++) {
-               hashvalue ^= (uint) edges[i].node_ptr;
+               hashvalue ^= (uint) ((uintptr_t) edges[i].node_ptr);
                hashvalue = (hashvalue << 3) | (hashvalue >> 29); //rotate left by 3 bits
        }
        return (uint) hashvalue;
@@ -546,7 +546,8 @@ void produceCNF(CNF * cnf, Edge e) {
        /// 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);
+       if (!propagate(cnf, & expPos, expNeg, true))
+               propagate(cnf, & expNeg, expPos, true);
        
        // The polarity heuristic entails visiting the discovery polarity first
        if (isPosEdge(e)) {

diff --git a/src/Collections/vector.h b/src/Collections/vector.h
index fdaf0f416d84a9e079770eef4b13069b9eb0f375..0538ff3fb4584e65d48204cee2928ec3c69085d6 100644 (file)
--- a/src/Collections/vector.h
+++ b/src/Collections/vector.h
@@ -48,7 +48,7 @@
                vector->size--;                                                                                                                                                                                                                 \
        }                                                                                                                                                                                                                                                                                       \
        type lastVector ## name(Vector ## name *vector) {                                                                                       \
-               return vector->array[vector->size];                                                                                                                                     \
+               return vector->array[vector->size-1];                                                                                                                           \
        }                                                                                                                                                                                                                                                                                       \
        void setSizeVector ## name(Vector ## name *vector, uint size) {                         \
                if (size <= vector->size) {                                                                                                                                                                     \