Refactor.

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

diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h
index a3faf0942cc94157ff5f8b91262bd1f888fb05ec..7fdcb313defefa77fc1102268b1821a78f9fac1f 100644 (file)
--- a/src/STPManager/UserDefinedFlags.h
+++ b/src/STPManager/UserDefinedFlags.h
@@ -143,6 +143,15 @@ namespace BEEV
        config_options[n] = v;
     }
 
+    void disableSimplifications()
+    {
+      optimize_flag = false;
+      bitConstantProp_flag = false;
+      set("enable-unconstrained","0");
+      set("use-intervals","0");
+      wordlevel_solve_flag = false;
+    }
+
     string get(string n)
     {
        return get(n,"");

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 5908bbd4e224f5e4a2f44aa1445fcfb70d745e59..79474e5d879d0fad5d74d304b5b2b4534a2fc15c 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -301,11 +301,7 @@ int main(int argc, char ** argv) {
                                   bm->UserFlags.solver_to_use = UserDefinedFlags::MINISAT_SOLVER;
                                   break;
                           case DISABLE_SIMPLIFICATIONS:
-                                  bm->UserFlags.optimize_flag = false;
-                                  bm->UserFlags.bitConstantProp_flag = false;
-                                  bm->UserFlags.set("enable-unconstrained","0");
-                                  bm->UserFlags.set("use-intervals","0");
-                                  bm->UserFlags.wordlevel_solve_flag = false;
+                                  bm->UserFlags.disableSimplifications();
                                 break;
                          default:
                                  fprintf(stderr,usage,prog);