diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/arith_utilities.h | 2 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 115 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 3 | ||||
-rw-r--r-- | src/theory/output_channel.h | 11 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 13 |
5 files changed, 90 insertions, 54 deletions
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index d50c48552..25aff4e75 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -237,10 +237,12 @@ inline int deltaCoeff(Kind k){ case kind::EQUAL: return kind::DISTINCT; default: + Unreachable(); return kind::UNDEFINED_KIND; } } default: + Unreachable(); return kind::UNDEFINED_KIND; } } diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 181632812..7b768d9af 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -103,21 +103,8 @@ ArithVar TheoryArith::findBasicRow(ArithVar variable){ void TheoryArith::preRegisterTerm(TNode n) { Debug("arith_preregister") <<"begin arith::preRegisterTerm("<< n <<")"<< endl; Kind k = n.getKind(); - if(k == EQUAL){ - TNode left = n[0]; - TNode right = n[1]; - - Node lt = NodeManager::currentNM()->mkNode(LT, left,right); - Node gt = NodeManager::currentNM()->mkNode(GT, left,right); - Node eagerSplit = NodeManager::currentNM()->mkNode(OR, n, lt, gt); - - d_splits.push_back(eagerSplit); - - d_out->augmentingLemma(eagerSplit); - } - - bool isStrictlyVarList = n.getKind() == kind::MULT && VarList::isMember(n); + bool isStrictlyVarList = k == kind::MULT && VarList::isMember(n); if(isStrictlyVarList){ d_out->setIncomplete(); @@ -307,15 +294,49 @@ bool TheoryArith::assertionCases(TNode assertion){ <<x_i<<" "<< simpKind <<" "<< c_i << ")" << std::endl; switch(simpKind){ case LEQ: + if (d_partialModel.hasLowerBound(x_i) && d_partialModel.getLowerBound(x_i) == c_i) { + Node diseq = assertion[0].eqNode(assertion[1]).notNode(); + if (d_diseq.find(diseq) != d_diseq.end()) { + NodeBuilder<3> conflict(kind::AND); + conflict << diseq << assertion << d_partialModel.getLowerConstraint(x_i); + d_out->conflict((TNode)conflict); + return true; + } + } case LT: return d_simplex.AssertUpper(x_i, c_i, assertion); - case GT: case GEQ: + if (d_partialModel.hasUpperBound(x_i) && d_partialModel.getUpperBound(x_i) == c_i) { + Node diseq = assertion[0].eqNode(assertion[1]).notNode(); + if (d_diseq.find(diseq) != d_diseq.end()) { + NodeBuilder<3> conflict(kind::AND); + conflict << diseq << assertion << d_partialModel.getUpperConstraint(x_i); + d_out->conflict((TNode)conflict); + return true; + } + } + case GT: return d_simplex.AssertLower(x_i, c_i, assertion); case EQUAL: return d_simplex.AssertEquality(x_i, c_i, assertion); case DISTINCT: - d_diseq.push_back(assertion); + { + d_diseq.insert(assertion); + // Check if it conflicts with the the bounds + TNode eq = assertion[0]; + Assert(eq.getKind() == kind::EQUAL); + TNode lhs = eq[0]; + TNode rhs = eq[1]; + Assert(rhs.getKind() == CONST_RATIONAL); + ArithVar lhsVar = determineLeftVariable(eq, kind::EQUAL); + DeltaRational rhsValue = determineRightConstant(eq, kind::EQUAL); + if (d_partialModel.hasLowerBound(lhsVar) && d_partialModel.hasUpperBound(lhsVar) && + d_partialModel.getLowerBound(lhsVar) == rhsValue && d_partialModel.getUpperBound(lhsVar) == rhsValue) { + NodeBuilder<3> conflict(kind::AND); + conflict << assertion << d_partialModel.getLowerConstraint(lhsVar) << d_partialModel.getUpperConstraint(lhsVar); + d_out->conflict((TNode)conflict); + } + } return false; default: Unreachable(); @@ -323,7 +344,7 @@ bool TheoryArith::assertionCases(TNode assertion){ } } -void TheoryArith::check(Effort level){ +void TheoryArith::check(Effort effortLevel){ Debug("arith") << "TheoryArith::check begun" << std::endl; while(!done()){ @@ -339,8 +360,25 @@ void TheoryArith::check(Effort level){ } } - //TODO This must be done everytime for the time being - if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); } + if(Debug.isOn("arith::print_assertions") && fullEffort(effortLevel)) { + Debug("arith::print_assertions") << "Assertions:" << endl; + for (ArithVar i = 0; i < d_variables.size(); ++ i) { + if (d_partialModel.hasLowerBound(i)) { + Node lConstr = d_partialModel.getLowerConstraint(i); + Debug("arith::print_assertions") << lConstr.toString() << endl; + } + + if (d_partialModel.hasUpperBound(i)) { + Node uConstr = d_partialModel.getUpperConstraint(i); + Debug("arith::print_assertions") << uConstr.toString() << endl; + } + } + context::CDSet<Node, NodeHashFunction>::iterator it = d_diseq.begin(); + context::CDSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end(); + for(; it != it_end; ++ it) { + Debug("arith::print_assertions") << *it << endl; + } + } Node possibleConflict = d_simplex.updateInconsistentVars(); if(possibleConflict != Node::null()){ @@ -355,10 +393,36 @@ void TheoryArith::check(Effort level){ Debug("arith_conflict") <<"Found a conflict "<< possibleConflict << endl; }else{ d_partialModel.commitAssignmentChanges(); + + if (fullEffort(effortLevel)) { + context::CDSet<Node, NodeHashFunction>::iterator it = d_diseq.begin(); + context::CDSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end(); + for(; it != it_end; ++ it) { + TNode eq = (*it)[0]; + Assert(eq.getKind() == kind::EQUAL); + TNode lhs = eq[0]; + TNode rhs = eq[1]; + Assert(rhs.getKind() == CONST_RATIONAL); + ArithVar lhsVar = determineLeftVariable(eq, kind::EQUAL); + if(d_tableau.isEjected(lhsVar)){ + d_simplex.reinjectVariable(lhsVar); + } + DeltaRational lhsValue = d_partialModel.getAssignment(lhsVar); + DeltaRational rhsValue = determineRightConstant(eq, kind::EQUAL); + if (lhsValue == rhsValue) { + Debug("arith_lemma") << "Splitting on " << eq << endl; + Debug("arith_lemma") << "LHS value = " << lhsValue << endl; + Debug("arith_lemma") << "RHS value = " << rhsValue << endl; + Node ltNode = NodeBuilder<2>(kind::LT) << lhs << rhs; + Node gtNode = NodeBuilder<2>(kind::GT) << lhs << rhs; + Node lemma = NodeBuilder<3>(OR) << eq << ltNode << gtNode; + d_out->lemma(lemma); + } + } + } } if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); } - Debug("arith") << "TheoryArith::check end" << std::endl; if(Debug.isOn("arith::print_model")) { @@ -372,17 +436,6 @@ void TheoryArith::check(Effort level){ Debug("arith::print_model") << endl; } } - if(Debug.isOn("arith::print_assertions")) { - Debug("arith::print_assertions") << "Assertions:" << endl; - for (ArithVar i = 0; i < d_variables.size(); ++ i) { - Node lConstr = d_partialModel.getLowerConstraint(i); - Debug("arith::print_assertions") << lConstr.toString() << endl; - - Node uConstr = d_partialModel.getUpperConstraint(i); - Debug("arith::print_assertions") << uConstr.toString() << endl; - - } - } } void TheoryArith::explain(TNode n, Effort e) { diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index af52da444..5c65b993d 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -24,6 +24,7 @@ #include "theory/theory.h" #include "context/context.h" #include "context/cdlist.h" +#include "context/cdset.h" #include "expr/node.h" #include "theory/arith/arith_utilities.h" @@ -86,7 +87,7 @@ private: /** * List of all of the inequalities asserted in the current context. */ - context::CDList<Node> d_diseq; + context::CDSet<Node, NodeHashFunction> d_diseq; /** * The tableau for all of the constraints seen thus far in the system. diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 1c48c0160..269f28732 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -100,17 +100,6 @@ public: throw(Interrupted, AssertionException) = 0; /** - * Tell the core to add the following valid lemma as if it were a - * user assertion. This should NOT be called during solving, only - * preprocessing. - * - * @param n - a theory lemma valid to be asserted - * @param safe - whether it is safe to be interrupted - */ - virtual void augmentingLemma(TNode n, bool safe = false) - throw(Interrupted, AssertionException) = 0; - - /** * Provide an explanation in response to an explanation request. * * @param n - an explanation diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index b2f047824..7958d977e 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -106,11 +106,7 @@ class TheoryEngine { ++(d_engine->d_statistics.d_statLemma); d_engine->newLemma(node); } - void augmentingLemma(TNode node, bool) - throw(theory::Interrupted, AssertionException) { - ++(d_engine->d_statistics.d_statAugLemma); - d_engine->newAugmentingLemma(node); - } + void explanation(TNode explanationNode, bool) throw(theory::Interrupted, AssertionException) { d_explanationNode = explanationNode; @@ -322,12 +318,7 @@ public: } inline void newLemma(TNode node) { - d_propEngine->assertLemma(node); - } - - inline void newAugmentingLemma(TNode node) { - Node preprocessed = preprocess(node); - d_propEngine->assertFormula(preprocessed); + d_propEngine->assertLemma(preprocess(node)); } /** |