* 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.
arith_prop_manager.h \
arith_prop_manager.cpp \
arithvar_node_map.h \
+ atom_database.h \
+ atom_database.cpp \
normal_form.h\
normal_form.cpp \
arith_utilities.h \
arith_priority_queue.cpp \
simplex.h \
simplex.cpp \
- unate_propagator.h \
- unate_propagator.cpp \
theory_arith.h \
theory_arith.cpp
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;
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;
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 {
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;
#include "theory/valuation.h"
#include "theory/arith/arith_utilities.h"
#include "theory/arith/arithvar_node_map.h"
-#include "theory/arith/unate_propagator.h"
+#include "theory/arith/atom_database.h"
#include "theory/arith/delta_rational.h"
#include "context/context.h"
#include "context/cdlist.h"
d_reasons.push_back(reason);
d_propagated.push_back(n);
- //std::cout << n << std::endl << "<="<< reason<< std::endl;
+ Debug("ArithPropManager") << n << std::endl << "<="<< reason<< std::endl;
}
bool hasMorePropagations() const {
class ArithPropManager : public PropManager {
private:
const ArithVarNodeMap& d_arithvarNodeMap;
- const ArithUnatePropagator& d_propagator;
+ const ArithAtomDatabase& d_atomDatabase;
Valuation d_valuation;
public:
ArithPropManager(context::Context* c,
const ArithVarNodeMap& map,
- const ArithUnatePropagator& prop,
+ const ArithAtomDatabase& db,
Valuation v):
- PropManager(c), d_arithvarNodeMap(map), d_propagator(prop), d_valuation(v)
+ PropManager(c), d_arithvarNodeMap(map), d_atomDatabase(db), d_valuation(v)
{}
/**
Node boundAsNode(bool upperbound, ArithVar var, const DeltaRational& b) const;
Node strictlyWeakerLowerBound(TNode n) const{
- return d_propagator.getWeakerImpliedLowerBound(n);
+ return d_atomDatabase.getWeakerImpliedLowerBound(n);
}
Node strictlyWeakerUpperBound(TNode n) const{
- return d_propagator.getWeakerImpliedUpperBound(n);
+ return d_atomDatabase.getWeakerImpliedUpperBound(n);
}
Node strictlyWeakerAssertedUpperBound(ArithVar v, const DeltaRational& b) const;
Node getBestImpliedUpperBound(ArithVar v, const DeltaRational& b) const;
bool containsLiteral(TNode n) const {
- return d_propagator.containsLiteral(n);
+ return d_atomDatabase.containsLiteral(n);
}
private:
}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::current()->rewriteArithEqualities && reduction.getKind() == kind::EQUAL){
+ }
+ /* BREADCRUMB : Move this rewrite into preprocessing
+ else if( Options::current()->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);
--- /dev/null
+/********************* */
+/*! \file atom_database.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "theory/arith/atom_database.h"
+#include "theory/arith/arith_utilities.h"
+
+#include <list>
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::arith;
+
+using namespace CVC4::kind;
+
+using namespace std;
+
+ArithAtomDatabase::ArithAtomDatabase(context::Context* cxt, OutputChannel& out) :
+ d_arithOut(out), d_setsMap()
+{ }
+
+bool ArithAtomDatabase::leftIsSetup(TNode left) const{
+ return d_setsMap.find(left) != d_setsMap.end();
+}
+
+const ArithAtomDatabase::VariablesSets& ArithAtomDatabase::getVariablesSets(TNode left) const{
+ Assert(leftIsSetup(left));
+ NodeToSetsMap::const_iterator i = d_setsMap.find(left);
+ return i->second;
+}
+ArithAtomDatabase::VariablesSets& ArithAtomDatabase::getVariablesSets(TNode left){
+ Assert(leftIsSetup(left));
+ NodeToSetsMap::iterator i = d_setsMap.find(left);
+ return i->second;
+}
+EqualValueSet& ArithAtomDatabase::getEqualValueSet(TNode left){
+ Assert(leftIsSetup(left));
+ return getVariablesSets(left).d_eqValueSet;
+}
+
+const EqualValueSet& ArithAtomDatabase::getEqualValueSet(TNode left) const{
+ Assert(leftIsSetup(left));
+ return getVariablesSets(left).d_eqValueSet;
+}
+
+BoundValueSet& ArithAtomDatabase::getBoundValueSet(TNode left){
+ Assert(leftIsSetup(left));
+ return getVariablesSets(left).d_boundValueSet;
+}
+
+const BoundValueSet& ArithAtomDatabase::getBoundValueSet(TNode left) const{
+ Assert(leftIsSetup(left));
+ return getVariablesSets(left).d_boundValueSet;
+}
+
+bool ArithAtomDatabase::hasAnyAtoms(TNode v) const{
+ Assert(!leftIsSetup(v)
+ || !(getEqualValueSet(v)).empty()
+ || !(getBoundValueSet(v)).empty());
+
+ return leftIsSetup(v);
+}
+
+void ArithAtomDatabase::setupLefthand(TNode left){
+ Assert(!leftIsSetup(left));
+
+ d_setsMap[left] = VariablesSets();
+}
+
+bool ArithAtomDatabase::containsLiteral(TNode lit) const{
+ switch(lit.getKind()){
+ case NOT: return containsAtom(lit[0]);
+ default: return containsAtom(lit);
+ }
+}
+
+bool ArithAtomDatabase::containsAtom(TNode atom) const{
+ switch(atom.getKind()){
+ case EQUAL: return containsEquality(atom);
+ case LEQ: return containsLeq(atom);
+ case GEQ: return containsGeq(atom);
+ default:
+ Unreachable();
+ }
+}
+
+bool ArithAtomDatabase::containsEquality(TNode atom) const{
+ TNode left = atom[0];
+ const EqualValueSet& eqSet = getEqualValueSet(left);
+ return eqSet.find(atom) != eqSet.end();
+}
+
+bool ArithAtomDatabase::containsLeq(TNode atom) const{
+ TNode left = atom[0];
+ const Rational& value = rightHandRational(atom);
+
+ const BoundValueSet& bvSet = getBoundValueSet(left);
+ BoundValueSet::const_iterator i = bvSet.find(value);
+ if(i == bvSet.end()){
+ return false;
+ }else{
+ const BoundValueEntry& entry = i->second;
+ return entry.hasLeq();
+ }
+}
+
+bool ArithAtomDatabase::containsGeq(TNode atom) const{
+ TNode left = atom[0];
+ const Rational& value = rightHandRational(atom);
+
+ const BoundValueSet& bvSet = getBoundValueSet(left);
+ BoundValueSet::const_iterator i = bvSet.find(value);
+ if(i == bvSet.end()){
+ return false;
+ }else{
+ const BoundValueEntry& entry = i->second;
+ return entry.hasGeq();
+ }
+}
+
+void ArithAtomDatabase::addAtom(TNode atom){
+ TNode left = atom[0];
+ TNode right = atom[1];
+
+ if(!leftIsSetup(left)){
+ setupLefthand(left);
+ }
+
+ const Rational& value = rightHandRational(atom);
+
+ switch(atom.getKind()){
+ case EQUAL:
+ {
+ Assert(!containsEquality(atom));
+ addImplicationsUsingEqualityAndEqualityValues(atom);
+ addImplicationsUsingEqualityAndBoundValues(atom);
+
+ pair<EqualValueSet::iterator, bool> res = getEqualValueSet(left).insert(atom);
+ Assert(res.second);
+ break;
+ }
+ case LEQ:
+ {
+ addImplicationsUsingLeqAndEqualityValues(atom);
+ addImplicationsUsingLeqAndBoundValues(atom);
+
+ BoundValueSet& bvSet = getBoundValueSet(left);
+ if(hasBoundValueEntry(atom)){
+ BoundValueSet::iterator i = bvSet.find(value);
+ BoundValueEntry& inSet = i->second;
+ inSet.addLeq(atom);
+ }else{
+ bvSet.insert(make_pair(value, BoundValueEntry::mkFromLeq(atom)));
+ }
+ break;
+ }
+ case GEQ:
+ {
+ addImplicationsUsingGeqAndEqualityValues(atom);
+ addImplicationsUsingGeqAndBoundValues(atom);
+
+ BoundValueSet& bvSet = getBoundValueSet(left);
+ if(hasBoundValueEntry(atom)){
+ BoundValueSet::iterator i = bvSet.find(value);
+ BoundValueEntry& inSet = i->second;
+ inSet.addGeq(atom);
+ }else{
+ bvSet.insert(make_pair(value, BoundValueEntry::mkFromGeq(atom)));
+ }
+ break;
+ }
+ default:
+ Unreachable();
+ }
+}
+
+bool ArithAtomDatabase::hasBoundValueEntry(TNode atom){
+ TNode left = atom[0];
+ const Rational& value = rightHandRational(atom);
+ BoundValueSet& bvSet = getBoundValueSet(left);
+ return bvSet.find(value) != bvSet.end();
+}
+
+bool rightHandRationalIsEqual(TNode a, TNode b){
+ TNode secondA = a[1];
+ TNode secondB = b[1];
+
+ const Rational& qA = secondA.getConst<Rational>();
+ const Rational& qB = secondB.getConst<Rational>();
+
+ return qA == qB;
+}
+
+
+bool rightHandRationalIsLT(TNode a, TNode b){
+ //This version is sticking around because it is easier to read!
+ return RightHandRationalLT()(a,b);
+}
+
+void ArithAtomDatabase::addImplicationsUsingEqualityAndEqualityValues(TNode atom){
+ Assert(atom.getKind() == EQUAL);
+ TNode left = atom[0];
+ EqualValueSet& eqSet = getEqualValueSet(left);
+
+ Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
+
+ for(EqualValueSet::iterator eqIter = eqSet.begin(), endIter = eqSet.end();
+ eqIter != endIter; ++eqIter){
+ TNode eq = *eqIter;
+ Assert(eq != atom);
+ addImplication(eq, negation);
+ }
+}
+
+// if weaker, do not return an equivalent node
+// if strict, get the strongest bound implied by (< x value)
+// if !strict, get the strongest bound implied by (<= x value)
+Node getUpperBound(const BoundValueSet& bvSet, const Rational& value, bool strict, bool weaker){
+ BoundValueSet::const_iterator bv = bvSet.lower_bound(value);
+ if(bv == bvSet.end()){
+ return Node::null();
+ }
+
+ if((bv->second).getValue() == value){
+ const BoundValueEntry& entry = bv->second;
+ if(strict && entry.hasGeq() && !weaker){
+ return NodeBuilder<1>(NOT) << entry.getGeq();
+ }else if(entry.hasLeq() && (strict || !weaker)){
+ return entry.getLeq();
+ }
+ }
+ ++bv;
+ if(bv == bvSet.end()){
+ return Node::null();
+ }
+ Assert(bv->second.getValue() > value);
+ const BoundValueEntry& entry = bv->second;
+ if(entry.hasGeq()){
+ return NodeBuilder<1>(NOT) << entry.getGeq();
+ }else{
+ Assert(entry.hasLeq());
+ return entry.getLeq();
+ }
+}
+
+
+
+
+// if weaker, do not return an equivalent node
+// if strict, get the strongest bound implied by (> x value)
+// if !strict, get the strongest bound implied by (>= x value)
+Node getLowerBound(const BoundValueSet& bvSet, const Rational& value, bool strict, bool weaker){
+ static int time = 0;
+ ++time;
+
+ if(bvSet.empty()){
+ return Node::null();
+ }
+ Debug("getLowerBound") << "getLowerBound" << bvSet.size() << " " << value << " " << strict << weaker << endl;
+
+ BoundValueSet::const_iterator bv = bvSet.lower_bound(value);
+ if(bv == bvSet.end()){
+ Debug("getLowerBound") << "got end " << value << " " << (bvSet.rbegin()->second).getValue() << endl;
+ Assert(value > (bvSet.rbegin()->second).getValue());
+ }else{
+ Debug("getLowerBound") << value << ", " << bv->second.getValue() << endl;
+ Assert(value <= bv->second.getValue());
+ }
+
+ if(bv != bvSet.end() && (bv->second).getValue() == value){
+ const BoundValueEntry& entry = bv->second;
+ Debug("getLowerBound") << entry.hasLeq() << entry.hasGeq() << endl;
+ if(strict && entry.hasLeq() && !weaker){
+ return NodeBuilder<1>(NOT) << entry.getLeq();
+ }else if(entry.hasGeq() && (strict || !weaker)){
+ return entry.getGeq();
+ }
+ }
+ if(bv == bvSet.begin()){
+ return Node::null();
+ }else{
+ --bv;
+ // (and (>= x v) (>= v v')) then (> x v')
+ Assert(bv->second.getValue() < value);
+ const BoundValueEntry& entry = bv->second;
+ if(entry.hasLeq()){
+ return NodeBuilder<1>(NOT) << entry.getLeq();
+ }else{
+ Assert(entry.hasGeq());
+ return entry.getGeq();
+ }
+ }
+}
+
+void ArithAtomDatabase::addImplicationsUsingEqualityAndBoundValues(TNode atom){
+ Assert(atom.getKind() == EQUAL);
+ Node left = atom[0];
+
+ const Rational& value = rightHandRational(atom);
+
+ BoundValueSet& bvSet = getBoundValueSet(left);
+ Node ub = getUpperBound(bvSet, value, false, false);
+ Node lb = getLowerBound(bvSet, value, false, false);
+
+ if(!ub.isNull()){
+ addImplication(atom, ub);
+ }
+
+ if(!lb.isNull()){
+ addImplication(atom, lb);
+ }
+}
+
+void ArithAtomDatabase::addImplicationsUsingLeqAndBoundValues(TNode atom)
+{
+ Assert(atom.getKind() == LEQ);
+ Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
+
+ Node ub = getImpliedUpperBoundUsingLeq(atom, false);
+ Node lb = getImpliedLowerBoundUsingGT(negation, false);
+
+ if(!ub.isNull()){
+ addImplication(atom, ub);
+ }
+
+ if(!lb.isNull()){
+ addImplication(negation, lb);
+ }
+}
+
+void ArithAtomDatabase::addImplicationsUsingLeqAndEqualityValues(TNode atom) {
+ Assert(atom.getKind() == LEQ);
+ Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
+
+ TNode left = atom[0];
+ EqualValueSet& eqSet = getEqualValueSet(left);
+
+ //TODO Improve this later
+ for(EqualValueSet::iterator eqIter = eqSet.begin(); eqIter != eqSet.end(); ++eqIter){
+ TNode eq = *eqIter;
+ if(rightHandRationalIsEqual(atom, eq)){
+ // (x = b' /\ b = b') => x <= b
+ addImplication(eq, atom);
+ }else if(rightHandRationalIsLT(atom, eq)){
+ // (x = b' /\ b' > b) => x > b
+ addImplication(eq, negation);
+ }else{
+ // (x = b' /\ b' < b) => x <= b
+ addImplication(eq, atom);
+ }
+ }
+}
+
+
+void ArithAtomDatabase::addImplicationsUsingGeqAndBoundValues(TNode atom){
+ Assert(atom.getKind() == GEQ);
+ Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
+
+ Node lb = getImpliedLowerBoundUsingGeq(atom, false); //What is implied by (>= left value)
+ Node ub = getImpliedUpperBoundUsingLT(negation, false);
+
+ if(!lb.isNull()){
+ addImplication(atom, lb);
+ }
+
+ if(!ub.isNull()){
+ addImplication(negation, ub);
+ }
+}
+void ArithAtomDatabase::addImplicationsUsingGeqAndEqualityValues(TNode atom){
+
+ Assert(atom.getKind() == GEQ);
+ Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
+ Node left = atom[0];
+ EqualValueSet& eqSet = getEqualValueSet(left);
+
+ //TODO Improve this later
+ for(EqualValueSet::iterator eqIter = eqSet.begin(); eqIter != eqSet.end(); ++eqIter){
+ TNode eq = *eqIter;
+ if(rightHandRationalIsEqual(atom, eq)){
+ // (x = b' /\ b = b') => x >= b
+ addImplication(eq, atom);
+ }else if(rightHandRationalIsLT(eq, atom)){
+ // (x = b' /\ b' < b) => x < b
+ addImplication(eq, negation);
+ }else{
+ // (x = b' /\ b' > b) => x >= b
+ addImplication(eq, atom);
+ }
+ }
+}
+
+void ArithAtomDatabase::addImplication(TNode a, TNode b){
+ Node imp = NodeBuilder<2>(IMPLIES) << a << b;
+
+ Debug("arith::unate") << "ArithAtomDatabase::addImplication"
+ << "(" << a << ", " << b <<")" << endl;
+
+ d_arithOut.lemma(imp);
+}
+
+
+Node ArithAtomDatabase::getImpliedUpperBoundUsingLeq(TNode leq, bool weaker) const {
+ Assert(leq.getKind() == LEQ);
+ Node left = leq[0];
+
+ if(!leftIsSetup(left)) return Node::null();
+
+ const Rational& value = rightHandRational(leq);
+ const BoundValueSet& bvSet = getBoundValueSet(left);
+
+ Node ub = getUpperBound(bvSet, value, false, weaker);
+ return ub;
+}
+
+Node ArithAtomDatabase::getImpliedUpperBoundUsingLT(TNode lt, bool weaker) const {
+ Assert(lt.getKind() == NOT && lt[0].getKind() == GEQ);
+ Node atom = lt[0];
+ Node left = atom[0];
+
+ if(!leftIsSetup(left)) return Node::null();
+
+ const Rational& value = rightHandRational(atom);
+ const BoundValueSet& bvSet = getBoundValueSet(left);
+
+ return getUpperBound(bvSet, value, true, weaker);
+}
+
+Node ArithAtomDatabase::getBestImpliedUpperBound(TNode upperBound) const {
+ Node result = Node::null();
+ if(upperBound.getKind() == LEQ ){
+ result = getImpliedUpperBoundUsingLeq(upperBound, false);
+ }else if(upperBound.getKind() == NOT && upperBound[0].getKind() == GEQ){
+ result = getImpliedUpperBoundUsingLT(upperBound, false);
+ }else if(upperBound.getKind() == LT){
+ Node geq = NodeBuilder<2>(GEQ) << upperBound[0] << upperBound[1];
+ Node lt = NodeBuilder<1>(NOT) << geq;
+ result = getImpliedUpperBoundUsingLT(lt, false);
+ }else{
+ Unreachable();
+ }
+
+ Debug("arith::unate") << upperBound <<" -> " << result << std::endl;
+ return result;
+}
+
+Node ArithAtomDatabase::getWeakerImpliedUpperBound(TNode upperBound) const {
+ Node result = Node::null();
+ if(upperBound.getKind() == LEQ ){
+ result = getImpliedUpperBoundUsingLeq(upperBound, true);
+ }else if(upperBound.getKind() == NOT && upperBound[0].getKind() == GEQ){
+ result = getImpliedUpperBoundUsingLT(upperBound, true);
+ }else if(upperBound.getKind() == LT){
+ Node geq = NodeBuilder<2>(GEQ) << upperBound[0] << upperBound[1];
+ Node lt = NodeBuilder<1>(NOT) << geq;
+ result = getImpliedUpperBoundUsingLT(lt, true);
+ }else{
+ Unreachable();
+ }
+ Assert(upperBound != result);
+ Debug("arith::unate") << upperBound <<" -> " << result << std::endl;
+ return result;
+}
+
+Node ArithAtomDatabase::getImpliedLowerBoundUsingGT(TNode gt, bool weaker) const {
+ Assert(gt.getKind() == NOT && gt[0].getKind() == LEQ);
+ Node atom = gt[0];
+ Node left = atom[0];
+
+ if(!leftIsSetup(left)) return Node::null();
+
+ const Rational& value = rightHandRational(atom);
+ const BoundValueSet& bvSet = getBoundValueSet(left);
+
+ return getLowerBound(bvSet, value, true, weaker);
+}
+
+Node ArithAtomDatabase::getImpliedLowerBoundUsingGeq(TNode geq, bool weaker) const {
+ Assert(geq.getKind() == GEQ);
+ Node left = geq[0];
+
+ if(!leftIsSetup(left)) return Node::null();
+
+ const Rational& value = rightHandRational(geq);
+ const BoundValueSet& bvSet = getBoundValueSet(left);
+
+ return getLowerBound(bvSet, value, false, weaker);
+}
+
+Node ArithAtomDatabase::getBestImpliedLowerBound(TNode lowerBound) const {
+ Node result = Node::null();
+ if(lowerBound.getKind() == GEQ ){
+ result = getImpliedLowerBoundUsingGeq(lowerBound, false);
+ }else if(lowerBound.getKind() == NOT && lowerBound[0].getKind() == LEQ){
+ result = getImpliedLowerBoundUsingGT(lowerBound, false);
+ }else if(lowerBound.getKind() == GT){
+ Node leq = NodeBuilder<2>(LEQ)<<lowerBound[0]<< lowerBound[1];
+ Node gt = NodeBuilder<1>(NOT) << leq;
+ result = getImpliedLowerBoundUsingGT(gt, false);
+ }else{
+ Unreachable();
+ }
+ Debug("arith::unate") << lowerBound <<" -> " << result << std::endl;
+ return result;
+}
+
+Node ArithAtomDatabase::getWeakerImpliedLowerBound(TNode lowerBound) const {
+ Node result = Node::null();
+ if(lowerBound.getKind() == GEQ ){
+ result = getImpliedLowerBoundUsingGeq(lowerBound, true);
+ }else if(lowerBound.getKind() == NOT && lowerBound[0].getKind() == LEQ){
+ result = getImpliedLowerBoundUsingGT(lowerBound, true);
+ }else if(lowerBound.getKind() == GT){
+ Node leq = NodeBuilder<2>(LEQ)<<lowerBound[0]<< lowerBound[1];
+ Node gt = NodeBuilder<1>(NOT) << leq;
+ result = getImpliedLowerBoundUsingGT(gt, true);
+ }else{
+ Unreachable();
+ }
+ Assert(result != lowerBound);
+
+ Debug("arith::unate") << lowerBound <<" -> " << result << std::endl;
+ return result;
+}
--- /dev/null
+/********************* */
+/*! \file atom_database.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief ArithAtomDatabase keeps a database of the arithmetic atoms.
+ ** Importantly, ArithAtomDatabase also handles unate propagations,
+ ** i.e. it constructs implications of the form
+ ** "if x < c and c < b, then x < b" (where c and b are constants).
+ **
+ ** ArithAtomDatabase detects unate implications amongst the atoms
+ ** associated with the theory of arithmetic and informs the SAT solver of the
+ ** implication. A unate implication is an implication of the form:
+ ** "if x < c and c < b, then x < b" (where c and b are constants).
+ ** Unate implications are always 2-SAT clauses.
+ ** ArithAtomDatabase sends the implications to the SAT solver in an
+ ** online fashion.
+ ** This means that atoms may be added during solving or before.
+ **
+ ** ArithAtomDatabase maintains sorted lists containing all atoms associated
+ ** for each unique left hand side, the "x" in the inequality "x < c".
+ ** The lists are sorted by the value of the right hand side which must be a
+ ** rational constant.
+ **
+ ** ArithAtomDatabase tries to send out a minimal number of additional
+ ** lemmas per atom added. Let (x < a), (x < b), (x < c) be arithmetic atoms s.t.
+ ** a < b < c.
+ ** If the the order of adding the atoms is (x < a), (x < b), and (x < c), then
+ ** then set of all lemmas added is:
+ ** {(=> (x<a) (x < b)), (=> (x<b) (x < c))}
+ ** If the order is changed to (x < a), (x < c), and (x < b), then
+ ** the final set of implications emitted is:
+ ** {(=> (x<a) (x < c)), (=> (x<a) (x < b)), (=> (x<b) (x < c))}
+ **
+ ** \todo document this file
+ **/
+
+
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__ARITH_ATOM_DATABASE_H
+#define __CVC4__THEORY__ARITH__ARITH_ATOM_DATABASE_H
+
+#include "expr/node.h"
+#include "context/context.h"
+
+#include "theory/output_channel.h"
+#include "theory/arith/ordered_set.h"
+
+#include <ext/hash_map>
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class ArithAtomDatabase {
+private:
+ /**
+ * OutputChannel for the theory of arithmetic.
+ * The propagator uses this to pass implications back to the SAT solver.
+ */
+ OutputChannel& d_arithOut;
+
+ struct VariablesSets {
+ BoundValueSet d_boundValueSet;
+ EqualValueSet d_eqValueSet;
+ };
+
+ typedef __gnu_cxx::hash_map<TNode, VariablesSets, NodeHashFunction> NodeToSetsMap;
+ NodeToSetsMap d_setsMap;
+
+public:
+ ArithAtomDatabase(context::Context* cxt, OutputChannel& arith);
+
+ /**
+ * Adds an atom to the propagator.
+ * Any resulting lemmas will be output via d_arithOut.
+ */
+ void addAtom(TNode atom);
+
+ /** Returns true if v has been added as a left hand side in an atom */
+ bool hasAnyAtoms(TNode v) const;
+
+ bool containsLiteral(TNode lit) const;
+ bool containsAtom(TNode atom) const;
+ bool containsEquality(TNode atom) const;
+ bool containsLeq(TNode atom) const;
+ bool containsGeq(TNode atom) const;
+
+
+
+private:
+ VariablesSets& getVariablesSets(TNode left);
+ BoundValueSet& getBoundValueSet(TNode left);
+ EqualValueSet& getEqualValueSet(TNode left);
+
+ const VariablesSets& getVariablesSets(TNode left) const;
+ const BoundValueSet& getBoundValueSet(TNode left) const;
+ const EqualValueSet& getEqualValueSet(TNode left) const;
+
+ /** Sends an implication (=> a b) to the PropEngine via d_arithOut. */
+ void addImplication(TNode a, TNode b);
+
+ /** Check to make sure an lhs has been properly set-up. */
+ bool leftIsSetup(TNode left) const;
+
+ /** Initializes the lists associated with a unique lhs. */
+ void setupLefthand(TNode left);
+
+
+ /**
+ * The addImplicationsUsingKAndJList(...)
+ * functions are the work horses of the unate part of ArithAtomDatabase.
+ * These take an atom of the kind K that has just been added
+ * to its associated list, and the ordered list of Js associated with the lhs,
+ * and uses these to deduce unate implications.
+ * (K and J vary over EQUAL, LEQ, and GEQ.)
+ *
+ * Input:
+ * atom - the atom being inserted of kind K
+ * Jset - the list of atoms of kind J associated with the lhs.
+ *
+ * Unfortunately, these tend to be an absolute bear to read because
+ * of all of the special casing and C++ iterator manipulation required.
+ */
+
+ void addImplicationsUsingEqualityAndEqualityValues(TNode eq);
+ void addImplicationsUsingEqualityAndBoundValues(TNode eq);
+
+ void addImplicationsUsingLeqAndEqualityValues(TNode leq);
+ void addImplicationsUsingLeqAndBoundValues(TNode leq);
+
+ void addImplicationsUsingGeqAndEqualityValues(TNode geq);
+ void addImplicationsUsingGeqAndBoundValues(TNode geq);
+
+ bool hasBoundValueEntry(TNode n);
+
+ Node getImpliedUpperBoundUsingLeq(TNode leq, bool weaker) const;
+ Node getImpliedUpperBoundUsingLT(TNode lt, bool weaker) const;
+
+ Node getImpliedLowerBoundUsingGeq(TNode geq, bool weaker) const;
+ Node getImpliedLowerBoundUsingGT(TNode gt, bool weaker) const;
+
+public:
+ Node getBestImpliedUpperBound(TNode upperBound) const;
+ Node getBestImpliedLowerBound(TNode lowerBound) const;
+
+
+ Node getWeakerImpliedUpperBound(TNode upperBound) const;
+ Node getWeakerImpliedLowerBound(TNode lowerBound) const;
+};
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH__ARITH_ATOM_DATABASE_H */
#include "theory/arith/arithvar_set.h"
#include "theory/arith/arith_rewriter.h"
-#include "theory/arith/unate_propagator.h"
+#include "theory/arith/atom_database.h"
#include "theory/arith/theory_arith.h"
#include "theory/arith/normal_form.h"
d_diseq(c),
d_tableau(),
d_restartsCounter(0),
- d_presolveHasBeenCalled(false),
+ d_rowHasBeenAdded(false),
d_tableauResetDensity(1.6),
d_tableauResetPeriod(10),
- d_propagator(c, out),
- d_propManager(c, d_arithvarNodeMap, d_propagator, valuation),
+ d_atomDatabase(c, out),
+ d_propManager(c, d_arithvarNodeMap, d_atomDatabase, valuation),
d_simplex(d_propManager, d_partialModel, d_tableau),
d_DELTA_ZERO(0),
d_statistics()
Debug("arith_preregister") <<"begin arith::preRegisterTerm("<< n <<")"<< endl;
Kind k = n.getKind();
+ /* BREADCRUMB: I am using this bool to compile time enable testing for arbitrary equalities. */
+ static bool turnOffEqualityPreRegister = false;
+ if(turnOffEqualityPreRegister){
+ if(k == LEQ || k == LT || k == GT || k == GEQ){
+ TNode left = n[0];
+ delayedSetupPolynomial(left);
+
+ d_atomDatabase.addAtom(n);
+ }
+ return;
+ }
+
bool isStrictlyVarList = k == kind::MULT && VarList::isMember(n);
if(isStrictlyVarList){
if(isRelationOperator(k)){
Assert(Comparison::isNormalAtom(n));
- //cout << n << endl;
-
- d_propagator.addAtom(n);
+ d_atomDatabase.addAtom(n);
TNode left = n[0];
TNode right = n[1];
++(d_statistics.d_statSlackVariables);
left.setAttribute(Slack(), true);
+ d_rowHasBeenAdded = true;
+
ArithVar varSlack = requestArithVar(left, true);
Polynomial polyLeft = Polynomial::parsePolynomial(left);
return conflict;
}
+void TheoryArith::delayedSetupMonomial(const Monomial& mono){
+
+ Debug("arith::delay") << "delayedSetupMonomial(" << mono.getNode() << ")" << endl;
+
+ Assert(!mono.isConstant());
+ VarList vl = mono.getVarList();
+
+ if(!d_arithvarNodeMap.hasArithVar(vl.getNode())){
+ for(VarList::iterator i = vl.begin(), end = vl.end(); i != end; ++i){
+ Variable var = *i;
+ Node n = var.getNode();
+
+ ++(d_statistics.d_statUserVariables);
+ ArithVar varN = requestArithVar(n,false);
+ setupInitialValue(varN);
+ }
+
+ if(!vl.singleton()){
+ d_out->setIncomplete();
+
+ Node n = vl.getNode();
+ ++(d_statistics.d_statUserVariables);
+ ArithVar varN = requestArithVar(n,false);
+ setupInitialValue(varN);
+ }
+ }
+}
+
+void TheoryArith::delayedSetupPolynomial(TNode polynomial){
+ Debug("arith::delay") << "delayedSetupPolynomial(" << polynomial << ")" << endl;
+
+ Assert(Polynomial::isMember(polynomial));
+ // if d_nodeMap.hasArithVar() all of the variables and it are setup
+ if(!d_arithvarNodeMap.hasArithVar(polynomial)){
+ Polynomial poly = Polynomial::parsePolynomial(polynomial);
+ Assert(!poly.containsConstant());
+ for(Polynomial::iterator i = poly.begin(), end = poly.end(); i != end; ++i){
+ Monomial mono = *i;
+ delayedSetupMonomial(mono);
+ }
+
+ if(polynomial.getKind() == PLUS){
+ Assert(!polynomial.getAttribute(Slack()),
+ "Polynomial has slack attribute but not does not have arithvar");
+ setupSlack(polynomial);
+ }
+ }
+}
+
+void TheoryArith::delayedSetupEquality(TNode equality){
+ Debug("arith::delay") << "delayedSetupEquality(" << equality << ")" << endl;
+
+ Assert(equality.getKind() == EQUAL);
+
+ TNode left = equality[0];
+ delayedSetupPolynomial(left);
+}
+
+bool TheoryArith::canSafelyAvoidEqualitySetup(TNode equality){
+ Assert(equality.getKind() == EQUAL);
+ return d_arithvarNodeMap.hasArithVar(equality[0]);
+}
+
Node TheoryArith::assertionCases(TNode assertion){
Kind simpKind = simplifiedKind(assertion);
Assert(simpKind != UNDEFINED_KIND);
+ if(simpKind == EQUAL || simpKind == DISTINCT){
+ Node eq = (simpKind == DISTINCT) ? assertion[0] : assertion;
+
+ if(!canSafelyAvoidEqualitySetup(eq)){
+ delayedSetupEquality(eq);
+ }
+ }
+
ArithVar x_i = determineLeftVariable(assertion, simpKind);
DeltaRational c_i = determineRightConstant(assertion, simpKind);
- Debug("arith_assertions") << "arith assertion(" << assertion
- << " \\-> "
- <<x_i<<" "<< simpKind <<" "<< c_i << ")" << std::endl;
+ Debug("arith::assertions") << "arith assertion(" << assertion
+ << " \\-> "
+ <<x_i<<" "<< simpKind <<" "<< c_i << ")" << std::endl;
switch(simpKind){
case LEQ:
if (d_partialModel.hasLowerBound(x_i) && d_partialModel.getLowerBound(x_i) == c_i) {
uint32_t currSize = d_tableau.size();
uint32_t copySize = d_smallTableauCopy.size();
- //d_statistics.d_tableauSizeHistory << currSize;
if(debugResetPolicy){
cout << "curr " << currSize << " copy " << copySize << endl;
}
- if(d_presolveHasBeenCalled && copySize == 0 && currSize > 0){
+ if(d_rowHasBeenAdded){
if(debugResetPolicy){
- cout << "initial copy " << d_restartsCounter << endl;
+ cout << "row has been added must copy " << d_restartsCounter << endl;
}
- d_smallTableauCopy = d_tableau; // The initial copy
+ d_smallTableauCopy = d_tableau;
+ d_rowHasBeenAdded = false;
}
- if(d_presolveHasBeenCalled && d_restartsCounter >= RESET_START){
+ if(!d_rowHasBeenAdded && d_restartsCounter >= RESET_START){
if(copySize >= currSize * 1.1 ){
++d_statistics.d_smallerSetToCurr;
d_smallTableauCopy = d_tableau;
// It appears that this can happen after other variables have been removed!
// Tread carefullty with this one.
+ Assert(Options::current()->variableRemovalEnabled);
+
bool noRow = false;
if(!d_tableau.isBasic(v)){
void TheoryArith::presolve(){
TimerStat::CodeTimer codeTimer(d_statistics.d_presolveTime);
- typedef std::vector<Node>::const_iterator VarIter;
- for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){
- Node variableNode = *i;
- ArithVar var = d_arithvarNodeMap.asArithVar(variableNode);
- if(d_userVariables.isMember(var) && !d_propagator.hasAnyAtoms(variableNode)){
- //The user variable is unconstrained.
- //Remove this variable permanently
- permanentlyRemoveVariable(var);
+ /* BREADCRUMB : Turn this on for QF_LRA/QF_RDL problems.
+ *
+ * The big problem for adding things back is that if they are readded they may
+ * need to be assigned an initial value at ALL context values.
+ * This is unsupported with our current datastructures.
+ *
+ * A better solution is to KNOW when the permantent removal is safe.
+ * This is true for single query QF_LRA/QF_RDL problems.
+ * Maybe a mechanism to ask "the sharing manager"
+ * if this variable/row can be used in sharing?
+ */
+ if(Options::current()->variableRemovalEnabled){
+ typedef std::vector<Node>::const_iterator VarIter;
+ for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){
+ Node variableNode = *i;
+ ArithVar var = d_arithvarNodeMap.asArithVar(variableNode);
+ if(d_userVariables.isMember(var) && !d_atomDatabase.hasAnyAtoms(variableNode)){
+ //The user variable is unconstrained.
+ //Remove this variable permanently
+ permanentlyRemoveVariable(var);
+ }
}
}
Debug("arith::presolve") << "TheoryArith::presolve #" << (callCount++) << endl;
learner.clear();
-
- d_presolveHasBeenCalled = true;
check(FULL_EFFORT);
}
#include "theory/arith/tableau.h"
#include "theory/arith/arith_rewriter.h"
#include "theory/arith/partial_model.h"
-#include "theory/arith/unate_propagator.h"
+#include "theory/arith/atom_database.h"
#include "theory/arith/simplex.h"
#include "theory/arith/arith_static_learner.h"
#include "theory/arith/arith_prop_manager.h"
* If d >= s_TABLEAU_RESET_DENSITY * d_initialDensity, the tableau
* is set to d_initialTableau.
*/
- bool d_presolveHasBeenCalled;
+ bool d_rowHasBeenAdded;
double d_tableauResetDensity;
uint32_t d_tableauResetPeriod;
static const uint32_t s_TABLEAU_RESET_INCREMENT = 5;
*/
Tableau d_smallTableauCopy;
- ArithUnatePropagator d_propagator;
+ /**
+ * The atom database keeps track of the atoms that have been preregistered.
+ * Used to add unate propagations.
+ */
+ ArithAtomDatabase d_atomDatabase;
+ /** This manager keeps track of information needed to propagate. */
ArithPropManager d_propManager;
+ /** This implements the Simplex decision procedure. */
SimplexDecisionProcedure d_simplex;
public:
/** Initial (not context dependent) sets up for a new slack variable.*/
void setupSlack(TNode left);
+ /**
+ * Performs *permanent* static setup for equalities that have not been
+ * preregistered.
+ * Currently these MUST be introduced by combination.
+ */
+ void delayedSetupEquality(TNode equality);
+
+ void delayedSetupPolynomial(TNode polynomial);
+ void delayedSetupMonomial(const Monomial& mono);
+
+ /**
+ * Performs a check to see if it is definitely true that setup can be avoided.
+ */
+ bool canSafelyAvoidEqualitySetup(TNode equality);
/**
* Handles the case splitting for check() for a new assertion.
+++ /dev/null
-/********************* */
-/*! \file unate_propagator.cpp
- ** \verbatim
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "theory/arith/unate_propagator.h"
-#include "theory/arith/arith_utilities.h"
-
-#include <list>
-
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arith;
-
-using namespace CVC4::kind;
-
-using namespace std;
-
-ArithUnatePropagator::ArithUnatePropagator(context::Context* cxt, OutputChannel& out) :
- d_arithOut(out), d_setsMap()
-{ }
-
-bool ArithUnatePropagator::leftIsSetup(TNode left) const{
- return d_setsMap.find(left) != d_setsMap.end();
-}
-
-const ArithUnatePropagator::VariablesSets& ArithUnatePropagator::getVariablesSets(TNode left) const{
- Assert(leftIsSetup(left));
- NodeToSetsMap::const_iterator i = d_setsMap.find(left);
- return i->second;
-}
-ArithUnatePropagator::VariablesSets& ArithUnatePropagator::getVariablesSets(TNode left){
- Assert(leftIsSetup(left));
- NodeToSetsMap::iterator i = d_setsMap.find(left);
- return i->second;
-}
-EqualValueSet& ArithUnatePropagator::getEqualValueSet(TNode left){
- Assert(leftIsSetup(left));
- return getVariablesSets(left).d_eqValueSet;
-}
-
-const EqualValueSet& ArithUnatePropagator::getEqualValueSet(TNode left) const{
- Assert(leftIsSetup(left));
- return getVariablesSets(left).d_eqValueSet;
-}
-
-BoundValueSet& ArithUnatePropagator::getBoundValueSet(TNode left){
- Assert(leftIsSetup(left));
- return getVariablesSets(left).d_boundValueSet;
-}
-
-const BoundValueSet& ArithUnatePropagator::getBoundValueSet(TNode left) const{
- Assert(leftIsSetup(left));
- return getVariablesSets(left).d_boundValueSet;
-}
-
-bool ArithUnatePropagator::hasAnyAtoms(TNode v) const{
- Assert(!leftIsSetup(v)
- || !(getEqualValueSet(v)).empty()
- || !(getBoundValueSet(v)).empty());
-
- return leftIsSetup(v);
-}
-
-void ArithUnatePropagator::setupLefthand(TNode left){
- Assert(!leftIsSetup(left));
-
- d_setsMap[left] = VariablesSets();
-}
-
-bool ArithUnatePropagator::containsLiteral(TNode lit) const{
- switch(lit.getKind()){
- case NOT: return containsAtom(lit[0]);
- default: return containsAtom(lit);
- }
-}
-
-bool ArithUnatePropagator::containsAtom(TNode atom) const{
- switch(atom.getKind()){
- case EQUAL: return containsEquality(atom);
- case LEQ: return containsLeq(atom);
- case GEQ: return containsGeq(atom);
- default:
- Unreachable();
- }
-}
-
-bool ArithUnatePropagator::containsEquality(TNode atom) const{
- TNode left = atom[0];
- const EqualValueSet& eqSet = getEqualValueSet(left);
- return eqSet.find(atom) != eqSet.end();
-}
-
-bool ArithUnatePropagator::containsLeq(TNode atom) const{
- TNode left = atom[0];
- const Rational& value = rightHandRational(atom);
-
- const BoundValueSet& bvSet = getBoundValueSet(left);
- BoundValueSet::const_iterator i = bvSet.find(value);
- if(i == bvSet.end()){
- return false;
- }else{
- const BoundValueEntry& entry = i->second;
- return entry.hasLeq();
- }
-}
-
-bool ArithUnatePropagator::containsGeq(TNode atom) const{
- TNode left = atom[0];
- const Rational& value = rightHandRational(atom);
-
- const BoundValueSet& bvSet = getBoundValueSet(left);
- BoundValueSet::const_iterator i = bvSet.find(value);
- if(i == bvSet.end()){
- return false;
- }else{
- const BoundValueEntry& entry = i->second;
- return entry.hasGeq();
- }
-}
-
-void ArithUnatePropagator::addAtom(TNode atom){
- TNode left = atom[0];
- TNode right = atom[1];
-
- if(!leftIsSetup(left)){
- setupLefthand(left);
- }
-
- const Rational& value = rightHandRational(atom);
-
- switch(atom.getKind()){
- case EQUAL:
- {
- Assert(!containsEquality(atom));
- addImplicationsUsingEqualityAndEqualityValues(atom);
- addImplicationsUsingEqualityAndBoundValues(atom);
-
- pair<EqualValueSet::iterator, bool> res = getEqualValueSet(left).insert(atom);
- Assert(res.second);
- break;
- }
- case LEQ:
- {
- addImplicationsUsingLeqAndEqualityValues(atom);
- addImplicationsUsingLeqAndBoundValues(atom);
-
- BoundValueSet& bvSet = getBoundValueSet(left);
- if(hasBoundValueEntry(atom)){
- BoundValueSet::iterator i = bvSet.find(value);
- BoundValueEntry& inSet = i->second;
- inSet.addLeq(atom);
- }else{
- bvSet.insert(make_pair(value, BoundValueEntry::mkFromLeq(atom)));
- }
- break;
- }
- case GEQ:
- {
- addImplicationsUsingGeqAndEqualityValues(atom);
- addImplicationsUsingGeqAndBoundValues(atom);
-
- BoundValueSet& bvSet = getBoundValueSet(left);
- if(hasBoundValueEntry(atom)){
- BoundValueSet::iterator i = bvSet.find(value);
- BoundValueEntry& inSet = i->second;
- inSet.addGeq(atom);
- }else{
- bvSet.insert(make_pair(value, BoundValueEntry::mkFromGeq(atom)));
- }
- break;
- }
- default:
- Unreachable();
- }
-}
-
-bool ArithUnatePropagator::hasBoundValueEntry(TNode atom){
- TNode left = atom[0];
- const Rational& value = rightHandRational(atom);
- BoundValueSet& bvSet = getBoundValueSet(left);
- return bvSet.find(value) != bvSet.end();
-}
-
-bool rightHandRationalIsEqual(TNode a, TNode b){
- TNode secondA = a[1];
- TNode secondB = b[1];
-
- const Rational& qA = secondA.getConst<Rational>();
- const Rational& qB = secondB.getConst<Rational>();
-
- return qA == qB;
-}
-
-
-bool rightHandRationalIsLT(TNode a, TNode b){
- //This version is sticking around because it is easier to read!
- return RightHandRationalLT()(a,b);
-}
-
-void ArithUnatePropagator::addImplicationsUsingEqualityAndEqualityValues(TNode atom){
- Assert(atom.getKind() == EQUAL);
- TNode left = atom[0];
- EqualValueSet& eqSet = getEqualValueSet(left);
-
- Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
-
- for(EqualValueSet::iterator eqIter = eqSet.begin(), endIter = eqSet.end();
- eqIter != endIter; ++eqIter){
- TNode eq = *eqIter;
- Assert(eq != atom);
- addImplication(eq, negation);
- }
-}
-
-// if weaker, do not return an equivalent node
-// if strict, get the strongest bound implied by (< x value)
-// if !strict, get the strongest bound implied by (<= x value)
-Node getUpperBound(const BoundValueSet& bvSet, const Rational& value, bool strict, bool weaker){
- BoundValueSet::const_iterator bv = bvSet.lower_bound(value);
- if(bv == bvSet.end()){
- return Node::null();
- }
-
- if((bv->second).getValue() == value){
- const BoundValueEntry& entry = bv->second;
- if(strict && entry.hasGeq() && !weaker){
- return NodeBuilder<1>(NOT) << entry.getGeq();
- }else if(entry.hasLeq() && (strict || !weaker)){
- return entry.getLeq();
- }
- }
- ++bv;
- if(bv == bvSet.end()){
- return Node::null();
- }
- Assert(bv->second.getValue() > value);
- const BoundValueEntry& entry = bv->second;
- if(entry.hasGeq()){
- return NodeBuilder<1>(NOT) << entry.getGeq();
- }else{
- Assert(entry.hasLeq());
- return entry.getLeq();
- }
-}
-
-
-
-
-// if weaker, do not return an equivalent node
-// if strict, get the strongest bound implied by (> x value)
-// if !strict, get the strongest bound implied by (>= x value)
-Node getLowerBound(const BoundValueSet& bvSet, const Rational& value, bool strict, bool weaker){
- static int time = 0;
- ++time;
-
- if(bvSet.empty()){
- return Node::null();
- }
- Debug("getLowerBound") << "getLowerBound" << bvSet.size() << " " << value << " " << strict << weaker << endl;
-
- BoundValueSet::const_iterator bv = bvSet.lower_bound(value);
- if(bv == bvSet.end()){
- Debug("getLowerBound") << "got end " << value << " " << (bvSet.rbegin()->second).getValue() << endl;
- Assert(value > (bvSet.rbegin()->second).getValue());
- }else{
- Debug("getLowerBound") << value << ", " << bv->second.getValue() << endl;
- Assert(value <= bv->second.getValue());
- }
-
- if(bv != bvSet.end() && (bv->second).getValue() == value){
- const BoundValueEntry& entry = bv->second;
- Debug("getLowerBound") << entry.hasLeq() << entry.hasGeq() << endl;
- if(strict && entry.hasLeq() && !weaker){
- return NodeBuilder<1>(NOT) << entry.getLeq();
- }else if(entry.hasGeq() && (strict || !weaker)){
- return entry.getGeq();
- }
- }
- if(bv == bvSet.begin()){
- return Node::null();
- }else{
- --bv;
- // (and (>= x v) (>= v v')) then (> x v')
- Assert(bv->second.getValue() < value);
- const BoundValueEntry& entry = bv->second;
- if(entry.hasLeq()){
- return NodeBuilder<1>(NOT) << entry.getLeq();
- }else{
- Assert(entry.hasGeq());
- return entry.getGeq();
- }
- }
-}
-
-void ArithUnatePropagator::addImplicationsUsingEqualityAndBoundValues(TNode atom){
- Assert(atom.getKind() == EQUAL);
- Node left = atom[0];
-
- const Rational& value = rightHandRational(atom);
-
- BoundValueSet& bvSet = getBoundValueSet(left);
- Node ub = getUpperBound(bvSet, value, false, false);
- Node lb = getLowerBound(bvSet, value, false, false);
-
- if(!ub.isNull()){
- addImplication(atom, ub);
- }
-
- if(!lb.isNull()){
- addImplication(atom, lb);
- }
-}
-
-void ArithUnatePropagator::addImplicationsUsingLeqAndBoundValues(TNode atom)
-{
- Assert(atom.getKind() == LEQ);
- Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
-
- Node ub = getImpliedUpperBoundUsingLeq(atom, false);
- Node lb = getImpliedLowerBoundUsingGT(negation, false);
-
- if(!ub.isNull()){
- addImplication(atom, ub);
- }
-
- if(!lb.isNull()){
- addImplication(negation, lb);
- }
-}
-
-void ArithUnatePropagator::addImplicationsUsingLeqAndEqualityValues(TNode atom) {
- Assert(atom.getKind() == LEQ);
- Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
-
- TNode left = atom[0];
- EqualValueSet& eqSet = getEqualValueSet(left);
-
- //TODO Improve this later
- for(EqualValueSet::iterator eqIter = eqSet.begin(); eqIter != eqSet.end(); ++eqIter){
- TNode eq = *eqIter;
- if(rightHandRationalIsEqual(atom, eq)){
- // (x = b' /\ b = b') => x <= b
- addImplication(eq, atom);
- }else if(rightHandRationalIsLT(atom, eq)){
- // (x = b' /\ b' > b) => x > b
- addImplication(eq, negation);
- }else{
- // (x = b' /\ b' < b) => x <= b
- addImplication(eq, atom);
- }
- }
-}
-
-
-void ArithUnatePropagator::addImplicationsUsingGeqAndBoundValues(TNode atom){
- Assert(atom.getKind() == GEQ);
- Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
-
- Node lb = getImpliedLowerBoundUsingGeq(atom, false); //What is implied by (>= left value)
- Node ub = getImpliedUpperBoundUsingLT(negation, false);
-
- if(!lb.isNull()){
- addImplication(atom, lb);
- }
-
- if(!ub.isNull()){
- addImplication(negation, ub);
- }
-}
-void ArithUnatePropagator::addImplicationsUsingGeqAndEqualityValues(TNode atom){
-
- Assert(atom.getKind() == GEQ);
- Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
- Node left = atom[0];
- EqualValueSet& eqSet = getEqualValueSet(left);
-
- //TODO Improve this later
- for(EqualValueSet::iterator eqIter = eqSet.begin(); eqIter != eqSet.end(); ++eqIter){
- TNode eq = *eqIter;
- if(rightHandRationalIsEqual(atom, eq)){
- // (x = b' /\ b = b') => x >= b
- addImplication(eq, atom);
- }else if(rightHandRationalIsLT(eq, atom)){
- // (x = b' /\ b' < b) => x < b
- addImplication(eq, negation);
- }else{
- // (x = b' /\ b' > b) => x >= b
- addImplication(eq, atom);
- }
- }
-}
-
-void ArithUnatePropagator::addImplication(TNode a, TNode b){
- Node imp = NodeBuilder<2>(IMPLIES) << a << b;
-
- Debug("arith::unate") << "ArithUnatePropagator::addImplication"
- << "(" << a << ", " << b <<")" << endl;
-
- d_arithOut.lemma(imp);
-}
-
-
-Node ArithUnatePropagator::getImpliedUpperBoundUsingLeq(TNode leq, bool weaker) const {
- Assert(leq.getKind() == LEQ);
- Node left = leq[0];
-
- if(!leftIsSetup(left)) return Node::null();
-
- const Rational& value = rightHandRational(leq);
- const BoundValueSet& bvSet = getBoundValueSet(left);
-
- Node ub = getUpperBound(bvSet, value, false, weaker);
- return ub;
-}
-
-Node ArithUnatePropagator::getImpliedUpperBoundUsingLT(TNode lt, bool weaker) const {
- Assert(lt.getKind() == NOT && lt[0].getKind() == GEQ);
- Node atom = lt[0];
- Node left = atom[0];
-
- if(!leftIsSetup(left)) return Node::null();
-
- const Rational& value = rightHandRational(atom);
- const BoundValueSet& bvSet = getBoundValueSet(left);
-
- return getUpperBound(bvSet, value, true, weaker);
-}
-
-Node ArithUnatePropagator::getBestImpliedUpperBound(TNode upperBound) const {
- Node result = Node::null();
- if(upperBound.getKind() == LEQ ){
- result = getImpliedUpperBoundUsingLeq(upperBound, false);
- }else if(upperBound.getKind() == NOT && upperBound[0].getKind() == GEQ){
- result = getImpliedUpperBoundUsingLT(upperBound, false);
- }else if(upperBound.getKind() == LT){
- Node geq = NodeBuilder<2>(GEQ) << upperBound[0] << upperBound[1];
- Node lt = NodeBuilder<1>(NOT) << geq;
- result = getImpliedUpperBoundUsingLT(lt, false);
- }else{
- Unreachable();
- }
-
- Debug("arith::unate") << upperBound <<" -> " << result << std::endl;
- return result;
-}
-
-Node ArithUnatePropagator::getWeakerImpliedUpperBound(TNode upperBound) const {
- Node result = Node::null();
- if(upperBound.getKind() == LEQ ){
- result = getImpliedUpperBoundUsingLeq(upperBound, true);
- }else if(upperBound.getKind() == NOT && upperBound[0].getKind() == GEQ){
- result = getImpliedUpperBoundUsingLT(upperBound, true);
- }else if(upperBound.getKind() == LT){
- Node geq = NodeBuilder<2>(GEQ) << upperBound[0] << upperBound[1];
- Node lt = NodeBuilder<1>(NOT) << geq;
- result = getImpliedUpperBoundUsingLT(lt, true);
- }else{
- Unreachable();
- }
- Assert(upperBound != result);
- Debug("arith::unate") << upperBound <<" -> " << result << std::endl;
- return result;
-}
-
-Node ArithUnatePropagator::getImpliedLowerBoundUsingGT(TNode gt, bool weaker) const {
- Assert(gt.getKind() == NOT && gt[0].getKind() == LEQ);
- Node atom = gt[0];
- Node left = atom[0];
-
- if(!leftIsSetup(left)) return Node::null();
-
- const Rational& value = rightHandRational(atom);
- const BoundValueSet& bvSet = getBoundValueSet(left);
-
- return getLowerBound(bvSet, value, true, weaker);
-}
-
-Node ArithUnatePropagator::getImpliedLowerBoundUsingGeq(TNode geq, bool weaker) const {
- Assert(geq.getKind() == GEQ);
- Node left = geq[0];
-
- if(!leftIsSetup(left)) return Node::null();
-
- const Rational& value = rightHandRational(geq);
- const BoundValueSet& bvSet = getBoundValueSet(left);
-
- return getLowerBound(bvSet, value, false, weaker);
-}
-
-Node ArithUnatePropagator::getBestImpliedLowerBound(TNode lowerBound) const {
- Node result = Node::null();
- if(lowerBound.getKind() == GEQ ){
- result = getImpliedLowerBoundUsingGeq(lowerBound, false);
- }else if(lowerBound.getKind() == NOT && lowerBound[0].getKind() == LEQ){
- result = getImpliedLowerBoundUsingGT(lowerBound, false);
- }else if(lowerBound.getKind() == GT){
- Node leq = NodeBuilder<2>(LEQ)<<lowerBound[0]<< lowerBound[1];
- Node gt = NodeBuilder<1>(NOT) << leq;
- result = getImpliedLowerBoundUsingGT(gt, false);
- }else{
- Unreachable();
- }
- Debug("arith::unate") << lowerBound <<" -> " << result << std::endl;
- return result;
-}
-
-Node ArithUnatePropagator::getWeakerImpliedLowerBound(TNode lowerBound) const {
- Node result = Node::null();
- if(lowerBound.getKind() == GEQ ){
- result = getImpliedLowerBoundUsingGeq(lowerBound, true);
- }else if(lowerBound.getKind() == NOT && lowerBound[0].getKind() == LEQ){
- result = getImpliedLowerBoundUsingGT(lowerBound, true);
- }else if(lowerBound.getKind() == GT){
- Node leq = NodeBuilder<2>(LEQ)<<lowerBound[0]<< lowerBound[1];
- Node gt = NodeBuilder<1>(NOT) << leq;
- result = getImpliedLowerBoundUsingGT(gt, true);
- }else{
- Unreachable();
- }
- Assert(result != lowerBound);
-
- Debug("arith::unate") << lowerBound <<" -> " << result << std::endl;
- return result;
-}
+++ /dev/null
-/********************* */
-/*! \file unate_propagator.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief ArithUnatePropagator constructs implications of the form
- ** "if x < c and c < b, then x < b" (where c and b are constants).
- **
- ** ArithUnatePropagator detects unate implications amongst the atoms
- ** associated with the theory of arithmetic and informs the SAT solver of the
- ** implication. A unate implication is an implication of the form:
- ** "if x < c and c < b, then x < b" (where c and b are constants).
- ** Unate implications are always 2-SAT clauses.
- ** ArithUnatePropagator sends the implications to the SAT solver in an
- ** online fashion.
- ** This means that atoms may be added during solving or before.
- **
- ** ArithUnatePropagator maintains sorted lists containing all atoms associated
- ** for each unique left hand side, the "x" in the inequality "x < c".
- ** The lists are sorted by the value of the right hand side which must be a
- ** rational constant.
- **
- ** ArithUnatePropagator tries to send out a minimal number of additional
- ** lemmas per atom added. Let (x < a), (x < b), (x < c) be arithmetic atoms s.t.
- ** a < b < c.
- ** If the the order of adding the atoms is (x < a), (x < b), and (x < c), then
- ** then set of all lemmas added is:
- ** {(=> (x<a) (x < b)), (=> (x<b) (x < c))}
- ** If the order is changed to (x < a), (x < c), and (x < b), then
- ** the final set of implications emitted is:
- ** {(=> (x<a) (x < c)), (=> (x<a) (x < b)), (=> (x<b) (x < c))}
- **
- ** \todo document this file
- **/
-
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__ARITH__ARITH_PROPAGATOR_H
-#define __CVC4__THEORY__ARITH__ARITH_PROPAGATOR_H
-
-#include "expr/node.h"
-#include "context/context.h"
-
-#include "theory/output_channel.h"
-#include "theory/arith/ordered_set.h"
-
-#include <ext/hash_map>
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-class ArithUnatePropagator {
-private:
- /**
- * OutputChannel for the theory of arithmetic.
- * The propagator uses this to pass implications back to the SAT solver.
- */
- OutputChannel& d_arithOut;
-
- struct VariablesSets {
- BoundValueSet d_boundValueSet;
- EqualValueSet d_eqValueSet;
- };
-
- /** TODO: justify making this a TNode. */
- typedef __gnu_cxx::hash_map<TNode, VariablesSets, NodeHashFunction> NodeToSetsMap;
- NodeToSetsMap d_setsMap;
-
-public:
- ArithUnatePropagator(context::Context* cxt, OutputChannel& arith);
-
- /**
- * Adds an atom to the propagator.
- * Any resulting lemmas will be output via d_arithOut.
- */
- void addAtom(TNode atom);
-
- /** Returns true if v has been added as a left hand side in an atom */
- bool hasAnyAtoms(TNode v) const;
-
- bool containsLiteral(TNode lit) const;
- bool containsAtom(TNode atom) const;
- bool containsEquality(TNode atom) const;
- bool containsLeq(TNode atom) const;
- bool containsGeq(TNode atom) const;
-
-
-
-private:
- VariablesSets& getVariablesSets(TNode left);
- BoundValueSet& getBoundValueSet(TNode left);
- EqualValueSet& getEqualValueSet(TNode left);
-
- const VariablesSets& getVariablesSets(TNode left) const;
- const BoundValueSet& getBoundValueSet(TNode left) const;
- const EqualValueSet& getEqualValueSet(TNode left) const;
-
- /** Sends an implication (=> a b) to the PropEngine via d_arithOut. */
- void addImplication(TNode a, TNode b);
-
- /** Check to make sure an lhs has been properly set-up. */
- bool leftIsSetup(TNode left) const;
-
- /** Initializes the lists associated with a unique lhs. */
- void setupLefthand(TNode left);
-
-
- /**
- * The addImplicationsUsingKAndJList(...)
- * functions are the work horses of ArithUnatePropagator.
- * These take an atom of the kind K that has just been added
- * to its associated list, and the ordered list of Js associated with the lhs,
- * and uses these to deduce unate implications.
- * (K and J vary over EQUAL, LEQ, and GEQ.)
- *
- * Input:
- * atom - the atom being inserted of kind K
- * Jset - the list of atoms of kind J associated with the lhs.
- *
- * Unfortunately, these tend to be an absolute bear to read because
- * of all of the special casing and C++ iterator manipulation required.
- */
-
- void addImplicationsUsingEqualityAndEqualityValues(TNode eq);
- void addImplicationsUsingEqualityAndBoundValues(TNode eq);
-
- void addImplicationsUsingLeqAndEqualityValues(TNode leq);
- void addImplicationsUsingLeqAndBoundValues(TNode leq);
-
- void addImplicationsUsingGeqAndEqualityValues(TNode geq);
- void addImplicationsUsingGeqAndBoundValues(TNode geq);
-
- bool hasBoundValueEntry(TNode n);
-
- Node getImpliedUpperBoundUsingLeq(TNode leq, bool weaker) const;
- Node getImpliedUpperBoundUsingLT(TNode lt, bool weaker) const;
-
- Node getImpliedLowerBoundUsingGeq(TNode geq, bool weaker) const;
- Node getImpliedLowerBoundUsingGT(TNode gt, bool weaker) const;
-
-public:
- Node getBestImpliedUpperBound(TNode upperBound) const;
- Node getBestImpliedLowerBound(TNode lowerBound) const;
-
-
- Node getWeakerImpliedUpperBound(TNode upperBound) const;
- Node getWeakerImpliedLowerBound(TNode lowerBound) const;
-};
-
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__ARITH__THEORY_ARITH_H */
replayFilename(""),
replayStream(NULL),
replayLog(NULL),
- rewriteArithEqualities(false),
+ variableRemovalEnabled(false),
arithPropagation(false),
satRandomFreq(0.0),
satRandomSeed(91648253),// Minisat's default value
--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";
PIVOT_RULE,
RANDOM_FREQUENCY,
RANDOM_SEED,
- REWRITE_ARITHMETIC_EQUALITIES,
+ ENABLE_VARIABLE_REMOVAL,
ARITHMETIC_PROPAGATION
};/* enum OptionValue */
{ "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! */
#endif /* CVC4_REPLAY */
break;
- case REWRITE_ARITHMETIC_EQUALITIES:
- rewriteArithEqualities = true;
+ case ENABLE_VARIABLE_REMOVAL:
+ variableRemovalEnabled = true;
break;
case ARITHMETIC_PROPAGATION:
/** Log to write replay instructions to; NULL if not logging. */
std::ostream* replayLog;
- /** Whether to rewrite equalities in arithmetic theory */
- bool rewriteArithEqualities;
+ /** Determines whether arithmetic will try to variables. */
+ bool variableRemovalEnabled;
/** Turn on and of arithmetic propagation. */
bool arithPropagation;
arith.02.cvc \
arith.03.cvc \
delta-minimized-row-vector-bug.smt \
+ fuzz_3-eq.smt \
leq.01.smt \
miplibtrick.smt
--- /dev/null
+(benchmark fuzzsmt
+:logic QF_LRA
+:extrafuns ((v0 Real))
+:extrafuns ((v2 Real))
+:extrafuns ((v1 Real))
+:status sat
+:formula
+(let (?n1 2)
+(let (?n2 (* ?n1 ?n1))
+(let (?n3 (~ v0))
+(let (?n4 (* ?n1 ?n3))
+(let (?n5 (- ?n1 ?n1))
+(let (?n6 (- ?n5 v0))
+(let (?n7 (- ?n4 ?n6))
+(flet ($n8 (= ?n2 ?n7))
+(flet ($n9 false)
+(let (?n10 (ite $n9 ?n1 v1))
+(let (?n11 (+ ?n1 v2))
+(flet ($n12 (= ?n10 ?n11))
+(let (?n13 (ite $n9 v0 ?n2))
+(let (?n14 (~ ?n1))
+(let (?n15 (ite $n9 ?n14 ?n1))
+(flet ($n16 (= ?n13 ?n15))
+(flet ($n17 (= ?n1 ?n7))
+(let (?n18 (+ ?n1 ?n1))
+(flet ($n19 (= v2 ?n18))
+(let (?n20 (ite $n19 v2 ?n1))
+(let (?n21 (ite $n17 ?n18 ?n20))
+(flet ($n22 (= ?n21 ?n2))
+(let (?n23 (ite $n9 ?n21 ?n2))
+(flet ($n24 (= ?n23 ?n1))
+(flet ($n25 (= ?n7 ?n2))
+(flet ($n26 (iff $n24 $n25))
+(let (?n27 (~ ?n7))
+(flet ($n28 (= ?n27 ?n1))
+(let (?n29 (ite $n28 ?n1 ?n1))
+(flet ($n30 (= ?n1 ?n29))
+(flet ($n31 (implies $n26 $n30))
+(flet ($n32 (implies $n9 $n9))
+(flet ($n33 (if_then_else $n22 $n31 $n32))
+(flet ($n34 (and $n9 $n33))
+(flet ($n35 (if_then_else $n16 $n34 $n9))
+(flet ($n36 (iff $n12 $n35))
+(flet ($n37 (and $n8 $n36))
+$n37
+))))))))))))))))))))))))))))))))))))))
projects / cvc5.git / commitdiff