Added the command line flag --rewrite-arithmetic-equalities. This sets a static flag in Options that the ArithRewriter uses to determine the equality rewriting policy.

3 files changed, 16 insertions, 1 deletions

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 941394138..cecbefdee 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -261,8 +261,13 @@ RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){
   }else if(reduction.getKind() == kind::LT){
     Node geq = currNM->mkNode(kind::GEQ, reduction[0], reduction[1]);
     reduction = currNM->mkNode(kind::NOT, geq);
+  }else if( Options::rewriteArithEqualities && reduction.getKind() == kind::EQUAL){
+    Node geq = currNM->mkNode(kind::GEQ, reduction[0], reduction[1]);
+    Node leq = currNM->mkNode(kind::LEQ, reduction[0], reduction[1]);
+    reduction = currNM->mkNode(kind::AND, geq, leq);
   }
 
+
   return RewriteResponse(REWRITE_DONE, reduction);
 }
 
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 6fc71bae3..94d479166 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -67,6 +67,7 @@ static const string optionsDescription = "\
    --produce-models       support the get-value command\n\
    --produce-assignments  support the get-assignment command\n\
    --lazy-definition-expansion expand define-fun lazily\n\
+   --rewrite-arithmetic-equalities rewrite (= x y) to (and (<= x y) (>= x y)) in arithmetic \n\
    --incremental          enable incremental solving\n";
 
 static const string languageDescription = "\
@@ -121,7 +122,8 @@ enum OptionValue {
   LAZY_TYPE_CHECKING,
   EAGER_TYPE_CHECKING,
   INCREMENTAL,
-  PIVOT_RULE
+  PIVOT_RULE,
+  REWRITE_ARITHMETIC_EQUALITIES
 };/* enum OptionValue */
 
 /**
@@ -179,6 +181,7 @@ static struct option cmdlineOptions[] = {
   { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING},
   { "incremental", no_argument, NULL, INCREMENTAL},
   { "pivot-rule" , required_argument, NULL, PIVOT_RULE  },
+  { "rewrite-arithmetic-equalities" , no_argument, NULL, REWRITE_ARITHMETIC_EQUALITIES},
   { NULL         , no_argument      , NULL, '\0'        }
 };/* if you add things to the above, please remember to update usage.h! */
 
@@ -376,6 +379,10 @@ throw(OptionException) {
       incrementalSolving = true;
       break;
 
+    case REWRITE_ARITHMETIC_EQUALITIES:
+      rewriteArithEqualities = true;
+      break;
+
     case PIVOT_RULE:
       if(!strcmp(optarg, "min")) {
         pivotRule = MINIMUM;
@@ -438,4 +445,6 @@ throw(OptionException) {
   return optind;
 }
 
+bool Options::rewriteArithEqualities = false;
+
 }/* CVC4 namespace */
diff --git a/src/util/options.h b/src/util/options.h
index 2618f8512..2ddc8224f 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -129,6 +129,7 @@ struct CVC4_PUBLIC Options {
   /** Whether incemental solving (push/pop) */
   bool incrementalSolving;
 
+  static bool rewriteArithEqualities;
 
   typedef enum { MINIMUM, BREAK_TIES, MAXIMUM } ArithPivotRule;
   ArithPivotRule pivotRule;