diff options
author | Tim King <taking@cs.nyu.edu> | 2011-05-31 01:06:16 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-05-31 01:06:16 +0000 |
commit | 46a299aa48bcb0bff64bdb607f61f75a05987962 (patch) | |
tree | 3880ed92599b84b59d4b135ab4513dd7c50f76e4 /src/theory/arith/arith_prop_manager.cpp | |
parent | b9ffc0f2cf5d2f05e5269ffb8b5f58c5d7f71e0c (diff) |
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.
Diffstat (limited to 'src/theory/arith/arith_prop_manager.cpp')
-rw-r--r-- | src/theory/arith/arith_prop_manager.cpp | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/theory/arith/arith_prop_manager.cpp b/src/theory/arith/arith_prop_manager.cpp index 77d32ef0b..7f38c74a7 100644 --- a/src/theory/arith/arith_prop_manager.cpp +++ b/src/theory/arith/arith_prop_manager.cpp @@ -34,10 +34,10 @@ Node ArithPropManager::strictlyWeakerAssertedUpperBound(ArithVar v, const DeltaR Node weaker = bound; do { if(largeEpsilon){ - weaker = d_propagator.getBestImpliedUpperBound(weaker); + weaker = d_atomDatabase.getBestImpliedUpperBound(weaker); largeEpsilon = false; }else{ - weaker = d_propagator.getWeakerImpliedUpperBound(weaker); + weaker = d_atomDatabase.getWeakerImpliedUpperBound(weaker); } }while(!weaker.isNull() && !isAsserted(weaker)); return weaker; @@ -54,10 +54,10 @@ Node ArithPropManager::strictlyWeakerAssertedLowerBound(ArithVar v, const DeltaR Debug("ArithPropManager") << bound << b << endl; do { if(largeEpsilon){ - weaker = d_propagator.getBestImpliedLowerBound(weaker); + weaker = d_atomDatabase.getBestImpliedLowerBound(weaker); largeEpsilon = false; }else{ - weaker = d_propagator.getWeakerImpliedLowerBound(weaker); + weaker = d_atomDatabase.getWeakerImpliedLowerBound(weaker); } }while(!weaker.isNull() && !isAsserted(weaker)); Debug("ArithPropManager") << "res: " << weaker << endl; @@ -66,11 +66,11 @@ Node ArithPropManager::strictlyWeakerAssertedLowerBound(ArithVar v, const DeltaR Node ArithPropManager::getBestImpliedLowerBound(ArithVar v, const DeltaRational& b) const{ Node bound = boundAsNode(false, v, b); - return d_propagator.getBestImpliedLowerBound(bound); + return d_atomDatabase.getBestImpliedLowerBound(bound); } Node ArithPropManager::getBestImpliedUpperBound(ArithVar v, const DeltaRational& b) const{ Node bound = boundAsNode(true, v, b); - return d_propagator.getBestImpliedUpperBound(bound); + return d_atomDatabase.getBestImpliedUpperBound(bound); } Node ArithPropManager::boundAsNode(bool upperbound, ArithVar var, const DeltaRational& b) const { @@ -106,8 +106,8 @@ bool ArithPropManager::propagateArithVar(bool upperbound, ArithVar var, const De Node bAsNode = boundAsNode(upperbound, var ,b); Node bestImplied = upperbound ? - d_propagator.getBestImpliedUpperBound(bAsNode): - d_propagator.getBestImpliedLowerBound(bAsNode); + d_atomDatabase.getBestImpliedUpperBound(bAsNode): + d_atomDatabase.getBestImpliedLowerBound(bAsNode); Debug("ArithPropManager") << upperbound <<","<< var <<","<< b <<","<< reason << endl << bestImplied << endl; |