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

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index 4dbe32bcb7a93c72d60c3006ef1e2fa97bbaec68..884a99055b66cab1ede8c441985122bd42bb00c8 100644 (file)
--- 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 5d5a17f93f71e24b5ad71f10d1044e8b952c5736..060764a105cd4fab52c88fd7cd7338214cb2d7d9 100644 (file)
--- 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 65fb85a7b836805d32611caf37d1663d2d32341a..359df1f51bbceb599a983c0c05a0af61c14f3996 100644 (file)
--- 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 20f4bb020352335b4560cce36a1ce3503c1b4949..caae1856684360be897bd96c8d7353d5290f5b60 100644 (file)
--- 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 6eb34922cc311eb785b53d68a6e14b6a147b1ef5..7202de28653362a47856dbed192667c83e7cbc63 100644 (file)
--- 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 9338c61588f81a107dfc0499a05dbcbef913ef22..2df4a41e6a2f6b187cf9a8143079c9b1ec02f37b 100644 (file)
--- 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 3c6cce01fd77d49b167528928d3b277d3f62a731..8cd957f451a6edf1d18d8c3775e0ddddd3806bfd 100644 (file)
--- 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 (file)
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;
+