cdcirclist.h \
cdcirclist_forward.h \
cdvector.h \
+ cdmaybe.h \
stacking_map.h \
stacking_vector.h
--- /dev/null
+/**
+ * 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<bool> 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 T>
+class CDMaybe {
+private:
+ typedef std::pair<bool, T> BoolTPair;
+ context::CDO<BoolTPair> 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<T> */
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
+
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 \
--- /dev/null
+#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("<<x<<")"<<std::endl;
+ if(inConflict()){
+ return true;
+ }
+
+ Node rewritten = Rewriter::rewrite(x);
+
+ //Need to still propagate this!
+ if(rewritten.getKind() == kind::CONST_BOOLEAN){
+ pushBack(x);
+
+ if(rewritten.getConst<bool>()){
+ return true;
+ }else{
+ ++(d_statistics.d_conflicts);
+
+ Node conf = explainInternal(x);
+ d_conflict.set(conf);
+ Debug("arith::congruenceManager") << "rewritten to false "<<x<<" with explanation "<< conf << std::endl;
+ return false;
+ }
+ }
+
+ Assert(rewritten.getKind() != kind::CONST_BOOLEAN);
+
+ Constraint c = d_constraintDatabase.lookup(rewritten);
+ if(c == NullConstraint){
+ //using setup as there may not be a corresponding congruence literal yet
+ d_setupLiteral(rewritten);
+ c = d_constraintDatabase.lookup(rewritten);
+ Assert(c != NullConstraint);
+ }
+
+ Debug("arith::congruenceManager")<< "x is "
+ << c->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<TNode>& 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<TNode> s, NodeBuilder<>& nb){
+ std::set<TNode>::const_iterator it = s.begin();
+ std::set<TNode>::const_iterator it_end = s.end();
+ for(; it != it_end; ++it) {
+ nb << *it;
+ }
+}
+
+Node ArithCongruenceManager::explainInternal(TNode internal){
+ std::vector<TNode> assumptions;
+ explain(internal, assumptions);
+
+ std::set<TNode> 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<TNode> assumptions;
+ explain(internal, assumptions);
+ std::set<TNode> 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 */
--- /dev/null
+
+
+#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<Node> 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<Node> d_keepAlive;
+
+ /** Store the propagations. */
+ context::CDTrailQueue<Node> 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<Node, size_t, NodeHashFunction> ExplainMap;
+ ExplainMap d_explanationMap;
+
+ ConstraintDatabase& d_constraintDatabase;
+ TNodeCallBack& d_setupLiteral;
+
+ const ArithVarNodeMap& d_av2Node;
+
+ theory::uf::EqualityEngine<ArithCongruenceNotify> 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<TNode>& 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<bool> 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<TNode> 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 */
+
+
}
}
-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())
{
}
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 {
#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"
return d_av2nodeMap;
}
- DifferenceManager& d_differenceManager;
+ ArithCongruenceManager& d_congruenceManager;
//Constraint allocateConstraintForLiteral(ArithVar v, Node literal);
ConstraintDatabase( context::Context* satContext,
context::Context* userContext,
const ArithVarNodeMap& av2nodeMap,
- DifferenceManager& dm);
+ ArithCongruenceManager& dm);
~ConstraintDatabase();
+++ /dev/null
-#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<bool>(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("<<x<<")"<<std::endl;
- if(inConflict()){
- return true;
- }
-
- Node rewritten = Rewriter::rewrite(x);
-
- //Need to still propagate this!
- if(rewritten.getKind() == kind::CONST_BOOLEAN){
- pushBack(x);
- }
-
- Assert(rewritten.getKind() != kind::CONST_BOOLEAN);
-
- Constraint c = d_constraintDatabase.lookup(rewritten);
- if(c == NullConstraint){
- //using setup as there may not be a corresponding difference literal yet
- d_setupLiteral(rewritten);
- c = d_constraintDatabase.lookup(rewritten);
- Assert(c != NullConstraint);
- //c = d_constraintDatabase.addLiteral(rewritten);
- }
-
- Debug("arith::differenceManager")<< "x is "
- << c->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<TNode>& 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<TNode> s, NodeBuilder<>& nb){
- std::set<TNode>::const_iterator it = s.begin();
- std::set<TNode>::const_iterator it_end = s.end();
- for(; it != it_end; ++it) {
- nb << *it;
- }
-}
-
-Node DifferenceManager::explainInternal(TNode internal){
- std::vector<TNode> assumptions;
- explain(internal, assumptions);
-
- std::set<TNode> 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<TNode> assumptions;
- explain(internal, assumptions);
- std::set<TNode> 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 */
+++ /dev/null
-
-
-#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 T>
-class CDMaybe {
-private:
- typedef std::pair<bool, T> BoolTPair;
- context::CDO<BoolTPair> 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<Node> 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<LiteralsQueueElem> d_literalsQueue;
- //PropManager& d_queue;
-
- /** Store the propagations. */
- context::CDTrailQueue<Node> 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<Node, size_t, NodeHashFunction> 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<DifferenceNotifyClass> d_ee;
-
- bool propagate(TNode x);
- void explain(TNode literal, std::vector<TNode>& 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<bool> 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<TNode> 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 */
-
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()
}
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));
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);
}
}
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()){
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);
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);
}
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()){
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;
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);
}
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)){
//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);
}
}
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)){
}
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();
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());
}
}
}
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();
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);
}
}
}
}
- 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.
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));
#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"
*/
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;
# Regression tests for SMT inputs
SMT_TESTS = \
+ constants0.smt \
simple.01.cvc \
simple.02.cvc \
simple.03.cvc \
--- /dev/null
+(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
projects / cvc5.git / commitdiff