From ec4e1bdba56565d6372cb19ded12c9cadc506870 Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 15 Nov 2010 21:15:45 +0000 Subject: [PATCH] This commit merges the arith-prop-opt branch into the main trunk. This was done by way of the intermediate branch arith-prop-tmp. Both arith-prop-opt and arith-prop-tmp will now be phased out. --- src/prop/prop_engine.cpp | 7 + src/prop/prop_engine.h | 1 + src/theory/arith/Makefile.am | 4 +- src/theory/arith/arith_propagator.cpp | 366 ------------------------- src/theory/arith/arith_propagator.h | 128 --------- src/theory/arith/ordered_set.h | 35 +++ src/theory/arith/theory_arith.cpp | 41 +-- src/theory/arith/theory_arith.h | 4 +- src/theory/arith/unate_propagator.cpp | 381 ++++++++++++++++++++++++++ src/theory/arith/unate_propagator.h | 125 +++++++++ src/theory/theory_engine.h | 2 +- src/theory/theory_test_utils.h | 6 + test/unit/theory/theory_arith_white.h | 123 +++------ 13 files changed, 623 insertions(+), 600 deletions(-) delete mode 100644 src/theory/arith/arith_propagator.cpp delete mode 100644 src/theory/arith/arith_propagator.h create mode 100644 src/theory/arith/ordered_set.h create mode 100644 src/theory/arith/unate_propagator.cpp create mode 100644 src/theory/arith/unate_propagator.h diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index d89b8ec2f..f3caead8b 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -87,6 +87,13 @@ void PropEngine::assertLemma(TNode node) { d_cnfStream->convertAndAssert(node, true, false); } +void PropEngine::assertSafeLemma(TNode node) { + if(d_inCheckSat){ + assertLemma(node); + }else{ + assertFormula(node); + } +} void PropEngine::printSatisfyingAssignment(){ const CnfStream::TranslationCache& transCache = diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index b43c2d859..c0483e943 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -103,6 +103,7 @@ public: * @param node the formula to assert */ void assertLemma(TNode node); + void assertSafeLemma(TNode node); /** * Checks the current context for satisfiability. diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 7d78b1e6c..aa566b307 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -25,8 +25,8 @@ libarith_la_SOURCES = \ simplex.cpp \ row_vector.h \ row_vector.cpp \ - arith_propagator.h \ - arith_propagator.cpp \ + unate_propagator.h \ + unate_propagator.cpp \ theory_arith.h \ theory_arith.cpp diff --git a/src/theory/arith/arith_propagator.cpp b/src/theory/arith/arith_propagator.cpp deleted file mode 100644 index bf14e882e..000000000 --- a/src/theory/arith/arith_propagator.cpp +++ /dev/null @@ -1,366 +0,0 @@ -/********************* */ -/*! \file arith_propagator.cpp - ** \verbatim - ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "theory/arith/arith_propagator.h" -#include "theory/arith/arith_utilities.h" - -#include - -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::theory::arith; -using namespace CVC4::theory::arith::propagator; - -using namespace CVC4::kind; - -using namespace std; - -ArithUnatePropagator::ArithUnatePropagator(context::Context* cxt) : - d_assertions(cxt), d_pendingAssertions(cxt,0) -{ } - - -bool acceptedKinds(Kind k){ - switch(k){ - case EQUAL: - case LEQ: - case GEQ: - return true; - default: - return false; - } -} - -void ArithUnatePropagator::addAtom(TNode atom){ - Assert(acceptedKinds(atom.getKind())); - - TNode left = atom[0]; - TNode right = atom[1]; - - if(!leftIsSetup(left)){ - setupLefthand(left); - } - - switch(atom.getKind()){ - case EQUAL: - { - OrderedBoundsList* eqList = left.getAttribute(propagator::PropagatorEqList()); - Assert(!eqList->contains(atom)); - eqList->append(atom); - break; - } - case LEQ: - { - OrderedBoundsList* leqList = left.getAttribute(propagator::PropagatorLeqList()); - Assert(! leqList->contains(atom)); - leqList->append(atom); - break; - } - break; - case GEQ: - { - OrderedBoundsList* geqList = left.getAttribute(propagator::PropagatorGeqList()); - Assert(! geqList->contains(atom)); - geqList->append(atom); - break; - } - default: - Unreachable(); - } -} -bool ArithUnatePropagator::leftIsSetup(TNode left){ - return left.hasAttribute(propagator::PropagatorEqList()); -} - -void ArithUnatePropagator::setupLefthand(TNode left){ - Assert(!leftIsSetup(left)); - - OrderedBoundsList* eqList = new OrderedBoundsList(); - OrderedBoundsList* geqList = new OrderedBoundsList(); - OrderedBoundsList* leqList = new OrderedBoundsList(); - - left.setAttribute(propagator::PropagatorEqList(), eqList); - left.setAttribute(propagator::PropagatorLeqList(), leqList); - left.setAttribute(propagator::PropagatorGeqList(), geqList); -} - -void ArithUnatePropagator::assertLiteral(TNode lit){ - - if(lit.getKind() == NOT){ - Assert(!lit[0].getAttribute(propagator::PropagatorMarked())); - lit[0].setAttribute(propagator::PropagatorMarked(), true); - }else{ - Assert(!lit.getAttribute(propagator::PropagatorMarked())); - lit.setAttribute(propagator::PropagatorMarked(), true); - } - d_assertions.push_back(lit); -} - -std::vector ArithUnatePropagator::getImpliedLiterals(){ - std::vector impliedButNotAsserted; - - while(d_pendingAssertions < d_assertions.size()){ - TNode assertion = d_assertions[d_pendingAssertions]; - d_pendingAssertions = d_pendingAssertions + 1; - - enqueueImpliedLiterals(assertion, impliedButNotAsserted); - } - - if(Debug.isOn("arith::propagator")){ - for(std::vector::iterator i = impliedButNotAsserted.begin(), - endIter = impliedButNotAsserted.end(); i != endIter; ++i){ - Node imp = *i; - Debug("arith::propagator") << explain(imp) << " (prop)-> " << imp << endl; - } - } - - return impliedButNotAsserted; -} - -/** This function is effectively a case split. */ -void ArithUnatePropagator::enqueueImpliedLiterals(TNode lit, std::vector& buffer){ - switch(lit.getKind()){ - case EQUAL: - enqueueEqualityImplications(lit, buffer); - break; - case LEQ: - enqueueUpperBoundImplications(lit, lit, buffer); - break; - case GEQ: - enqueueLowerBoundImplications(lit, lit, buffer); - break; - case NOT: - { - TNode under = lit[0]; - switch(under.getKind()){ - case EQUAL: - //Do nothing - break;; - case LEQ: - enqueueLowerBoundImplications(under, lit, buffer); - break; - case GEQ: - enqueueUpperBoundImplications(under, lit, buffer); - break; - default: - Unreachable(); - } - break; - } - default: - Unreachable(); - } -} - -/** - * An equality (x = c) has been asserted. - * In this case we can propagate everything by comparing against the other constants. - */ -void ArithUnatePropagator::enqueueEqualityImplications(TNode orig, std::vector& buffer){ - TNode left = orig[0]; - TNode right = orig[1]; - const Rational& c = right.getConst(); - - OrderedBoundsList* eqList = left.getAttribute(propagator::PropagatorEqList()); - OrderedBoundsList* leqList = left.getAttribute(propagator::PropagatorLeqList()); - OrderedBoundsList* geqList = left.getAttribute(propagator::PropagatorGeqList()); - - - /* (x = c) /\ (c !=d) => (x != d) */ - for(OrderedBoundsList::iterator i = eqList->begin(); i != eqList->end(); ++i){ - TNode eq = *i; - Assert(eq.getKind() == EQUAL); - if(!eq.getAttribute(propagator::PropagatorMarked())){ //Note that (x = c) is marked - Assert(eq[1].getConst() != c); - - eq.setAttribute(propagator::PropagatorMarked(), true); - - Node neq = NodeManager::currentNM()->mkNode(NOT, eq); - neq.setAttribute(propagator::PropagatorExplanation(), orig); - buffer.push_back(neq); - } - } - for(OrderedBoundsList::iterator i = leqList->begin(); i != leqList->end(); ++i){ - TNode leq = *i; - Assert(leq.getKind() == LEQ); - if(!leq.getAttribute(propagator::PropagatorMarked())){ - leq.setAttribute(propagator::PropagatorMarked(), true); - const Rational& d = leq[1].getConst(); - if(c <= d){ - /* (x = c) /\ (c <= d) => (x <= d) */ - leq.setAttribute(propagator::PropagatorExplanation(), orig); - buffer.push_back(leq); - }else{ - /* (x = c) /\ (c > d) => (x > d) */ - Node gt = NodeManager::currentNM()->mkNode(NOT, leq); - gt.setAttribute(propagator::PropagatorExplanation(), orig); - buffer.push_back(gt); - } - } - } - - for(OrderedBoundsList::iterator i = geqList->begin(); i != geqList->end(); ++i){ - TNode geq = *i; - Assert(geq.getKind() == GEQ); - if(!geq.getAttribute(propagator::PropagatorMarked())){ - geq.setAttribute(propagator::PropagatorMarked(), true); - const Rational& d = geq[1].getConst(); - if(c >= d){ - /* (x = c) /\ (c >= d) => (x >= d) */ - geq.setAttribute(propagator::PropagatorExplanation(), orig); - buffer.push_back(geq); - }else{ - /* (x = c) /\ (c >= d) => (x >= d) */ - Node lt = NodeManager::currentNM()->mkNode(NOT, geq); - lt.setAttribute(propagator::PropagatorExplanation(), orig); - buffer.push_back(lt); - } - } - } -} - -void ArithUnatePropagator::enqueueUpperBoundImplications(TNode atom, TNode orig, std::vector& buffer){ - - Assert(atom.getKind() == LEQ || (orig.getKind() == NOT && atom.getKind() == GEQ)); - - TNode left = atom[0]; - TNode right = atom[1]; - const Rational& c = right.getConst(); - - OrderedBoundsList* eqList = left.getAttribute(propagator::PropagatorEqList()); - OrderedBoundsList* leqList = left.getAttribute(propagator::PropagatorLeqList()); - OrderedBoundsList* geqList = left.getAttribute(propagator::PropagatorGeqList()); - - - //For every node (x <= d), we will restrict ourselves to look at the cases when (d >= c) - for(OrderedBoundsList::iterator i = leqList->lower_bound(atom); i != leqList->end(); ++i){ - TNode leq = *i; - Assert(leq.getKind() == LEQ); - if(!leq.getAttribute(propagator::PropagatorMarked())){ - leq.setAttribute(propagator::PropagatorMarked(), true); - const Rational& d = leq[1].getConst(); - Assert( c <= d ); - - leq.setAttribute(propagator::PropagatorExplanation(), orig); - buffer.push_back(leq); // (x<=c) /\ (c <= d) => (x <= d) - //Note that if c=d, that at the node is not marked this can only be reached when (x < c) - //So we do not have to worry about a circular dependency - }else if(leq != atom){ - break; //No need to examine the rest, this atom implies the rest of the possible propagataions - } - } - - for(OrderedBoundsList::iterator i = geqList->upper_bound(atom); i != geqList->end(); ++i){ - TNode geq = *i; - Assert(geq.getKind() == GEQ); - if(!geq.getAttribute(propagator::PropagatorMarked())){ - geq.setAttribute(propagator::PropagatorMarked(), true); - const Rational& d = geq[1].getConst(); - Assert( c < d ); - - Node lt = NodeManager::currentNM()->mkNode(NOT, geq); - lt.setAttribute(propagator::PropagatorExplanation(), orig); - buffer.push_back(lt); // x<=c /\ d > c => x < d - }else{ - break; //No need to examine this atom implies the rest - } - } - - for(OrderedBoundsList::iterator i = eqList->upper_bound(atom); i != eqList->end(); ++i){ - TNode eq = *i; - Assert(eq.getKind() == EQUAL); - if(!eq.getAttribute(propagator::PropagatorMarked())){ - eq.setAttribute(propagator::PropagatorMarked(), true); - const Rational& d = eq[1].getConst(); - Assert( c < d ); - - Node neq = NodeManager::currentNM()->mkNode(NOT, eq); - neq.setAttribute(propagator::PropagatorExplanation(), orig); - buffer.push_back(neq); // x<=c /\ c < d => x != d - } - } -} - -void ArithUnatePropagator::enqueueLowerBoundImplications(TNode atom, TNode orig, std::vector& buffer){ - - Assert(atom.getKind() == GEQ || (orig.getKind() == NOT && atom.getKind() == LEQ)); - - TNode left = atom[0]; - TNode right = atom[1]; - const Rational& c = right.getConst(); - - OrderedBoundsList* eqList = left.getAttribute(propagator::PropagatorEqList()); - OrderedBoundsList* leqList = left.getAttribute(propagator::PropagatorLeqList()); - OrderedBoundsList* geqList = left.getAttribute(propagator::PropagatorGeqList()); - - - for(OrderedBoundsList::reverse_iterator i = geqList->reverse_lower_bound(atom); - i != geqList->rend(); i++){ - TNode geq = *i; - Assert(geq.getKind() == GEQ); - if(!geq.getAttribute(propagator::PropagatorMarked())){ - geq.setAttribute(propagator::PropagatorMarked(), true); - const Rational& d = geq[1].getConst(); - Assert( c >= d ); - - geq.setAttribute(propagator::PropagatorExplanation(), orig); - buffer.push_back(geq); // x>=c /\ c >= d => x >= d - }else if(geq != atom){ - break; //No need to examine the rest, this atom implies the rest of the possible propagataions - } - } - - for(OrderedBoundsList::reverse_iterator i = leqList->reverse_upper_bound(atom); - i != leqList->rend(); ++i){ - TNode leq = *i; - Assert(leq.getKind() == LEQ); - if(!leq.getAttribute(propagator::PropagatorMarked())){ - leq.setAttribute(propagator::PropagatorMarked(), true); - const Rational& d = leq[1].getConst(); - Assert( c > d ); - - Node gt = NodeManager::currentNM()->mkNode(NOT, leq); - gt.setAttribute(propagator::PropagatorExplanation(), orig); - buffer.push_back(gt); // x>=c /\ d < c => x > d - }else{ - break; //No need to examine this atom implies the rest - } - } - - for(OrderedBoundsList::reverse_iterator i = eqList->reverse_upper_bound(atom); - i != eqList->rend(); ++i){ - TNode eq = *i; - Assert(eq.getKind() == EQUAL); - if(!eq.getAttribute(propagator::PropagatorMarked())){ - eq.setAttribute(propagator::PropagatorMarked(), true); - const Rational& d = eq[1].getConst(); - Assert( c > d ); - - Node neq = NodeManager::currentNM()->mkNode(NOT, eq); - neq.setAttribute(propagator::PropagatorExplanation(), orig); - buffer.push_back(neq); // x>=c /\ c > d => x != d - } - } - -} - -Node ArithUnatePropagator::explain(TNode lit){ - Assert(lit.hasAttribute(propagator::PropagatorExplanation())); - return lit.getAttribute(propagator::PropagatorExplanation()); -} diff --git a/src/theory/arith/arith_propagator.h b/src/theory/arith/arith_propagator.h deleted file mode 100644 index 8ea628f25..000000000 --- a/src/theory/arith/arith_propagator.h +++ /dev/null @@ -1,128 +0,0 @@ -/********************* */ -/*! \file arith_propagator.h - ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__ARITH__ARITH_PROPAGATOR_H -#define __CVC4__THEORY__ARITH__ARITH_PROPAGATOR_H - -#include "expr/node.h" -#include "context/cdlist.h" -#include "context/context.h" -#include "context/cdo.h" -#include "theory/arith/ordered_bounds_list.h" - -#include -#include - -namespace CVC4 { -namespace theory { -namespace arith { - -class ArithUnatePropagator { -private: - /** Index of assertions. */ - context::CDList d_assertions; - - /** Index of the last assertion in d_assertions to be asserted. */ - context::CDO d_pendingAssertions; - -public: - ArithUnatePropagator(context::Context* cxt); - - /** - * Adds a new atom for the propagator to watch. - * Atom is assumed to have been rewritten by TheoryArith::rewrite(). - */ - void addAtom(TNode atom); - - /** - * Informs the propagator that a literal has been asserted to the theory. - */ - void assertLiteral(TNode lit); - - - /** - * returns a vector of literals that are - */ - std::vector getImpliedLiterals(); - - /** Explains a literal that was asserted in the current context. */ - Node explain(TNode lit); - -private: - /** returns true if the left hand side side left has been setup. */ - bool leftIsSetup(TNode left); - - /** - * Sets up a left hand side. - * This initializes the attributes PropagatorEqList, PropagatorGeqList, and PropagatorLeqList for left. - */ - void setupLefthand(TNode left); - - /** - * Given that the literal lit is now asserted, - * enqueue additional entailed assertions in buffer. - */ - void enqueueImpliedLiterals(TNode lit, std::vector& buffer); - - void enqueueEqualityImplications(TNode original, std::vector& buffer); - void enqueueLowerBoundImplications(TNode atom, TNode original, std::vector& buffer); - /** - * Given that the literal original is now asserted, which is either (<= x c) or (not (>= x c)), - * enqueue additional entailed assertions in buffer. - */ - void enqueueUpperBoundImplications(TNode atom, TNode original, std::vector& buffer); -}; - - - -namespace propagator { - -/** Basic memory management wrapper for deleting PropagatorEqList, PropagatorGeqList, and PropagatorLeqList.*/ -struct ListCleanupStrategy{ - static void cleanup(OrderedBoundsList* l){ - Debug("arithgc") << "cleaning up " << l << "\n"; - delete l; - } -}; - - -struct PropagatorEqListID {}; -typedef expr::Attribute PropagatorEqList; - -struct PropagatorGeqListID {}; -typedef expr::Attribute PropagatorGeqList; - -struct PropagatorLeqListID {}; -typedef expr::Attribute PropagatorLeqList; - - -struct PropagatorMarkedID {}; -typedef expr::CDAttribute PropagatorMarked; - -struct PropagatorExplanationID {}; -typedef expr::CDAttribute PropagatorExplanation; -}/* CVC4::theory::arith::propagator */ - -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__ARITH__THEORY_ARITH_H */ diff --git a/src/theory/arith/ordered_set.h b/src/theory/arith/ordered_set.h new file mode 100644 index 000000000..fa606188a --- /dev/null +++ b/src/theory/arith/ordered_set.h @@ -0,0 +1,35 @@ +#include +#include "expr/kind.h" +#include "expr/node.h" +#include "util/Assert.h" + + +namespace CVC4 { +namespace theory { +namespace arith { + +struct RightHandRationalLT +{ + bool operator()(TNode s1, TNode s2) const + { + TNode rh1 = s1[1]; + TNode rh2 = s2[1]; + const Rational& c1 = rh1.getConst(); + const Rational& c2 = rh2.getConst(); + int cmpRes = c1.cmp(c2); + return cmpRes < 0; + } +}; + +typedef std::set OrderedSet; + +struct SetCleanupStrategy{ + static void cleanup(OrderedSet* l){ + Debug("arithgc") << "cleaning up " << l << "\n"; + delete l; + } +}; + +}/* 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 7cedbcd20..bf5f285a5 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -34,7 +34,7 @@ #include "theory/arith/arithvar_dense_set.h" #include "theory/arith/arith_rewriter.h" -#include "theory/arith/arith_propagator.h" +#include "theory/arith/unate_propagator.h" #include "theory/arith/theory_arith.h" #include "theory/arith/normal_form.h" @@ -62,7 +62,7 @@ TheoryArith::TheoryArith(int id, context::Context* c, OutputChannel& out) : d_diseq(c), d_tableau(d_activityMonitor, d_basicManager), d_rewriter(&d_constants), - d_propagator(c), + d_propagator(c, out), d_simplex(d_constants, d_partialModel, d_basicManager, d_out, d_activityMonitor, d_tableau), d_statistics() {} @@ -71,15 +71,21 @@ TheoryArith::~TheoryArith(){} TheoryArith::Statistics::Statistics(): d_statUserVariables("theory::arith::UserVariables", 0), - d_statSlackVariables("theory::arith::SlackVariables", 0) + d_statSlackVariables("theory::arith::SlackVariables", 0), + d_statDisequalitySplits("theory::arith::DisequalitySplits", 0), + d_statDisequalityConflicts("theory::arith::DisequalityConflicts", 0) { StatisticsRegistry::registerStat(&d_statUserVariables); StatisticsRegistry::registerStat(&d_statSlackVariables); + StatisticsRegistry::registerStat(&d_statDisequalitySplits); + StatisticsRegistry::registerStat(&d_statDisequalityConflicts); } TheoryArith::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_statUserVariables); StatisticsRegistry::unregisterStat(&d_statSlackVariables); + StatisticsRegistry::unregisterStat(&d_statDisequalitySplits); + StatisticsRegistry::unregisterStat(&d_statDisequalityConflicts); } @@ -299,6 +305,7 @@ bool TheoryArith::assertionCases(TNode assertion){ if (d_diseq.find(diseq) != d_diseq.end()) { NodeBuilder<3> conflict(kind::AND); conflict << diseq << assertion << d_partialModel.getLowerConstraint(x_i); + ++(d_statistics.d_statDisequalityConflicts); d_out->conflict((TNode)conflict); return true; } @@ -311,6 +318,7 @@ bool TheoryArith::assertionCases(TNode assertion){ if (d_diseq.find(diseq) != d_diseq.end()) { NodeBuilder<3> conflict(kind::AND); conflict << diseq << assertion << d_partialModel.getUpperConstraint(x_i); + ++(d_statistics.d_statDisequalityConflicts); d_out->conflict((TNode)conflict); return true; } @@ -351,7 +359,7 @@ void TheoryArith::check(Effort effortLevel){ Node assertion = get(); - d_propagator.assertLiteral(assertion); + //d_propagator.assertLiteral(assertion); bool conflictDuringAnAssert = assertionCases(assertion); if(conflictDuringAnAssert){ @@ -426,6 +434,7 @@ void TheoryArith::check(Effort effortLevel){ // All the implication Node impClosure = NodeBuilder<3>(kind::AND) << imp1 << imp2 << imp3; + ++(d_statistics.d_statDisequalitySplits); d_out->lemma(lemma.andNode(impClosure)); } } @@ -449,22 +458,22 @@ void TheoryArith::check(Effort effortLevel){ } void TheoryArith::explain(TNode n, Effort e) { - Node explanation = d_propagator.explain(n); - Debug("arith") << "arith::explain("<" - << explanation << endl; - d_out->explanation(explanation, true); + // Node explanation = d_propagator.explain(n); + // Debug("arith") << "arith::explain("<" + // << explanation << endl; + // d_out->explanation(explanation, true); } void TheoryArith::propagate(Effort e) { - if(quickCheckOrMore(e)){ - std::vector implied = d_propagator.getImpliedLiterals(); - for(std::vector::iterator i = implied.begin(); - i != implied.end(); - ++i){ - d_out->propagate(*i); - } - } + // if(quickCheckOrMore(e)){ + // std::vector implied = d_propagator.getImpliedLiterals(); + // for(std::vector::iterator i = implied.begin(); + // i != implied.end(); + // ++i){ + // d_out->propagate(*i); + // } + // } } Node TheoryArith::getValue(TNode n, TheoryEngine* engine) { diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 5c65b993d..81711a101 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -33,7 +33,7 @@ #include "theory/arith/tableau.h" #include "theory/arith/arith_rewriter.h" #include "theory/arith/partial_model.h" -#include "theory/arith/arith_propagator.h" +#include "theory/arith/unate_propagator.h" #include "theory/arith/simplex.h" #include "util/stats.h" @@ -176,6 +176,8 @@ private: class Statistics { public: IntStat d_statUserVariables, d_statSlackVariables; + IntStat d_statDisequalitySplits; + IntStat d_statDisequalityConflicts; Statistics(); ~Statistics(); diff --git a/src/theory/arith/unate_propagator.cpp b/src/theory/arith/unate_propagator.cpp new file mode 100644 index 000000000..38bc06555 --- /dev/null +++ b/src/theory/arith/unate_propagator.cpp @@ -0,0 +1,381 @@ +/********************* */ +/*! \file arith_propagator.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "theory/arith/unate_propagator.h" +#include "theory/arith/arith_utilities.h" + +#include + +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::arith; + +using namespace CVC4::kind; + +using namespace std; + +struct PropagatorLeqSetID {}; +typedef expr::Attribute PropagatorLeqSet; + +struct PropagatorEqSetID {}; +typedef expr::Attribute PropagatorEqSet; + +struct PropagatorGeqSetID {}; +typedef expr::Attribute PropagatorGeqSet; + +ArithUnatePropagator::ArithUnatePropagator(context::Context* cxt, OutputChannel& out) : + d_arithOut(out) +{ } + +bool ArithUnatePropagator::leftIsSetup(TNode left){ + return left.hasAttribute(PropagatorEqSet()); +} + +void ArithUnatePropagator::setupLefthand(TNode left){ + Assert(!leftIsSetup(left)); + + OrderedSet* eqList = new OrderedSet(); + OrderedSet* leqList = new OrderedSet(); + OrderedSet* geqList = new OrderedSet(); + + left.setAttribute(PropagatorEqSet(), eqList); + left.setAttribute(PropagatorLeqSet(), geqList); + left.setAttribute(PropagatorGeqSet(), leqList); +} + +void ArithUnatePropagator::addAtom(TNode atom){ + TNode left = atom[0]; + TNode right = atom[1]; + + if(!leftIsSetup(left)){ + setupLefthand(left); + } + + OrderedSet* eqSet = left.getAttribute(PropagatorEqSet()); + OrderedSet* leqSet = left.getAttribute(PropagatorLeqSet()); + OrderedSet* geqSet = left.getAttribute(PropagatorGeqSet()); + + switch(atom.getKind()){ + case EQUAL: + { + pair res = eqSet->insert(atom); + Assert(res.second); + addEqualityToEqualities(atom, eqSet, res.first); + addEqualityToLeqs(atom, leqSet); + addEqualityToGeqs(atom, geqSet); + break; + } + case LEQ: + { + pair res = leqSet->insert(atom); + Assert(res.second); + + addLeqToLeqs(atom, leqSet, res.first); + addLeqToEqualities(atom, eqSet); + addLeqToGeqs(atom, geqSet); + break; + } + case GEQ: + { + pair res = geqSet->insert(atom); + Assert(res.second); + + addGeqToGeqs(atom, geqSet, res.first); + addGeqToEqualities(atom, eqSet); + addGeqToLeqs(atom, leqSet); + + break; + } + default: + Unreachable(); + } +} + +bool rightHandRationalIsEqual(TNode a, TNode b){ + TNode secondA = a[1]; + TNode secondB = b[1]; + + const Rational& qA = secondA.getConst(); + const Rational& qB = secondB.getConst(); + + return qA == qB; +} +bool rightHandRationalIsLT(TNode a, TNode b){ + TNode secondA = a[1]; + TNode secondB = b[1]; + + const Rational& qA = secondA.getConst(); + const Rational& qB = secondB.getConst(); + + return qA < qB; +} + +void ArithUnatePropagator::addEqualityToEqualities(TNode atom, + OrderedSet* eqSet, + OrderedSet::iterator eqPos){ + Assert(atom.getKind() == EQUAL); + Node negation = NodeManager::currentNM()->mkNode(NOT, atom); + for(OrderedSet::iterator eqIter = eqSet->begin(); + eqIter != eqSet->end(); ++eqIter){ + if(eqIter == eqPos) continue; + TNode eq = *eqIter; + Assert(!rightHandRationalIsEqual(eq, atom)); + addImplication(eq, negation); + } +} + +void ArithUnatePropagator::addEqualityToLeqs(TNode atom, OrderedSet* leqSet) +{ + Assert(atom.getKind() == EQUAL); + Node negation = NodeManager::currentNM()->mkNode(NOT, atom); + + OrderedSet::iterator leqIter = leqSet->lower_bound(atom); + if(leqIter != leqSet->end()){ + TNode lowerBound = *leqIter; + if(rightHandRationalIsEqual(atom, lowerBound)){ + addImplication(atom, lowerBound); // x=b /\ b = b' => x <= b' + if(leqIter != leqSet->begin()){ + --leqIter; + Assert(rightHandRationalIsLT(*leqIter, atom)); + addImplication(*leqIter, negation); // x=b /\ b > b' => x > b' + } + }else{ + //probably wrong + Assert(rightHandRationalIsLT(atom, lowerBound)); + addImplication(atom, lowerBound);// x=b /\ b < b' => x <= b' + + if(leqIter != leqSet->begin()){ + --leqIter; + Assert(rightHandRationalIsLT(*leqIter, atom)); + addImplication(*leqIter, negation);// x=b /\ b > b' => x > b' + } + } + }else if(leqIter != leqSet->begin()){ + --leqIter; + TNode strictlyLessThan = *leqIter; + Assert(rightHandRationalIsLT(strictlyLessThan, atom)); + addImplication(*leqIter, negation); // x=b /\ b < b' => x <= b' + }else{ + Assert(leqSet->empty()); + } +} + +void ArithUnatePropagator::addEqualityToGeqs(TNode atom, OrderedSet* geqSet){ + + Assert(atom.getKind() == EQUAL); + Node negation = NodeManager::currentNM()->mkNode(NOT, atom); + + OrderedSet::iterator geqIter = geqSet->lower_bound(atom); + if(geqIter != geqSet->end()){ + TNode lowerBound = *geqIter; + if(rightHandRationalIsEqual(atom, lowerBound)){ + addImplication(atom, lowerBound); // x=b /\ b = b' => x >= b' + ++geqIter; + if(geqIter != geqSet->end()){ // x=b /\ b < b' => x < b' + TNode strictlyGt = *geqIter; + Assert(rightHandRationalIsLT( atom, strictlyGt )); + addImplication(strictlyGt, negation); + } + }else{ + Assert(rightHandRationalIsLT(atom, lowerBound)); + addImplication(lowerBound, negation);// x=b /\ b < b' => x < b' + if(geqIter != geqSet->begin()){ + --geqIter; + TNode strictlyLessThan = *geqIter; + Assert(rightHandRationalIsLT(strictlyLessThan, atom)); + addImplication(atom, strictlyLessThan);// x=b /\ b > b' => x >= b' + } + } + }else if(geqIter != geqSet->begin()){ + --geqIter; + TNode strictlyLT = *geqIter; + Assert(rightHandRationalIsLT(strictlyLT, atom)); + addImplication(atom, strictlyLT);// x=b /\ b > b' => x >= b' + }else{ + Assert(geqSet->empty()); + } +} + +void ArithUnatePropagator::addLeqToLeqs +(TNode atom, + OrderedSet* leqSet, + OrderedSet::iterator atomPos) +{ + Assert(atom.getKind() == LEQ); + Node negation = NodeManager::currentNM()->mkNode(NOT, atom); + + if(atomPos != leqSet->begin()){ + --atomPos; + TNode beforeLeq = *atomPos; + Assert(rightHandRationalIsLT(beforeLeq, atom)); + addImplication(beforeLeq, atom);// x<=b' /\ b' < b => x <= b + ++atomPos; + } + ++atomPos; + if(atomPos != leqSet->end()){ + TNode afterLeq = *atomPos; + Assert(rightHandRationalIsLT(atom, afterLeq)); + addImplication(atom, afterLeq);// x<=b /\ b < b' => x <= b' + } +} +void ArithUnatePropagator::addLeqToGeqs(TNode atom, OrderedSet* geqSet) { + + Assert(atom.getKind() == LEQ); + Node negation = NodeManager::currentNM()->mkNode(NOT, atom); + + OrderedSet::iterator geqIter = geqSet->lower_bound(atom); + if(geqIter != geqSet->end()){ + TNode lowerBound = *geqIter; + if(rightHandRationalIsEqual(atom, lowerBound)){ + Assert(rightHandRationalIsEqual(atom, lowerBound)); + addImplication(negation, lowerBound);// (x > b) => (x >= b) + ++geqIter; + if(geqIter != geqSet->end()){ + TNode next = *geqIter; + Assert(rightHandRationalIsLT(atom, next)); + addImplication(next, negation);// x>=b' /\ b' > b => x > b + } + }else{ + Assert(rightHandRationalIsLT(atom, lowerBound)); + addImplication(lowerBound, negation);// x>=b' /\ b' > b => x > b + if(geqIter != geqSet->begin()){ + --geqIter; + TNode prev = *geqIter; + Assert(rightHandRationalIsLT(prev, atom)); + addImplication(negation, prev);// (x>b /\ b > b') => x >= b' + } + } + }else if(geqIter != geqSet->begin()){ + --geqIter; + TNode strictlyLT = *geqIter; + Assert(rightHandRationalIsLT(strictlyLT, atom)); + addImplication(negation, strictlyLT);// (x>b /\ b > b') => x >= b' + }else{ + Assert(geqSet->empty()); + } +} + +void ArithUnatePropagator::addLeqToEqualities(TNode atom, OrderedSet* eqSet) { + Assert(atom.getKind() == LEQ); + Node negation = NodeManager::currentNM()->mkNode(NOT, atom); + + //TODO Improve this later + for(OrderedSet::iterator eqIter = eqSet->begin(); eqIter != eqSet->end(); ++eqIter){ + TNode eq = *eqIter; + if(rightHandRationalIsEqual(atom, eq)){ + // (x = b' /\ b = b') => x <= b + addImplication(eq, atom); + }else if(rightHandRationalIsLT(atom, eq)){ + // (x = b' /\ b' > b) => x > b + addImplication(eq, negation); + }else{ + // (x = b' /\ b' < b) => x <= b + addImplication(eq, atom); + } + } +} + + +void ArithUnatePropagator::addGeqToGeqs +(TNode atom, OrderedSet* geqSet, OrderedSet::iterator atomPos) +{ + Assert(atom.getKind() == GEQ); + Node negation = NodeManager::currentNM()->mkNode(NOT, atom); + + if(atomPos != geqSet->begin()){ + --atomPos; + TNode beforeGeq = *atomPos; + Assert(rightHandRationalIsLT(beforeGeq, atom)); + addImplication(atom, beforeGeq);// x>=b /\ b > b' => x >= b' + ++atomPos; + } + ++atomPos; + if(atomPos != geqSet->end()){ + TNode afterGeq = *atomPos; + Assert(rightHandRationalIsLT(atom, afterGeq)); + addImplication(afterGeq, atom);// x>=b' /\ b' > b => x >= b + } +} + +void ArithUnatePropagator::addGeqToLeqs(TNode atom, OrderedSet* leqSet){ + + Assert(atom.getKind() == GEQ); + Node negation = NodeManager::currentNM()->mkNode(NOT, atom); + + OrderedSet::iterator leqIter = leqSet->lower_bound(atom); + if(leqIter != leqSet->end()){ + TNode lowerBound = *leqIter; + if(rightHandRationalIsEqual(atom, lowerBound)){ + Assert(rightHandRationalIsEqual(atom, lowerBound)); + addImplication(negation, lowerBound);// (x < b) => (x <= b) + + if(leqIter != leqSet->begin()){ + --leqIter; + TNode prev = *leqIter; + Assert(rightHandRationalIsLT(prev, atom)); + addImplication(prev, negation);// x<=b' /\ b' < b => x < b + } + }else{ + Assert(rightHandRationalIsLT(atom, lowerBound)); + addImplication(negation, lowerBound);// (x < b /\ b < b') => x <= b' + ++leqIter; + if(leqIter != leqSet->end()){ + TNode next = *leqIter; + Assert(rightHandRationalIsLT(atom, next)); + addImplication(negation, next);// (x < b /\ b < b') => x <= b' + } + } + }else if(leqIter != leqSet->begin()){ + --leqIter; + TNode strictlyLT = *leqIter; + Assert(rightHandRationalIsLT(strictlyLT, atom)); + addImplication(strictlyLT, negation);// (x <= b' /\ b' < b) => x < b + }else{ + Assert(leqSet->empty()); + } +} +void ArithUnatePropagator::addGeqToEqualities(TNode atom, OrderedSet* eqSet){ + + Assert(atom.getKind() == GEQ); + Node negation = NodeManager::currentNM()->mkNode(NOT, atom); + + //TODO Improve this later + for(OrderedSet::iterator eqIter = eqSet->begin(); eqIter != eqSet->end(); ++eqIter){ + TNode eq = *eqIter; + if(rightHandRationalIsEqual(atom, eq)){ + // (x = b' /\ b = b') => x >= b + addImplication(eq, atom); + }else if(rightHandRationalIsLT(eq, atom)){ + // (x = b' /\ b' < b) => x < b + addImplication(eq, negation); + }else{ + // (x = b' /\ b' > b) => x >= b + addImplication(eq, atom); + } + } +} + +void ArithUnatePropagator::addImplication(TNode a, TNode b){ + Node imp = NodeBuilder<2>(IMPLIES) << a << b; + + Debug("arith-propagate") << "ArithUnatePropagator::addImplication"; + Debug("arith-propagate") << "(" << a << ", " << b <<")" << endl; + + d_arithOut.lemma(imp); +} diff --git a/src/theory/arith/unate_propagator.h b/src/theory/arith/unate_propagator.h new file mode 100644 index 000000000..88020b52b --- /dev/null +++ b/src/theory/arith/unate_propagator.h @@ -0,0 +1,125 @@ +/********************* */ +/*! \file arith_propagator.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief ArithUnatePropagator constructs implications of the form + ** "if x < c and c < b, then x < b" (where c and b are constants). + ** + ** ArithUnatePropagator detects unate implications amongst the atoms + ** associated with the theory of arithmetic and informs the SAT solver of the + ** implication. A unate implication is an implication of the form: + ** "if x < c and c < b, then x < b" (where c and b are constants). + ** Unate implications are always 2-SAT clauses. + ** ArithUnatePropagator sends the implications to the SAT solver in an + ** online fashion. + ** This means that atoms may be added during solving or before. + ** + ** ArithUnatePropagator maintains sorted lists containing all atoms associated + ** for each unique left hand side, the "x" in the inequality "x < c". + ** The lists are sorted by the value of the right hand side which must be a + ** rational constant. + ** + ** ArithUnatePropagator tries to send out a minimal number of additional + ** lemmas per atom added. Let (x < a), (x < b), (x < c) be arithmetic atoms s.t. + ** a < b < c. + ** If the the order of adding the atoms is (x < a), (x < b), and (x < c), then + ** then set of all lemmas added is: + ** {(=> (x (x (x (x (x a b) to the PropEngine via d_arithOut. */ + void addImplication(TNode a, TNode b); + + /** Check to make sure an lhs has been properly set-up. */ + bool leftIsSetup(TNode left); + + /** Initializes the lists associated with a unique lhs. */ + void setupLefthand(TNode left); + + + /** + * The addKtoJs(...) functions are the work horses of ArithUnatePropagator. + * These take an atom of the kind K that has just been added + * to its associated list, and the list of Js associated with the lhs, + * and uses these to deduce unate implications. + * (K and J vary over EQUAL, LEQ, and GEQ.) + * + * Input: + * atom - the atom being inserted + * Kset - the list of atoms of kind K associated with the lhs. + * atomPos - the atoms Position in its own list after being inserted. + * + * Unfortunately, these tend to be an absolute bear to read because + * of all of the special casing and C++ iterator manipulation required. + */ + + void addEqualityToEqualities(TNode eq, OrderedSet* eqSet, OrderedSet::iterator eqPos); + void addEqualityToLeqs(TNode eq, OrderedSet* leqSet); + void addEqualityToGeqs(TNode eq, OrderedSet* geqSet); + + void addLeqToLeqs(TNode leq, OrderedSet* leqSet, OrderedSet::iterator leqPos); + void addLeqToGeqs(TNode leq, OrderedSet* geqSet); + void addLeqToEqualities(TNode leq, OrderedSet* eqSet); + + void addGeqToGeqs(TNode geq, OrderedSet* geqSet, OrderedSet::iterator geqPos); + void addGeqToLeqs(TNode geq, OrderedSet* leqSet); + void addGeqToEqualities(TNode geq, OrderedSet* eqSet); + +}; + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__ARITH__THEORY_ARITH_H */ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 7958d977e..813b38d93 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -318,7 +318,7 @@ public: } inline void newLemma(TNode node) { - d_propEngine->assertLemma(preprocess(node)); + d_propEngine->assertSafeLemma(preprocess(node)); } /** diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index 7d147f6a5..8c34370d7 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -114,6 +114,12 @@ public: return d_callHistory.size(); } + void printIth(std::ostream& os, int i){ + os << "[TestOutputChannel " << i; + os << " " << getIthCallType(i); + os << " " << getIthNode(i) << "]"; + } + private: void push(OutputChannelCallType call, TNode n) { d_callHistory.push_back(std::make_pair(call,n)); diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 7cadf1b04..b045f38e7 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -141,59 +141,6 @@ public: return dis; } -// void testBasicConflict() { -// Node x = d_nm->mkVar(*d_realType); -// Node c = d_nm->mkConst(d_zero); -// -// Node eq = d_nm->mkNode(EQUAL, x, c); -// Node lt = d_nm->mkNode(NOT, d_nm->mkNode(GEQ, x, c)); -// Node expectedDisjunct = simulateSplit(x,c); -// -// fakeTheoryEnginePreprocess(eq); -// fakeTheoryEnginePreprocess(lt); -// -// d_arith->assertFact(eq); -// d_arith->assertFact(lt); -// -// d_arith->check(d_level); -// -// TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 2u); -// TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), expectedDisjunct); -// TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), AUG_LEMMA); -// -// TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), CONFLICT); -// -// Node expectedClonflict = d_nm->mkNode(AND, eq, lt); -// -// TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), expectedClonflict); -// } - -// void testBasicPropagate() { -// Node x = d_nm->mkVar(*d_realType); -// Node c = d_nm->mkConst(d_zero); -// -// Node eq = d_nm->mkNode(EQUAL, x, c); -// Node lt = d_nm->mkNode(NOT, d_nm->mkNode(GEQ, x, c)); -// Node expectedDisjunct = simulateSplit(x,c); -// -// fakeTheoryEnginePreprocess(eq); -// fakeTheoryEnginePreprocess(lt); -// -// d_arith->assertFact(eq); -// -// -// d_arith->check(d_level); -// d_arith->propagate(d_level); -// -// TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 2u); -// TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), AUG_LEMMA); -// -// -// Node expectedProp = d_nm->mkNode(GEQ, x, c); -// TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), PROPAGATE); -// TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), expectedProp); -// -// } void testTPLt1() { Node x = d_nm->mkVar(*d_realType); Node c0 = d_nm->mkConst(d_zero); @@ -214,17 +161,20 @@ public: d_arith->check(d_level); d_arith->propagate(d_level); -#ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS( d_arith->explain(leq0, d_level), AssertionException ); - TS_ASSERT_THROWS( d_arith->explain(lt1, d_level), AssertionException ); -#endif - d_arith->explain(leq1, d_level); - - TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 2u); - TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), PROPAGATE); - TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), EXPLANATION); - TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq1); - TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), lt1); + Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1); + Node lt1ThenLeq1 = NodeBuilder<2>(IMPLIES) << lt1 << leq1; + Node leq0ThenLt1 = NodeBuilder<2>(IMPLIES) << leq0 << lt1; + + TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u); + + TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq0ThenLeq1); + + TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), lt1ThenLeq1); + + TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq0ThenLt1); } @@ -246,27 +196,21 @@ public: d_arith->check(d_level); - d_arith->propagate(d_level); + Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1); + Node lt1ThenLeq1 = NodeBuilder<2>(IMPLIES) << lt1 << leq1; + Node leq0ThenLt1 = NodeBuilder<2>(IMPLIES) << leq0 << lt1; - d_arith->explain(lt1, d_level); -#ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS( d_arith->explain(leq0, d_level), AssertionException ); -#endif - d_arith->explain(leq1, d_level); + TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u); - TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 4u); - TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), PROPAGATE); - TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), PROPAGATE); - TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), EXPLANATION); - TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(3), EXPLANATION); + TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq0ThenLeq1); - TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), lt1); - TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq1); + TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), lt1ThenLeq1); - - TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq0); - TS_ASSERT_EQUALS(d_outputChannel.getIthNode(3), leq0); + TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq0ThenLt1); } void testTPLeq1() { Node x = d_nm->mkVar(*d_realType); @@ -288,12 +232,19 @@ public: d_arith->check(d_level); d_arith->propagate(d_level); -#ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS( d_arith->explain(leq0, d_level), AssertionException ); - TS_ASSERT_THROWS( d_arith->explain(leq1, d_level), AssertionException ); - TS_ASSERT_THROWS( d_arith->explain(lt1, d_level), AssertionException ); -#endif + Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1); + Node lt1ThenLeq1 = NodeBuilder<2>(IMPLIES) << lt1 << leq1; + Node leq0ThenLt1 = NodeBuilder<2>(IMPLIES) << leq0 << lt1; - TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 0u); + TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u); + + TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq0ThenLeq1); + + TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), lt1ThenLeq1); + + TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq0ThenLt1); } }; -- 2.30.2