diff options
author | Tim King <taking@cs.nyu.edu> | 2011-03-30 15:07:02 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-03-30 15:07:02 +0000 |
commit | 6495988f28ad6c9b318fc506e5d85d8613b03640 (patch) | |
tree | f8679ffdf53b9d38f307e03b34aed251ba37bfbd | |
parent | 10cabf82a20258da80be53eb6d23b1a536e82eb5 (diff) |
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.
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 5 | ||||
-rw-r--r-- | src/util/options.cpp | 11 | ||||
-rw-r--r-- | src/util/options.h | 1 |
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; |