From: Tim King Date: Mon, 18 Apr 2011 16:48:52 +0000 (+0000) Subject: This commit merges the branch arithmetic/propagation-again into trunk. X-Git-Tag: cvc5-1.0.0~8590 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=abe849b486ea3707fd51a612c7982554f3d6581f;p=cvc5.git This commit merges the branch arithmetic/propagation-again into trunk. - This adds code for bounds refinement, and conflict weakening. - This adds util/boolean_simplification.h. - This adds a propagation manager to theory of arithmetic. - Propagation is disabled by default. - Propagation can be enabled by the command line flag "--enable-arithmetic-propagation" - Propagation interacts *heavily* with rewriting equalities, and will work best if the command line flag "--rewrite-arithmetic-equalities" is enabled. --- diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 12088b493..c5534560b 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -11,6 +11,9 @@ libarith_la_SOURCES = \ arith_rewriter.cpp \ arith_static_learner.h \ arith_static_learner.cpp \ + arith_prop_manager.h \ + arith_prop_manager.cpp \ + arithvar_node_map.h \ normal_form.h\ normal_form.cpp \ arith_utilities.h \ diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp index 4905f4dc5..872c25e3b 100644 --- a/src/theory/arith/arith_priority_queue.cpp +++ b/src/theory/arith/arith_priority_queue.cpp @@ -160,7 +160,7 @@ void ArithPriorityQueue::transitionToDifferenceMode() { Assert(d_diffQueue.empty()); Debug("arith::priorityqueue") << "transitionToDifferenceMode()" << endl; - d_varSet.clear(); + d_varSet.purge(); ArithVarArray::const_iterator i = d_candidates.begin(), end = d_candidates.end(); for(; i != end; ++i){ @@ -232,18 +232,18 @@ void ArithPriorityQueue::clear(){ switch(d_modeInUse){ case Collection: d_candidates.clear(); - d_varSet.clear(); + d_varSet.purge(); break; case VariableOrder: if(!d_varOrderQueue.empty()) { d_varOrderQueue.clear(); - d_varSet.clear(); + d_varSet.purge(); } break; case Difference: if(!d_diffQueue.empty()){ d_diffQueue.clear(); - d_varSet.clear(); + d_varSet.purge(); } break; default: diff --git a/src/theory/arith/arith_prop_manager.cpp b/src/theory/arith/arith_prop_manager.cpp new file mode 100644 index 000000000..a09bed8e8 --- /dev/null +++ b/src/theory/arith/arith_prop_manager.cpp @@ -0,0 +1,174 @@ + +#include "theory/arith/arith_prop_manager.h" + +#include "theory/arith/arith_utilities.h" +#include "context/context.h" +#include "context/cdlist.h" +#include "context/cdmap.h" +#include "context/cdo.h" + +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::arith; +using namespace CVC4::kind; +using namespace std; + + +bool ArithPropManager::isAsserted(TNode n) const{ + Node satValue = d_valuation.getSatValue(n); + if(satValue.isNull()){ + return false; + }else{ + //Assert(satValue.getConst()); + return true; + } +} + +// Node ArithPropManager::strictlyWeakerAssertedUpperBound(TNode n) const{ +// Node weaker = n; +// do { +// weaker = d_propagator.getWeakerImpliedUpperBound(weaker); +// }while(!weaker.isNull() && !isAsserted(weaker)); +// Assert(weaker != n); +// return weaker; +// } + +// Node ArithPropManager::strictlyWeakerAssertedLowerBound(TNode n) const{ +// Node weaker = n; +// do { +// weaker = d_propagator.getWeakerImpliedLowerBound(weaker); +// }while(!weaker.isNull() && !isAsserted(weaker)); +// Assert(weaker != n); +// return weaker; +// } + +Node ArithPropManager::strictlyWeakerAssertedUpperBound(ArithVar v, const DeltaRational& b) const{ + Node bound = boundAsNode(true, v, b); + + Assert(b.getInfinitesimalPart() <= 0); + bool largeEpsilon = (b.getInfinitesimalPart() < -1); + + Node weaker = bound; + do { + if(largeEpsilon){ + weaker = d_propagator.getBestImpliedUpperBound(weaker); + largeEpsilon = false; + }else{ + weaker = d_propagator.getWeakerImpliedUpperBound(weaker); + } + }while(!weaker.isNull() && !isAsserted(weaker)); + return weaker; +} + +Node ArithPropManager::strictlyWeakerAssertedLowerBound(ArithVar v, const DeltaRational& b) const{ + Debug("ArithPropManager") << "strictlyWeakerAssertedLowerBound" << endl; + Node bound = boundAsNode(false, v, b); + + Assert(b.getInfinitesimalPart() >= 0); + bool largeEpsilon = (b.getInfinitesimalPart() > 1); + + Node weaker = bound; + Debug("ArithPropManager") << bound << b << endl; + do { + if(largeEpsilon){ + weaker = d_propagator.getBestImpliedLowerBound(weaker); + largeEpsilon = false; + }else{ + weaker = d_propagator.getWeakerImpliedLowerBound(weaker); + } + }while(!weaker.isNull() && !isAsserted(weaker)); + Debug("ArithPropManager") << "res: " << weaker << endl; + return weaker; +} + +Node ArithPropManager::getBestImpliedLowerBound(ArithVar v, const DeltaRational& b) const{ + Node bound = boundAsNode(false, v, b); + return d_propagator.getBestImpliedLowerBound(bound); +} +Node ArithPropManager::getBestImpliedUpperBound(ArithVar v, const DeltaRational& b) const{ + Node bound = boundAsNode(true, v, b); + return d_propagator.getBestImpliedUpperBound(bound); +} + +bool ArithPropManager::hasStrongerLowerBound(TNode n) const{ + bool haveAcompilerWarning; + return true; +} +bool ArithPropManager::hasStrongerUpperBound(TNode n) const{ + return true; +} + +Node ArithPropManager::boundAsNode(bool upperbound, ArithVar var, const DeltaRational& b) const { + Assert((!upperbound) || (b.getInfinitesimalPart() <= 0) ); + Assert(upperbound || (b.getInfinitesimalPart() >= 0) ); + + Node varAsNode = d_arithvarNodeMap.asNode(var); + Kind kind; + bool negate; + if(upperbound){ + negate = b.getInfinitesimalPart() < 0; + kind = negate ? GEQ : LEQ; + } else{ + negate = b.getInfinitesimalPart() > 0; + kind = negate ? LEQ : GEQ; + } + + Node righthand = mkRationalNode(b.getNoninfinitesimalPart()); + Node bAsNode = NodeBuilder<2>(kind) << varAsNode << righthand; + + if(negate){ + bAsNode = NodeBuilder<1>(NOT) << bAsNode; + } + + return bAsNode; +} + +bool ArithPropManager::propagateArithVar(bool upperbound, ArithVar var, const DeltaRational& b, TNode reason){ + bool success = false; + + ++d_statistics.d_propagateArithVarCalls; + + Node bAsNode = boundAsNode(upperbound, var ,b); + + Node bestImplied = upperbound ? + d_propagator.getBestImpliedUpperBound(bAsNode): + d_propagator.getBestImpliedLowerBound(bAsNode); + + Debug("ArithPropManager") << upperbound <<","<< var <<","<< b <<","<< reason << endl + << bestImplied << endl; + + if(!bestImplied.isNull()){ + bool asserted = isAsserted(bestImplied); + + if( !asserted && !isPropagated(bestImplied)){ + propagate(bestImplied, reason); + ++d_statistics.d_addedPropagation; + success = true; + }else if(!asserted){ + ++d_statistics.d_alreadyPropagatedNode; + }else if(!isPropagated(bestImplied)){ + ++d_statistics.d_alreadySetSatLiteral; + } + } + return success; +} + +ArithPropManager::Statistics::Statistics(): + d_propagateArithVarCalls("arith::prop-manager::propagateArithVarCalls",0), + d_addedPropagation("arith::prop-manager::addedPropagation",0), + d_alreadySetSatLiteral("arith::prop-manager::alreadySetSatLiteral",0), + d_alreadyPropagatedNode("arith::prop-manager::alreadyPropagatedNode",0) +{ + StatisticsRegistry::registerStat(&d_propagateArithVarCalls); + StatisticsRegistry::registerStat(&d_alreadySetSatLiteral); + StatisticsRegistry::registerStat(&d_alreadyPropagatedNode); + StatisticsRegistry::registerStat(&d_addedPropagation); +} + +ArithPropManager::Statistics::~Statistics() +{ + StatisticsRegistry::unregisterStat(&d_propagateArithVarCalls); + StatisticsRegistry::unregisterStat(&d_alreadySetSatLiteral); + StatisticsRegistry::unregisterStat(&d_alreadyPropagatedNode); + StatisticsRegistry::unregisterStat(&d_addedPropagation); +} diff --git a/src/theory/arith/arith_prop_manager.h b/src/theory/arith/arith_prop_manager.h new file mode 100644 index 000000000..1fd23dd62 --- /dev/null +++ b/src/theory/arith/arith_prop_manager.h @@ -0,0 +1,144 @@ +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__ARITH__ARITH_PROP_MANAGER_H +#define __CVC4__THEORY__ARITH__ARITH_PROP_MANAGER_H + +#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/delta_rational.h" +#include "context/context.h" +#include "context/cdlist.h" +#include "context/cdmap.h" +#include "context/cdo.h" + +#include "util/stats.h" + +namespace CVC4 { +namespace theory { +namespace arith { + +class PropManager { +private: + context::CDList d_propagated; + context::CDO d_propagatedPos; + typedef context::CDMap ExplainMap; + + ExplainMap d_explanationMap; + + context::CDList d_reasons; + +public: + + PropManager(context::Context* c): + d_propagated(c), + d_propagatedPos(c, 0), + d_explanationMap(c), + d_reasons(c) + { } + + bool isPropagated(TNode n) const { + return d_explanationMap.find(n) != d_explanationMap.end(); + } + + void propagate(TNode n, Node reason) { + Assert(!isPropagated(n)); + Assert(reason.getKind() == kind::AND); + + d_explanationMap.insert(n, reason); + + d_reasons.push_back(reason); + d_propagated.push_back(n); + + //std::cout << n << std::endl << "<="<< reason<< std::endl; + } + + bool hasMorePropagations() const { + return d_propagatedPos < d_propagated.size(); + } + + TNode getPropagation() { + Assert(hasMorePropagations()); + TNode prop = d_propagated[d_propagatedPos]; + d_propagatedPos = d_propagatedPos + 1; + return prop; + } + + TNode explain(TNode n) const { + Assert(isPropagated(n)); + ExplainMap::iterator p = d_explanationMap.find(n); + return (*p).second; + } + +};/* class PropManager */ + +class ArithPropManager : public PropManager { +private: + const ArithVarNodeMap& d_arithvarNodeMap; + const ArithUnatePropagator& d_propagator; + Valuation d_valuation; + +public: + ArithPropManager(context::Context* c, + const ArithVarNodeMap& map, + const ArithUnatePropagator& prop, + Valuation v): + PropManager(c), d_arithvarNodeMap(map), d_propagator(prop), d_valuation(v) + {} + + /** + * Returns true if the node has a value in sat solver in the current context. + * In debug mode this fails an Assert() if the node has a negative assignment. + */ + bool isAsserted(TNode n) const; + + /** Returns true if a bound was added. */ + bool propagateArithVar(bool upperbound, ArithVar var, const DeltaRational& b, TNode reason); + + Node boundAsNode(bool upperbound, ArithVar var, const DeltaRational& b) const; + + Node strictlyWeakerLowerBound(TNode n) const{ + return d_propagator.getWeakerImpliedLowerBound(n); + } + Node strictlyWeakerUpperBound(TNode n) const{ + return d_propagator.getWeakerImpliedUpperBound(n); + } + + + //Node strictlyWeakerAssertedUpperBound(TNode n) const; + //Node strictlyWeakerAssertedLowerBound(TNode n) const; + + Node strictlyWeakerAssertedUpperBound(ArithVar v, const DeltaRational& b) const; + + Node strictlyWeakerAssertedLowerBound(ArithVar v, const DeltaRational& b) const; + + Node getBestImpliedLowerBound(ArithVar v, const DeltaRational& b) const; + Node getBestImpliedUpperBound(ArithVar v, const DeltaRational& b) const; + + bool hasStrongerLowerBound(TNode current) const; + bool hasStrongerUpperBound(TNode current) const; + + bool containsLiteral(TNode n) const { + return d_propagator.containsLiteral(n); + } + +private: + class Statistics { + public: + IntStat d_propagateArithVarCalls; + IntStat d_addedPropagation; + IntStat d_alreadySetSatLiteral; + IntStat d_alreadyPropagatedNode; + + Statistics(); + ~Statistics(); + }; + Statistics d_statistics; +}; + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__ARITH__ARITH_PROP_MANAGER_H */ diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 59b4e9bef..78b77eb00 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -25,6 +25,7 @@ #include "util/rational.h" #include "expr/node.h" #include "expr/attribute.h" +#include "theory/arith/delta_rational.h" #include #include #include @@ -204,6 +205,38 @@ inline int deltaCoeff(Kind k){ } } +template +inline TNode getSide(TNode assertion, Kind simpleKind){ + switch(simpleKind){ + case kind::LT: + case kind::GT: + case kind::DISTINCT: + return selectLeft ? (assertion[0])[0] : (assertion[0])[1]; + case kind::LEQ: + case kind::GEQ: + case kind::EQUAL: + return selectLeft ? assertion[0] : assertion[1]; + default: + Unreachable(); + return TNode::null(); + } +} + +inline DeltaRational determineRightConstant(TNode assertion, Kind simpleKind){ + TNode right = getSide(assertion, simpleKind); + + Assert(right.getKind() == kind::CONST_RATIONAL); + const Rational& noninf = right.getConst(); + + Rational inf = Rational(Integer(deltaCoeff(simpleKind))); + return DeltaRational(noninf, inf); +} + +inline DeltaRational asDeltaRational(TNode n){ + Kind simp = simplifiedKind(n); + return determineRightConstant(n, simp); +} + /** * Takes two nodes with exactly 2 children, * the second child of both are of kind CONST_RATIONAL, @@ -236,6 +269,19 @@ inline Node negateConjunctionAsClause(TNode conjunction){ return orBuilder; } +inline Node maybeUnaryConvert(NodeBuilder<>& builder){ + Assert(builder.getKind() == kind::OR || + builder.getKind() == kind::AND || + builder.getKind() == kind::PLUS || + builder.getKind() == kind::MULT); + Assert(builder.getNumChildren() >= 1); + if(builder.getNumChildren() == 1){ + return builder[0]; + }else{ + return builder; + } +} + }; /* namesapce arith */ }; /* namespace theory */ }; /* namespace CVC4 */ diff --git a/src/theory/arith/arithvar_node_map.h b/src/theory/arith/arithvar_node_map.h new file mode 100644 index 000000000..aca61878d --- /dev/null +++ b/src/theory/arith/arithvar_node_map.h @@ -0,0 +1,59 @@ +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H +#define __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H + + +#include "theory/arith/arith_utilities.h" +#include "context/context.h" +#include "context/cdlist.h" +#include "context/cdmap.h" +#include "context/cdo.h" + +namespace CVC4 { +namespace theory { +namespace arith { + +class ArithVarNodeMap { +private: + /** + * Bidirectional map between Nodes and ArithVars. + */ + NodeToArithVarMap d_nodeToArithVarMap; + ArithVarToNodeMap d_arithVarToNodeMap; + +public: + ArithVarNodeMap() {} + + inline bool hasArithVar(TNode x) const { + return d_nodeToArithVarMap.find(x) != d_nodeToArithVarMap.end(); + } + + inline ArithVar asArithVar(TNode x) const{ + Assert(hasArithVar(x)); + Assert((d_nodeToArithVarMap.find(x))->second <= ARITHVAR_SENTINEL); + return (d_nodeToArithVarMap.find(x))->second; + } + inline Node asNode(ArithVar a) const{ + Assert(d_arithVarToNodeMap.find(a) != d_arithVarToNodeMap.end()); + return (d_arithVarToNodeMap.find(a))->second; + } + + inline void setArithVar(TNode x, ArithVar a){ + Assert(!hasArithVar(x)); + Assert(d_arithVarToNodeMap.find(a) == d_arithVarToNodeMap.end()); + d_arithVarToNodeMap[a] = x; + d_nodeToArithVarMap[x] = a; + } + + const ArithVarToNodeMap& getArithVarToNodeMap() const { + return d_arithVarToNodeMap; + } + +};/* class ArithVarNodeMap */ + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H */ diff --git a/src/theory/arith/arithvar_set.h b/src/theory/arith/arithvar_set.h index 0d59e3aea..4cd205172 100644 --- a/src/theory/arith/arithvar_set.h +++ b/src/theory/arith/arithvar_set.h @@ -72,9 +72,12 @@ public: return d_posVector.size(); } - void clear(){ + void purge() { + for(VarList::const_iterator i=d_list.begin(), endIter=d_list.end();i!= endIter; ++i){ + d_posVector[*i] = ARITHVAR_SENTINEL; + } d_list.clear(); - d_posVector.clear(); + Assert(empty()); } void increaseSize(ArithVar max){ @@ -117,6 +120,16 @@ public: const_iterator begin() const{ return d_list.begin(); } const_iterator end() const{ return d_list.end(); } + /** + * Invalidates iterators. + * Adds x to the set if it is not already in the set. + */ + void softAdd(ArithVar x){ + if(!isMember(x)){ + add(x); + } + } + const VarList& getList() const{ return d_list; } @@ -125,8 +138,16 @@ public: void remove(ArithVar x){ Assert(isMember(x)); swapToBack(x); - d_posVector[x] = ARITHVAR_SENTINEL; + Assert(d_list.back() == x); + pop_back(); + } + + ArithVar pop_back() { + Assert(!empty()); + ArithVar atBack = d_list.back(); + d_posVector[atBack] = ARITHVAR_SENTINEL; d_list.pop_back(); + return atBack; } private: diff --git a/src/theory/arith/ordered_set.h b/src/theory/arith/ordered_set.h index 68c5e18c9..43ccd7815 100644 --- a/src/theory/arith/ordered_set.h +++ b/src/theory/arith/ordered_set.h @@ -1,3 +1,4 @@ +#include #include #include "expr/kind.h" #include "expr/node.h" @@ -9,16 +10,84 @@ namespace CVC4 { namespace theory { namespace arith { +inline const Rational& rightHandRational(TNode ineq){ + Assert(ineq.getKind() == kind::LEQ + || ineq.getKind() == kind::GEQ + || ineq.getKind() == kind::EQUAL); + TNode righthand = ineq[1]; + Assert(righthand.getKind() == kind::CONST_RATIONAL); + return righthand.getConst(); +} -typedef std::set OrderedSet; +class BoundValueEntry { +private: + const Rational& value; + TNode d_leq, d_geq; -struct SetCleanupStrategy{ - static void cleanup(OrderedSet* l){ - Debug("arithgc") << "cleaning up " << l << "\n"; - delete l; + BoundValueEntry(const Rational& v, TNode l, TNode g): + value(v), + d_leq(l), + d_geq(g) + {} + +public: + Node getLeq() const{ + Assert(hasLeq()); + return d_leq; + } + Node getGeq() const{ + Assert(hasGeq()); + return d_geq; + } + + static BoundValueEntry mkFromLeq(TNode leq){ + Assert(leq.getKind() == kind::LEQ); + return BoundValueEntry(rightHandRational(leq), leq, TNode::null()); + } + + static BoundValueEntry mkFromGeq(TNode geq){ + Assert(geq.getKind() == kind::GEQ); + return BoundValueEntry(rightHandRational(geq), TNode::null(), geq); + } + + void addLeq(TNode leq){ + Assert(leq.getKind() == kind::LEQ); + Assert(rightHandRational(leq) == getValue()); + Assert(!hasLeq()); + d_leq = leq; + } + + void addGeq(TNode geq){ + Assert(geq.getKind() == kind::GEQ); + Assert(rightHandRational(geq) == getValue()); + Assert(!hasGeq()); + d_geq = geq; + } + + bool hasGeq() const { return d_geq != TNode::null(); } + bool hasLeq() const { return d_leq != TNode::null(); } + + + const Rational& getValue() const{ + return value; + } + + bool operator<(const BoundValueEntry& other){ + return value < other.value; } }; +typedef std::map BoundValueSet; + +typedef std::set EqualValueSet; + +// struct SetCleanupStrategy{ +// static void cleanup(OrderedSet* l){ +// Debug("arithgc") << "cleaning up " << l << "\n"; +// delete l; +// } +// }; + }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index 39685a2a1..3cd8ed926 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -184,6 +184,21 @@ bool ArithPartialModel::belowLowerBound(ArithVar x, const DeltaRational& c, bool } } +bool ArithPartialModel::equalsLowerBound(ArithVar x, const DeltaRational& c){ + if(!hasLowerBound(x)){ + return false; + }else{ + return c == d_lowerBound[x]; + } +} +bool ArithPartialModel::equalsUpperBound(ArithVar x, const DeltaRational& c){ + if(!hasUpperBound(x)){ + return false; + }else{ + return c == d_upperBound[x]; + } +} + bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict){ if(!hasUpperBound(x)){ // u = \intfy @@ -216,6 +231,30 @@ bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x){ return d_lowerBound[x] < d_assignment[x]; } +/** + * x <= u + * ? c < u + */ +bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x, const DeltaRational& c){ + Assert(inMaps(x)); + if(!hasUpperBound(x)){ // u = \infty + return true; + } + return c < d_upperBound[x]; +} + +/** + * x <= u + * ? c < u + */ +bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x, const DeltaRational& c){ + Assert(inMaps(x)); + if(!hasLowerBound(x)){ // l = -\infty + return true; + } + return d_lowerBound[x] < c; +} + bool ArithPartialModel::assignmentIsConsistent(ArithVar x){ const DeltaRational& beta = getAssignment(x); diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index 2edfdebca..171c74942 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -48,8 +48,8 @@ private: context::CDVector d_upperBound; context::CDVector d_lowerBound; - context::CDVector d_upperConstraint; - context::CDVector d_lowerConstraint; + context::CDVector d_upperConstraint; + context::CDVector d_lowerConstraint; bool d_deltaIsSafe; Rational d_delta; @@ -68,10 +68,10 @@ public: d_hasSafeAssignment(), d_assignment(), d_safeAssignment(), - d_upperBound(c, false), - d_lowerBound(c, false), - d_upperConstraint(c,false), - d_lowerConstraint(c,false), + d_upperBound(c, true), + d_lowerBound(c, true), + d_upperConstraint(c,true), + d_lowerConstraint(c,true), d_deltaIsSafe(false), d_delta(-1,1), d_history() @@ -114,17 +114,32 @@ public: /** - * x <= l + * x >= l * ? c < l */ bool belowLowerBound(ArithVar x, const DeltaRational& c, bool strict); /** * x <= u - * ? c < u + * ? c > u */ bool aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict); + bool equalsLowerBound(ArithVar x, const DeltaRational& c); + bool equalsUpperBound(ArithVar x, const DeltaRational& c); + + /** + * x <= u + * ? c < u + */ + bool strictlyBelowUpperBound(ArithVar x, const DeltaRational& c); + + /** + * x <= u + * ? c < u + */ + bool strictlyAboveLowerBound(ArithVar x, const DeltaRational& c); + bool strictlyBelowUpperBound(ArithVar x); bool strictlyAboveLowerBound(ArithVar x); bool assignmentIsConsistent(ArithVar x); diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 1a9c39984..b804cb1aa 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -14,6 +14,33 @@ static const uint32_t NUM_CHECKS = 10; static const bool CHECK_AFTER_PIVOT = true; static const uint32_t VARORDER_CHECK_PERIOD = 200; +SimplexDecisionProcedure::SimplexDecisionProcedure(ArithPropManager& propManager, + ArithPartialModel& pm, + Tableau& tableau) : + d_partialModel(pm), + d_tableau(tableau), + d_queue(pm, tableau), + d_propManager(propManager), + d_numVariables(0), + d_delayedLemmas(), + d_ZERO(0), + d_DELTA_ZERO(0,0) +{ + switch(Options::ArithPivotRule rule = Options::current()->pivotRule) { + case Options::MINIMUM: + d_queue.setPivotRule(ArithPriorityQueue::MINIMUM); + break; + case Options::BREAK_TIES: + d_queue.setPivotRule(ArithPriorityQueue::BREAK_TIES); + break; + case Options::MAXIMUM: + d_queue.setPivotRule(ArithPriorityQueue::MAXIMUM); + break; + default: + Unhandled(rule); + } +} + SimplexDecisionProcedure::Statistics::Statistics(): d_statPivots("theory::arith::pivots",0), d_statUpdates("theory::arith::updates",0), @@ -31,6 +58,13 @@ SimplexDecisionProcedure::Statistics::Statistics(): d_successDuringVarOrderSearch("theory::arith::qi::DuringVarOrderSearch::success",0), d_attemptAfterVarOrderSearch("theory::arith::qi::AfterVarOrderSearch::attempt",0), d_successAfterVarOrderSearch("theory::arith::qi::AfterVarOrderSearch::success",0), + d_weakeningAttempts("theory::arith::weakening::attempts",0), + d_weakeningSuccesses("theory::arith::weakening::success",0), + d_weakenings("theory::arith::weakening::total",0), + d_weakenTime("theory::arith::weakening::time"), + d_boundComputationTime("theory::arith::bound::time"), + d_boundComputations("theory::arith::bound::boundComputations",0), + d_boundPropagations("theory::arith::bound::boundPropagations",0), d_delayedConflicts("theory::arith::delayedConflicts",0), d_pivotTime("theory::arith::pivotTime"), d_avgNumRowsNotContainingOnUpdate("theory::arith::avgNumRowsNotContainingOnUpdate"), @@ -55,6 +89,15 @@ SimplexDecisionProcedure::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_attemptAfterVarOrderSearch); StatisticsRegistry::registerStat(&d_successAfterVarOrderSearch); + StatisticsRegistry::registerStat(&d_weakeningAttempts); + StatisticsRegistry::registerStat(&d_weakeningSuccesses); + StatisticsRegistry::registerStat(&d_weakenings); + StatisticsRegistry::registerStat(&d_weakenTime); + + StatisticsRegistry::registerStat(&d_boundComputationTime); + StatisticsRegistry::registerStat(&d_boundComputations); + StatisticsRegistry::registerStat(&d_boundPropagations); + StatisticsRegistry::registerStat(&d_delayedConflicts); StatisticsRegistry::registerStat(&d_pivotTime); @@ -83,6 +126,15 @@ SimplexDecisionProcedure::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_attemptAfterVarOrderSearch); StatisticsRegistry::unregisterStat(&d_successAfterVarOrderSearch); + StatisticsRegistry::unregisterStat(&d_weakeningAttempts); + StatisticsRegistry::unregisterStat(&d_weakeningSuccesses); + StatisticsRegistry::unregisterStat(&d_weakenings); + StatisticsRegistry::unregisterStat(&d_weakenTime); + + StatisticsRegistry::unregisterStat(&d_boundComputationTime); + StatisticsRegistry::unregisterStat(&d_boundComputations); + StatisticsRegistry::unregisterStat(&d_boundPropagations); + StatisticsRegistry::unregisterStat(&d_delayedConflicts); StatisticsRegistry::unregisterStat(&d_pivotTime); @@ -94,9 +146,21 @@ SimplexDecisionProcedure::Statistics::~Statistics(){ Node SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode original){ Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl; - if(d_partialModel.belowLowerBound(x_i, c_i, false)){ + if(d_partialModel.belowLowerBound(x_i, c_i, true)){ return Node::null(); } + // if(d_partialModel.equalsLowerBound(x_i, c_i) && original.getKind() != AND){ + // TNode prevConstraint = d_partialModel.getLowerConstraint(x_i); + // if(prevConstraint.getKind() == EQUAL){ + // return Node::null(); + // }else{ + // Debug("beat::ya") << x_i << " "<< c_i << original << prevConstraint << endl; + // Assert(prevConstraint.getKind() == AND); + // d_partialModel.setLowerConstraint(x_i,original); + // return Node::null(); + // } + // } + if(d_partialModel.aboveUpperBound(x_i, c_i, true)){ Node ubc = d_partialModel.getUpperConstraint(x_i); Node conflict = NodeManager::currentNM()->mkNode(AND, ubc, original); @@ -109,6 +173,8 @@ Node SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_ d_partialModel.setLowerConstraint(x_i,original); d_partialModel.setLowerBound(x_i, c_i); + d_updatedBounds.softAdd(x_i); + if(!d_tableau.isBasic(x_i)){ if(d_partialModel.getAssignment(x_i) < c_i){ update(x_i, c_i); @@ -127,23 +193,34 @@ Node SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_ Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl; - if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){ // \upperbound(x_i) <= c_i - //return false; //sat - return Node::null(); + if(d_partialModel.aboveUpperBound(x_i, c_i, true) ){ // \upperbound(x_i) <= c_i + return Node::null(); //sat } + + // if(d_partialModel.equalsUpperBound(x_i, c_i) && original.getKind() != AND){ + // TNode prevConstraint = d_partialModel.getUpperConstraint(x_i); + // if(prevConstraint.getKind() == EQUAL){ + // return Node::null(); + // }else{ + // Debug("beat::ya") << x_i << " "<< c_i << original << prevConstraint << endl; + // Assert(prevConstraint.getKind() == AND); + // d_partialModel.setUpperConstraint(x_i,original); + // return Node::null(); + // } + // } if(d_partialModel.belowLowerBound(x_i, c_i, true)){// \lowerbound(x_i) > c_i Node lbc = d_partialModel.getLowerConstraint(x_i); Node conflict = NodeManager::currentNM()->mkNode(AND, lbc, original); Debug("arith") << "AssertUpper conflict " << conflict << endl; ++(d_statistics.d_statAssertUpperConflicts); - //d_out->conflict(conflict); return conflict; - //return true; } d_partialModel.setUpperConstraint(x_i,original); d_partialModel.setUpperBound(x_i, c_i); + d_updatedBounds.softAdd(x_i); + if(!d_tableau.isBasic(x_i)){ if(d_partialModel.getAssignment(x_i) > c_i){ update(x_i, c_i); @@ -155,7 +232,6 @@ Node SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_ if(Debug.isOn("model")) { d_partialModel.printModel(x_i); } return Node::null(); - //return false; } @@ -168,16 +244,13 @@ Node SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational& // This can happen if both c_i <= x_i and x_i <= c_i are in the system. if(d_partialModel.belowLowerBound(x_i, c_i, false) && d_partialModel.aboveUpperBound(x_i, c_i, false)){ - //return false; //sat - return Node::null(); + return Node::null(); //sat } if(d_partialModel.aboveUpperBound(x_i, c_i, true)){ Node ubc = d_partialModel.getUpperConstraint(x_i); Node conflict = NodeManager::currentNM()->mkNode(AND, ubc, original); - //d_out->conflict(conflict); Debug("arith") << "AssertLower conflict " << conflict << endl; - //return true; return conflict; } @@ -185,8 +258,6 @@ Node SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational& Node lbc = d_partialModel.getLowerConstraint(x_i); Node conflict = NodeManager::currentNM()->mkNode(AND, lbc, original); Debug("arith") << "AssertUpper conflict " << conflict << endl; - //d_out->conflict(conflict); - //return true; return conflict; } @@ -196,52 +267,18 @@ Node SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational& d_partialModel.setUpperConstraint(x_i,original); d_partialModel.setUpperBound(x_i, c_i); + d_updatedBounds.softAdd(x_i); + if(!d_tableau.isBasic(x_i)){ if(!(d_partialModel.getAssignment(x_i) == c_i)){ update(x_i, c_i); } }else{ d_queue.enqueueIfInconsistent(x_i); - //checkBasicVariable(x_i); } - - //return false; return Node::null(); } -// set tableauAndHasSet(Tableau& tab, ArithVar v){ -// set has; -// for(ArithVarSet::const_iterator basicIter = tab.beginBasic(); -// basicIter != tab.endBasic(); -// ++basicIter){ -// ArithVar basic = *basicIter; -// ReducedRowVector& row = tab.lookup(basic); - -// if(row.has(v)){ -// has.insert(basic); -// } -// } -// return has; -// } - -// set columnIteratorSet(Tableau& tab,ArithVar v){ -// set has; -// Column::iterator basicIter = tab.beginColumn(v); -// Column::iterator endIter = tab.endColumn(v); -// for(; basicIter != endIter; ++basicIter){ -// ArithVar basic = *basicIter; -// has.insert(basic); -// } -// return has; -// } - - -/* -bool matchingSets(Tableau& tab, ArithVar v){ - return tableauAndHasSet(tab, v) == columnIteratorSet(tab, v); -} -*/ - void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){ Assert(!d_tableau.isBasic(x_i)); DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i); @@ -279,6 +316,116 @@ void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){ if(Debug.isOn("paranoid:check_tableau")){ debugCheckTableau(); } } + +bool SimplexDecisionProcedure::propagateCandidateBound(ArithVar basic, bool upperBound){ + + DeltaRational bound = upperBound ? + computeUpperBound(basic): + computeLowerBound(basic); + + if((upperBound && d_partialModel.strictlyBelowUpperBound(basic, bound)) || + (!upperBound && d_partialModel.strictlyAboveLowerBound(basic, bound))){ + Node bestImplied = upperBound ? + d_propManager.getBestImpliedUpperBound(basic, bound): + d_propManager.getBestImpliedLowerBound(basic, bound); + + if(!bestImplied.isNull()){ + bool asserted = d_propManager.isAsserted(bestImplied); + bool propagated = d_propManager.isPropagated(bestImplied); + if( !asserted && !propagated){ + + NodeBuilder<> nb(kind::AND); + if(upperBound){ + explainNonbasicsUpperBound(basic, nb); + }else{ + explainNonbasicsLowerBound(basic, nb); + } + Node explanation = nb; + d_propManager.propagate(bestImplied, explanation); + return true; + }else{ + Debug("arith::prop") << basic << " " << asserted << " " << propagated << endl; + } + } + } + return false; +} + + +bool SimplexDecisionProcedure::hasBounds(ArithVar basic, bool upperBound){ + for(Tableau::RowIterator iter = d_tableau.rowIterator(basic); !iter.atEnd(); ++iter){ + const TableauEntry& entry = *iter; + + ArithVar var = entry.getColVar(); + if(var == basic) continue; + int sgn = entry.getCoefficient().sgn(); + if(upperBound){ + if( (sgn < 0 && !d_partialModel.hasLowerBound(var)) || + (sgn > 0 && !d_partialModel.hasUpperBound(var))){ + return false; + } + }else{ + if( (sgn < 0 && !d_partialModel.hasUpperBound(var)) || + (sgn > 0 && !d_partialModel.hasLowerBound(var))){ + return false; + } + } + } + return true; +} +void SimplexDecisionProcedure::propagateCandidate(ArithVar basic){ + bool success = false; + if(d_partialModel.strictlyAboveLowerBound(basic) && + (!d_partialModel.hasLowerBound(basic) || d_propManager.hasStrongerLowerBound(d_partialModel.getLowerConstraint(basic))) && + hasLowerBounds(basic)){ + ++d_statistics.d_boundComputations; + success |= propagateCandidateLowerBound(basic); + } + if(d_partialModel.strictlyBelowUpperBound(basic) && + (!d_partialModel.hasUpperBound(basic) || d_propManager.hasStrongerUpperBound(d_partialModel.getUpperConstraint(basic))) && + hasUpperBounds(basic)){ + ++d_statistics.d_boundComputations; + success |= propagateCandidateUpperBound(basic); + } + if(success){ + ++d_statistics.d_boundPropagations; + } +} + +void SimplexDecisionProcedure::propagateCandidates(){ + TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime); + + Assert(d_candidateBasics.empty()); + + if(d_updatedBounds.empty()){ return; } + + PermissiveBackArithVarSet::const_iterator i = d_updatedBounds.begin(); + PermissiveBackArithVarSet::const_iterator end = d_updatedBounds.end(); + for(; i != end; ++i){ + ArithVar var = *i; + if(d_tableau.isBasic(var)){ + d_candidateBasics.softAdd(var); + }else{ + Tableau::ColIterator basicIter = d_tableau.colIterator(var); + for(; !basicIter.atEnd(); ++basicIter){ + const TableauEntry& entry = *basicIter; + ArithVar rowVar = entry.getRowVar(); + Assert(entry.getColVar() == var); + Assert(d_tableau.isBasic(rowVar)); + d_candidateBasics.softAdd(rowVar); + } + } + } + d_updatedBounds.purge(); + + while(!d_candidateBasics.empty()){ + ArithVar candidate = d_candidateBasics.pop_back(); + Assert(d_tableau.isBasic(candidate)); + propagateCandidate(candidate); + } +} + + void SimplexDecisionProcedure::debugPivotSimplex(ArithVar x_i, ArithVar x_j){ Debug("arith::simplex:row") << "debugRowSimplex(" << x_i << "|->" << x_j @@ -545,14 +692,14 @@ Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){ const DeltaRational& beta = d_partialModel.getAssignment(basic); if(d_partialModel.belowLowerBound(basic, beta, true)){ - ArithVar x_j = selectSlackBelow(basic); + ArithVar x_j = selectSlackUpperBound(basic); if(x_j == ARITHVAR_SENTINEL ){ - return generateConflictBelow(basic); + return generateConflictBelowLowerBound(basic); } }else if(d_partialModel.aboveUpperBound(basic, beta, true)){ - ArithVar x_j = selectSlackAbove(basic); + ArithVar x_j = selectSlackLowerBound(basic); if(x_j == ARITHVAR_SENTINEL ){ - return generateConflictAbove(basic); + return generateConflictAboveUpperBound(basic); } } return Node::null(); @@ -580,30 +727,43 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera ArithVar x_j = ARITHVAR_SENTINEL; if(d_partialModel.belowLowerBound(x_i, beta_i, true)){ - x_j = selectSlackBelow(x_i); + x_j = selectSlackUpperBound(x_i); if(x_j == ARITHVAR_SENTINEL ){ ++(d_statistics.d_statUpdateConflicts); - return generateConflictBelow(x_i); //unsat + return generateConflictBelowLowerBound(x_i); //unsat } DeltaRational l_i = d_partialModel.getLowerBound(x_i); pivotAndUpdate(x_i, x_j, l_i); }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){ - x_j = selectSlackAbove(x_i); + x_j = selectSlackLowerBound(x_i); if(x_j == ARITHVAR_SENTINEL ){ ++(d_statistics.d_statUpdateConflicts); - return generateConflictAbove(x_i); //unsat + return generateConflictAboveUpperBound(x_i); //unsat } DeltaRational u_i = d_partialModel.getUpperBound(x_i); pivotAndUpdate(x_i, x_j, u_i); } Assert(x_j != ARITHVAR_SENTINEL); + //Check to see if we already have a conflict with x_j to prevent wasteful work if(CHECK_AFTER_PIVOT){ - Node earlyConflict = checkBasicForConflict(x_j); - if(!earlyConflict.isNull()){ - return earlyConflict; + Node possibleConflict = checkBasicForConflict(x_j); + if(!possibleConflict.isNull()){ + return possibleConflict; } + // if(selectSlackUpperBound(x_j) == ARITHVAR_SENTINEL){ + // Node possibleConflict = deduceUpperBound(x_j); + // if(!possibleConflict.isNull()){ + // return possibleConflict; + // } + // } + // if(selectSlackLowerBound(x_j) == ARITHVAR_SENTINEL){ + // Node possibleConflict = deduceLowerBound(x_j); + // if(!possibleConflict.isNull()){ + // return possibleConflict; + // } + // } } } Assert(remainingIterations == 0); @@ -611,93 +771,289 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera return Node::null(); } +template +void SimplexDecisionProcedure::explainNonbasics(ArithVar basic, NodeBuilder<>& output){ + Assert(d_tableau.isBasic(basic)); -Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){ - - NodeBuilder<> nb(kind::AND); - TNode bound = d_partialModel.getUpperConstraint(conflictVar); - - Debug("arith") << "generateConflictAbove " - << "conflictVar " << conflictVar - << " " << d_partialModel.getAssignment(conflictVar) - << " " << bound << endl; + Debug("arith::explainNonbasics") << "SimplexDecisionProcedure::explainNonbasics(" + << basic <<") start" << endl; - nb << bound; - Tableau::RowIterator iter = d_tableau.rowIterator(conflictVar); + Tableau::RowIterator iter = d_tableau.rowIterator(basic); for(; !iter.atEnd(); ++iter){ const TableauEntry& entry = *iter; ArithVar nonbasic = entry.getColVar(); - if(nonbasic == conflictVar) continue; + if(nonbasic == basic) continue; const Rational& a_ij = entry.getCoefficient(); Assert(a_ij != d_ZERO); + TNode bound = TNode::null(); int sgn = a_ij.sgn(); Assert(sgn != 0); - if(sgn < 0){ - bound = d_partialModel.getUpperConstraint(nonbasic); - Debug("arith") << "below 0 " << nonbasic << " " - << d_partialModel.getAssignment(nonbasic) - << " " << bound << endl; - nb << bound; + if(upperBound){ + if(sgn < 0){ + bound = d_partialModel.getLowerConstraint(nonbasic); + }else{ + Assert(sgn > 0); + bound = d_partialModel.getUpperConstraint(nonbasic); + } }else{ - Assert(sgn > 0); - bound = d_partialModel.getLowerConstraint(nonbasic); - Debug("arith") << " above 0 " << nonbasic << " " - << d_partialModel.getAssignment(nonbasic) - << " " << bound << endl; - nb << bound; + if(sgn < 0){ + bound = d_partialModel.getUpperConstraint(nonbasic); + }else{ + Assert(sgn > 0); + bound = d_partialModel.getLowerConstraint(nonbasic); + } } + Assert(!bound.isNull()); + Debug("arith::explainNonbasics") << "\t" << nonbasic << " " << sgn << " " << bound + << endl; + output << bound; } - Node conflict = nb; - return conflict; + Debug("arith::explainNonbasics") << "SimplexDecisionProcedure::explainNonbasics(" + << basic << ") done" << endl; } -Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){ - NodeBuilder<> nb(kind::AND); - TNode bound = d_partialModel.getLowerConstraint(conflictVar); - - Debug("arith") << "generateConflictBelow " - << "conflictVar " << conflictVar - << d_partialModel.getAssignment(conflictVar) << " " - << " " << bound << endl; - nb << bound; +TNode SimplexDecisionProcedure::weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic){ + + int sgn = coeff.sgn(); + bool ub = aboveUpper?(sgn < 0) : (sgn > 0); + TNode exp = ub ? + d_partialModel.getUpperConstraint(v) : + d_partialModel.getLowerConstraint(v); + DeltaRational bound = ub? + d_partialModel.getUpperBound(v) : + d_partialModel.getLowerBound(v); + + bool weakened; + do{ + weakened = false; + + Node weaker = ub? + d_propManager.strictlyWeakerAssertedUpperBound(v, bound): + d_propManager.strictlyWeakerAssertedLowerBound(v, bound); + + if(!weaker.isNull()){ + DeltaRational weakerBound = asDeltaRational(weaker); + + DeltaRational diff = aboveUpper ? bound - weakerBound : weakerBound - bound; + //if var == basic, + // if aboveUpper, weakerBound > bound, multiply by -1 + // if !aboveUpper, weakerBound < bound, multiply by -1 + diff = diff * coeff; + if(surplus > diff){ + ++d_statistics.d_weakenings; + weakened = true; + anyWeakening = true; + surplus = surplus - diff; + + Debug("weak") << "found:" << endl; + if(v == basic){ + Debug("weak") << " basic: "; + } + Debug("weak") << " " << surplus << " "<< diff << endl + << " " << bound << exp << endl + << " " << weakerBound << weaker << endl; - Tableau::RowIterator iter = d_tableau.rowIterator(conflictVar); - for(; !iter.atEnd(); ++iter){ - const TableauEntry& entry = *iter; - ArithVar nonbasic = entry.getColVar(); - if(nonbasic == conflictVar) continue; + if(exp.getKind() == AND){ + Debug("weak") << "VICTORY" << endl; + } - const Rational& a_ij = entry.getCoefficient(); + Assert(diff > d_DELTA_ZERO); + exp = weaker; + bound = weakerBound; + } + } + }while(weakened); - int sgn = a_ij.sgn(); - Assert(a_ij != d_ZERO); - Assert(sgn != 0); + if(exp.getKind() == AND){ + Debug("weak") << "boo: " << exp << endl; + } + return exp; +} - if(sgn < 0){ - TNode bound = d_partialModel.getLowerConstraint(nonbasic); - Debug("arith") << "Lower "<< nonbasic << " " - << d_partialModel.getAssignment(nonbasic) << " " - << bound << endl; +Node SimplexDecisionProcedure::weakenConflict(bool aboveUpper, ArithVar basicVar){ + TimerStat::CodeTimer codeTimer(d_statistics.d_weakenTime); - nb << bound; - }else{ - Assert(sgn > 0); - TNode bound = d_partialModel.getUpperConstraint(nonbasic); - Debug("arith") << "Upper "<< nonbasic << " " - << d_partialModel.getAssignment(nonbasic) << " " - << bound << endl; + const DeltaRational& assignment = d_partialModel.getAssignment(basicVar); + DeltaRational surplus; + if(aboveUpper){ + Assert(d_partialModel.hasUpperBound(basicVar)); + Assert(assignment > d_partialModel.getUpperBound(basicVar)); + surplus = assignment - d_partialModel.getUpperBound(basicVar); + }else{ + Assert(d_partialModel.hasLowerBound(basicVar)); + Assert(assignment < d_partialModel.getLowerBound(basicVar)); + surplus = d_partialModel.getLowerBound(basicVar) - assignment; + } - nb << bound; - } + NodeBuilder<> conflict(kind::AND); + bool anyWeakenings = false; + for(Tableau::RowIterator i = d_tableau.rowIterator(basicVar); !i.atEnd(); ++i){ + const TableauEntry& entry = *i; + ArithVar v = entry.getColVar(); + const Rational& coeff = entry.getCoefficient(); + conflict << weakestExplanation(aboveUpper, surplus, v, coeff, anyWeakenings, basicVar); + } + ++d_statistics.d_weakeningAttempts; + if(anyWeakenings){ + ++d_statistics.d_weakeningSuccesses; } - Node conflict (nb.constructNode()); return conflict; } + +// Node SimplexDecisionProcedure::weakenLowerBoundConflict(ArithVar basicVar){ +// TimerStat::CodeTimer codeTimer(d_statistics.d_weakenTime); + +// bool anyWeakenings = false; +// const DeltaRational& assignment = d_partialModel.getAssignment(basicVar); +// Assert(d_partialModel.hasLowerBound(basicVar)); +// Assert(assignment < d_partialModel.getLowerBound(basicVar)); + +// DeltaRational surplus = d_partialModel.getLowerBound(basicVar) - assignment; + +// vector weakeningElements; +// queue potentialWeakingings; +// for(Tableau::RowIterator i = d_tableau.rowIterator(basicVar); !i.atEnd(); ++i){ +// const TableauEntry& entry = *i; +// ArithVar v = entry.getColVar(); +// const Rational& coeff = entry.getCoefficient(); + +// int sgn = coeff.sgn(); +// bool ub = (sgn > 0); +// Node exp = ub ? +// d_partialModel.getUpperConstraint(v) : +// d_partialModel.getLowerConstraint(v); +// DeltaRational bound = ub? +// d_partialModel.getUpperBound(v) : +// d_partialModel.getLowerBound(v); +// potentialWeakingings.push(weakeningElements.size()); +// weakeningElements.push_back(WeakeningElem(v, &coeff, ub, bound, exp)); +// } + +// vector conflict; + +// Debug("weak") << "weakenLowerBoundConflict" << endl; +// while(!potentialWeakingings.empty()){ +// uint32_t pos = potentialWeakingings.front(); +// potentialWeakingings.pop(); + +// WeakeningElem& curr = weakeningElements[pos]; + +// Node weaker = curr.upperBound? +// d_propManager.strictlyWeakerAssertedUpperBound(curr.var, curr.bound): +// d_propManager.strictlyWeakerAssertedLowerBound(curr.var, curr.bound); + +// bool weakened = false; +// if(!weaker.isNull()){ +// DeltaRational weakerBound = asDeltaRational(weaker); +// DeltaRational diff = weakerBound - curr.bound; +// //if var == basic, weakerBound < curr.bound +// // multiply by -1 +// diff = diff * (*curr.coeff); + +// if(surplus > diff){ +// ++d_statistics.d_weakenings; +// anyWeakenings = true; +// weakened = true; +// surplus = surplus - diff; + +// Debug("weak") << "found:" << endl; +// if(curr.var == basicVar){ +// Debug("weak") << " basic: "; +// } +// Debug("weak") << " " << surplus << " "<< diff << endl +// << " " << curr.bound << weakerBound << endl +// << " " << curr.explanation << weaker << endl; + +// if(curr.explanation.getKind() == AND){ +// Debug("weak") << "VICTORY" << endl; +// } + +// Assert(diff > d_DELTA_ZERO); +// curr.explanation = weaker; +// curr.bound = weakerBound; +// } +// } + +// if(weakened){ +// potentialWeakingings.push(pos); +// }else{ +// if(curr.explanation.getKind() == AND){ +// Debug("weak") << "boo: " << curr.explanation << endl; +// } +// conflict.push_back(curr.explanation); +// } +// } + +// ++d_statistics.d_weakeningAttempts; +// if(anyWeakenings){ +// ++d_statistics.d_weakeningSuccesses; +// } + +// NodeBuilder<> nb(AND); +// nb.append(conflict); +// return nb; +// } + +// Node SimplexDecisionProcedure::deduceUpperBound(ArithVar basicVar){ +// Assert(d_tableau.isBasic(basicVar)); +// Assert(selectSlackUpperBound(basicVar) == ARITHVAR_SENTINEL); + +// const DeltaRational& assignment = d_partialModel.getAssignment(basicVar); + +// Assert(assignment.getInfinitesimalPart() <= 0); + +// if(d_partialModel.strictlyBelowUpperBound(basicVar, assignment)){ +// NodeBuilder<> nb(kind::AND); +// explainNonbasicsUpperBound(basicVar, nb); +// Node explanation = maybeUnaryConvert(nb); +// Debug("waka-waka") << basicVar << " ub " << assignment << " "<< explanation << endl; +// Node res = AssertUpper(basicVar, assignment, explanation); +// if(res.isNull()){ +// d_propManager.propagateArithVar(true, basicVar, assignment, explanation); +// } +// return res; +// }else{ +// return Node::null(); +// } +// } + +// Node SimplexDecisionProcedure::deduceLowerBound(ArithVar basicVar){ +// Assert(d_tableau.isBasic(basicVar)); +// Assert(selectSlackLowerBound(basicVar) == ARITHVAR_SENTINEL); +// const DeltaRational& assignment = d_partialModel.getAssignment(basicVar); + +// if(Debug.isOn("paranoid:check_tableau")){ debugCheckTableau(); } + +// Assert(assignment.getInfinitesimalPart() >= 0); + +// if(d_partialModel.strictlyAboveLowerBound(basicVar, assignment)){ +// NodeBuilder<> nb(kind::AND); +// explainNonbasicsLowerBound(basicVar, nb); +// Node explanation = maybeUnaryConvert(nb); +// Debug("waka-waka") << basicVar << " lb " << assignment << " "<< explanation << endl; +// Node res = AssertLower(basicVar, assignment, explanation); +// if(res.isNull()){ +// d_propManager.propagateArithVar(false, basicVar, assignment, explanation); +// } +// return res; +// }else{ +// return Node::null(); +// } +// } + +Node SimplexDecisionProcedure::generateConflictAboveUpperBound(ArithVar conflictVar){ + return weakenConflict(true, conflictVar); +} + +Node SimplexDecisionProcedure::generateConflictBelowLowerBound(ArithVar conflictVar){ + return weakenConflict(false, conflictVar); +} + /** * Computes the value of a basic variable using the current assignment. */ @@ -717,6 +1073,26 @@ DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe return sum; } +DeltaRational SimplexDecisionProcedure::computeBound(ArithVar basic, bool upperBound){ + DeltaRational sum(0,0); + for(Tableau::RowIterator i = d_tableau.rowIterator(basic); !i.atEnd(); ++i){ + const TableauEntry& entry = (*i); + ArithVar nonbasic = entry.getColVar(); + if(nonbasic == basic) continue; + const Rational& coeff = entry.getCoefficient(); + int sgn = coeff.sgn(); + bool ub = upperBound ? (sgn > 0) : (sgn < 0); + + const DeltaRational& bound = ub ? + d_partialModel.getUpperBound(nonbasic): + d_partialModel.getLowerBound(nonbasic); + + DeltaRational diff = bound * coeff; + sum = sum + diff; + } + return sum; +} + /** * This check is quite expensive. * It should be wrapped in a Debug.isOn() guard. diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index b1ebe2972..f0dc5d62e 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -10,6 +10,7 @@ #include "theory/arith/delta_rational.h" #include "theory/arith/tableau.h" #include "theory/arith/partial_model.h" +#include "theory/arith/arith_prop_manager.h" #include "util/options.h" @@ -33,36 +34,23 @@ private: Tableau& d_tableau; ArithPriorityQueue d_queue; + ArithPropManager& d_propManager; + ArithVar d_numVariables; std::queue d_delayedLemmas; + PermissiveBackArithVarSet d_updatedBounds; + PermissiveBackArithVarSet d_candidateBasics; + Rational d_ZERO; + DeltaRational d_DELTA_ZERO; public: - SimplexDecisionProcedure(ArithPartialModel& pm, - Tableau& tableau) : - d_partialModel(pm), - d_tableau(tableau), - d_queue(pm, tableau), - d_numVariables(0), - d_delayedLemmas(), - d_ZERO(0) - { - switch(Options::ArithPivotRule rule = Options::current()->pivotRule) { - case Options::MINIMUM: - d_queue.setPivotRule(ArithPriorityQueue::MINIMUM); - break; - case Options::BREAK_TIES: - d_queue.setPivotRule(ArithPriorityQueue::BREAK_TIES); - break; - case Options::MAXIMUM: - d_queue.setPivotRule(ArithPriorityQueue::MAXIMUM); - break; - default: - Unhandled(rule); - } - } + SimplexDecisionProcedure(ArithPropManager& propManager, + ArithPartialModel& pm, + Tableau& tableau); + /** * Assert*(n, orig) takes an bound n that is implied by orig. @@ -165,32 +153,49 @@ private: * This returns ARITHVAR_SENTINEL if none exists. * * More formally one of the following conditions must be satisfied: - * - above && a_ij < 0 && assignment(x_j) < upperbound(x_j) - * - above && a_ij > 0 && assignment(x_j) > lowerbound(x_j) - * - !above && a_ij > 0 && assignment(x_j) < upperbound(x_j) - * - !above && a_ij < 0 && assignment(x_j) > lowerbound(x_j) + * - lowerBound && a_ij < 0 && assignment(x_j) < upperbound(x_j) + * - lowerBound && a_ij > 0 && assignment(x_j) > lowerbound(x_j) + * - !lowerBound && a_ij > 0 && assignment(x_j) < upperbound(x_j) + * - !lowerBound && a_ij < 0 && assignment(x_j) > lowerbound(x_j) * */ - template ArithVar selectSlack(ArithVar x_i); - template ArithVar selectSlackBelow(ArithVar x_i) { - return selectSlack(x_i); - } - template ArithVar selectSlackAbove(ArithVar x_i) { + template ArithVar selectSlack(ArithVar x_i); + template ArithVar selectSlackLowerBound(ArithVar x_i) { return selectSlack(x_i); } + template ArithVar selectSlackUpperBound(ArithVar x_i) { + return selectSlack(x_i); + } /** * Returns the smallest basic variable whose assignment is not consistent * with its upper and lower bounds. */ ArithVar selectSmallestInconsistentVar(); + + /** + * Exports either the explanation of an upperbound or a lower bound + * of the basic variable basic, using the non-basic variables in the row. + */ + template + void explainNonbasics(ArithVar basic, NodeBuilder<>& output); + void explainNonbasicsLowerBound(ArithVar basic, NodeBuilder<>& output){ + explainNonbasics(basic, output); + } + void explainNonbasicsUpperBound(ArithVar basic, NodeBuilder<>& output){ + explainNonbasics(basic, output); + } + + Node deduceUpperBound(ArithVar basicVar); + Node deduceLowerBound(ArithVar basicVar); + /** * Given a non-basic variable that is know to not be updatable * to a consistent value, construct and return a conflict. * Follows section 4.2 in the CAV06 paper. */ - Node generateConflictAbove(ArithVar conflictVar); - Node generateConflictBelow(ArithVar conflictVar); + Node generateConflictAboveUpperBound(ArithVar conflictVar); + Node generateConflictBelowLowerBound(ArithVar conflictVar); public: /** @@ -210,6 +215,11 @@ public: */ DeltaRational computeRowValue(ArithVar x, bool useSafe); + bool hasAnyUpdates() { return !d_updatedBounds.empty(); } + void clearUpdates(){ + d_updatedBounds.purge(); + } + void propagateCandidates(); void increaseMax() {d_numVariables++;} @@ -234,7 +244,7 @@ private: /** Adds a conflict as a lemma to the queue. */ void delayConflictAsLemma(Node conflict){ - Node negatedConflict = negateConjunctionAsClause(conflict); + Node negatedConflict = negateConjunctionAsClause(conflict); pushLemma(negatedConflict); } @@ -254,6 +264,36 @@ private: */ Node checkBasicForConflict(ArithVar b); + Node weakenConflict(bool aboveUpper, ArithVar basicVar); + TNode weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic); + + void propagateCandidate(ArithVar basic); + bool propagateCandidateBound(ArithVar basic, bool upperBound); + + inline bool propagateCandidateLowerBound(ArithVar basic){ + return propagateCandidateBound(basic, false); + } + inline bool propagateCandidateUpperBound(ArithVar basic){ + return propagateCandidateBound(basic, true); + } + + bool hasBounds(ArithVar basic, bool upperBound); + bool hasLowerBounds(ArithVar basic){ + return hasBounds(basic, false); + } + bool hasUpperBounds(ArithVar basic){ + return hasBounds(basic, true); + } + DeltaRational computeBound(ArithVar basic, bool upperBound); + + inline DeltaRational computeLowerBound(ArithVar basic){ + return computeBound(basic, false); + } + inline DeltaRational computeUpperBound(ArithVar basic){ + return computeBound(basic, true); + } + + /** These fields are designed to be accessable to TheoryArith methods. */ class Statistics { public: @@ -270,6 +310,12 @@ private: IntStat d_attemptDuringVarOrderSearch, d_successDuringVarOrderSearch; IntStat d_attemptAfterVarOrderSearch, d_successAfterVarOrderSearch; + IntStat d_weakeningAttempts, d_weakeningSuccesses, d_weakenings; + TimerStat d_weakenTime; + + TimerStat d_boundComputationTime; + IntStat d_boundComputations, d_boundPropagations; + IntStat d_delayedConflicts; TimerStat d_pivotTime; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index c22b0019d..3c275fae0 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -26,6 +26,8 @@ #include "util/rational.h" #include "util/integer.h" +#include "util/boolean_simplification.h" + #include "theory/rewriter.h" @@ -40,6 +42,7 @@ #include "theory/arith/theory_arith.h" #include "theory/arith/normal_form.h" +#include "theory/arith/arith_prop_manager.h" #include @@ -54,7 +57,7 @@ using namespace CVC4::theory::arith; static const uint32_t RESET_START = 2; struct SlackAttrID; -typedef expr::Attribute Slack; +typedef expr::Attribute Slack; TheoryArith::TheoryArith(context::Context* c, OutputChannel& out, Valuation valuation) : Theory(THEORY_ARITH, c, out, valuation), @@ -67,7 +70,8 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out, Valuation valu d_tableauResetDensity(1.6), d_tableauResetPeriod(10), d_propagator(c, out), - d_simplex(d_partialModel, d_tableau), + d_propManager(c, d_arithvarNodeMap, d_propagator, valuation), + d_simplex(d_propManager, d_partialModel, d_tableau), d_DELTA_ZERO(0), d_statistics() {} @@ -171,6 +175,7 @@ void TheoryArith::preRegisterTerm(TNode n) { if(isRelationOperator(k)){ Assert(Comparison::isNormalAtom(n)); + //cout << n << endl; d_propagator.addAtom(n); @@ -179,7 +184,7 @@ void TheoryArith::preRegisterTerm(TNode n) { if(left.getKind() == PLUS){ //We may need to introduce a slack variable. Assert(left.getNumChildren() >= 2); - if(!left.hasAttribute(Slack())){ + if(!left.getAttribute(Slack())){ setupSlack(left); } } @@ -189,15 +194,15 @@ void TheoryArith::preRegisterTerm(TNode n) { ArithVar TheoryArith::requestArithVar(TNode x, bool basic){ - Assert(isLeaf(x)); - Assert(!hasArithVar(x)); + Assert(isLeaf(x) || x.getKind() == PLUS); + Assert(!d_arithvarNodeMap.hasArithVar(x)); ArithVar varX = d_variables.size(); d_variables.push_back(Node(x)); d_simplex.increaseMax(); - setArithVar(x,varX); + d_arithvarNodeMap.setArithVar(x,varX); d_userVariables.init(varX, !basic); d_tableau.increaseSize(); @@ -218,9 +223,9 @@ void TheoryArith::asVectors(Polynomial& p, std::vector& coeffs, std::v Debug("rewriter") << "should be var: " << n << endl; Assert(isLeaf(n)); - Assert(hasArithVar(n)); + Assert(d_arithvarNodeMap.hasArithVar(n)); - ArithVar av = asArithVar(n); + ArithVar av = d_arithvarNodeMap.asArithVar(n); coeffs.push_back(constant.getValue()); variables.push_back(av); @@ -228,13 +233,12 @@ void TheoryArith::asVectors(Polynomial& p, std::vector& coeffs, std::v } void TheoryArith::setupSlack(TNode left){ + Assert(!left.getAttribute(Slack())); ++(d_statistics.d_statSlackVariables); - TypeNode real_type = NodeManager::currentNM()->realType(); - Node slack = NodeManager::currentNM()->mkVar(real_type); - left.setAttribute(Slack(), slack); + left.setAttribute(Slack(), true); - ArithVar varSlack = requestArithVar(slack, true); + ArithVar varSlack = requestArithVar(left, true); Polynomial polyLeft = Polynomial::parsePolynomial(left); @@ -273,44 +277,18 @@ void TheoryArith::registerTerm(TNode tn){ Debug("arith") << "registerTerm(" << tn << ")" << endl; } -template -TNode getSide(TNode assertion, Kind simpleKind){ - switch(simpleKind){ - case LT: - case GT: - case DISTINCT: - return selectLeft ? (assertion[0])[0] : (assertion[0])[1]; - case LEQ: - case GEQ: - case EQUAL: - return selectLeft ? assertion[0] : assertion[1]; - default: - Unreachable(); - return TNode::null(); - } -} ArithVar TheoryArith::determineLeftVariable(TNode assertion, Kind simpleKind){ TNode left = getSide(assertion, simpleKind); if(isLeaf(left)){ - return asArithVar(left); + return d_arithvarNodeMap.asArithVar(left); }else{ Assert(left.hasAttribute(Slack())); - TNode slack = left.getAttribute(Slack()); - return asArithVar(slack); + return d_arithvarNodeMap.asArithVar(left); } } -DeltaRational determineRightConstant(TNode assertion, Kind simpleKind){ - TNode right = getSide(assertion, simpleKind); - - Assert(right.getKind() == CONST_RATIONAL); - const Rational& noninf = right.getConst(); - - Rational inf = Rational(Integer(deltaCoeff(simpleKind))); - return DeltaRational(noninf, inf); -} Node TheoryArith::disequalityConflict(TNode eq, TNode lb, TNode ub){ NodeBuilder<3> conflict(kind::AND); @@ -390,19 +368,28 @@ void TheoryArith::check(Effort effortLevel){ if(!possibleConflict.isNull()){ d_partialModel.revertAssignmentChanges(); + //Node simpleConflict = BooleanSimplification::simplifyConflict(possibleConflict); + + Debug("arith::conflict") << "conflict " << possibleConflict << endl; + + d_simplex.clearUpdates(); d_out->conflict(possibleConflict); return; } } - if(Debug.isOn("arith::print_assertions") && fullEffort(effortLevel)) { + if(Debug.isOn("arith::print_assertions")) { debugPrintAssertions(); } Node possibleConflict = d_simplex.updateInconsistentVars(); if(possibleConflict != Node::null()){ - d_partialModel.revertAssignmentChanges(); + d_simplex.clearUpdates(); + + //Node simpleConflict = BooleanSimplification::simplifyConflict(possibleConflict); + + Debug("arith::conflict") << "conflict " << possibleConflict << endl; d_out->conflict(possibleConflict); }else{ @@ -489,14 +476,137 @@ void TheoryArith::debugPrintModel(){ } } +/* +bool TheoryArith::isImpliedUpperBound(ArithVar var, Node exp){ + Node varAsNode = asNode(var); + const DeltaRational& ub = d_partialModel.getUpperBound(var); + Assert(ub.getInfinitesimalPart() <= 0 ); + Kind kind = ub.getInfinitesimalPart() < 0 ? LT : LEQ; + Node ubAsNode = NodeBuilder<2>(kind) << varAsNode << mkRationalNode(ub.getNoninfinitesimalPart()); + Node bestImplied = d_propagator.getBestImpliedUpperBound(ubAsNode); + + return bestImplied == exp; +} + +bool TheoryArith::isImpliedLowerBound(ArithVar var, Node exp){ + Node varAsNode = asNode(var); + const DeltaRational& lb = d_partialModel.getLowerBound(var); + Assert(lb.getInfinitesimalPart() >= 0 ); + Kind kind = lb.getInfinitesimalPart() > 0 ? GT : GEQ; + Node lbAsIneq = NodeBuilder<2>(kind) << varAsNode << mkRationalNode(lb.getNoninfinitesimalPart()); + Node bestImplied = d_propagator.getBestImpliedLowerBound(lbAsIneq); + return bestImplied == exp; +} +*/ + void TheoryArith::explain(TNode n) { + Debug("explain") << "explain @" << getContext()->getLevel() << ": " << n << endl; + //Assert(n.hasAttribute(Propagated())); + + //NodeBuilder<> explainBuilder(AND); + //internalExplain(n,explainBuilder); + Assert(d_propManager.isPropagated(n)); + Node explanation = d_propManager.explain(n); + //Node flatExplanation = BooleanSimplification::simplifyConflict(explanation); + + d_out->explanation(explanation, true); +} +/* +void TheoryArith::internalExplain(TNode n, NodeBuilder<>& explainBuilder){ + Assert(n.hasAttribute(Propagated())); + Node bound = n.getAttribute(Propagated()); + + AlwaysAssert(bound.getKind() == kind::AND); + + for(Node::iterator i = bound.begin(), end = bound.end(); i != end; ++i){ + Node lit = *i; + if(lit.hasAttribute(Propagated())){ + cout << "hoop the sadjklasdj" << endl; + internalExplain(lit, explainBuilder); + }else{ + explainBuilder << lit; + } + } +} +*/ +/* +static const bool EXPORT_LEMMA_INSTEAD_OF_PROPAGATE = false; +void TheoryArith::propagateArithVar(bool upperbound, ArithVar var ){ + Node varAsNode = asNode(var); + const DeltaRational& b = upperbound ? + d_partialModel.getUpperBound(var) : d_partialModel.getLowerBound(var); + + Assert((!upperbound) || (b.getInfinitesimalPart() <= 0) ); + Assert(upperbound || (b.getInfinitesimalPart() >= 0) ); + Kind kind; + if(upperbound){ + kind = b.getInfinitesimalPart() < 0 ? LT : LEQ; + } else{ + kind = b.getInfinitesimalPart() > 0 ? GT : GEQ; + } + + Node bAsNode = NodeBuilder<2>(kind) << varAsNode + << mkRationalNode(b.getNoninfinitesimalPart()); + + Node bestImplied = upperbound ? + d_propagator.getBestImpliedUpperBound(bAsNode): + d_propagator.getBestImpliedLowerBound(bAsNode); + + if(!bestImplied.isNull()){ + Node satValue = d_valuation.getSatValue(bestImplied); + if(satValue.isNull()){ + + Node reason = upperbound ? + d_partialModel.getUpperConstraint(var) : + d_partialModel.getLowerConstraint(var); + + //cout << getContext()->getLevel() << " " << bestImplied << " " << reason << endl; + if(EXPORT_LEMMA_INSTEAD_OF_PROPAGATE){ + Node lemma = NodeBuilder<2>(IMPLIES) << reason + << bestImplied; + + //Temporary + Node clause = BooleanSimplification::simplifyHornClause(lemma); + d_out->lemma(clause); + }else{ + Assert(!bestImplied.hasAttribute(Propagated())); + bestImplied.setAttribute(Propagated(), reason); + d_reasons.push_back(reason); + d_out->propagate(bestImplied); + } + }else{ + Assert(!satValue.isNull()); + Assert(satValue.getKind() == CONST_BOOLEAN); + Assert(satValue.getConst()); + } + } } +*/ void TheoryArith::propagate(Effort e) { if(quickCheckOrMore(e)){ - while(d_simplex.hasMoreLemmas()){ - Node lemma = d_simplex.popLemma(); - d_out->lemma(lemma); + bool propagated = false; + if(Options::current()->arithPropagation && d_simplex.hasAnyUpdates()){ + d_simplex.propagateCandidates(); + }else{ + d_simplex.clearUpdates(); + } + + while(d_propManager.hasMorePropagations()){ + TNode toProp = d_propManager.getPropagation(); + Node satValue = d_valuation.getSatValue(toProp); + AlwaysAssert(satValue.isNull()); + TNode exp = d_propManager.explain(toProp); + propagated = true; + d_out->propagate(toProp); + } + + if(!propagated){ + //Opportunistically export previous conflicts + while(d_simplex.hasMoreLemmas()){ + Node lemma = d_simplex.popLemma(); + d_out->lemma(lemma); + } } } } @@ -506,7 +616,7 @@ Node TheoryArith::getValue(TNode n) { switch(n.getKind()) { case kind::VARIABLE: { - ArithVar var = asArithVar(n); + ArithVar var = d_arithvarNodeMap.asArithVar(n); if(d_removedRows.find(var) != d_removedRows.end()){ Node eq = d_removedRows.find(var)->second; @@ -634,7 +744,7 @@ void TheoryArith::notifyRestart(){ bool TheoryArith::entireStateIsConsistent(){ typedef std::vector::const_iterator VarIter; for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){ - ArithVar var = asArithVar(*i); + ArithVar var = d_arithvarNodeMap.asArithVar(*i); if(!d_partialModel.assignmentIsConsistent(var)){ d_partialModel.printModel(var); cerr << "Assignment is not consistent for " << var << *i << endl; @@ -669,7 +779,7 @@ void TheoryArith::permanentlyRemoveVariable(ArithVar v){ Assert(!noRow); //remove the row from the tableau - Node eq = d_tableau.rowAsEquality(v, d_arithVarToNodeMap); + Node eq = d_tableau.rowAsEquality(v, d_arithvarNodeMap.getArithVarToNodeMap()); d_tableau.removeRow(v); if(Debug.isOn("tableau")) d_tableau.printTableau(); @@ -681,8 +791,8 @@ void TheoryArith::permanentlyRemoveVariable(ArithVar v){ d_removedRows[v] = eq; } - Debug("arith::permanentlyRemoveVariable") << "Permanently removed variable " - << v << ":" << asNode(v) << endl; + Debug("arith::permanentlyRemoveVariable") << "Permanently removed variable " << v + << ":" << d_arithvarNodeMap.asNode(v) <::const_iterator VarIter; for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){ Node variableNode = *i; - ArithVar var = asArithVar(variableNode); + ArithVar var = d_arithvarNodeMap.asArithVar(variableNode); if(d_userVariables.isMember(var) && !d_propagator.hasAnyAtoms(variableNode)){ //The user variable is unconstrained. //Remove this variable permanently diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 85f554849..9580a6c71 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -36,6 +36,8 @@ #include "theory/arith/unate_propagator.h" #include "theory/arith/simplex.h" #include "theory/arith/arith_static_learner.h" +#include "theory/arith/arith_prop_manager.h" +#include "theory/arith/arithvar_node_map.h" #include "util/stats.h" @@ -64,6 +66,8 @@ private: */ std::vector d_variables; + ArithVarNodeMap d_arithvarNodeMap; + /** * If ArithVar v maps to the node n in d_removednode, * then n = (= asNode(v) rhs) where rhs is a term that @@ -82,32 +86,7 @@ private: */ ArithVarSet d_userVariables; - /** - * Bidirectional map between Nodes and ArithVars. - */ - NodeToArithVarMap d_nodeToArithVarMap; - ArithVarToNodeMap d_arithVarToNodeMap; - - inline bool hasArithVar(TNode x) const { - return d_nodeToArithVarMap.find(x) != d_nodeToArithVarMap.end(); - } - - inline ArithVar asArithVar(TNode x) const{ - Assert(hasArithVar(x)); - Assert((d_nodeToArithVarMap.find(x))->second <= ARITHVAR_SENTINEL); - return (d_nodeToArithVarMap.find(x))->second; - } - inline Node asNode(ArithVar a) const{ - Assert(d_arithVarToNodeMap.find(a) != d_arithVarToNodeMap.end()); - return (d_arithVarToNodeMap.find(a))->second; - } - - inline void setArithVar(TNode x, ArithVar a){ - Assert(!hasArithVar(x)); - Assert(d_arithVarToNodeMap.find(a) == d_arithVarToNodeMap.end()); - d_arithVarToNodeMap[a] = x; - d_nodeToArithVarMap[x] = a; - } + /** * List of all of the inequalities asserted in the current context. @@ -141,6 +120,9 @@ private: Tableau d_smallTableauCopy; ArithUnatePropagator d_propagator; + + ArithPropManager d_propManager; + SimplexDecisionProcedure d_simplex; public: @@ -175,6 +157,9 @@ private: /** The constant zero. */ DeltaRational d_DELTA_ZERO; + /** propagates an arithvar */ + void propagateArithVar(bool upperbound, ArithVar var ); + /** * Using the simpleKind return the ArithVar associated with the * left hand side of assertion. @@ -228,6 +213,11 @@ private: */ void permanentlyRemoveVariable(ArithVar v); + bool isImpliedUpperBound(ArithVar var, Node exp); + bool isImpliedLowerBound(ArithVar var, Node exp); + + void internalExplain(TNode n, NodeBuilder<>& explainBuilder); + void asVectors(Polynomial& p, std::vector& coeffs, diff --git a/src/theory/arith/unate_propagator.cpp b/src/theory/arith/unate_propagator.cpp index 069f4f0f3..2785f0773 100644 --- a/src/theory/arith/unate_propagator.cpp +++ b/src/theory/arith/unate_propagator.cpp @@ -31,36 +31,47 @@ using namespace CVC4::kind; using namespace std; ArithUnatePropagator::ArithUnatePropagator(context::Context* cxt, OutputChannel& out) : - d_arithOut(out), d_orderedListMap() + d_arithOut(out), d_setsMap() { } -bool ArithUnatePropagator::leftIsSetup(TNode left){ - return d_orderedListMap.find(left) != d_orderedListMap.end(); +bool ArithUnatePropagator::leftIsSetup(TNode left) const{ + return d_setsMap.find(left) != d_setsMap.end(); } -ArithUnatePropagator::OrderedSetTriple& ArithUnatePropagator::getOrderedSetTriple(TNode left){ +const ArithUnatePropagator::VariablesSets& ArithUnatePropagator::getVariablesSets(TNode left) const{ Assert(leftIsSetup(left)); - return d_orderedListMap[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; } -OrderedSet& ArithUnatePropagator::getEqSet(TNode left){ +const EqualValueSet& ArithUnatePropagator::getEqualValueSet(TNode left) const{ Assert(leftIsSetup(left)); - return getOrderedSetTriple(left).d_eqSet; + return getVariablesSets(left).d_eqValueSet; } -OrderedSet& ArithUnatePropagator::getLeqSet(TNode left){ + +BoundValueSet& ArithUnatePropagator::getBoundValueSet(TNode left){ Assert(leftIsSetup(left)); - return getOrderedSetTriple(left).d_leqSet; + return getVariablesSets(left).d_boundValueSet; } -OrderedSet& ArithUnatePropagator::getGeqSet(TNode left){ + +const BoundValueSet& ArithUnatePropagator::getBoundValueSet(TNode left) const{ Assert(leftIsSetup(left)); - return getOrderedSetTriple(left).d_geqSet; + return getVariablesSets(left).d_boundValueSet; } -bool ArithUnatePropagator::hasAnyAtoms(TNode v){ +bool ArithUnatePropagator::hasAnyAtoms(TNode v) const{ Assert(!leftIsSetup(v) - || !(getEqSet(v)).empty() - || !(getLeqSet(v)).empty() - || !(getGeqSet(v)).empty()); + || !(getEqualValueSet(v)).empty() + || !(getBoundValueSet(v)).empty()); return leftIsSetup(v); } @@ -68,7 +79,58 @@ bool ArithUnatePropagator::hasAnyAtoms(TNode v){ void ArithUnatePropagator::setupLefthand(TNode left){ Assert(!leftIsSetup(left)); - d_orderedListMap[left] = OrderedSetTriple(); + 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){ @@ -79,39 +141,47 @@ void ArithUnatePropagator::addAtom(TNode atom){ setupLefthand(left); } - OrderedSet& eqSet = getEqSet(left); - OrderedSet& leqSet = getLeqSet(left); - OrderedSet& geqSet = getGeqSet(left); + const Rational& value = rightHandRational(atom); switch(atom.getKind()){ case EQUAL: { - pair res = eqSet.insert(atom); + Assert(!containsEquality(atom)); + addImplicationsUsingEqualityAndEqualityValues(atom); + addImplicationsUsingEqualityAndBoundValues(atom); + + pair res = getEqualValueSet(left).insert(atom); Assert(res.second); - addImplicationsUsingEqualityAndEqualityList(atom, eqSet); - addImplicationsUsingEqualityAndLeqList(atom, leqSet); - addImplicationsUsingEqualityAndGeqList(atom, geqSet); break; } case LEQ: { - pair res = leqSet.insert(atom); - Assert(res.second); - - addImplicationsUsingLeqAndEqualityList(atom, eqSet); - addImplicationsUsingLeqAndLeqList(atom, leqSet); - addImplicationsUsingLeqAndGeqList(atom, geqSet); + 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: { - pair res = geqSet.insert(atom); - Assert(res.second); - - addImplicationsUsingGeqAndEqualityList(atom, eqSet); - addImplicationsUsingGeqAndLeqList(atom, leqSet); - addImplicationsUsingGeqAndGeqList(atom, geqSet); - + 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: @@ -119,6 +189,13 @@ void ArithUnatePropagator::addAtom(TNode atom){ } } +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]; @@ -135,162 +212,146 @@ bool rightHandRationalIsLT(TNode a, TNode b){ return RightHandRationalLT()(a,b); } -//void addImplicationsUsingEqualityAndEqualityList(TNode eq, OrderedSet* eqSet); - -void ArithUnatePropagator::addImplicationsUsingEqualityAndEqualityList(TNode atom, OrderedSet& eqSet){ +void ArithUnatePropagator::addImplicationsUsingEqualityAndEqualityValues(TNode atom){ Assert(atom.getKind() == EQUAL); - OrderedSet::iterator eqPos = eqSet.find(atom); - Assert(eqPos != eqSet.end()); - Assert(*eqPos == atom); + TNode left = atom[0]; + EqualValueSet& eqSet = getEqualValueSet(left); Node negation = NodeManager::currentNM()->mkNode(NOT, atom); - for(OrderedSet::iterator eqIter = eqSet.begin(); - eqIter != eqSet.end(); ++eqIter){ - if(eqIter == eqPos) continue; + + for(EqualValueSet::iterator eqIter = eqSet.begin(), endIter = eqSet.end(); + eqIter != endIter; ++eqIter){ TNode eq = *eqIter; - Assert(!rightHandRationalIsEqual(eq, atom)); + Assert(eq != atom); addImplication(eq, negation); } } -void ArithUnatePropagator::addImplicationsUsingEqualityAndLeqList(TNode atom, OrderedSet& leqSet){ - - Assert(atom.getKind() == EQUAL); - Node negation = NodeManager::currentNM()->mkNode(NOT, atom); +// 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(); + } - OrderedSet::iterator leqIter = leqSet.lower_bound(atom); - if(leqIter != leqSet.end()){ - TNode lowerBound = *leqIter; - if(rightHandRationalIsEqual(atom, lowerBound)){ - addImplication(atom, lowerBound); // x=b /\ b = b' => x <= b' - if(leqIter != leqSet.begin()){ - --leqIter; - Assert(rightHandRationalIsLT(*leqIter, atom)); - addImplication(*leqIter, negation); // x=b /\ b > b' => x > b' - } - }else{ - //probably wrong - Assert(rightHandRationalIsLT(atom, lowerBound)); - addImplication(atom, lowerBound);// x=b /\ b < b' => x <= b' - - if(leqIter != leqSet.begin()){ - --leqIter; - Assert(rightHandRationalIsLT(*leqIter, atom)); - addImplication(*leqIter, negation);// x=b /\ b > b' => x > b' - } + 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(); } - }else if(leqIter != leqSet.begin()){ - --leqIter; - TNode strictlyLessThan = *leqIter; - Assert(rightHandRationalIsLT(strictlyLessThan, atom)); - addImplication(*leqIter, negation); // x=b /\ b < b' => x <= b' + } + ++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(leqSet.empty()); + Assert(entry.hasLeq()); + return entry.getLeq(); } } -void ArithUnatePropagator::addImplicationsUsingEqualityAndGeqList(TNode atom, OrderedSet& geqSet){ - Assert(atom.getKind() == EQUAL); - Node negation = NodeManager::currentNM()->mkNode(NOT, atom); - OrderedSet::iterator geqIter = geqSet.lower_bound(atom); - if(geqIter != geqSet.end()){ - TNode lowerBound = *geqIter; - if(rightHandRationalIsEqual(atom, lowerBound)){ - addImplication(atom, lowerBound); // x=b /\ b = b' => x >= b' - ++geqIter; - if(geqIter != geqSet.end()){ // x=b /\ b < b' => x < b' - TNode strictlyGt = *geqIter; - Assert(rightHandRationalIsLT( atom, strictlyGt )); - addImplication(strictlyGt, negation); - } - }else{ - Assert(rightHandRationalIsLT(atom, lowerBound)); - addImplication(lowerBound, negation);// x=b /\ b < b' => x < b' - if(geqIter != geqSet.begin()){ - --geqIter; - TNode strictlyLessThan = *geqIter; - Assert(rightHandRationalIsLT(strictlyLessThan, atom)); - addImplication(atom, strictlyLessThan);// x=b /\ b > b' => x >= b' - } + +// 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(); } - }else if(geqIter != geqSet.begin()){ - --geqIter; - TNode strictlyLT = *geqIter; - Assert(rightHandRationalIsLT(strictlyLT, atom)); - addImplication(atom, strictlyLT);// x=b /\ b > b' => x >= b' + } + if(bv == bvSet.begin()){ + return Node::null(); }else{ - Assert(geqSet.empty()); + --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::addImplicationsUsingLeqAndLeqList(TNode atom, OrderedSet& leqSet) -{ - Assert(atom.getKind() == LEQ); - Node negation = NodeManager::currentNM()->mkNode(NOT, atom); +void ArithUnatePropagator::addImplicationsUsingEqualityAndBoundValues(TNode atom){ + Assert(atom.getKind() == EQUAL); + Node left = atom[0]; - OrderedSet::iterator atomPos = leqSet.find(atom); - Assert(atomPos != leqSet.end()); - Assert(*atomPos == atom); + const Rational& value = rightHandRational(atom); - if(atomPos != leqSet.begin()){ - --atomPos; - TNode beforeLeq = *atomPos; - Assert(rightHandRationalIsLT(beforeLeq, atom)); - addImplication(beforeLeq, atom);// x<=b' /\ b' < b => x <= b - ++atomPos; + BoundValueSet& bvSet = getBoundValueSet(left); + Node ub = getUpperBound(bvSet, value, false, false); + Node lb = getLowerBound(bvSet, value, false, false); + + if(!ub.isNull()){ + addImplication(atom, ub); } - ++atomPos; - if(atomPos != leqSet.end()){ - TNode afterLeq = *atomPos; - Assert(rightHandRationalIsLT(atom, afterLeq)); - addImplication(atom, afterLeq);// x<=b /\ b < b' => x <= b' + + if(!lb.isNull()){ + addImplication(atom, lb); } } -void ArithUnatePropagator::addImplicationsUsingLeqAndGeqList(TNode atom, OrderedSet& geqSet) { +void ArithUnatePropagator::addImplicationsUsingLeqAndBoundValues(TNode atom) +{ Assert(atom.getKind() == LEQ); Node negation = NodeManager::currentNM()->mkNode(NOT, atom); - OrderedSet::iterator geqIter = geqSet.lower_bound(atom); - if(geqIter != geqSet.end()){ - TNode lowerBound = *geqIter; - if(rightHandRationalIsEqual(atom, lowerBound)){ - Assert(rightHandRationalIsEqual(atom, lowerBound)); - addImplication(negation, lowerBound);// (x > b) => (x >= b) - ++geqIter; - if(geqIter != geqSet.end()){ - TNode next = *geqIter; - Assert(rightHandRationalIsLT(atom, next)); - addImplication(next, negation);// x>=b' /\ b' > b => x > b - } - }else{ - Assert(rightHandRationalIsLT(atom, lowerBound)); - addImplication(lowerBound, negation);// x>=b' /\ b' > b => x > b - if(geqIter != geqSet.begin()){ - --geqIter; - TNode prev = *geqIter; - Assert(rightHandRationalIsLT(prev, atom)); - addImplication(negation, prev);// (x>b /\ b > b') => x >= b' - } - } - }else if(geqIter != geqSet.begin()){ - --geqIter; - TNode strictlyLT = *geqIter; - Assert(rightHandRationalIsLT(strictlyLT, atom)); - addImplication(negation, strictlyLT);// (x>b /\ b > b') => x >= b' - }else{ - Assert(geqSet.empty()); + Node ub = getImpliedUpperBoundUsingLeq(atom, false); + Node lb = getImpliedLowerBoundUsingGT(negation, false); + + if(!ub.isNull()){ + addImplication(atom, ub); + } + + if(!lb.isNull()){ + addImplication(negation, lb); } } -void ArithUnatePropagator::addImplicationsUsingLeqAndEqualityList(TNode atom, OrderedSet& eqSet) { +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(OrderedSet::iterator eqIter = eqSet.begin(); eqIter != eqSet.end(); ++eqIter){ + for(EqualValueSet::iterator eqIter = eqSet.begin(); eqIter != eqSet.end(); ++eqIter){ TNode eq = *eqIter; if(rightHandRationalIsEqual(atom, eq)){ // (x = b' /\ b = b') => x <= b @@ -306,73 +367,30 @@ void ArithUnatePropagator::addImplicationsUsingLeqAndEqualityList(TNode atom, Or } -void ArithUnatePropagator::addImplicationsUsingGeqAndGeqList(TNode atom, OrderedSet& geqSet){ +void ArithUnatePropagator::addImplicationsUsingGeqAndBoundValues(TNode atom){ Assert(atom.getKind() == GEQ); Node negation = NodeManager::currentNM()->mkNode(NOT, atom); - OrderedSet::iterator atomPos = geqSet.find(atom); - Assert(atomPos != geqSet.end()); - Assert(*atomPos == atom); + Node lb = getImpliedLowerBoundUsingGeq(atom, false); //What is implied by (>= left value) + Node ub = getImpliedUpperBoundUsingLT(negation, false); - if(atomPos != geqSet.begin()){ - --atomPos; - TNode beforeGeq = *atomPos; - Assert(rightHandRationalIsLT(beforeGeq, atom)); - addImplication(atom, beforeGeq);// x>=b /\ b > b' => x >= b' - ++atomPos; - } - ++atomPos; - if(atomPos != geqSet.end()){ - TNode afterGeq = *atomPos; - Assert(rightHandRationalIsLT(atom, afterGeq)); - addImplication(afterGeq, atom);// x>=b' /\ b' > b => x >= b + if(!lb.isNull()){ + addImplication(atom, lb); } -} - -void ArithUnatePropagator::addImplicationsUsingGeqAndLeqList(TNode atom, OrderedSet& leqSet){ - Assert(atom.getKind() == GEQ); - Node negation = NodeManager::currentNM()->mkNode(NOT, atom); - - OrderedSet::iterator leqIter = leqSet.lower_bound(atom); - if(leqIter != leqSet.end()){ - TNode lowerBound = *leqIter; - if(rightHandRationalIsEqual(atom, lowerBound)){ - Assert(rightHandRationalIsEqual(atom, lowerBound)); - addImplication(negation, lowerBound);// (x < b) => (x <= b) - - if(leqIter != leqSet.begin()){ - --leqIter; - TNode prev = *leqIter; - Assert(rightHandRationalIsLT(prev, atom)); - addImplication(prev, negation);// x<=b' /\ b' < b => x < b - } - }else{ - Assert(rightHandRationalIsLT(atom, lowerBound)); - addImplication(negation, lowerBound);// (x < b /\ b < b') => x <= b' - ++leqIter; - if(leqIter != leqSet.end()){ - TNode next = *leqIter; - Assert(rightHandRationalIsLT(atom, next)); - addImplication(negation, next);// (x < b /\ b < b') => x <= b' - } - } - }else if(leqIter != leqSet.begin()){ - --leqIter; - TNode strictlyLT = *leqIter; - Assert(rightHandRationalIsLT(strictlyLT, atom)); - addImplication(strictlyLT, negation);// (x <= b' /\ b' < b) => x < b - }else{ - Assert(leqSet.empty()); + if(!ub.isNull()){ + addImplication(negation, ub); } } -void ArithUnatePropagator::addImplicationsUsingGeqAndEqualityList(TNode atom, OrderedSet& eqSet){ +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(OrderedSet::iterator eqIter = eqSet.begin(); eqIter != eqSet.end(); ++eqIter){ + for(EqualValueSet::iterator eqIter = eqSet.begin(); eqIter != eqSet.end(); ++eqIter){ TNode eq = *eqIter; if(rightHandRationalIsEqual(atom, eq)){ // (x = b' /\ b = b') => x >= b @@ -390,8 +408,132 @@ void ArithUnatePropagator::addImplicationsUsingGeqAndEqualityList(TNode atom, Or void ArithUnatePropagator::addImplication(TNode a, TNode b){ Node imp = NodeBuilder<2>(IMPLIES) << a << b; - Debug("arith-propagate") << "ArithUnatePropagator::addImplication"; - Debug("arith-propagate") << "(" << a << ", " << b <<")" << endl; + 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)<(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)<(NOT) << leq; + result = getImpliedLowerBoundUsingGT(gt, true); + }else{ + Unreachable(); + } + Assert(result != lowerBound); + + Debug("arith::unate") << lowerBound <<" -> " << result << std::endl; + return result; +} diff --git a/src/theory/arith/unate_propagator.h b/src/theory/arith/unate_propagator.h index 383b9f8e8..8c2720aea 100644 --- a/src/theory/arith/unate_propagator.h +++ b/src/theory/arith/unate_propagator.h @@ -68,15 +68,14 @@ private: */ OutputChannel& d_arithOut; - struct OrderedSetTriple { - OrderedSet d_leqSet; - OrderedSet d_eqSet; - OrderedSet d_geqSet; + struct VariablesSets { + BoundValueSet d_boundValueSet; + EqualValueSet d_eqValueSet; }; /** TODO: justify making this a TNode. */ - typedef __gnu_cxx::hash_map NodeToOrderedSetMap; - NodeToOrderedSetMap d_orderedListMap; + typedef __gnu_cxx::hash_map NodeToSetsMap; + NodeToSetsMap d_setsMap; public: ArithUnatePropagator(context::Context* cxt, OutputChannel& arith); @@ -88,20 +87,30 @@ public: void addAtom(TNode atom); /** Returns true if v has been added as a left hand side in an atom */ - bool hasAnyAtoms(TNode v); + 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: - OrderedSetTriple& getOrderedSetTriple(TNode left); - OrderedSet& getEqSet(TNode left); - OrderedSet& getLeqSet(TNode left); - OrderedSet& getGeqSet(TNode left); + 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); + bool leftIsSetup(TNode left) const; /** Initializes the lists associated with a unique lhs. */ void setupLefthand(TNode left); @@ -123,18 +132,30 @@ private: * of all of the special casing and C++ iterator manipulation required. */ - void addImplicationsUsingEqualityAndEqualityList(TNode eq, OrderedSet& eqSet); - void addImplicationsUsingEqualityAndLeqList(TNode eq, OrderedSet& leqSet); - void addImplicationsUsingEqualityAndGeqList(TNode eq, OrderedSet& geqSet); + void addImplicationsUsingEqualityAndEqualityValues(TNode eq); + void addImplicationsUsingEqualityAndBoundValues(TNode eq); + + void addImplicationsUsingLeqAndEqualityValues(TNode leq); + void addImplicationsUsingLeqAndBoundValues(TNode leq); + + void addImplicationsUsingGeqAndEqualityValues(TNode geq); + void addImplicationsUsingGeqAndBoundValues(TNode geq); - void addImplicationsUsingLeqAndEqualityList(TNode leq, OrderedSet& eqSet); - void addImplicationsUsingLeqAndLeqList(TNode leq, OrderedSet& leqSet); - void addImplicationsUsingLeqAndGeqList(TNode leq, OrderedSet& geqSet); + 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; - void addImplicationsUsingGeqAndEqualityList(TNode geq, OrderedSet& eqSet); - void addImplicationsUsingGeqAndLeqList(TNode geq, OrderedSet& leqSet); - void addImplicationsUsingGeqAndGeqList(TNode geq, OrderedSet& geqSet); + Node getWeakerImpliedUpperBound(TNode upperBound) const; + Node getWeakerImpliedLowerBound(TNode lowerBound) const; }; }/* CVC4::theory::arith namespace */ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 6226406d7..6973a7cad 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -103,6 +103,8 @@ class TheoryEngine { void propagate(TNode lit, bool) throw(theory::Interrupted, AssertionException) { + Debug("theory") << "EngineOutputChannel::propagate(" + << lit << ")" << std::endl; d_propagatedLiterals.push_back(lit); ++(d_engine->d_statistics.d_statPropagate); } @@ -117,6 +119,8 @@ class TheoryEngine { void explanation(TNode explanationNode, bool) throw(theory::Interrupted, AssertionException) { + Debug("theory") << "EngineOutputChannel::explanation(" + << explanationNode << ")" << std::endl; d_explanationNode = explanationNode; ++(d_engine->d_statistics.d_statExplanation); } diff --git a/src/util/Makefile.am b/src/util/Makefile.am index eb63885a2..aaf9ca03b 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -47,7 +47,9 @@ libutil_la_SOURCES = \ language.h \ triple.h \ trans_closure.h \ - trans_closure.cpp + trans_closure.cpp \ + boolean_simplification.h + libutil_la_LIBADD = \ @builddir@/libutilcudd.la libutilcudd_la_SOURCES = \ diff --git a/src/util/boolean_simplification.h b/src/util/boolean_simplification.h new file mode 100644 index 000000000..062bf11b6 --- /dev/null +++ b/src/util/boolean_simplification.h @@ -0,0 +1,116 @@ +/********************* */ +/*! \file bitvector.h + ** \verbatim + ** Original author: dejan + ** Major contributors: cconway + ** Minor contributors (to current version): mdeters + ** 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 "cvc4_private.h" + +#ifndef __CVC4__BOOLEAN_SIMPLIFICATION_H +#define __CVC4__BOOLEAN_SIMPLIFICATION_H + +#include "expr/node.h" +#include "util/Assert.h" +#include + + +namespace CVC4 { + +class BooleanSimplification { +public: + + static const uint32_t DUPLICATE_REMOVAL_THRESHOLD = 10; + + static void removeDuplicates(std::vector& buffer){ + if(buffer.size() < DUPLICATE_REMOVAL_THRESHOLD){ + std::sort(buffer.begin(), buffer.end()); + std::vector::iterator new_end = std::unique(buffer.begin(), buffer.end()); + buffer.erase(new_end, buffer.end()); + } + } + + static Node simplifyConflict(Node andNode){ + Assert(andNode.getKind() == kind::AND); + std::vector buffer; + push_back_associative_commute(andNode, buffer, kind::AND, kind::OR, false); + + removeDuplicates(buffer); + + NodeBuilder<> nb(kind::AND); + nb.append(buffer); + return nb; + } + + static Node simplifyClause(Node orNode){ + Assert(orNode.getKind() == kind::OR); + std::vector buffer; + push_back_associative_commute(orNode, buffer, kind::OR, kind::AND, false); + + removeDuplicates(buffer); + + NodeBuilder<> nb(kind::OR); + nb.append(buffer); + return nb; + } + + static Node simplifyHornClause(Node implication){ + Assert(implication.getKind() == kind::IMPLIES); + TNode left = implication[0]; + TNode right = implication[1]; + Node notLeft = NodeBuilder<1>(kind::NOT)<(kind::OR)<< notLeft << right; + return simplifyClause(clause); + } + + static void push_back_associative_commute(Node n, std::vector& buffer, Kind k, Kind notK, bool negateNode){ + Node::iterator i = n.begin(), end = n.end(); + for(; i != end; ++i){ + Node child = *i; + if(child.getKind() == k){ + push_back_associative_commute(child, buffer, k, notK, negateNode); + }else if(child.getKind() == kind::NOT && child[0].getKind() == notK){ + push_back_associative_commute(child, buffer, notK, k, !negateNode); + }else{ + if(negateNode){ + buffer.push_back(negate(child)); + }else{ + buffer.push_back(child); + } + } + } + } + + static Node negate(TNode n){ + bool polarity = true; + TNode base = n; + while(base.getKind() == kind::NOT){ + base = base[0]; + polarity = !polarity; + } + if(polarity){ + return base.notNode(); + }else{ + return base; + } + } + +};/* class BitVector */ + + + +}/* CVC4 namespace */ + +#endif /* __CVC4__BITVECTOR_H */ diff --git a/src/util/options.cpp b/src/util/options.cpp index 03dedfe00..6018ce611 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -81,6 +81,7 @@ Options::Options() : replayStream(NULL), replayLog(NULL), rewriteArithEqualities(false), + arithPropagation(false), satRandomFreq(0.0), satRandomSeed(91648253), //Minisat's default value pivotRule(MINIMUM) @@ -120,6 +121,7 @@ static const string optionsDescription = "\ --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\ + --enable-arithmetic-propagation turns on arithmetic propagation\n \ --incremental enable incremental solving\n"; static const string languageDescription = "\ @@ -179,7 +181,8 @@ enum OptionValue { PIVOT_RULE, RANDOM_FREQUENCY, RANDOM_SEED, - REWRITE_ARITHMETIC_EQUALITIES + REWRITE_ARITHMETIC_EQUALITIES, + ARITHMETIC_PROPAGATION };/* enum OptionValue */ /** @@ -247,6 +250,7 @@ static struct option cmdlineOptions[] = { { "random-freq" , required_argument, NULL, RANDOM_FREQUENCY }, { "random-seed" , required_argument, NULL, RANDOM_SEED }, { "rewrite-arithmetic-equalities", no_argument, NULL, REWRITE_ARITHMETIC_EQUALITIES }, + { "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! */ @@ -477,6 +481,10 @@ throw(OptionException) { rewriteArithEqualities = true; break; + case ARITHMETIC_PROPAGATION: + arithPropagation = true; + break; + case RANDOM_SEED: satRandomSeed = atof(optarg); break; diff --git a/src/util/options.h b/src/util/options.h index 8273db458..be432e5a7 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -143,6 +143,9 @@ struct CVC4_PUBLIC Options { /** Whether to rewrite equalities in arithmetic theory */ bool rewriteArithEqualities; + /** Turn on and of arithmetic propagation. */ + bool arithPropagation; + /** * Frequency for the sat solver to make random decisions. * Should be between 0 and 1. diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 060c3036d..fb82a7ac9 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -150,6 +150,8 @@ public: Node leq1 = d_nm->mkNode(LEQ, x, c1); Node geq1 = d_nm->mkNode(GEQ, x, c1); Node lt1 = d_nm->mkNode(NOT, geq1); + Node gt0 = d_nm->mkNode(NOT, leq0); + Node gt1 = d_nm->mkNode(NOT, leq1); fakeTheoryEnginePreprocess(leq0); fakeTheoryEnginePreprocess(leq1); @@ -161,20 +163,20 @@ public: d_arith->check(d_level); d_arith->propagate(d_level); - Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1); + Node gt1ThenGt0 = NodeBuilder<2>(IMPLIES) << gt1 << gt0; + Node geq1ThenGt0 = NodeBuilder<2>(IMPLIES) << geq1 << gt0; Node lt1ThenLeq1 = NodeBuilder<2>(IMPLIES) << lt1 << leq1; - Node leq0ThenLt1 = NodeBuilder<2>(IMPLIES) << leq0 << lt1; TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA); - TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq0ThenLeq1); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt1ThenGt0); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA); - TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), lt1ThenLeq1); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq1ThenGt0); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA); - TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq0ThenLt1); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), lt1ThenLeq1); } @@ -187,6 +189,8 @@ public: Node leq1 = d_nm->mkNode(LEQ, x, c1); Node geq1 = d_nm->mkNode(GEQ, x, c1); Node lt1 = d_nm->mkNode(NOT, geq1); + Node gt0 = d_nm->mkNode(NOT, leq0); + Node gt1 = d_nm->mkNode(NOT, leq1); fakeTheoryEnginePreprocess(leq0); fakeTheoryEnginePreprocess(leq1); @@ -197,20 +201,20 @@ public: d_arith->check(d_level); - Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1); + Node gt1ThenGt0 = NodeBuilder<2>(IMPLIES) << gt1 << gt0; + Node geq1ThenGt0 = NodeBuilder<2>(IMPLIES) << geq1 << gt0; Node lt1ThenLeq1 = NodeBuilder<2>(IMPLIES) << lt1 << leq1; - Node leq0ThenLt1 = NodeBuilder<2>(IMPLIES) << leq0 << lt1; TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA); - TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq0ThenLeq1); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt1ThenGt0); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA); - TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), lt1ThenLeq1); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq1ThenGt0); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA); - TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq0ThenLt1); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), lt1ThenLeq1); } void testTPLeq1() { Node x = d_nm->mkVar(*d_realType); @@ -221,6 +225,8 @@ public: Node leq1 = d_nm->mkNode(LEQ, x, c1); Node geq1 = d_nm->mkNode(GEQ, x, c1); Node lt1 = d_nm->mkNode(NOT, geq1); + Node gt0 = d_nm->mkNode(NOT, leq0); + Node gt1 = d_nm->mkNode(NOT, leq1); fakeTheoryEnginePreprocess(leq0); fakeTheoryEnginePreprocess(leq1); @@ -232,19 +238,19 @@ public: d_arith->check(d_level); d_arith->propagate(d_level); - Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1); + Node gt1ThenGt0 = NodeBuilder<2>(IMPLIES) << gt1 << gt0; + Node geq1ThenGt0 = NodeBuilder<2>(IMPLIES) << geq1 << gt0; Node lt1ThenLeq1 = NodeBuilder<2>(IMPLIES) << lt1 << leq1; - Node leq0ThenLt1 = NodeBuilder<2>(IMPLIES) << leq0 << lt1; TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA); - TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq0ThenLeq1); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt1ThenGt0); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA); - TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), lt1ThenLeq1); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq1ThenGt0); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA); - TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq0ThenLt1); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), lt1ThenLeq1); } };