Add IFF support

diff --git a/src/AST/ops.h b/src/AST/ops.h
index 8ad60c7545ad1884d7c18247473025749540a2aa..a26d1cd5068d6149625fe158eef79e57f3f3d146 100644 (file)
--- 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 bfc321cf7b76f62e7fc159e6a39045c1edad3398..a7df7c847a4160cde70c800df880855188bfb34f 100644 (file)
--- 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 38f32aebbcf2bde972bb019e7cb2f10dfb836c1c..14789304b49a797d74a14e4da5af02b6008dcd76 100644 (file)
--- 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 e053d78514f0b3d2b33868837aa2bd5ca97fb1c0..0de0ae477f423f4e8719bd98252a34882f92e3c2 100644 (file)
--- 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 4fd2deabb7e8ed973e02f34e14d4f3fdc447f5ce..42edbb919fb546720705b4a7cb72800f988a3d8b 100644 (file)
--- 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 29a99118eda43b1e26b6553afb11164d9ca2ea08..910565d07025db430bf0c9c37f77a76a84ce74e9 100644 (file)
--- 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 bb9b1e1f52267d02f36cccb3885d74a59f761a98..ba6b4066d4082a541ef440c65c7da14b83d3b532 100644 (file)
--- 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: