From 1d0ccd46837ad92a4506f6e32e2206da2f7556f3 Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Sun, 6 Dec 2009 21:49:20 +0000 Subject: [PATCH] added option to that allows STP to give randomized answers to queries git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@467 e59a4935-1847-0410-ae03-e826735625c1 --- scripts/Makefile.common | 16 ++++++++-------- src/AST/UsefulDefs.h | 3 ++- src/STPManager/UserDefinedFlags.h | 15 ++++++++++++--- src/c_interface/c_interface.cpp | 8 ++++++-- src/main/main.cpp | 10 +++++++++- src/to-sat/CallSAT.cpp | 1 - src/to-sat/ToSAT.cpp | 12 ++++++++++-- tests/crypto-tests/t3_flat.stp | 28 ++++++++++++++++++++++++++++ 8 files changed, 75 insertions(+), 18 deletions(-) create mode 100644 tests/crypto-tests/t3_flat.stp diff --git a/scripts/Makefile.common b/scripts/Makefile.common index 4dbe32b..884a990 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/AST/UsefulDefs.h b/src/AST/UsefulDefs.h index 5d5a17f..060764a 100644 --- a/src/AST/UsefulDefs.h +++ b/src/AST/UsefulDefs.h @@ -44,8 +44,9 @@ #define HASHMAP hash_map #define HASHSET hash_set #define HASHMULTISET hash_multiset -#define INITIAL_TABLE_SIZE 100 +#define INITIAL_TABLE_SIZE 100 #define CLAUSAL_ABSTRACTION_CUTOFF 0.5 +#define MAX_BUCKET_LIMIT 3 using namespace std; namespace BEEV { diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h index 65fb85a..359df1f 100644 --- a/src/STPManager/UserDefinedFlags.h +++ b/src/STPManager/UserDefinedFlags.h @@ -62,7 +62,11 @@ namespace BEEV //Flag that determines whether the Boolean SAT solver should //assign random polarity to the Boolean variables - bool rand_bool_polarity_flag; + bool random_seed_flag; + int random_seed; + + //Flag that allows the printing of the DIMACS format of the input + bool print_cnf_flag; //flag to decide whether to print "valid/invalid" or not bool print_output_flag; @@ -128,7 +132,7 @@ namespace BEEV //Determines the number of abstraction-refinement loop count for the //for-construct num_absrefine_flag = false; - int num_absrefine = 0; + num_absrefine = 0; //if this option is true then print the way dawson wants using a //different printer. do not use this printer. @@ -136,7 +140,12 @@ namespace BEEV //Flag that determines whether the Boolean SAT solver should //assign random polarity to the Boolean variables - rand_bool_polarity_flag = false; + random_seed_flag = false; + random_seed = 0; + + //Flag that allows the printing of the DIMACS format of the + //input + print_cnf_flag = false; //flag to decide whether to print "valid/invalid" or not print_output_flag = false; diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index 20f4bb0..caae185 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -36,7 +36,7 @@ bool cinterface_exprdelete_on_flag = false; extern int cvcparse(void*); extern int smtparse(void*); -void vc_setFlags(VC vc, char c, int num_absrefine) { +void vc_setFlags(VC vc, char c, int param_value) { bmstar b = (bmstar)(((stpstar)vc)->bm); std::string helpstring = @@ -88,7 +88,7 @@ void vc_setFlags(VC vc, char c, int num_absrefine) { break; case 'f': b->UserFlags.num_absrefine_flag = true; - b->UserFlags.num_absrefine = num_absrefine; + b->UserFlags.num_absrefine = param_value; break; case 'h': fprintf(stderr,BEEV::usage,BEEV::prog); @@ -96,6 +96,10 @@ void vc_setFlags(VC vc, char c, int num_absrefine) { //FatalError(""); //return -1; break; + case 'i': + b->UserFlags.random_seed_flag = true; + b->UserFlags.random_seed = param_value; + break; case 'n': b->UserFlags.print_output_flag = true; break; diff --git a/src/main/main.cpp b/src/main/main.cpp index 6eb3492..7202de2 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -158,7 +158,15 @@ int main(int argc, char ** argv) { return -1; break; case 'i': - bm->UserFlags.rand_bool_polarity_flag = true; + bm->UserFlags.random_seed_flag = true; + bm->UserFlags.random_seed = atoi(argv[++i]); + if(!(0 <= bm->UserFlags.random_seed)) + { + FatalError("Random Seed should be an integer >= 0\n"); + } + break; + case 'j': + bm->UserFlags.print_cnf_flag = true; break; case 'n': bm->UserFlags.print_output_flag = true; diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp index 9338c61..2df4a41 100644 --- a/src/to-sat/CallSAT.cpp +++ b/src/to-sat/CallSAT.cpp @@ -7,7 +7,6 @@ * LICENSE: Please view LICENSE file in the home dir of this Program ********************************************************************/ #include "ToSAT.h" -#define MAX_BUCKET_LIMIT 3 namespace BEEV { diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index 3c6cce0..8cd957f 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -78,9 +78,17 @@ namespace BEEV FatalError("toSATandSolve: Nothing to Solve", ASTUndefined); } - if(bm->UserFlags.rand_bool_polarity_flag) + if(bm->UserFlags.random_seed_flag) { - newSolver.polarity_mode = newSolver.polarity_rnd; + newSolver.setSeed(bm->UserFlags.random_seed); + //cerr << "We have set the seed value to " + // << bm->UserFlags.random_seed + // << endl; + } + + if(bm->UserFlags.print_cnf_flag) + { + #define DEBUG_LIB } #ifdef CRYPTOMINISAT newSolver.startClauseAdding(); diff --git a/tests/crypto-tests/t3_flat.stp b/tests/crypto-tests/t3_flat.stp new file mode 100644 index 0000000..75718a6 --- /dev/null +++ b/tests/crypto-tests/t3_flat.stp @@ -0,0 +1,28 @@ + +a,b,c,x,y : BITVECTOR(96); + + +ASSERT(a[0:0] = 0bin1); +ASSERT(b[0:0] = 0bin1); +ASSERT(c=0hex0000000000000056E35E38CD); +ASSERT(a[95:48] = 0hex000000000000); +ASSERT(b[95:48] = 0hex000000000000); + + +QUERY( + NOT ( + c=BVMULT(96,a,b) AND NOT + a=0hex000000000000000000000001 + AND + NOT + b=0hex000000000000000000000001 + AND NOT + a=c + AND NOT + b=c + + ) +); + +COUNTEREXAMPLE; + -- 2.47.3