From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 7 Dec 2009 21:42:45 +0000 (+0000)
Subject: XOR output for ITE
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=e9a15e9aece9bf9b35a4f3440e220ed7d5fb2e4c;p=francis%2Fstp.git

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 884a990..55f0cc5 100644
--- 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 d3c7cf5..8eac631 100644
--- 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 5b1ae40..5ff029a 100644
--- 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)