changed the way BVDIV is bitblasted

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

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index 2922cfc70e7f87354b450596a4146a61ced4a143..4dbe32bcb7a93c72d60c3006ef1e2fa97bbaec68 100644 (file)
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -12,7 +12,7 @@
 OPTIMIZE      = -g                # Debugging
 OPTIMIZE      = -O3               # Maximum optimization
 #OPTIMIZE      = -O3 -march=native # Maximum optimization
-#OPTIMIZE     = -O3 -DNDEBUG -DLESSBYTES_PERNODE
+#OPTIMIZE     = -O3 -march=native -DNDEBUG -DLESSBYTES_PERNODE
 #CFLAGS_M32   = -m32
 CFLAGS_BASE   = $(OPTIMIZE)
 

diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp
index 07d22ddb83a6ce291a270a623c9fdf59ebd5443e..f5572257b65064d83a8e1e8df43cd7a0f02705bd 100644 (file)
--- a/src/to-sat/BitBlast.cpp
+++ b/src/to-sat/BitBlast.cpp
@@ -867,7 +867,8 @@ namespace BEEV
         ASTVec notylessxqval = BBITE(yeqx, one, ygtrxqval);
         ASTVec notylessxrval = BBITE(yeqx, BBfill(width, ASTFalse), ygtrxrval);
         // y < x <=> not x >= y.
-        ASTNode ylessx = _bm->CreateSimpNot(BBBVLE(x, y, false));
+        //ASTNode ylessx = _bm->CreateSimpNot(BBBVLE(x, y, false));
+        ASTNode ylessx = BBBVLE(y, x, false, true);
         // final values of q and r
         q = BBITE(ylessx, BBfill(width, ASTFalse), notylessxqval);
         r = BBITE(ylessx, y, notylessxrval);

diff --git a/src/to-sat/SimpBool.cpp b/src/to-sat/SimpBool.cpp
index b48b96b4a2f63bfd0ac123e0dbc9cd4a3d1018a5..977de28e8a94e671b72240a3876db25da6ce88ab 100644 (file)
--- a/src/to-sat/SimpBool.cpp
+++ b/src/to-sat/SimpBool.cpp
@@ -10,9 +10,6 @@
 // Simplifying create methods for Boolean operations.  These are only
 // very simple local simplifications.
 
-// This is somewhat redundant with Vijay's simplifier code.  They need
-// to be merged.  FIXME: control with optimize flag.
-
 static bool _trace_simpbool = 0;
 static bool _disable_simpbool = 0;