XOR output for ITE

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@480 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index 884a99055b66cab1ede8c441985122bd42bb00c8..55f0cc572bb10bb2383c05a44994c31b937f03c7 100644 (file)
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -17,16 +17,16 @@ OPTIMIZE      = -O3               # Maximum optimization
 CFLAGS_BASE   = $(OPTIMIZE)
 
 # OPTION to compile CRYPTOMiniSAT
-#CRYPTOMINISAT  = true
-#CFLAGS_BASE    = $(OPTIMIZE) -DCRYPTOMINISAT
-#MTL            = ../sat/cryptominisat/mtl
-#SOLVER_INCLUDE = ../sat/cryptominisat
+CRYPTOMINISAT  = true
+CFLAGS_BASE    = $(OPTIMIZE) -DCRYPTOMINISAT
+MTL            = ../sat/cryptominisat/mtl
+SOLVER_INCLUDE = ../sat/cryptominisat
 
 # OPTION to compile CRYPTOMiniSAT version 2.x
-CRYPTOMINISAT2 = true
-CFLAGS_BASE    = $(OPTIMIZE) -DCRYPTOMINISAT2
-MTL            = ../sat/cryptominisat2/mtl
-SOLVER_INCLUDE = ../sat/cryptominisat2
+# CRYPTOMINISAT2 = true
+# CFLAGS_BASE    = $(OPTIMIZE) -DCRYPTOMINISAT2
+# MTL            = ../sat/cryptominisat2/mtl
+# SOLVER_INCLUDE = ../sat/cryptominisat2
 
 # OPTION to compile MiniSAT
 #CORE          = true

diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp
index d3c7cf5f2787f9f478c4fbc7d33b453306570f9a..8eac6312d5d349b37dbc6144ae7e41c5cf337178 100644 (file)
--- a/src/to-sat/BitBlast.cpp
+++ b/src/to-sat/BitBlast.cpp
@@ -1104,6 +1104,7 @@ namespace BEEV
         return n;
       }
     else
-      return _bm->CreateSimpForm(IFF, *lit, *rit);
+      return _bm->CreateSimpForm(XOR, 
+                                _bm->CreateSimpForm(NOT,*lit), *rit);
   }
 } // BEEV namespace

diff --git a/src/to-sat/SimpBool.cpp b/src/to-sat/SimpBool.cpp
index 5b1ae409683da1b1d118688ee6ea100fa941b304..5ff029a8204d3eae84a7cd9ccc7105ab63b273d4 100644 (file)
--- a/src/to-sat/SimpBool.cpp
+++ b/src/to-sat/SimpBool.cpp
@@ -49,10 +49,6 @@ namespace BEEV
             break;
           case IFF:
             {
-              // Not sure children can ever be empty, but what the heck.
-              //        if (children.size() == 0) {
-              //          return ASTTrue;
-              //        }
               // Convert IFF to XOR ASAP to simplify flattening.
               children[0] = CreateSimpNot(children[0]);
               return CreateSimpXor(children);
@@ -61,8 +57,8 @@ namespace BEEV
           case XOR:
             return CreateSimpXor(children);
             break;
-            // FIXME: Earlier, check that this only has two arguments
           case IMPLIES:
+            // FIXME: Earlier, check that this only has two arguments
             return CreateSimpAndOr(0, CreateSimpNot(children[0]), children[1]);
             break;
           case ITE:
@@ -485,18 +481,26 @@ namespace BEEV
       {
         retval = CreateSimpAndOr(1, child0, child1);
       }
-    // ITE (x, !y, y) == x XOR y
-    //     else if (NOT == child1.GetKind() && (child1[0] == child2)) {
-    //       retval = CreateSimpXor(child0, child2);
-    //     }
-    //     // ITE (x, y, !y) == x IFF y.  I think other cases are covered
-    //     // by XOR/IFF optimizations
-    //     else if (NOT == child2.GetKind() && (child2[0] == child1)) {
-    //       retval = CreateSimpXor(CreateSimpNot(child0), child2);
-    //     }
+//     //ITE (x, !y, y) == x XOR y
+//     else if (NOT == child1.GetKind() && (child1[0] == child2))
+//       {
+//     retval = CreateSimpXor(child0, child2);
+//       }
+//     // ITE (x, y, !y) == x IFF y.  I think other cases are covered
+//     // by XOR/IFF optimizations
+//     else if (NOT == child2.GetKind() && (child2[0] == child1)) 
+//       {
+//     retval = CreateSimpXor(CreateSimpNot(child0), child2);
+//       }
     else
       {
-        retval = CreateNode(ITE, child0, child1, child2);
+       ASTNode left = 
+         CreateNode(AND, child0, child1);
+       ASTNode right = 
+         CreateNode(AND,
+                    CreateNode(NOT,child0),
+                    child2);
+        retval = CreateNode(XOR, left, right);
       }
 
     if (_trace_simpbool)