Start CNF Test Case

diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c
index a1e596ff1ae133d340dc4e5c7ddb193c359fda97..a6d9dcc3abf58fbae01ba4d4774a675e222cae56 100644 (file)
--- a/src/Backend/nodeedge.c
+++ b/src/Backend/nodeedge.c
@@ -519,19 +519,19 @@ 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)) {
+               } else if (isProxy(*dest)) {
                        bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
                        if (alwaysTrue) {
-                               Literal clause[] = {getProxy(dest)};
+                               Literal clause[] = {getProxy(*dest)};
                                addArrayClauseLiteral(cnf->solver, 1, clause);
                        } else {
-                               Literal clause[] = {-getProxy(dest)};
+                               Literal clause[] = {-getProxy(*dest)};
                                addArrayClauseLiteral(cnf->solver, 1, clause);
                        }
                        
                        *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
                } else {
-                       clearCNFExpr(dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
+                       clearCNFExpr(*dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
                }
                return true;
        }

diff --git a/src/Backend/nodeedge.h b/src/Backend/nodeedge.h
index ee9502b8977900350117ecc8e3aa5abbd05092fa..aff2c35b63baec4474ade034030352c02b30e60b 100644 (file)
--- a/src/Backend/nodeedge.h
+++ b/src/Backend/nodeedge.h
@@ -173,6 +173,9 @@ static inline Literal getProxy(CNFExpr *expr) {
        return (Literal) (((intptr_t) expr) >> 1);
 }
 
+CNF * createCNF();
+void deleteCNF(CNF * cnf);
+
 uint hashNode(NodeType type, uint numEdges, Edge * edges);
 Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashCode);
 bool compareNodes(Node * node, NodeType type, uint numEdges, Edge *edges);
@@ -187,6 +190,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 addConstraint(CNF *cnf, Edge constraint);
+
+
+
 void convertPass(CNF *cnf, bool backtrackLit);
 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge e, bool backtrackLit);
 void constrainCNF(CNF * cnf, Literal l, CNFExpr *exp);

diff --git a/src/Test/Makefile b/src/Test/Makefile
index b3b7cb35abbc2c3584389d0ae6bffc20b55c8577..be27d60f132d810e23426861b5f5bf3f2b2a423b 100644 (file)
--- a/src/Test/Makefile
+++ b/src/Test/Makefile
@@ -6,7 +6,7 @@ include $(BASE)/common.mk
 
 DEPS := $(join $(addsuffix ., $(dir $(OBJECTS))), $(addsuffix .d, $(notdir $(OBJECTS))))
 
-CPPFLAGS += -I$(BASE) -I$(BASE)/AST -I$(BASE)/Collections
+CPPFLAGS += -I$(BASE) -I$(BASE)/AST -I$(BASE)/Collections -I$(BASE)/Backend
 
 all: $(OBJECTS) ../bin/run.sh
 

diff --git a/src/Test/testcnf.c b/src/Test/testcnf.c
new file mode 100644 (file)
index 0000000..68e2104
--- /dev/null
+++ b/src/Test/testcnf.c
@@ -0,0 +1,16 @@
+#include "nodeedge.h"
+
+int main(int numargs, char ** argv) {
+       CNF *cnf=createCNF();
+       Edge v1=constraintNewVar(cnf);
+       Edge v2=constraintNewVar(cnf);
+       Edge v3=constraintNewVar(cnf);
+       Edge nv1=constraintNegate(v1);
+       Edge nv2=constraintNegate(v2);
+       Edge iff1=constraintIFF(cnf, nv1, v2);
+       Edge iff2=constraintIFF(cnf, nv2, v3);
+       Edge iff3=constraintIFF(cnf, v3, nv1);
+       Edge cand=constraintAND(cnf, 3, (Edge[]) {iff1, iff2, iff3});
+       addConstraint(cnf, cand);
+       deleteCNF(cnf);
+}