From c6512d5af03c7089ecf99bce3b4946e12e04aa72 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Wed, 30 Aug 2017 22:46:46 -0700
Subject: [PATCH] Add IFF support

---
 src/AST/ops.h                         |  2 +-
 src/AST/rewriter.cc                   |  6 ++++++
 src/ASTAnalyses/polarityassignment.cc |  2 ++
 src/Backend/satencoder.cc             |  2 ++
 src/Backend/solver_interface.h        |  6 +-----
 src/csolver.cc                        | 13 +++++++++++++
 src/csolver.h                         |  1 +
 7 files changed, 26 insertions(+), 6 deletions(-)

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 29a9911..910565d 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -249,6 +249,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 bb9b1e1..ba6b406 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:
-- 
2.34.1