summaryrefslogtreecommitdiff
path: root/src/theory/arith/difference_manager.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/difference_manager.cpp')
-rw-r--r--src/theory/arith/difference_manager.cpp242
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback