From c0f5194dd56c5127c5c6dab5e59997eccc2d78a5 Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 24 Apr 2012 18:36:40 +0000 Subject: [PATCH] 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 --- src/context/Makefile.am | 1 + src/context/cdmaybe.h | 65 ++++ src/theory/arith/Makefile.am | 4 +- src/theory/arith/congruence_manager.cpp | 322 ++++++++++++++++++ ...ference_manager.h => congruence_manager.h} | 164 +++++---- src/theory/arith/constraint.cpp | 9 +- src/theory/arith/constraint.h | 6 +- src/theory/arith/difference_manager.cpp | 242 ------------- src/theory/arith/theory_arith.cpp | 70 ++-- src/theory/arith/theory_arith.h | 10 +- test/regress/regress0/uflra/Makefile.am | 1 + test/regress/regress0/uflra/constants0.smt | 15 + 12 files changed, 536 insertions(+), 373 deletions(-) create mode 100644 src/context/cdmaybe.h create mode 100644 src/theory/arith/congruence_manager.cpp rename src/theory/arith/{difference_manager.h => congruence_manager.h} (53%) delete mode 100644 src/theory/arith/difference_manager.cpp create mode 100644 test/regress/regress0/uflra/constants0.smt 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/difference_manager.h b/src/theory/arith/congruence_manager.h similarity index 53% rename from src/theory/arith/difference_manager.h rename to src/theory/arith/congruence_manager.h index 7862a6b31..e70773030 100644 --- a/src/theory/arith/difference_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -2,106 +2,70 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H -#define __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_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 { -/** - * 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 { +class ArithCongruenceManager { 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; - } -}; + context::CDMaybe d_conflict; -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); - } - }; + /** + * 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 DifferenceNotifyClass { + class ArithCongruenceNotify { private: - DifferenceManager& d_dm; + ArithCongruenceManager& d_acm; public: - DifferenceNotifyClass(DifferenceManager& dm): d_dm(dm) {} + ArithCongruenceNotify(ArithCongruenceManager& acm): d_acm(acm) {} bool notify(TNode propagation) { - Debug("arith::differences") << "DifferenceNotifyClass::notify(" << propagation << ")" << std::endl; + Debug("arith::congruences") << "ArithCongruenceNotify::notify(" << propagation << ")" << std::endl; // Just forward to dm - return d_dm.propagate(propagation); + return d_acm.propagate(propagation); } void notify(TNode t1, TNode t2) { - Debug("arith::differences") << "DifferenceNotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl; + Debug("arith::congruences") << "ArithCongruenceNotify::notify(" << t1 << ", " << t2 << ")" << std::endl; Node equality = t1.eqNode(t2); - d_dm.propagate(equality); + d_acm.propagate(equality); } }; + ArithCongruenceNotify d_notify; - 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; + 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). + * This is node is potentially both the propagation or + * Rewriter::rewrite(propagation). */ typedef context::CDHashMap ExplainMap; ExplainMap d_explanationMap; @@ -109,6 +73,11 @@ private: ConstraintDatabase& d_constraintDatabase; TNodeCallBack& d_setupLiteral; + const ArithVarNodeMap& d_av2Node; + + theory::uf::EqualityEngine d_ee; + Node d_false; + public: bool inConflict() const{ @@ -138,35 +107,35 @@ public: private: Node externalToInternal(TNode n) const{ Assert(canExplain(n)); - size_t pos = (*(d_explanationMap.find(n))).second; + 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); - } - DifferenceNotifyClass d_notify; - theory::uf::EqualityEngine d_ee; + ++(d_statistics.d_propagations); + } 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; + //context::CDO d_hasSharedTerms; /** @@ -174,10 +143,11 @@ private: * 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); + //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 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(); @@ -189,36 +159,58 @@ private: public: - DifferenceManager(context::Context* satContext, ConstraintDatabase&, TNodeCallBack&); + ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, TNodeCallBack&, const ArithVarNodeMap&); Node explain(TNode literal); void explain(TNode lit, NodeBuilder<>& out); - void addDifference(ArithVar s, Node x, Node y); + void addWatchedPair(ArithVar s, TNode x, TNode y); - inline bool isDifferenceSlack(ArithVar s) const{ - if(s < d_differences.size()){ - return d_differences[s].isSlack; - }else{ - return false; - } + inline bool isWatchedVariable(ArithVar s) const { + return d_watchedVariables.isMember(s); } /** Assert an equality. */ - void differenceIsZero(Constraint eq); + void watchedVariableIsZero(Constraint eq); /** Assert a conjunction from lb and ub. */ - void differenceIsZero(Constraint lb, Constraint 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 differenceCannotBeZero(Constraint c); + 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); -};/* class DifferenceManager */ + +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 */ -#endif /* __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H */ 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/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 -- 2.30.2