more xor-clausing for equality and BVLE/BVLT etc

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

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index 4342f72864d6bca07052f141520846f0d8036378..22c76b7fd51514924a3036265b51d23d43fca7a2 100644 (file)
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -23,7 +23,7 @@ SOLVER_INCLUDE = ../sat/cryptominisat
 
 # OPTION to compile CRYPTOMiniSAT version 2.x
 #CRYPTOMINISAT2 = true
-#CFLAGS_BASE   = $(OPTIMIZE) -DCRYPTOMINISAT2
+#CFLAGS_BASE    = $(OPTIMIZE) -DCRYPTOMINISAT2
 #MTL            = ../sat/cryptominisat2/mtl
 #SOLVER_INCLUDE = ../sat/cryptominisat2
 

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 4a928fdd259435a7dfc64c31ffbbafbc579f6a05..20f4bb020352335b4560cce36a1ce3503c1b4949 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -765,6 +765,19 @@ Expr vc_orExpr(VC vc, Expr left, Expr right) {
   return output;
 }
 
+Expr vc_xorExpr(VC vc, Expr left, Expr right) {
+  bmstar b = (bmstar)(((stpstar)vc)->bm);
+  nodestar l = (nodestar)left;
+  nodestar r = (nodestar)right;
+
+  node o = b->CreateNode(BEEV::XOR,*l,*r);
+  BVTypeCheck(o);
+  nodestar output = new node(o);
+  //if(cinterface_exprdelete_on) created_exprs.push_back(output);
+  return output;
+}
+
+
 Expr vc_andExprN(VC vc, Expr* cc, int n) {
   bmstar b = (bmstar)(((stpstar)vc)->bm);
   nodestar * c = (nodestar *)cc;

diff --git a/src/c_interface/c_interface.h b/src/c_interface/c_interface.h
index cd57735452478e08578a7bcb9a62f06c20e8b6d6..f4a05d03b1775ec7e8ad1f395b79c67abfa55c64 100644 (file)
--- a/src/c_interface/c_interface.h
+++ b/src/c_interface/c_interface.h
@@ -94,6 +94,7 @@ extern "C" {
   Expr vc_andExpr(VC vc, Expr left, Expr right);
   Expr vc_andExprN(VC vc, Expr* children, int numOfChildNodes);
   Expr vc_orExpr(VC vc, Expr left, Expr right);
+  Expr vc_xorExpr(VC vc, Expr left, Expr right);
   Expr vc_orExprN(VC vc, Expr* children, int numOfChildNodes);
   Expr vc_impliesExpr(VC vc, Expr hyp, Expr conc);
   Expr vc_iffExpr(VC vc, Expr left, Expr right);

diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp
index 4193e4b5f953932bcc02f41fa4d6623adc422a55..a762e07001e481f16ee5f4852451eb4a2b142651 100644 (file)
--- a/src/to-sat/BitBlast.cpp
+++ b/src/to-sat/BitBlast.cpp
@@ -940,7 +940,10 @@ namespace BEEV
     ASTVec bit_comparisons;
     bit_comparisons.push_back(this_compare_bit);
     
-    ASTNode prev_eq_bit = _bm->CreateSimpForm(IFF, *lit, *rit);
+    ASTNode prev_eq_bit = 
+      _bm->CreateSimpForm(XOR, 
+                         _bm->CreateSimpForm(NOT,*lit), 
+                         *rit);
     for(lit++, rit++; lit < litend; lit++, rit++)
       {
         this_compare_bit = 
@@ -953,7 +956,9 @@ namespace BEEV
         // (neg(lit) OR rit)(lit OR neg(rit))
         ASTNode this_eq_bit = 
           _bm->CreateSimpForm(AND,
-                              _bm->CreateSimpForm(IFF,*lit,*rit),
+                              _bm->CreateSimpForm(XOR,
+                                                 _bm->CreateSimpForm(NOT,*lit),
+                                                 *rit),
                               prev_eq_bit);
         prev_eq_bit = this_eq_bit;
       }
@@ -966,50 +971,6 @@ namespace BEEV
       _bm->CreateSimpForm(OR, bit_comparisons);
 
     return output;
-    //     // "thisbit" represents BVLE of the suffixes of the BVs
-    //     // from that position .  if R < L, return TRUE, else if L < R
-    //     // return FALSE, else return BVLE of lower-order bits.  MSB is
-    //     // treated separately, because signed comparison is done by
-    //     // complementing the MSB of each BV, then doing an unsigned
-    //     // comparison.    
-    //     ASTVec::const_iterator lit = left.rbegin();
-    //     ASTVec::const_iterator litend = left.rend();
-    //     ASTVec::const_iterator rit = right.rbegin();
-    //     ASTNode prevbit = ASTTrue;
-    //     for (; lit < litend - 1; lit++, rit++)
-    //       {
-    //         ASTNode neglit = _bm->CreateSimpNot(*lit);
-    //         ASTNode thisbit = 
-    //           _bm->CreateSimpForm(OR, 
-    //                               _bm->CreateSimpForm(AND, neglit, *rit),
-    //                               _bm->CreateSimpForm(AND, 
-    //                                                   _bm->CreateSimpForm(OR, 
-    //                                                                       neglit,
-    //                                                                       *rit), 
-    //                                                   prevbit));    
-    //         prevbit = thisbit;
-    //       }
-
-    //     // Handle MSB -- negate MSBs if signed comparison
-    //     // FIXME: make into refs after it's debugged.
-    //     ASTNode lmsb = *lit;
-    //     ASTNode rmsb = *rit;
-    //     if (is_signed)
-    //       {
-    //         lmsb = _bm->CreateSimpNot(*lit);
-    //         rmsb = _bm->CreateSimpNot(*rit);
-    //       }
-
-    //     ASTNode neglmsb = _bm->CreateSimpNot(lmsb);
-    //     ASTNode msb = 
-    //       // TRUE if l < r
-    //       _bm->CreateSimpForm(OR, _bm->CreateSimpForm(AND, neglmsb, rmsb), 
-    //                           _bm->CreateSimpForm(AND, 
-    //                                               _bm->CreateSimpForm(OR, 
-    //                                                                   neglmsb,
-    //                                                                   rmsb),
-    //                                               prevbit)); // else prevbit
-    //     return msb;
   }
 
   // Left shift  within fixed field inserting zeros at LSB.
@@ -1141,7 +1102,9 @@ namespace BEEV
       {
         for (; lit != litend; lit++, rit++)
           {
-            ASTNode biteq = _bm->CreateSimpForm(IFF, *lit, *rit);
+            ASTNode biteq = _bm->CreateSimpForm(XOR, 
+                                               _bm->CreateSimpForm(NOT,*lit), 
+                                               *rit);
             // fast path exit
             if (biteq == ASTFalse)
               {