From 65b49121f7d28e52b0ac1ad1a4d1713d9bd8be5b Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Sat, 5 Dec 2009 23:12:21 +0000 Subject: [PATCH] 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 --- scripts/Makefile.common | 2 +- src/to-sat/BitBlast.cpp | 3 ++- src/to-sat/SimpBool.cpp | 3 --- 3 files changed, 3 insertions(+), 5 deletions(-) diff --git a/scripts/Makefile.common b/scripts/Makefile.common index 2922cfc..4dbe32b 100644 --- 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 07d22dd..f557225 100644 --- 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 b48b96b..977de28 100644 --- 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; -- 2.47.3