Add IFF support

[satune.git] / src / csolver.cc

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) {