From: Tim King Date: Tue, 24 Apr 2012 18:36:40 +0000 (+0000) Subject: This commit merges in the branch branches/arithmetic/congruence into trunk. Here... X-Git-Tag: cvc5-1.0.0~8220 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c0f5194dd56c5127c5c6dab5e59997eccc2d78a5;p=cvc5.git This commit merges in the branch branches/arithmetic/congruence into trunk. Here are a summary of the changes: - Adds CDMaybe and CDRaised in cdmaybe.h - Add test for congruence over arithmetic terms and constants - Renames DifferenceManager to CongruenceManager - Changes a number of internal details for CongruenceManager --- diff --git a/src/context/Makefile.am b/src/context/Makefile.am index d0c2b9783..13a151ffc 100644 --- a/src/context/Makefile.am +++ b/src/context/Makefile.am @@ -23,5 +23,6 @@ libcontext_la_SOURCES = \ cdcirclist.h \ cdcirclist_forward.h \ cdvector.h \ + cdmaybe.h \ stacking_map.h \ stacking_vector.h diff --git a/src/context/cdmaybe.h b/src/context/cdmaybe.h new file mode 100644 index 000000000..3c95ab126 --- /dev/null +++ b/src/context/cdmaybe.h @@ -0,0 +1,65 @@ +/** + * This implements a CDMaybe. + * This has either been set in the context or it has not. + * T must have a default constructor and support assignment. + */ + +#include "cvc4_private.h" + +#pragma once + +#include "context/cdo.h" +#include "context/context.h" + +namespace CVC4 { +namespace context { + +class CDRaised { +private: + context::CDO d_flag; + +public: + CDRaised(context::Context* c) + : d_flag(c, false) + {} + + + bool isRaised() const { + return d_flag.get(); + } + + void raise(){ + Assert(!isRaised()); + d_flag.set(true); + } + +}; /* class CDRaised */ + +template +class CDMaybe { +private: + typedef std::pair BoolTPair; + context::CDO d_data; + +public: + CDMaybe(context::Context* c) : d_data(c, std::make_pair(false, T())) + {} + + bool isSet() const { + return d_data.get().first; + } + + void set(const T& d){ + Assert(!isSet()); + d_data.set(std::make_pair(true, d)); + } + + const T& get() const{ + Assert(isSet()); + return d_data.get().second; + } +}; /* class CDMaybe */ + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ + diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index b97a6f384..f9c423ef7 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -16,8 +16,8 @@ libarith_la_SOURCES = \ constraint_forward.h \ constraint.h \ constraint.cpp \ - difference_manager.h \ - difference_manager.cpp \ + congruence_manager.h \ + congruence_manager.cpp \ normal_form.h\ normal_form.cpp \ arith_utilities.h \ diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp new file mode 100644 index 000000000..201eb08e7 --- /dev/null +++ b/src/theory/arith/congruence_manager.cpp @@ -0,0 +1,322 @@ +#include "theory/arith/congruence_manager.h" +#include "theory/uf/equality_engine_impl.h" + +#include "theory/arith/constraint.h" +#include "theory/arith/arith_utilities.h" + +namespace CVC4 { +namespace theory { +namespace arith { + +ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDatabase& cd, TNodeCallBack& setup, const ArithVarNodeMap& av2Node) + : d_conflict(c), + d_notify(*this), + d_keepAlive(c), + d_propagatations(c), + d_explanationMap(c), + d_constraintDatabase(cd), + d_setupLiteral(setup), + d_av2Node(av2Node), + d_ee(d_notify, c, "theory::arith::ArithCongruenceManager"), + d_false(mkBoolNode(false)) +{} + +ArithCongruenceManager::Statistics::Statistics(): + d_watchedVariables("theory::arith::congruence::watchedVariables", 0), + d_watchedVariableIsZero("theory::arith::congruence::watchedVariableIsZero", 0), + d_watchedVariableIsNotZero("theory::arith::congruence::watchedVariableIsNotZero", 0), + d_equalsConstantCalls("theory::arith::congruence::equalsConstantCalls", 0), + d_propagations("theory::arith::congruence::propagations", 0), + d_propagateConstraints("theory::arith::congruence::propagateConstraints", 0), + d_conflicts("theory::arith::congruence::conflicts", 0) +{ + StatisticsRegistry::registerStat(&d_watchedVariables); + StatisticsRegistry::registerStat(&d_watchedVariableIsZero); + StatisticsRegistry::registerStat(&d_watchedVariableIsNotZero); + StatisticsRegistry::registerStat(&d_equalsConstantCalls); + StatisticsRegistry::registerStat(&d_propagations); + StatisticsRegistry::registerStat(&d_propagateConstraints); + StatisticsRegistry::registerStat(&d_conflicts); +} + +ArithCongruenceManager::Statistics::~Statistics(){ + StatisticsRegistry::unregisterStat(&d_watchedVariables); + StatisticsRegistry::unregisterStat(&d_watchedVariableIsZero); + StatisticsRegistry::unregisterStat(&d_watchedVariableIsNotZero); + StatisticsRegistry::unregisterStat(&d_equalsConstantCalls); + StatisticsRegistry::unregisterStat(&d_propagations); + StatisticsRegistry::unregisterStat(&d_propagateConstraints); + StatisticsRegistry::unregisterStat(&d_conflicts); +} + +void ArithCongruenceManager::watchedVariableIsZero(Constraint lb, Constraint ub){ + Assert(lb->isLowerBound()); + Assert(ub->isUpperBound()); + Assert(lb->getVariable() == ub->getVariable()); + Assert(lb->getValue().sgn() == 0); + Assert(ub->getValue().sgn() == 0); + + ++(d_statistics.d_watchedVariableIsZero); + + ArithVar s = lb->getVariable(); + Node reason = ConstraintValue::explainConflict(lb,ub); + + d_keepAlive.push_back(reason); + assertionToEqualityEngine(true, s, reason); +} + +void ArithCongruenceManager::watchedVariableIsZero(Constraint eq){ + Assert(eq->isEquality()); + Assert(eq->getValue().sgn() == 0); + + ++(d_statistics.d_watchedVariableIsZero); + + ArithVar s = eq->getVariable(); + + //Explain for conflict is correct as these proofs are generated + //and stored eagerly + //These will be safe for propagation later as well + Node reason = eq->explainForConflict(); + + d_keepAlive.push_back(reason); + assertionToEqualityEngine(true, s, reason); +} + +void ArithCongruenceManager::watchedVariableCannotBeZero(Constraint c){ + ++(d_statistics.d_watchedVariableIsNotZero); + + ArithVar s = c->getVariable(); + + //Explain for conflict is correct as these proofs are generated and stored eagerly + //These will be safe for propagation later as well + Node reason = c->explainForConflict(); + + d_keepAlive.push_back(reason); + assertionToEqualityEngine(false, s, reason); +} + + +bool ArithCongruenceManager::propagate(TNode x){ + Debug("arith::congruenceManager")<< "ArithCongruenceManager::propagate("<()){ + return true; + }else{ + ++(d_statistics.d_conflicts); + + Node conf = explainInternal(x); + d_conflict.set(conf); + Debug("arith::congruenceManager") << "rewritten to false "<hasProof() << " " + << (x == rewritten) << " " + << c->canBePropagated() << " " + << c->negationHasProof() << std::endl; + + if(c->negationHasProof()){ + Node expC = explainInternal(x); + Node neg = c->getNegation()->explainForConflict(); + Node conf = expC.andNode(neg); + Node final = flattenAnd(conf); + + ++(d_statistics.d_conflicts); + d_conflict.set(final); + Debug("arith::congruenceManager") << "congruenceManager found a conflict " << final << std::endl; + return false; + } + + // Cases for propagation + // C : c has a proof + // S : x == rewritten + // P : c can be propagated + // + // CSP + // 000 : propagate x, and mark C it as being explained + // 001 : propagate x, and propagate c after marking it as being explained + // 01* : propagate x, mark c but do not propagate c + // 10* : propagate x, do not mark c and do not propagate c + // 11* : drop the constraint, do not propagate x or c + + if(!c->hasProof() && x != rewritten){ + pushBack(x, rewritten); + + c->setEqualityEngineProof(); + if(c->canBePropagated() && !c->assertedToTheTheory()){ + + ++(d_statistics.d_propagateConstraints); + c->propagate(); + } + }else if(!c->hasProof() && x == rewritten){ + pushBack(x, rewritten); + c->setEqualityEngineProof(); + }else if(c->hasProof() && x != rewritten){ + pushBack(x, rewritten); + }else{ + Assert(c->hasProof() && x == rewritten); + } + return true; +} + +void ArithCongruenceManager::explain(TNode literal, std::vector& 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.explainEquality(lhs, rhs, assumptions); +} + +void ArithCongruenceManager::enqueueIntoNB(const std::set s, NodeBuilder<>& nb){ + std::set::const_iterator it = s.begin(); + std::set::const_iterator it_end = s.end(); + for(; it != it_end; ++it) { + nb << *it; + } +} + +Node ArithCongruenceManager::explainInternal(TNode internal){ + std::vector assumptions; + explain(internal, assumptions); + + std::set assumptionSet; + assumptionSet.insert(assumptions.begin(), assumptions.end()); + + if (assumptionSet.size() == 1) { + // All the same, or just one + return assumptions[0]; + }else{ + NodeBuilder<> conjunction(kind::AND); + enqueueIntoNB(assumptionSet, conjunction); + return conjunction; + } +} +Node ArithCongruenceManager::explain(TNode external){ + Node internal = externalToInternal(external); + return explainInternal(internal); +} + +void ArithCongruenceManager::explain(TNode external, NodeBuilder<>& out){ + Node internal = externalToInternal(external); + + std::vector assumptions; + explain(internal, assumptions); + std::set assumptionSet; + assumptionSet.insert(assumptions.begin(), assumptions.end()); + + enqueueIntoNB(assumptionSet, out); +} + +void ArithCongruenceManager::addWatchedPair(ArithVar s, TNode x, TNode y){ + Assert(!isWatchedVariable(s)); + + Debug("arith::congruenceManager") + << "addWatchedPair(" << s << ", " << x << ", " << y << ")" << std::endl; + + + ++(d_statistics.d_watchedVariables); + + d_watchedVariables.add(s); + + Node eq = x.eqNode(y); + d_watchedEqualities[s] = eq; +} + +void ArithCongruenceManager::assertionToEqualityEngine(bool isEquality, ArithVar s, TNode reason){ + Assert(isWatchedVariable(s)); + + TNode eq = d_watchedEqualities[s]; + Assert(eq.getKind() == kind::EQUAL); + + TNode x = eq[0]; + TNode y = eq[1]; + + if(isEquality){ + d_ee.addEquality(x, y, reason); + }else{ + d_ee.addDisequality(x, y, reason); + } +} + +void ArithCongruenceManager::equalsConstant(Constraint c){ + Assert(c->isEquality()); + + ++(d_statistics.d_equalsConstantCalls); + Debug("equalsConstant") << "equals constant " << c << std::endl; + + ArithVar x = c->getVariable(); + Node xAsNode = d_av2Node.asNode(x); + Node asRational = mkRationalNode(c->getValue().getNoninfinitesimalPart()); + + + //No guarentee this is in normal form! + Node eq = xAsNode.eqNode(asRational); + d_keepAlive.push_back(eq); + + Node reason = c->explainForConflict(); + d_keepAlive.push_back(reason); + + d_ee.addEquality(xAsNode, asRational, reason); +} + +void ArithCongruenceManager::equalsConstant(Constraint lb, Constraint ub){ + Assert(lb->isLowerBound()); + Assert(ub->isUpperBound()); + Assert(lb->getVariable() == ub->getVariable()); + + ++(d_statistics.d_equalsConstantCalls); + Debug("equalsConstant") << "equals constant " << lb << std::endl + << ub << std::endl; + + ArithVar x = lb->getVariable(); + Node reason = ConstraintValue::explainConflict(lb,ub); + + Node xAsNode = d_av2Node.asNode(x); + Node asRational = mkRationalNode(lb->getValue().getNoninfinitesimalPart()); + + //No guarentee this is in normal form! + Node eq = xAsNode.eqNode(asRational); + d_keepAlive.push_back(eq); + d_keepAlive.push_back(reason); + + + d_ee.addEquality(xAsNode, asRational, reason); +} + +void ArithCongruenceManager::addSharedTerm(Node x){ + d_ee.addTriggerTerm(x); +} + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h new file mode 100644 index 000000000..e70773030 --- /dev/null +++ b/src/theory/arith/congruence_manager.h @@ -0,0 +1,216 @@ + + +#include "cvc4_private.h" + +#pragma once + +#include "theory/arith/arithvar.h" +#include "theory/arith/arithvar_set.h" +#include "theory/arith/arithvar_node_map.h" +#include "theory/arith/constraint_forward.h" + +#include "theory/uf/equality_engine.h" + +#include "context/cdo.h" +#include "context/cdlist.h" +#include "context/context.h" +#include "context/cdtrail_queue.h" +#include "context/cdmaybe.h" + +#include "util/stats.h" + +namespace CVC4 { +namespace theory { +namespace arith { + +class ArithCongruenceManager { +private: + context::CDMaybe d_conflict; + + /** + * The set of ArithVars equivalent to a pair of terms. + * If this is 0 or cannot be 0, this can be signalled. + * The pair of terms for the congruence is stored in watched equalities. + */ + PermissiveBackArithVarSet d_watchedVariables; + /** d_watchedVariables |-> (= x y) */ + ArithVarToNodeMap d_watchedEqualities; + + + class ArithCongruenceNotify { + private: + ArithCongruenceManager& d_acm; + public: + ArithCongruenceNotify(ArithCongruenceManager& acm): d_acm(acm) {} + + bool notify(TNode propagation) { + Debug("arith::congruences") << "ArithCongruenceNotify::notify(" << propagation << ")" << std::endl; + // Just forward to dm + return d_acm.propagate(propagation); + } + + void notify(TNode t1, TNode t2) { + Debug("arith::congruences") << "ArithCongruenceNotify::notify(" << t1 << ", " << t2 << ")" << std::endl; + Node equality = t1.eqNode(t2); + d_acm.propagate(equality); + } + }; + ArithCongruenceNotify d_notify; + + context::CDList d_keepAlive; + + /** Store the propagations. */ + context::CDTrailQueue d_propagatations; + + /* This maps the node a theory engine will request on an explain call to + * to its corresponding PropUnit. + * This is node is potentially both the propagation or + * Rewriter::rewrite(propagation). + */ + typedef context::CDHashMap ExplainMap; + ExplainMap d_explanationMap; + + ConstraintDatabase& d_constraintDatabase; + TNodeCallBack& d_setupLiteral; + + const ArithVarNodeMap& d_av2Node; + + theory::uf::EqualityEngine d_ee; + Node d_false; + +public: + + bool inConflict() const{ + return d_conflict.isSet(); + }; + + Node conflict() const{ + Assert(inConflict()); + return d_conflict.get(); + } + + bool hasMorePropagations() const { + return !d_propagatations.empty(); + } + + const Node getNextPropagation() { + Assert(hasMorePropagations()); + Node prop = d_propagatations.front(); + d_propagatations.dequeue(); + return prop; + } + + bool canExplain(TNode n) const { + return d_explanationMap.find(n) != d_explanationMap.end(); + } + +private: + Node externalToInternal(TNode n) const{ + Assert(canExplain(n)); + ExplainMap::const_iterator iter = d_explanationMap.find(n); + size_t pos = (*iter).second; + return d_propagatations[pos]; + } + + void pushBack(TNode n){ + d_explanationMap.insert(n, d_propagatations.size()); + d_propagatations.enqueue(n); + + ++(d_statistics.d_propagations); + } + + void pushBack(TNode n, TNode r){ + d_explanationMap.insert(r, d_propagatations.size()); + d_explanationMap.insert(n, d_propagatations.size()); + d_propagatations.enqueue(n); + + ++(d_statistics.d_propagations); + } + + bool propagate(TNode x); + void explain(TNode literal, std::vector& assumptions); + + /** + * This is set to true when the first shared term is added. + * When this is set to true in the context, d_queue is emptied + * and not used again in the context. + */ + //context::CDO d_hasSharedTerms; + + + /** + * The generalization of asserting an equality or a disequality. + * If there are shared equalities, this is added to the equality engine. + * Otherwise, this is put on a queue until there is a shared term. + */ + //void assertLiteral(bool eq, ArithVar s, TNode reason); + + /** This sends a shared term to the uninterpretted equality engine. */ + //void addAssertionToEqualityEngine(bool eq, ArithVar s, TNode reason); + void assertionToEqualityEngine(bool eq, ArithVar s, TNode reason); + + /** Dequeues the delay queue and asserts these equalities.*/ + void enableSharedTerms(); + void dequeueLiterals(); + + void enqueueIntoNB(const std::set all, NodeBuilder<>& nb); + + Node explainInternal(TNode internal); + +public: + + ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, TNodeCallBack&, const ArithVarNodeMap&); + + Node explain(TNode literal); + void explain(TNode lit, NodeBuilder<>& out); + + void addWatchedPair(ArithVar s, TNode x, TNode y); + + inline bool isWatchedVariable(ArithVar s) const { + return d_watchedVariables.isMember(s); + } + + /** Assert an equality. */ + void watchedVariableIsZero(Constraint eq); + + /** Assert a conjunction from lb and ub. */ + void watchedVariableIsZero(Constraint lb, Constraint ub); + + /** Assert that the value cannot be zero. */ + void watchedVariableCannotBeZero(Constraint c); + + /** Assert that the value cannot be zero. */ + void watchedVariableCannotBeZero(Constraint c, Constraint d); + + + /** Assert that the value is congruent to a constant. */ + void equalsConstant(Constraint eq); + void equalsConstant(Constraint lb, Constraint ub); + + + void addSharedTerm(Node x); + +private: + class Statistics { + public: + IntStat d_watchedVariables; + IntStat d_watchedVariableIsZero; + IntStat d_watchedVariableIsNotZero; + + IntStat d_equalsConstantCalls; + + IntStat d_propagations; + IntStat d_propagateConstraints; + IntStat d_conflicts; + + Statistics(); + ~Statistics(); + } d_statistics; + +};/* class CongruenceManager */ + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + + diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index f78ecdddf..460877a23 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -444,14 +444,13 @@ Constraint ConstraintValue::makeNegation(ArithVar v, ConstraintType t, const Del } } -ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Context* userContext, const ArithVarNodeMap& av2nodeMap, - DifferenceManager& dm) +ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Context* userContext, const ArithVarNodeMap& av2nodeMap, ArithCongruenceManager& cm) : d_varDatabases(), d_toPropagate(satContext), d_proofs(satContext, false), d_watches(new Watches(satContext, userContext)), d_av2nodeMap(av2nodeMap), - d_differenceManager(dm), + d_congruenceManager(cm), d_satContext(satContext), d_satAllocationLevel(d_satContext->getLevel()) { @@ -997,12 +996,12 @@ Constraint ConstraintDatabase::getBestImpliedBound(ArithVar v, ConstraintType t, } Node ConstraintDatabase::eeExplain(const ConstraintValue* const c) const{ Assert(c->hasLiteral()); - return d_differenceManager.explain(c->getLiteral()); + return d_congruenceManager.explain(c->getLiteral()); } void ConstraintDatabase::eeExplain(const ConstraintValue* const c, NodeBuilder<>& nb) const{ Assert(c->hasLiteral()); - d_differenceManager.explain(c->getLiteral(), nb); + d_congruenceManager.explain(c->getLiteral(), nb); } bool ConstraintDatabase::variableDatabaseIsSetup(ArithVar v) const { diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index e1939159b..2e0a9d067 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -77,7 +77,7 @@ #include "theory/arith/arithvar_node_map.h" #include "theory/arith/delta_rational.h" -#include "theory/arith/difference_manager.h" +#include "theory/arith/congruence_manager.h" #include "theory/arith/constraint_forward.h" @@ -746,7 +746,7 @@ private: return d_av2nodeMap; } - DifferenceManager& d_differenceManager; + ArithCongruenceManager& d_congruenceManager; //Constraint allocateConstraintForLiteral(ArithVar v, Node literal); @@ -760,7 +760,7 @@ public: ConstraintDatabase( context::Context* satContext, context::Context* userContext, const ArithVarNodeMap& av2nodeMap, - DifferenceManager& dm); + ArithCongruenceManager& dm); ~ConstraintDatabase(); diff --git a/src/theory/arith/difference_manager.cpp b/src/theory/arith/difference_manager.cpp deleted file mode 100644 index 70588bc16..000000000 --- a/src/theory/arith/difference_manager.cpp +++ /dev/null @@ -1,242 +0,0 @@ -#include "theory/arith/difference_manager.h" -#include "theory/uf/equality_engine_impl.h" - -#include "theory/arith/constraint.h" -#include "theory/arith/arith_utilities.h" - -namespace CVC4 { -namespace theory { -namespace arith { - -DifferenceManager::DifferenceManager(context::Context* c, ConstraintDatabase& cd, TNodeCallBack& setup) - : d_conflict(c), - d_literalsQueue(c), - d_propagatations(c), - d_explanationMap(c), - d_constraintDatabase(cd), - d_setupLiteral(setup), - d_notify(*this), - d_ee(d_notify, c, "theory::arith::DifferenceManager"), - d_false(NodeManager::currentNM()->mkConst(false)), - d_hasSharedTerms(c, false) -{} - -void DifferenceManager::differenceIsZero(Constraint lb, Constraint ub){ - Assert(lb->isLowerBound()); - Assert(ub->isUpperBound()); - Assert(lb->getVariable() == ub->getVariable()); - Assert(lb->getValue().sgn() == 0); - Assert(ub->getValue().sgn() == 0); - - ArithVar s = lb->getVariable(); - Node reason = ConstraintValue::explainConflict(lb,ub); - - assertLiteral(true, s, reason); -} - -void DifferenceManager::differenceIsZero(Constraint eq){ - Assert(eq->isEquality()); - Assert(eq->getValue().sgn() == 0); - - ArithVar s = eq->getVariable(); - - //Explain for conflict is correct as these proofs are generated and stored eagerly - //These will be safe for propagation later as well - Node reason = eq->explainForConflict(); - - assertLiteral(true, s, reason); -} - -void DifferenceManager::differenceCannotBeZero(Constraint c){ - ArithVar s = c->getVariable(); - - //Explain for conflict is correct as these proofs are generated and stored eagerly - //These will be safe for propagation later as well - Node reason = c->explainForConflict(); - assertLiteral(false, s, reason); -} - - -bool DifferenceManager::propagate(TNode x){ - Debug("arith::differenceManager")<< "DifferenceManager::propagate("<hasProof() << " " - << (x == rewritten) << " " - << c->canBePropagated() << " " - << c->negationHasProof() << std::endl; - - if(c->negationHasProof()){ - Node expC = explainInternal(x); - Node neg = c->getNegation()->explainForConflict(); - Node conf = expC.andNode(neg); - Node final = flattenAnd(conf); - - d_conflict.set(final); - Debug("arith::differenceManager") << "differenceManager found a conflict " << final << std::endl; - return false; - } - - // Cases for propagation - // C : c has a proof - // S : x == rewritten - // P : c can be propagated - // - // CSP - // 000 : propagate x, and mark C it as being explained - // 001 : propagate x, and propagate c after marking it as being explained - // 01* : propagate x, mark c but do not propagate c - // 10* : propagate x, do not mark c and do not propagate c - // 11* : drop the constraint, do not propagate x or c - - if(!c->hasProof() && x != rewritten){ - pushBack(x, rewritten); - - c->setEqualityEngineProof(); - if(c->canBePropagated() && !c->assertedToTheTheory()){ - c->propagate(); - } - }else if(!c->hasProof() && x == rewritten){ - pushBack(x, rewritten); - c->setEqualityEngineProof(); - }else if(c->hasProof() && x != rewritten){ - pushBack(x, rewritten); - }else{ - Assert(c->hasProof() && x == rewritten); - } - return true; -} - -void DifferenceManager::explain(TNode literal, std::vector& 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.explainEquality(lhs, rhs, assumptions); -} - -void DifferenceManager::enqueueIntoNB(const std::set s, NodeBuilder<>& nb){ - std::set::const_iterator it = s.begin(); - std::set::const_iterator it_end = s.end(); - for(; it != it_end; ++it) { - nb << *it; - } -} - -Node DifferenceManager::explainInternal(TNode internal){ - std::vector assumptions; - explain(internal, assumptions); - - std::set assumptionSet; - assumptionSet.insert(assumptions.begin(), assumptions.end()); - - if (assumptionSet.size() == 1) { - // All the same, or just one - return assumptions[0]; - }else{ - NodeBuilder<> conjunction(kind::AND); - enqueueIntoNB(assumptionSet, conjunction); - return conjunction; - } -} -Node DifferenceManager::explain(TNode external){ - Node internal = externalToInternal(external); - return explainInternal(internal); -} - -void DifferenceManager::explain(TNode external, NodeBuilder<>& out){ - Node internal = externalToInternal(external); - - std::vector assumptions; - explain(internal, assumptions); - std::set assumptionSet; - assumptionSet.insert(assumptions.begin(), assumptions.end()); - - enqueueIntoNB(assumptionSet, out); -} - -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::addAssertionToEqualityEngine(bool eq, ArithVar s, TNode reason){ - Assert(isDifferenceSlack(s)); - - TNode x = d_differences[s].x; - TNode y = d_differences[s].y; - - if(eq){ - d_ee.addEquality(x, y, reason); - }else{ - d_ee.addDisequality(x, y, reason); - } -} - -void DifferenceManager::dequeueLiterals(){ - Assert(d_hasSharedTerms); - while(!d_literalsQueue.empty() && !inConflict()){ - const LiteralsQueueElem& front = d_literalsQueue.front(); - d_literalsQueue.dequeue(); - - addAssertionToEqualityEngine(front.d_eq, front.d_var, front.d_reason); - } -} - -void DifferenceManager::enableSharedTerms(){ - Assert(!d_hasSharedTerms); - d_hasSharedTerms = true; - dequeueLiterals(); -} - -void DifferenceManager::assertLiteral(bool eq, ArithVar s, TNode reason){ - d_literalsQueue.enqueue(LiteralsQueueElem(eq, s, reason)); - if(d_hasSharedTerms){ - dequeueLiterals(); - } -} - -void DifferenceManager::addSharedTerm(Node x){ - if(!d_hasSharedTerms){ - enableSharedTerms(); - } - 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 deleted file mode 100644 index 7862a6b31..000000000 --- a/src/theory/arith/difference_manager.h +++ /dev/null @@ -1,224 +0,0 @@ - - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H -#define __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H - -#include "theory/arith/arithvar.h" -#include "theory/arith/constraint_forward.h" -#include "theory/uf/equality_engine.h" -#include "context/cdo.h" -#include "context/cdlist.h" -#include "context/context.h" -#include "context/cdtrail_queue.h" -#include "util/stats.h" - -namespace CVC4 { -namespace theory { -namespace arith { - -/** - * This implements a CDMaybe. - * This has either been set in the context or it has not. - * T must have a default constructor and support assignment. - */ -template -class CDMaybe { -private: - typedef std::pair BoolTPair; - context::CDO d_data; - -public: - CDMaybe(context::Context* c) : d_data(c, std::make_pair(false, T())) - {} - - bool isSet() const { - return d_data.get().first; - } - - void set(const T& d){ - Assert(!isSet()); - d_data.set(std::make_pair(true, d)); - } - - const T& get() const{ - Assert(isSet()); - return d_data.get().second; - } -}; - -class DifferenceManager { -private: - CDMaybe d_conflict; - - 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 - return d_dm.propagate(propagation); - } - - 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; - - struct LiteralsQueueElem { - bool d_eq; - ArithVar d_var; - Node d_reason; - LiteralsQueueElem() : d_eq(false), d_var(ARITHVAR_SENTINEL), d_reason() {} - LiteralsQueueElem(bool eq, ArithVar v, Node n) : d_eq(eq), d_var(v), d_reason(n) {} - }; - - /** Stores the queue of assertions. This keeps the Node backing the reasons */ - context::CDTrailQueue d_literalsQueue; - //PropManager& d_queue; - - /** Store the propagations. */ - context::CDTrailQueue d_propagatations; - - /* This maps the node a theory engine will request on an explain call to - * to its corresponding PropUnit. - * This is node is potentially both the propagation or Rewriter::rewrite(propagation). - */ - typedef context::CDHashMap ExplainMap; - ExplainMap d_explanationMap; - - ConstraintDatabase& d_constraintDatabase; - TNodeCallBack& d_setupLiteral; - -public: - - bool inConflict() const{ - return d_conflict.isSet(); - }; - - Node conflict() const{ - Assert(inConflict()); - return d_conflict.get(); - } - - bool hasMorePropagations() const { - return !d_propagatations.empty(); - } - - const Node getNextPropagation() { - Assert(hasMorePropagations()); - Node prop = d_propagatations.front(); - d_propagatations.dequeue(); - return prop; - } - - bool canExplain(TNode n) const { - return d_explanationMap.find(n) != d_explanationMap.end(); - } - -private: - Node externalToInternal(TNode n) const{ - Assert(canExplain(n)); - size_t pos = (*(d_explanationMap.find(n))).second; - return d_propagatations[pos]; - } - - void pushBack(TNode n){ - d_explanationMap.insert(n, d_propagatations.size()); - d_propagatations.enqueue(n); - } - - void pushBack(TNode n, TNode r){ - d_explanationMap.insert(r, d_propagatations.size()); - d_explanationMap.insert(n, d_propagatations.size()); - d_propagatations.enqueue(n); - } - - DifferenceNotifyClass d_notify; - theory::uf::EqualityEngine d_ee; - - bool propagate(TNode x); - void explain(TNode literal, std::vector& assumptions); - - Node d_false; - - /** - * This is set to true when the first shared term is added. - * When this is set to true in the context, d_queue is emptied - * and not used again in the context. - */ - context::CDO d_hasSharedTerms; - - - /** - * The generalization of asserting an equality or a disequality. - * If there are shared equalities, this is added to the equality engine. - * Otherwise, this is put on a queue until there is a shared term. - */ - void assertLiteral(bool eq, ArithVar s, TNode reason); - - /** This sends a shared term to the uninterpretted equality engine. */ - void addAssertionToEqualityEngine(bool eq, ArithVar s, TNode reason); - - /** Dequeues the delay queue and asserts these equalities.*/ - void enableSharedTerms(); - void dequeueLiterals(); - - void enqueueIntoNB(const std::set all, NodeBuilder<>& nb); - - Node explainInternal(TNode internal); - -public: - - DifferenceManager(context::Context* satContext, ConstraintDatabase&, TNodeCallBack&); - - Node explain(TNode literal); - void explain(TNode lit, NodeBuilder<>& out); - - 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; - } - } - - /** Assert an equality. */ - void differenceIsZero(Constraint eq); - - /** Assert a conjunction from lb and ub. */ - void differenceIsZero(Constraint lb, Constraint ub); - - /** Assert that the value cannot be zero. */ - void differenceCannotBeZero(Constraint c); - - 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/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 502a92962..bc8861996 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -72,9 +72,9 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha d_tableauResetPeriod(10), d_conflicts(c), d_conflictCallBack(d_conflicts), - d_differenceManager(c, d_constraintDatabase, d_setupLiteralCallback), + d_congruenceManager(c, d_constraintDatabase, d_setupLiteralCallback, d_arithvarNodeMap), d_simplex(d_linEq, d_conflictCallBack), - d_constraintDatabase(c, u, d_arithvarNodeMap, d_differenceManager), + d_constraintDatabase(c, u, d_arithvarNodeMap, d_congruenceManager), d_basicVarModelUpdateCallBack(d_simplex), d_DELTA_ZERO(0), d_statistics() @@ -151,7 +151,7 @@ TheoryArith::Statistics::~Statistics(){ } void TheoryArith::zeroDifferenceDetected(ArithVar x){ - Assert(d_differenceManager.isDifferenceSlack(x)); + Assert(d_congruenceManager.isWatchedVariable(x)); Assert(d_partialModel.upperBoundIsZero(x)); Assert(d_partialModel.lowerBoundIsZero(x)); @@ -159,11 +159,11 @@ void TheoryArith::zeroDifferenceDetected(ArithVar x){ Constraint ub = d_partialModel.getUpperBoundConstraint(x); if(lb->isEquality()){ - d_differenceManager.differenceIsZero(lb); + d_congruenceManager.watchedVariableIsZero(lb); }else if(ub->isEquality()){ - d_differenceManager.differenceIsZero(ub); + d_congruenceManager.watchedVariableIsZero(ub); }else{ - d_differenceManager.differenceIsZero(lb, ub); + d_congruenceManager.watchedVariableIsZero(lb, ub); } } @@ -195,6 +195,14 @@ Node TheoryArith::AssertLower(Constraint constraint){ if(isInteger(x_i)){ d_constantIntegerVariables.push_back(x_i); } + Constraint ub = d_partialModel.getUpperBoundConstraint(x_i); + + if(!d_congruenceManager.isWatchedVariable(x_i) || c_i.sgn() != 0){ + // if it is not a watched variable report it + // if it is is a watched variable and c_i == 0, + // let zeroDifferenceDetected(x_i) catch this + d_congruenceManager.equalsConstant(constraint, ub); + } const ValueCollection& vc = constraint->getValueCollection(); if(vc.hasDisequality()){ @@ -202,7 +210,7 @@ Node TheoryArith::AssertLower(Constraint constraint){ const Constraint eq = vc.getEquality(); const Constraint diseq = vc.getDisequality(); if(diseq->isTrue()){ - const Constraint ub = vc.getUpperBound(); + //const Constraint ub = vc.getUpperBound(); Node conflict = ConstraintValue::explainConflict(diseq, ub, constraint); ++(d_statistics.d_statDisequalityConflicts); @@ -217,10 +225,10 @@ Node TheoryArith::AssertLower(Constraint constraint){ d_partialModel.setLowerBoundConstraint(constraint); - if(d_differenceManager.isDifferenceSlack(x_i)){ + if(d_congruenceManager.isWatchedVariable(x_i)){ int sgn = c_i.sgn(); if(sgn > 0){ - d_differenceManager.differenceCannotBeZero(constraint); + d_congruenceManager.watchedVariableCannotBeZero(constraint); }else if(sgn == 0 && d_partialModel.upperBoundIsZero(x_i)){ zeroDifferenceDetected(x_i); } @@ -273,6 +281,13 @@ Node TheoryArith::AssertUpper(Constraint constraint){ if(isInteger(x_i)){ d_constantIntegerVariables.push_back(x_i); } + Constraint lb = d_partialModel.getLowerBoundConstraint(x_i); + if(!d_congruenceManager.isWatchedVariable(x_i) || c_i.sgn() != 0){ + // if it is not a watched variable report it + // if it is is a watched variable and c_i == 0, + // let zeroDifferenceDetected(x_i) catch this + d_congruenceManager.equalsConstant(lb, constraint); + } const ValueCollection& vc = constraint->getValueCollection(); if(vc.hasDisequality()){ @@ -280,7 +295,6 @@ Node TheoryArith::AssertUpper(Constraint constraint){ const Constraint diseq = vc.getDisequality(); const Constraint eq = vc.getEquality(); if(diseq->isTrue()){ - const Constraint lb = vc.getLowerBound(); Node conflict = ConstraintValue::explainConflict(diseq, lb, constraint); Debug("eq") << " assert upper conflict " << conflict << endl; return conflict; @@ -294,10 +308,10 @@ Node TheoryArith::AssertUpper(Constraint constraint){ d_partialModel.setUpperBoundConstraint(constraint); - if(d_differenceManager.isDifferenceSlack(x_i)){ + if(d_congruenceManager.isWatchedVariable(x_i)){ int sgn = c_i.sgn(); if(sgn < 0){ - d_differenceManager.differenceCannotBeZero(constraint); + d_congruenceManager.watchedVariableCannotBeZero(constraint); }else if(sgn == 0 && d_partialModel.lowerBoundIsZero(x_i)){ zeroDifferenceDetected(x_i); } @@ -370,16 +384,18 @@ Node TheoryArith::AssertEquality(Constraint constraint){ d_partialModel.setUpperBoundConstraint(constraint); d_partialModel.setLowerBoundConstraint(constraint); - if(d_differenceManager.isDifferenceSlack(x_i)){ + if(d_congruenceManager.isWatchedVariable(x_i)){ int sgn = c_i.sgn(); if(sgn == 0){ zeroDifferenceDetected(x_i); }else{ - d_differenceManager.differenceCannotBeZero(constraint); + d_congruenceManager.watchedVariableCannotBeZero(constraint); + d_congruenceManager.equalsConstant(constraint); } + }else{ + d_congruenceManager.equalsConstant(constraint); } - d_updatedBounds.softAdd(x_i); if(!d_tableau.isBasic(x_i)){ @@ -406,10 +422,10 @@ Node TheoryArith::AssertDisequality(Constraint constraint){ //Should be fine in integers Assert(!isInteger(x_i) || c_i.isIntegral()); - if(d_differenceManager.isDifferenceSlack(x_i)){ + if(d_congruenceManager.isWatchedVariable(x_i)){ int sgn = c_i.sgn(); if(sgn == 0){ - d_differenceManager.differenceCannotBeZero(constraint); + d_congruenceManager.watchedVariableCannotBeZero(constraint); } } @@ -444,7 +460,7 @@ Node TheoryArith::AssertDisequality(Constraint constraint){ if(c_i == d_partialModel.getAssignment(x_i)){ - Debug("eq") << "lemma now!" << endl; + Debug("eq") << "lemma now! " << constraint << endl; d_out->lemma(constraint->split()); return Node::null(); }else if(d_partialModel.strictlyLessThanLowerBound(x_i, c_i)){ @@ -460,7 +476,7 @@ Node TheoryArith::AssertDisequality(Constraint constraint){ } void TheoryArith::addSharedTerm(TNode n){ - d_differenceManager.addSharedTerm(n); + d_congruenceManager.addSharedTerm(n); if(!n.isConst() && !isSetup(n)){ Polynomial poly = Polynomial::parsePolynomial(n); Polynomial::iterator it = poly.begin(); @@ -713,7 +729,7 @@ void TheoryArith::setupPolynomial(const Polynomial& poly) { VarList vl0 = first.getVarList(); VarList vl1 = second.getVarList(); if(vl0.singleton() && vl1.singleton()){ - d_differenceManager.addDifference(varSlack, vl0.getNode(), vl1.getNode()); + d_congruenceManager.addWatchedPair(varSlack, vl0.getNode(), vl1.getNode()); } } } @@ -1137,8 +1153,8 @@ void TheoryArith::check(Effort effortLevel){ d_out->conflict(possibleConflict); return; } - if(d_differenceManager.inConflict()){ - Node c = d_differenceManager.conflict(); + if(d_congruenceManager.inConflict()){ + Node c = d_congruenceManager.conflict(); d_partialModel.revertAssignmentChanges(); Debug("arith::conflict") << "difference manager conflict " << c << endl; clearUpdates(); @@ -1344,9 +1360,9 @@ Node TheoryArith::explain(TNode n) { Debug("arith::explain") << "constraint explanation" << n << ":" << exp << endl; return exp; }else{ - Assert(d_differenceManager.canExplain(n)); + Assert(d_congruenceManager.canExplain(n)); Debug("arith::explain") << "dm explanation" << n << endl; - return d_differenceManager.explain(n); + return d_congruenceManager.explain(n); } } @@ -1379,8 +1395,8 @@ void TheoryArith::propagate(Effort e) { } } - while(d_differenceManager.hasMorePropagations()){ - TNode toProp = d_differenceManager.getNextPropagation(); + while(d_congruenceManager.hasMorePropagations()){ + TNode toProp = d_congruenceManager.getNextPropagation(); //Currently if the flag is set this came from an equality detected by the //equality engine in the the difference manager. @@ -1391,7 +1407,7 @@ void TheoryArith::propagate(Effort e) { Debug("arith::prop") << "propagating on non-constraint? " << toProp << endl; d_out->propagate(toProp); }else if(constraint->negationHasProof()){ - Node exp = d_differenceManager.explain(toProp); + Node exp = d_congruenceManager.explain(toProp); Node notNormalized = normalized.getKind() == NOT ? normalized[0] : normalized.notNode(); Node lp = flattenAnd(exp.andNode(notNormalized)); diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 4a5c398bd..3ed1d1941 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -38,7 +38,7 @@ #include "theory/arith/arith_static_learner.h" #include "theory/arith/arithvar_node_map.h" #include "theory/arith/dio_solver.h" -#include "theory/arith/difference_manager.h" +#include "theory/arith/congruence_manager.h" #include "theory/arith/constraint.h" @@ -241,14 +241,8 @@ private: */ Tableau d_smallTableauCopy; - /** - * The atom database keeps track of the atoms that have been preregistered. - * Used to add unate propagations. - */ - //ArithAtomDatabase d_atomDatabase; - /** This keeps track of difference equalities. Mostly for sharing. */ - DifferenceManager d_differenceManager; + ArithCongruenceManager d_congruenceManager; /** This implements the Simplex decision procedure. */ SimplexDecisionProcedure d_simplex; diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am index 4817582c0..0418fc3e9 100644 --- a/test/regress/regress0/uflra/Makefile.am +++ b/test/regress/regress0/uflra/Makefile.am @@ -13,6 +13,7 @@ MAKEFLAGS = -k # Regression tests for SMT inputs SMT_TESTS = \ + constants0.smt \ simple.01.cvc \ simple.02.cvc \ simple.03.cvc \ diff --git a/test/regress/regress0/uflra/constants0.smt b/test/regress/regress0/uflra/constants0.smt new file mode 100644 index 000000000..b07a6bc4e --- /dev/null +++ b/test/regress/regress0/uflra/constants0.smt @@ -0,0 +1,15 @@ +(benchmark mathsat +:logic QF_UFLRA +:status unsat +:category { crafted } +:extrafuns ((f Real Real)) +:extrafuns ((x Real)) +:extrafuns ((y Real)) +:formula +(and (or (= x 3) (= x 5)) + (or (= y 3) (= y 5)) + (not (= (f x) (f y))) + (implies (= (f 3) (f x)) (= (f 5) (f x))) + (implies (= (f 3) (f y)) (= (f 5) (f y))) +) +) \ No newline at end of file