This commit contains the code for allowing arbitrary equalities in the theory of arithmetic.

* This code has been partially tested. (My testing situation is currently not so great.)  The code for testing not preregistering equalities can be compile time enabled by setting the boolean turnOffEqualityPreRegister. Don't be shocked by slowdowns or failures.  This does pass make regress as well as a fresh checkout does. (The Mac version has issues.)
* I need to disable the permanent row removal heuristic by default.  We need to discuss why this needs to happen.  We should probably detect pure QF_LRA/QF_RDL problems and enable this when this can safely be done.
* I have disabled the arithmetic rewrite equality flag.  This code needs to be added to the parser. 
* For all of the above changes, I have annotated the code with the key word BREADCRUMB.
* I have renamed ArithUnatePropagator to ArithAtomDatabase.

1 files changed, 6 insertions, 6 deletions

diff --git a/src/util/options.cpp b/src/util/options.cpp
index f68b64ab6..337eba9b6 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -82,7 +82,7 @@ Options::Options() :
   replayFilename(""),
   replayStream(NULL),
   replayLog(NULL),
-  rewriteArithEqualities(false),
+  variableRemovalEnabled(false),
   arithPropagation(false),
   satRandomFreq(0.0),
   satRandomSeed(91648253),// Minisat's default value
@@ -123,7 +123,7 @@ static const string optionsDescription = "\
    --pivot-rule=RULE      change the pivot rule (see --pivot-rule help)\n\
    --random-freq=P        sets the frequency of random decisions in the sat solver(P=0.0 by default)\n\
    --random-seed=S        sets the random seed for the sat solver\n\
-   --rewrite-arithmetic-equalities rewrite (= x y) to (and (<= x y) (>= x y)) in arithmetic\n\
+   --variable-removal-enables enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\
    --enable-arithmetic-propagation turns on arithmetic propagation\n\
    --incremental          enable incremental solving\n";
 
@@ -213,7 +213,7 @@ enum OptionValue {
   PIVOT_RULE,
   RANDOM_FREQUENCY,
   RANDOM_SEED,
-  REWRITE_ARITHMETIC_EQUALITIES,
+  ENABLE_VARIABLE_REMOVAL,
   ARITHMETIC_PROPAGATION
 };/* enum OptionValue */
 
@@ -282,7 +282,7 @@ static struct option cmdlineOptions[] = {
   { "pivot-rule" , required_argument, NULL, PIVOT_RULE  },
   { "random-freq" , required_argument, NULL, RANDOM_FREQUENCY  },
   { "random-seed" , required_argument, NULL, RANDOM_SEED  },
-  { "rewrite-arithmetic-equalities", no_argument, NULL, REWRITE_ARITHMETIC_EQUALITIES },
+  { "enable-variable-removel", no_argument, NULL, ENABLE_VARIABLE_REMOVAL },
   { "enable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION },
   { NULL         , no_argument      , NULL, '\0'        }
 };/* if you add things to the above, please remember to update usage.h! */
@@ -532,8 +532,8 @@ throw(OptionException) {
 #endif /* CVC4_REPLAY */
       break;
 
-    case REWRITE_ARITHMETIC_EQUALITIES:
-      rewriteArithEqualities = true;
+    case ENABLE_VARIABLE_REMOVAL:
+      variableRemovalEnabled = true;
       break;
 
     case ARITHMETIC_PROPAGATION: