From: Tim King Date: Tue, 29 Nov 2011 21:11:45 +0000 (+0000) Subject: Merging the branch branches/arithmetic/shared-terms into trunk. Arithmetic now suppor... X-Git-Tag: cvc5-1.0.0~8374 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e9198d9b99c6037165362870436b45826674303f;p=cvc5.git Merging the branch branches/arithmetic/shared-terms into trunk. Arithmetic now supports propagating equalities when a slack variable corresponding to a difference of shared terms must be 0. Similarly disequalities are propagated when these variables cannot be zero. --- diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 8663a2f68..9b0b93f78 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -173,6 +173,8 @@ Result PropEngine::checkSat(unsigned long& millis, unsigned long& resource) { Node PropEngine::getValue(TNode node) const { Assert(node.getType().isBoolean()); + Assert(d_cnfStream->hasLiteral(node)); + SatLiteral lit = d_cnfStream->getLiteral(node); SatLiteralValue v = d_satSolver->value(lit); @@ -196,6 +198,8 @@ bool PropEngine::isTranslatedSatLiteral(TNode node) const { bool PropEngine::hasValue(TNode node, bool& value) const { Assert(node.getType().isBoolean()); + Assert(d_cnfStream->hasLiteral(node)); + SatLiteral lit = d_cnfStream->getLiteral(node); SatLiteralValue v = d_satSolver->value(lit); diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 36ab2cd68..4ca8aff0b 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -16,6 +16,8 @@ libarith_la_SOURCES = \ arithvar_node_map.h \ atom_database.h \ atom_database.cpp \ + difference_manager.h \ + difference_manager.cpp \ normal_form.h\ normal_form.cpp \ arith_utilities.h \ diff --git a/src/theory/arith/arith_prop_manager.cpp b/src/theory/arith/arith_prop_manager.cpp index d1fce5b90..6d2e04de1 100644 --- a/src/theory/arith/arith_prop_manager.cpp +++ b/src/theory/arith/arith_prop_manager.cpp @@ -135,7 +135,7 @@ bool ArithPropManager::propagateArithVar(bool upperbound, ArithVar var, const De bool asserted = isAsserted(bestImplied); if( !asserted && !isPropagated(bestImplied)){ - propagate(bestImplied, reason); + propagate(bestImplied, reason, false); ++d_statistics.d_addedPropagation; success = true; }else if(!asserted){ diff --git a/src/theory/arith/arith_prop_manager.h b/src/theory/arith/arith_prop_manager.h index 82f58c7a0..912c4fdf8 100644 --- a/src/theory/arith/arith_prop_manager.h +++ b/src/theory/arith/arith_prop_manager.h @@ -39,36 +39,55 @@ namespace theory { namespace arith { class PropManager { +public: + struct PropUnit { + // consequent <= antecedent + Node consequent; + Node antecedent; + bool flag; + PropUnit(Node c, Node a, bool f) : + consequent(c), antecedent(a), flag(f) + {} + }; + private: - context::CDList d_propagated; + context::CDList d_propagated; + context::CDO d_propagatedPos; - typedef context::CDMap ExplainMap; + typedef context::CDMap ExplainMap; ExplainMap d_explanationMap; - context::CDList d_reasons; + size_t getIndex(TNode n) const { + Assert(isPropagated(n)); + return (*(d_explanationMap.find(n))).second; + } public: PropManager(context::Context* c): d_propagated(c), d_propagatedPos(c, 0), - d_explanationMap(c), - d_reasons(c) + d_explanationMap(c) { } + const PropUnit& getUnit(TNode n) const { + return d_propagated[getIndex(n)]; + } + 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); + bool isFlagged(TNode n) const { + return getUnit(n).flag; + } - d_explanationMap.insert(n, reason); + void propagate(TNode n, Node reason, bool flag) { + Assert(!isPropagated(n)); - d_reasons.push_back(reason); - d_propagated.push_back(n); + d_explanationMap.insert(n, d_propagated.size()); + d_propagated.push_back(PropUnit(n, reason, flag)); Debug("ArithPropManager") << n << std::endl << "<="<< reason<< std::endl; } @@ -77,17 +96,15 @@ public: return d_propagatedPos < d_propagated.size(); } - TNode getPropagation() { + const PropUnit& getNextPropagation() { Assert(hasMorePropagations()); - TNode prop = d_propagated[d_propagatedPos]; + const PropUnit& 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; + return getUnit(n).antecedent; } };/* class PropManager */ diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index c8a5e39a7..fdc3bee3b 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -54,6 +54,15 @@ public: return c; } + int sgn() const { + int x = getNoninfinitesimalPart().sgn(); + if(x == 0){ + return getInfinitesimalPart().sgn(); + }else{ + return x; + } + } + DeltaRational operator+(const DeltaRational& other) const{ CVC4::Rational tmpC = c+other.c; CVC4::Rational tmpK = k+other.k; diff --git a/src/theory/arith/difference_manager.cpp b/src/theory/arith/difference_manager.cpp new file mode 100644 index 000000000..dfb07bcf4 --- /dev/null +++ b/src/theory/arith/difference_manager.cpp @@ -0,0 +1,102 @@ +#include "theory/arith/difference_manager.h" +#include "theory/uf/equality_engine_impl.h" + +namespace CVC4 { +namespace theory { +namespace arith { + +DifferenceManager::DifferenceManager(context::Context* c, PropManager& pm) + : d_reasons(c), + d_queue(pm), + d_notify(*this), + d_ee(d_notify, c, "theory::arith::DifferenceManager"), + d_false(NodeManager::currentNM()->mkConst(false)) +{} + +void DifferenceManager::propagate(TNode x){ + Debug("arith::differenceManager")<< "DifferenceManager::propagate("<& assumptions) { + TNode lhs, rhs; + switch (literal.getKind()) { + case kind::EQUAL: + lhs = literal[0]; + rhs = literal[1]; + break; + case kind::NOT: + lhs = literal[0]; + rhs = d_false; + break; + default: + Unreachable(); + } + d_ee.getExplanation(lhs, rhs, assumptions); +} + +#warning "Stolen from theory_uf.h verbatim. Generalize me!" +Node mkAnd(const std::vector& conjunctions) { + Assert(conjunctions.size() > 0); + + std::set all; + all.insert(conjunctions.begin(), conjunctions.end()); + + if (all.size() == 1) { + // All the same, or just one + return conjunctions[0]; + } + + NodeBuilder<> conjunction(kind::AND); + std::set::const_iterator it = all.begin(); + std::set::const_iterator it_end = all.end(); + while (it != it_end) { + conjunction << *it; + ++ it; + } + + return conjunction; +} + + +Node DifferenceManager::explain(TNode lit){ + std::vector assumptions; + explain(lit, assumptions); + return mkAnd(assumptions); +} + +void DifferenceManager::addDifference(ArithVar s, Node x, Node y){ + Assert(s >= d_differences.size() || !isDifferenceSlack(s)); + + Debug("arith::differenceManager") << s << x << y << std::endl; + + d_differences.resize(s+1); + d_differences[s] = Difference(x,y); +} + +void DifferenceManager::differenceIsZero(ArithVar s, TNode reason){ + Assert(isDifferenceSlack(s)); + TNode x = d_differences[s].x; + TNode y = d_differences[s].y; + + d_reasons.push_back(reason); + d_ee.addEquality(x, y, reason); +} + +void DifferenceManager::differenceCannotBeZero(ArithVar s, TNode reason){ + Assert(isDifferenceSlack(s)); + TNode x = d_differences[s].x; + TNode y = d_differences[s].y; + + d_reasons.push_back(reason); + d_ee.addDisequality(x, y, reason); +} + +void DifferenceManager::addSharedTerm(Node x){ + d_ee.addTriggerTerm(x); +} + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/arith/difference_manager.h b/src/theory/arith/difference_manager.h new file mode 100644 index 000000000..01f42dcfe --- /dev/null +++ b/src/theory/arith/difference_manager.h @@ -0,0 +1,95 @@ + + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H +#define __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H + +#include "theory/arith/arith_utilities.h" +#include "theory/uf/equality_engine.h" +#include "context/cdo.h" +#include "context/cdlist.h" +#include "context/context.h" +#include "util/stats.h" +#include "theory/arith/arith_prop_manager.h" + +namespace CVC4 { +namespace theory { +namespace arith { + +class DifferenceManager { +private: + struct Difference { + bool isSlack; + TNode x; + TNode y; + Difference() : isSlack(false), x(TNode::null()), y(TNode::null()){} + Difference(TNode a, TNode b) : isSlack(true), x(a), y(b) { + Assert(x < y); + } + }; + + + class DifferenceNotifyClass { + private: + DifferenceManager& d_dm; + public: + DifferenceNotifyClass(DifferenceManager& dm): d_dm(dm) {} + + bool notify(TNode propagation) { + Debug("arith::differences") << "DifferenceNotifyClass::notify(" << propagation << ")" << std::endl; + // Just forward to dm + d_dm.propagate(propagation); + return true; + } + + void notify(TNode t1, TNode t2) { + Debug("arith::differences") << "DifferenceNotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl; + Node equality = t1.eqNode(t2); + d_dm.propagate(equality); + } + }; + + std::vector< Difference > d_differences; + + context::CDList d_reasons; + PropManager& d_queue; + + + DifferenceNotifyClass d_notify; + theory::uf::EqualityEngine d_ee; + + void propagate(TNode x); + void explain(TNode literal, std::vector& assumptions); + + Node d_false; + +public: + + DifferenceManager(context::Context*, PropManager&); + + Node explain(TNode literal); + + void addDifference(ArithVar s, Node x, Node y); + + inline bool isDifferenceSlack(ArithVar s) const{ + if(s < d_differences.size()){ + return d_differences[s].isSlack; + }else{ + return false; + } + } + + void differenceIsZero(ArithVar s, TNode reason); + + void differenceCannotBeZero(ArithVar s, TNode reason); + + void addSharedTerm(Node x); +};/* class DifferenceManager */ + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H */ + diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index ed8f837d1..73f80a70d 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -27,19 +27,52 @@ using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::arith; + + +void ArithPartialModel::zeroDifferenceDetected(ArithVar x){ + Assert(d_dm.isDifferenceSlack(x)); + Assert(upperBoundIsZero(x)); + Assert(lowerBoundIsZero(x)); + + Node lb = getLowerConstraint(x); + Node ub = getUpperConstraint(x); + Node reason = lb != ub ? lb.andNode(ub) : lb; + d_dm.differenceIsZero(x, reason); +} + void ArithPartialModel::setUpperBound(ArithVar x, const DeltaRational& r){ d_deltaIsSafe = false; Debug("partial_model") << "setUpperBound(" << x << "," << r << ")" << endl; d_hasHadABound[x] = true; d_upperBound.set(x,r); + + if(d_dm.isDifferenceSlack(x)){ + int sgn = r.sgn(); + if(sgn < 0){ + d_dm.differenceCannotBeZero(x, getUpperConstraint(x)); + }else if(sgn == 0 && lowerBoundIsZero(x)){ + zeroDifferenceDetected(x); + } + } } void ArithPartialModel::setLowerBound(ArithVar x, const DeltaRational& r){ d_deltaIsSafe = false; + Debug("partial_model") << "setLowerBound(" << x << "," << r << ")" << endl; d_hasHadABound[x] = true; d_lowerBound.set(x,r); + + + if(d_dm.isDifferenceSlack(x)){ + int sgn = r.sgn(); + if(sgn > 0){ + d_dm.differenceCannotBeZero(x, getLowerConstraint(x)); + }else if(sgn == 0 && upperBoundIsZero(x)){ + zeroDifferenceDetected(x); + } + } } void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& r){ diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index 9c5e343ef..6e85f7e80 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -26,6 +26,8 @@ #include "expr/attribute.h" #include "expr/node.h" +#include "theory/arith/difference_manager.h" + #include #ifndef __CVC4__THEORY__ARITH__PARTIAL_MODEL_H @@ -52,6 +54,7 @@ private: context::CDVector d_upperConstraint; context::CDVector d_lowerConstraint; + bool d_deltaIsSafe; Rational d_delta; @@ -61,9 +64,11 @@ private: typedef std::vector HistoryList; HistoryList d_history; + DifferenceManager& d_dm; + public: - ArithPartialModel(context::Context* c): + ArithPartialModel(context::Context* c, DifferenceManager& dm): d_mapSize(0), d_hasHadABound(), d_hasSafeAssignment(), @@ -75,7 +80,8 @@ public: d_lowerConstraint(c,true), d_deltaIsSafe(false), d_delta(-1,1), - d_history() + d_history(), + d_dm(dm) { } void setLowerConstraint(ArithVar x, TNode constraint); @@ -98,6 +104,18 @@ public: void commitAssignmentChanges(); + inline bool lowerBoundIsZero(ArithVar x){ + return hasLowerBound(x) && getLowerBound(x).sgn() == 0; + } + + inline bool upperBoundIsZero(ArithVar x){ + return hasUpperBound(x) && getUpperBound(x).sgn() == 0; + } + +private: + void zeroDifferenceDetected(ArithVar x); + +public: void setUpperBound(ArithVar x, const DeltaRational& r); @@ -114,6 +132,7 @@ public: const DeltaRational& getAssignment(ArithVar x) const; + /** * x >= l * ? c < l diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 77e7e1060..27fb0bb02 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -339,7 +339,7 @@ bool SimplexDecisionProcedure::propagateCandidateBound(ArithVar basic, bool uppe explainNonbasicsLowerBound(basic, nb); } Node explanation = nb; - d_propManager.propagate(bestImplied, explanation); + d_propManager.propagate(bestImplied, explanation, false); return true; }else{ Debug("arith::prop") << basic << " " << asserted << " " << propagated << endl; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 289d5ace4..53559d949 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -61,7 +61,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha d_atomsInContext(c), d_learner(d_pbSubstitutions), d_nextIntegerCheckVar(0), - d_partialModel(c), + d_partialModel(c, d_differenceManager), d_userVariables(), d_diseq(c), d_tableau(), @@ -73,6 +73,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha d_tableauResetPeriod(10), d_atomDatabase(c, out), d_propManager(c, d_arithvarNodeMap, d_atomDatabase, valuation), + d_differenceManager(c, d_propManager), d_simplex(d_propManager, d_partialModel, d_tableau), d_DELTA_ZERO(0), d_statistics() @@ -89,6 +90,7 @@ TheoryArith::Statistics::Statistics(): d_staticLearningTimer("theory::arith::staticLearningTimer"), d_permanentlyRemovedVariables("theory::arith::permanentlyRemovedVariables", 0), d_presolveTime("theory::arith::presolveTime"), + d_externalBranchAndBounds("theory::arith::externalBranchAndBounds",0), d_initialTableauSize("theory::arith::initialTableauSize", 0), d_currSetToSmaller("theory::arith::currSetToSmaller", 0), d_smallerSetToCurr("theory::arith::smallerSetToCurr", 0), @@ -104,6 +106,7 @@ TheoryArith::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_permanentlyRemovedVariables); StatisticsRegistry::registerStat(&d_presolveTime); + StatisticsRegistry::registerStat(&d_externalBranchAndBounds); StatisticsRegistry::registerStat(&d_initialTableauSize); StatisticsRegistry::registerStat(&d_currSetToSmaller); @@ -122,6 +125,7 @@ TheoryArith::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_permanentlyRemovedVariables); StatisticsRegistry::unregisterStat(&d_presolveTime); + StatisticsRegistry::unregisterStat(&d_externalBranchAndBounds); StatisticsRegistry::unregisterStat(&d_initialTableauSize); StatisticsRegistry::unregisterStat(&d_currSetToSmaller); @@ -129,6 +133,11 @@ TheoryArith::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_restartTimer); } + +void TheoryArith::addSharedTerm(TNode n){ + d_differenceManager.addSharedTerm(n); +} + Node TheoryArith::preprocess(TNode atom) { Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl; @@ -332,6 +341,26 @@ void TheoryArith::setupPolynomial(const Polynomial& poly) { d_tableau.addRow(varSlack, coefficients, variables); setupInitialValue(varSlack); + //Add differences to the difference manager + Polynomial::iterator i = poly.begin(), end = poly.end(); + if(i != end){ + Monomial first = *i; + ++i; + if(i != end){ + Monomial second = *i; + ++i; + if(i == end){ + if(first.getConstant().isOne() && second.getConstant().getValue() == -1){ + VarList vl0 = first.getVarList(); + VarList vl1 = second.getVarList(); + if(vl0.singleton() && vl1.singleton()){ + d_differenceManager.addDifference(varSlack, vl0.getNode(), vl1.getNode()); + } + } + } + } + } + ++(d_statistics.d_statSlackVariables); markSetup(polyNode); } @@ -718,6 +747,7 @@ void TheoryArith::check(Effort effortLevel){ } else { Debug("integers") << " " << lem[1] << " is not assigned a SAT literal" << endl; } + ++(d_statistics.d_externalBranchAndBounds); d_out->lemma(lem); // split only on one var @@ -743,6 +773,7 @@ void TheoryArith::check(Effort effortLevel){ } else { Debug("integers") << " " << lem[1] << " is not assigned a SAT literal" << endl; } + ++(d_statistics.d_externalBranchAndBounds); d_out->lemma(lem); // split only on one var @@ -771,6 +802,7 @@ void TheoryArith::check(Effort effortLevel){ } else { Debug("integers") << " " << lem[1] << " is not assigned a SAT literal" << endl; } + ++(d_statistics.d_externalBranchAndBounds); d_out->lemma(lem); // split only on one var @@ -849,7 +881,12 @@ void TheoryArith::debugPrintModel(){ Node TheoryArith::explain(TNode n) { Debug("explain") << "explain @" << getContext()->getLevel() << ": " << n << endl; Assert(d_propManager.isPropagated(n)); - return d_propManager.explain(n); + + if(d_propManager.isFlagged(n)){ + return d_differenceManager.explain(n); + }else{ + return d_propManager.explain(n); + } } void TheoryArith::propagate(Effort e) { @@ -862,9 +899,20 @@ void TheoryArith::propagate(Effort e) { } while(d_propManager.hasMorePropagations()){ - TNode toProp = d_propManager.getPropagation(); + const PropManager::PropUnit next = d_propManager.getNextPropagation(); + bool flag = next.flag; + TNode toProp = next.consequent; + TNode atom = (toProp.getKind() == kind::NOT) ? toProp[0] : toProp; - if(inContextAtom(atom)){ + + Debug("arith::propagate") << "propagate " << flag << " " << toProp << endl; + + if(flag) { + //Currently if the flag is set this came from an equality detected by the + //equality engine in the the difference manager. + d_out->propagate(toProp); + propagated = true; + }else if(inContextAtom(atom)){ Node satValue = d_valuation.getSatValue(toProp); AlwaysAssert(satValue.isNull()); propagated = true; @@ -872,7 +920,7 @@ void TheoryArith::propagate(Effort e) { }else{ //Not clear if this is a good time to do this or not... Debug("arith::propagate") << "Atom is not in context" << toProp << endl; - #warning "enable remove atom in database" +#warning "enable remove atom in database" //d_atomDatabase.removeAtom(atom); } } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index e8d920084..6255efbbc 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -39,6 +39,7 @@ #include "theory/arith/arith_prop_manager.h" #include "theory/arith/arithvar_node_map.h" #include "theory/arith/dio_solver.h" +#include "theory/arith/difference_manager.h" #include "util/stats.h" @@ -196,9 +197,11 @@ private: /** This manager keeps track of information needed to propagate. */ ArithPropManager d_propManager; + /** This keeps track of difference equalities. Mostly for sharing. */ + DifferenceManager d_differenceManager; + /** This implements the Simplex decision procedure. */ SimplexDecisionProcedure d_simplex; - public: TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation); virtual ~TheoryArith(); @@ -228,6 +231,8 @@ public: EqualityStatus getEqualityStatus(TNode a, TNode b); + void addSharedTerm(TNode n); + private: /** The constant zero. */ DeltaRational d_DELTA_ZERO; @@ -329,6 +334,8 @@ private: IntStat d_permanentlyRemovedVariables; TimerStat d_presolveTime; + IntStat d_externalBranchAndBounds; + IntStat d_initialTableauSize; IntStat d_currSetToSmaller; IntStat d_smallerSetToCurr; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 386b8bbd4..e36d163a4 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -668,6 +668,8 @@ void TheoryEngine::explainEqualities(TheoryId theoryId, TNode literals, NodeBuil TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; if (atom.getKind() == kind::EQUAL) { explainEquality(theoryId, literal, builder); + } else if(literal.getKind() == kind::AND){ + explainEqualities(theoryId, literal, builder); } else { builder << literal; }