diff options
Diffstat (limited to 'src/theory/arith/difference_manager.cpp')
-rw-r--r-- | src/theory/arith/difference_manager.cpp | 242 |
1 files changed, 0 insertions, 242 deletions
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<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 */ |