From 46a299aa48bcb0bff64bdb607f61f75a05987962 Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 31 May 2011 01:06:16 +0000 Subject: 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. --- src/theory/arith/arith_prop_manager.cpp | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'src/theory/arith/arith_prop_manager.cpp') 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; -- cgit v1.2.3