Adding a logicOp test case + fixing bugs

diff --git a/src/AST/boolean.c b/src/AST/boolean.c
index 9f4b2191367e38e18e0ff587bb9a345b98376998..05feefb50996146ce76cad25930d15e91411d260 100644 (file)
--- a/src/AST/boolean.c
+++ b/src/AST/boolean.c
@@ -41,6 +41,8 @@ Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint n
 
 Boolean * allocBooleanLogicArray(CSolver *solver, LogicOp op, Boolean ** array, uint asize){
        BooleanLogic * This = ourmalloc(sizeof(BooleanLogic));
+       GETBOOLEANTYPE(This) = LOGICOP;
+       This->op = op;
        initDefVectorBoolean(GETBOOLEANPARENTS(This));
        initArrayInitBoolean(&This->inputs, array, asize);
        pushVectorBoolean(solver->allBooleans, (Boolean *) This);

diff --git a/src/Encoders/naiveencoder.c b/src/Encoders/naiveencoder.c
index da6700fa9edb059445a771ef13f16418ca42af7f..ef0e29e3b2b93c1fd2030b6c4a65871d79f9855c 100644 (file)
--- a/src/Encoders/naiveencoder.c
+++ b/src/Encoders/naiveencoder.c
@@ -30,6 +30,7 @@ void naiveEncodingConstraint(Boolean * This) {
        }
        case LOGICOP: {
                naiveEncodingLogicOp((BooleanLogic *) This);
+               return;
        }
        case PREDICATEOP: {
                naiveEncodingPredicate((BooleanPredicate *) This);

diff --git a/src/Test/logicopstest.c b/src/Test/logicopstest.c
new file mode 100644 (file)
index 0000000..7b9384d
--- /dev/null
+++ b/src/Test/logicopstest.c
@@ -0,0 +1,31 @@
+#include "csolver.h"
+
+/**
+ * b1 AND b2=>b3
+ * !b3 OR b4
+ * b1 XOR b4
+ * @param numargs
+ * @param argv
+ * @return 
+ */
+int main(int numargs, char** argv){
+       CSolver * solver=allocCSolver();
+       Boolean *b1= getBooleanVar(solver, 0);
+       Boolean *b2= getBooleanVar(solver, 0);
+       Boolean *b3= getBooleanVar(solver, 0);
+       Boolean *b4= getBooleanVar(solver, 0);
+       //L_AND, L_OR, L_NOT, L_XOR, L_IMPLIES
+       Boolean *andb1b2= applyLogicalOperation(solver, L_AND,(Boolean*[]) {b1, b2}, 2);
+       Boolean * imply = applyLogicalOperation(solver, L_IMPLIES, (Boolean*[]) {andb1b2, b3}, 2);
+       addConstraint(solver, imply);
+       Boolean* notb3 = applyLogicalOperation(solver, L_NOT, (Boolean*[]) {b3}, 1); 
+       addConstraint(solver, applyLogicalOperation(solver, L_OR, (Boolean*[]){notb3, b4} , 2));
+       addConstraint(solver, applyLogicalOperation(solver, L_XOR, (Boolean* []) {b1, b4}, 2));
+       if (startEncoding(solver)==1)
+               printf("b1=%d b2=%d b3=%d b4=%d\n", 
+                       getBooleanValue(solver,b1), getBooleanValue(solver, b2),
+                       getBooleanValue(solver, b3), getBooleanValue(solver, b4));
+       else
+               printf("UNSAT\n");
+       deleteSolver(solver);
+}
\ No newline at end of file