From: bdemsky <bdemsky@uci.edu>
Date: Thu, 31 Aug 2017 05:47:05 +0000 (-0700)
Subject: Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/constraint_compiler
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=28703eaeadb4b35e607a1d4441b31729177feb19;hp=7fb0eb9a3dcf843f413d858e1cf66e9e13de200f

Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/constraint_compiler
---

diff --git a/src/AST/ops.h b/src/AST/ops.h
index 8ad60c7..a26d1cd 100644
--- a/src/AST/ops.h
+++ b/src/AST/ops.h
@@ -1,6 +1,6 @@
 #ifndef OPS_H
 #define OPS_H
-enum LogicOp {SATC_AND, SATC_OR, SATC_NOT, SATC_XOR, SATC_IMPLIES};
+enum LogicOp {SATC_AND, SATC_OR, SATC_NOT, SATC_XOR, SATC_IFF, SATC_IMPLIES};
 typedef enum LogicOp LogicOp;
 
 enum ArithOp {SATC_ADD, SATC_SUB};
diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index bfc321c..a7df7c8 100644
--- a/src/AST/rewriter.cc
+++ b/src/AST/rewriter.cc
@@ -21,6 +21,9 @@ void CSolver::replaceBooleanWithTrue(Boolean *bexpr) {
 		case SATC_NOT:
 			replaceBooleanWithFalse(parent);
 			break;
+		case SATC_IFF:
+			handleXORFalse(logicop, bexpr);
+			break;
 		case SATC_XOR:
 			handleXORTrue(logicop, bexpr);
 			break;
@@ -153,6 +156,9 @@ void CSolver::replaceBooleanWithFalse(Boolean *bexpr) {
 		case SATC_NOT:
 			replaceBooleanWithTrue(parent);
 			break;
+		case SATC_IFF:
+			handleXORTrue(logicop, bexpr);
+			break;
 		case SATC_XOR:
 			handleXORFalse(logicop, bexpr);
 			break;
diff --git a/src/ASTAnalyses/polarityassignment.cc b/src/ASTAnalyses/polarityassignment.cc
index 38f32ae..1478930 100644
--- a/src/ASTAnalyses/polarityassignment.cc
+++ b/src/ASTAnalyses/polarityassignment.cc
@@ -95,6 +95,7 @@ void computeLogicOpPolarity(BooleanLogic *This) {
 		updatePolarity(tmp, negatePolarity(parentpolarity));
 		break;
 	}
+	case SATC_IFF:
 	case SATC_XOR: {
 		updatePolarity(This->inputs.get(0), P_BOTHTRUEFALSE);
 		updatePolarity(This->inputs.get(1), P_BOTHTRUEFALSE);
@@ -144,6 +145,7 @@ void computeLogicOpBooleanValue(BooleanLogic *This) {
 			updateMustValue(This->inputs.get(1), parentbv);
 		}
 		return;
+	case SATC_IFF:
 	case SATC_XOR:
 		return;
 	default:
diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index e053d78..0de0ae4 100644
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -93,6 +93,8 @@ Edge SATEncoder::encodeLogicSATEncoder(BooleanLogic *constraint) {
 		return constraintNegate(array[0]);
 	case SATC_XOR:
 		return constraintXOR(cnf, array[0], array[1]);
+	case SATC_IFF:
+		return constraintIFF(cnf, array[0], array[1]);
 	case SATC_IMPLIES:
 		return constraintIMPLIES(cnf, array[0], array[1]);
 	default:
diff --git a/src/Backend/solver_interface.h b/src/Backend/solver_interface.h
index 4fd2dea..42edbb9 100644
--- a/src/Backend/solver_interface.h
+++ b/src/Backend/solver_interface.h
@@ -12,11 +12,7 @@
 
 #define IS_OUT_FD 3
 
-#define IS_UNSAT 0
-#define IS_SAT 1
-#define IS_INDETER 2
-#define IS_FREEZE 3
-#define IS_RUNSOLVER 4
+enum SolverResult {IS_UNSAT=0, IS_SAT=1, IS_INDETER=2, IS_FREEZE=3, IS_RUNSOLVER=4};
 
 #define IS_BUFFERSIZE 1024
 
diff --git a/src/csolver.cc b/src/csolver.cc
index d0aa32e..0270758 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -251,6 +251,19 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
 		}
 		break;
 	}
+	case SATC_IFF: {
+		for(uint i=0;i<2;i++) {
+			if (array[i]->type == BOOLCONST) {
+				if (array[i]->isTrue()) {
+					return array[1-i];
+				} else {
+					newarray[0]=array[1-i];
+					return applyLogicalOperation(SATC_NOT, newarray, 1);
+				}
+			}
+		}
+		break;
+	}
 	case SATC_XOR: {
 		for(uint i=0;i<2;i++) {
 			if (array[i]->type == BOOLCONST) {
diff --git a/src/csolver.h b/src/csolver.h
index aa7ccd0..7942839 100644
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -4,6 +4,7 @@
 #include "ops.h"
 #include "corestructs.h"
 #include "asthash.h"
+#include "solver_interface.h"
 
 class CSolver {
 public: