- 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.
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 \
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){
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:
--- /dev/null
+
+#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<bool>());
+ 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);
+}
--- /dev/null
+#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<TNode> d_propagated;
+ context::CDO<uint32_t> d_propagatedPos;
+ typedef context::CDMap<TNode, TNode, TNodeHashFunction> ExplainMap;
+
+ ExplainMap d_explanationMap;
+
+ context::CDList<Node> 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 */
#include "util/rational.h"
#include "expr/node.h"
#include "expr/attribute.h"
+#include "theory/arith/delta_rational.h"
#include <vector>
#include <stdint.h>
#include <limits>
}
}
+template <bool selectLeft>
+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<false>(assertion, simpleKind);
+
+ Assert(right.getKind() == kind::CONST_RATIONAL);
+ const Rational& noninf = right.getConst<Rational>();
+
+ 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,
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 */
--- /dev/null
+#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 */
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){
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;
}
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:
+#include <map>
#include <set>
#include "expr/kind.h"
#include "expr/node.h"
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<Rational>();
+}
-typedef std::set<TNode, RightHandRationalLT> 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<Rational, BoundValueEntry> BoundValueSet;
+
+typedef std::set<TNode, RightHandRationalLT> 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 */
}
}
+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
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);
context::CDVector<DeltaRational> d_upperBound;
context::CDVector<DeltaRational> d_lowerBound;
- context::CDVector<TNode> d_upperConstraint;
- context::CDVector<TNode> d_lowerConstraint;
+ context::CDVector<Node> d_upperConstraint;
+ context::CDVector<Node> d_lowerConstraint;
bool d_deltaIsSafe;
Rational d_delta;
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()
/**
- * 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);
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),
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"),
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);
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);
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);
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);
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);
if(Debug.isOn("model")) { d_partialModel.printModel(x_i); }
return Node::null();
- //return false;
}
// 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;
}
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;
}
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<ArithVar> tableauAndHasSet(Tableau& tab, ArithVar v){
-// set<ArithVar> 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<ArithVar> columnIteratorSet(Tableau& tab,ArithVar v){
-// set<ArithVar> 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);
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
const DeltaRational& beta = d_partialModel.getAssignment(basic);
if(d_partialModel.belowLowerBound(basic, beta, true)){
- ArithVar x_j = selectSlackBelow<minVarOrder>(basic);
+ ArithVar x_j = selectSlackUpperBound<minVarOrder>(basic);
if(x_j == ARITHVAR_SENTINEL ){
- return generateConflictBelow(basic);
+ return generateConflictBelowLowerBound(basic);
}
}else if(d_partialModel.aboveUpperBound(basic, beta, true)){
- ArithVar x_j = selectSlackAbove<minVarOrder>(basic);
+ ArithVar x_j = selectSlackLowerBound<minVarOrder>(basic);
if(x_j == ARITHVAR_SENTINEL ){
- return generateConflictAbove(basic);
+ return generateConflictAboveUpperBound(basic);
}
}
return Node::null();
ArithVar x_j = ARITHVAR_SENTINEL;
if(d_partialModel.belowLowerBound(x_i, beta_i, true)){
- x_j = selectSlack
Below<pf>(x_i);
+ x_j = selectSlack
UpperBound<pf>(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 = selectSlack
Above<pf>(x_i);
+ x_j = selectSlack
LowerBound<pf>(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<pf>(x_j) == ARITHVAR_SENTINEL){
+ // Node possibleConflict = deduceUpperBound(x_j);
+ // if(!possibleConflict.isNull()){
+ // return possibleConflict;
+ // }
+ // }
+ // if(selectSlackLowerBound<pf>(x_j) == ARITHVAR_SENTINEL){
+ // Node possibleConflict = deduceLowerBound(x_j);
+ // if(!possibleConflict.isNull()){
+ // return possibleConflict;
+ // }
+ // }
}
}
Assert(remainingIterations == 0);
return Node::null();
}
+template <bool upperBound>
+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<WeakeningElem> weakeningElements;
+// queue<uint32_t> 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<Node> 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<minVarOrder>(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<minVarOrder>(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.
*/
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.
#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"
Tableau& d_tableau;
ArithPriorityQueue d_queue;
+ ArithPropManager& d_propManager;
+
ArithVar d_numVariables;
std::queue<Node> 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.
* 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 <bool above, PreferenceFunction> ArithVar selectSlack(ArithVar x_i);
- template <PreferenceFunction pf> ArithVar selectSlackBelow(ArithVar x_i) {
- return selectSlack<false, pf>(x_i);
- }
- template <PreferenceFunction pf> ArithVar selectSlackAbove(ArithVar x_i) {
+ template <bool lowerBound, PreferenceFunction> ArithVar selectSlack(ArithVar x_i);
+ template <PreferenceFunction pf> ArithVar selectSlackLowerBound(ArithVar x_i) {
return selectSlack<true, pf>(x_i);
}
+ template <PreferenceFunction pf> ArithVar selectSlackUpperBound(ArithVar x_i) {
+ return selectSlack<false, pf>(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 <bool upperBound>
+ void explainNonbasics(ArithVar basic, NodeBuilder<>& output);
+ void explainNonbasicsLowerBound(ArithVar basic, NodeBuilder<>& output){
+ explainNonbasics<false>(basic, output);
+ }
+ void explainNonbasicsUpperBound(ArithVar basic, NodeBuilder<>& output){
+ explainNonbasics<true>(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:
/**
*/
DeltaRational computeRowValue(ArithVar x, bool useSafe);
+ bool hasAnyUpdates() { return !d_updatedBounds.empty(); }
+ void clearUpdates(){
+ d_updatedBounds.purge();
+ }
+ void propagateCandidates();
void increaseMax() {d_numVariables++;}
/** Adds a conflict as a lemma to the queue. */
void delayConflictAsLemma(Node conflict){
- Node negatedConflict = negateConjunctionAsClause(conflict);
+ Node negatedConflict = negateConjunctionAsClause(conflict);
pushLemma(negatedConflict);
}
*/
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:
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;
#include "util/rational.h"
#include "util/integer.h"
+#include "util/boolean_simplification.h"
+
#include "theory/rewriter.h"
#include "theory/arith/theory_arith.h"
#include "theory/arith/normal_form.h"
+#include "theory/arith/arith_prop_manager.h"
#include <stdint.h>
static const uint32_t RESET_START = 2;
struct SlackAttrID;
-typedef expr::Attribute<SlackAttrID, Node> Slack;
+typedef expr::Attribute<SlackAttrID, bool> Slack;
TheoryArith::TheoryArith(context::Context* c, OutputChannel& out, Valuation valuation) :
Theory(THEORY_ARITH, c, out, valuation),
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()
{}
if(isRelationOperator(k)){
Assert(Comparison::isNormalAtom(n));
+ //cout << n << endl;
d_propagator.addAtom(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);
}
}
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();
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);
}
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);
Debug("arith") << "registerTerm(" << tn << ")" << endl;
}
-template <bool selectLeft>
-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<true>(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<false>(assertion, simpleKind);
-
- Assert(right.getKind() == CONST_RATIONAL);
- const Rational& noninf = right.getConst<Rational>();
-
- Rational inf = Rational(Integer(deltaCoeff(simpleKind)));
- return DeltaRational(noninf, inf);
-}
Node TheoryArith::disequalityConflict(TNode eq, TNode lb, TNode ub){
NodeBuilder<3> conflict(kind::AND);
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{
}
}
+/*
+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<bool>());
+ }
+ }
}
+*/
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);
+ }
}
}
}
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;
bool TheoryArith::entireStateIsConsistent(){
typedef std::vector<Node>::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;
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();
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) <<endl;
++(d_statistics.d_permanentlyRemovedVariables);
}
typedef std::vector<Node>::const_iterator VarIter;
for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){
Node variableNode = *i;
- ArithVar var = 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
#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"
*/
std::vector<Node> 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
*/
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.
Tableau d_smallTableauCopy;
ArithUnatePropagator d_propagator;
+
+ ArithPropManager d_propManager;
+
SimplexDecisionProcedure d_simplex;
public:
/** 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.
*/
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<Rational>& coeffs,
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);
}
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){
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<OrderedSet::iterator, bool> res = eqSet.insert(atom);
+ Assert(!containsEquality(atom));
+ addImplicationsUsingEqualityAndEqualityValues(atom);
+ addImplicationsUsingEqualityAndBoundValues(atom);
+
+ pair<EqualValueSet::iterator, bool> res = getEqualValueSet(left).insert(atom);
Assert(res.second);
- addImplicationsUsingEqualityAndEqualityList(atom, eqSet);
- addImplicationsUsingEqualityAndLeqList(atom, leqSet);
- addImplicationsUsingEqualityAndGeqList(atom, geqSet);
break;
}
case LEQ:
{
- pair<OrderedSet::iterator, bool> 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<OrderedSet::iterator, bool> 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:
}
}
+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];
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
}
-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
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)<<lowerBound[0]<< lowerBound[1];
+ Node gt = NodeBuilder<1>(NOT) << leq;
+ result = getImpliedLowerBoundUsingGT(gt, false);
+ }else{
+ Unreachable();
+ }
+ Debug("arith::unate") << lowerBound <<" -> " << result << std::endl;
+ return result;
+}
+
+Node ArithUnatePropagator::getWeakerImpliedLowerBound(TNode lowerBound) const {
+ Node result = Node::null();
+ if(lowerBound.getKind() == GEQ ){
+ result = getImpliedLowerBoundUsingGeq(lowerBound, true);
+ }else if(lowerBound.getKind() == NOT && lowerBound[0].getKind() == LEQ){
+ result = getImpliedLowerBoundUsingGT(lowerBound, true);
+ }else if(lowerBound.getKind() == GT){
+ Node leq = NodeBuilder<2>(LEQ)<<lowerBound[0]<< lowerBound[1];
+ Node gt = NodeBuilder<1>(NOT) << leq;
+ result = getImpliedLowerBoundUsingGT(gt, true);
+ }else{
+ Unreachable();
+ }
+ Assert(result != lowerBound);
+
+ Debug("arith::unate") << lowerBound <<" -> " << result << std::endl;
+ return result;
+}
*/
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<Node, OrderedSetTriple, NodeHashFunction> NodeToOrderedSetMap;
- NodeToOrderedSetMap d_orderedListMap;
+ typedef __gnu_cxx::hash_map<TNode, VariablesSets, NodeHashFunction> NodeToSetsMap;
+ NodeToSetsMap d_setsMap;
public:
ArithUnatePropagator(context::Context* cxt, OutputChannel& arith);
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);
* 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 */
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);
}
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);
}
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 = \
--- /dev/null
+/********************* */
+/*! \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 <vector>
+
+
+namespace CVC4 {
+
+class BooleanSimplification {
+public:
+
+ static const uint32_t DUPLICATE_REMOVAL_THRESHOLD = 10;
+
+ static void removeDuplicates(std::vector<Node>& buffer){
+ if(buffer.size() < DUPLICATE_REMOVAL_THRESHOLD){
+ std::sort(buffer.begin(), buffer.end());
+ std::vector<Node>::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<Node> 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<Node> 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)<<left;
+ Node clause = NodeBuilder<2>(kind::OR)<< notLeft << right;
+ return simplifyClause(clause);
+ }
+
+ static void push_back_associative_commute(Node n, std::vector<Node>& 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 */
replayStream(NULL),
replayLog(NULL),
rewriteArithEqualities(false),
+ arithPropagation(false),
satRandomFreq(0.0),
satRandomSeed(91648253), //Minisat's default value
pivotRule(MINIMUM)
--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 = "\
PIVOT_RULE,
RANDOM_FREQUENCY,
RANDOM_SEED,
- REWRITE_ARITHMETIC_EQUALITIES
+ REWRITE_ARITHMETIC_EQUALITIES,
+ ARITHMETIC_PROPAGATION
};/* enum OptionValue */
/**
{ "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! */
rewriteArithEqualities = true;
break;
+ case ARITHMETIC_PROPAGATION:
+ arithPropagation = true;
+ break;
+
case RANDOM_SEED:
satRandomSeed = atof(optarg);
break;
/** 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.
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);
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);
}
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);
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);
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);
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);
}
};
projects / cvc5.git / commitdiff