From: Hamed <hamed.gorjiara@gmail.com>
Date: Wed, 19 Jul 2017 18:21:49 +0000 (-0700)
Subject: Adding a logicOp test case + fixing bugs
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=2dec13914d952b4b180af8c242a9ffe87c9bdb39;p=satune.git

Adding a logicOp test case + fixing bugs
---

diff --git a/src/AST/boolean.c b/src/AST/boolean.c
index 9f4b219..05feefb 100644
--- 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 da6700f..ef0e29e 100644
--- 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
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