From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 29 Dec 2011 02:50:12 +0000 (+0000)
Subject: Improvement. Disable propagating equalities separately
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=abfd4673b00bdb340dd3ee97d693c650ae374732;p=francis%2Fstp.git

Improvement. Disable propagating equalities separately

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

diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h
index 3e83589..c511b61 100644
--- a/src/STPManager/UserDefinedFlags.h
+++ b/src/STPManager/UserDefinedFlags.h
@@ -80,6 +80,10 @@ namespace BEEV
     //turn on word level bitvector solver
     bool wordlevel_solve_flag;
     
+
+    bool propagate_equalities;
+
+
     //XOR flattening optimizations.
     bool xor_flatten_flag;
     
@@ -150,6 +154,7 @@ namespace BEEV
       set("enable-unconstrained","0");
       set("use-intervals","0");
       wordlevel_solve_flag = false;
+      propagate_equalities = false;
     }
 
     string get(string n)
@@ -234,6 +239,9 @@ namespace BEEV
       //turn on word level bitvector solver
       wordlevel_solve_flag = true;
       
+      //propagate equalities.
+      propagate_equalities = true;
+
       //turn off XOR flattening
       xor_flatten_flag = false;
       
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 771a16e..d260785 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -78,7 +78,7 @@ static const intptr_t INITIAL_MEMORY_PREALLOCATION_SIZE = 4000000;
  * step 5. Call SAT to determine if input is SAT or UNSAT
  ********************************************************************/
 
-typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB2,PRINT_BACK_SMTLIB1, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER, SMT_LIB2_FORMAT, SMT_LIB1_FORMAT, DISABLE_CBITP,EXIT_AFTER_CNF,USE_CRYPTOMINISAT_SOLVER,USE_MINISAT_SOLVER, DISABLE_SIMPLIFICATIONS, OLDSTYLE_REFINEMENT} OptionType;
+typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB2,PRINT_BACK_SMTLIB1, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER, SMT_LIB2_FORMAT, SMT_LIB1_FORMAT, DISABLE_CBITP,EXIT_AFTER_CNF,USE_CRYPTOMINISAT_SOLVER,USE_MINISAT_SOLVER, DISABLE_SIMPLIFICATIONS, OLDSTYLE_REFINEMENT, DISABLE_EQUALITY} OptionType;
 
 
 int main(int argc, char ** argv) {
@@ -127,6 +127,7 @@ int main(int argc, char ** argv) {
     "-w                     : switch wordlevel solver off (optimizations are ON by default)\n"
     "-a                     : disable potentially size-increasing optimisations\n"
     "--disable-cbitp        : disable constant bit propagation\n"
+    "--disable-equality     : disable equality propagation\n"
     "\n"
     "--cryptominisat        : use cryptominisat2 as the solver\n"
     "--simplifying-minisat  : use simplifying-minisat 2.2 as the solver\n"
@@ -142,8 +143,7 @@ int main(int argc, char ** argv) {
     "--print-back-GDL       : print AiSee's graph format, then exit\n"
     "--print-back-dot       : print dotty/neato's graph format, then exit\n"
     "\n"
-    "-m                     : use the SMTLIB1 parser\n"
-    "--SMTLIB1              : use the SMT-LIB1 format parser\n"
+    "--SMTLIB1 -m           : use the SMT-LIB1 format parser\n"
     "--SMTLIB2              : use the SMT-LIB2 format parser\n"
     "\n"
     "--output-CNF           : save the CNF into output_[0..n].cnf\n"
@@ -189,6 +189,8 @@ int main(int argc, char ** argv) {
 			  lookup.insert(make_pair(tolower("--disable-cbitp"),DISABLE_CBITP));
 			  lookup.insert(make_pair(tolower("--disable-simplify"),DISABLE_SIMPLIFICATIONS));
 			  lookup.insert(make_pair(tolower("--oldstyle-refinement"),OLDSTYLE_REFINEMENT));
+			  lookup.insert(make_pair(tolower("--disable-equality"),DISABLE_EQUALITY));
+
 
 			  if (!strncmp(argv[i],"--config_",strlen("--config_")))
 			  {
@@ -279,6 +281,10 @@ int main(int argc, char ** argv) {
                           case DISABLE_SIMPLIFICATIONS:
                                   bm->UserFlags.disableSimplifications();
                                 break;
+                          case DISABLE_EQUALITY:
+                                  bm->UserFlags.propagate_equalities = false;
+                                  break;
+
 			  default:
 				  fprintf(stderr,usage,prog);
 	               cout << helpstring;
diff --git a/src/simplifier/PropagateEqualities.cpp b/src/simplifier/PropagateEqualities.cpp
index d2fd504..46c21f5 100644
--- a/src/simplifier/PropagateEqualities.cpp
+++ b/src/simplifier/PropagateEqualities.cpp
@@ -21,7 +21,7 @@ namespace BEEV
 
     ASTNode PropagateEqualities::propagate(const ASTNode& a,  ArrayTransformer*at)
     {
-      if (!bm->UserFlags.wordlevel_solve_flag)
+      if (!bm->UserFlags.propagate_equalities)
         return a;
 
       ASTNode output;