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 3e83589e27e4fd15cf972a09fed39352d107722f..c511b611109d9404ab054416b87f17fcccdeeb23 100644 (file)
--- 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 771a16eceb84dcd90a768cb6d178e3c1a364969a..d2607852fa66cd78e53323fc5f9dcfeb9e8c8272 100644 (file)
--- 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 d2fd504091227dccb5c12aa28343b823014e5f71..46c21f518e5c0749f15cb2244b827cd125803b20 100644 (file)
--- 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;