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 =
* @param node the formula to assert
*/
void assertLemma(TNode node);
+ void assertSafeLemma(TNode node);
/**
* Checks the current context for satisfiability.
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
+++ /dev/null
-/********************* */
-/*! \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 <list>
-
-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<Node> ArithUnatePropagator::getImpliedLiterals(){
- std::vector<Node> 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<Node>::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<Node>& 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<Node>& buffer){
- TNode left = orig[0];
- TNode right = orig[1];
- const Rational& c = right.getConst<Rational>();
-
- 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<Rational>() != 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<Rational>();
- 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<Rational>();
- 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<Node>& buffer){
-
- Assert(atom.getKind() == LEQ || (orig.getKind() == NOT && atom.getKind() == GEQ));
-
- TNode left = atom[0];
- TNode right = atom[1];
- const Rational& c = right.getConst<Rational>();
-
- 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<Rational>();
- 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<Rational>();
- 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<Rational>();
- 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<Node>& buffer){
-
- Assert(atom.getKind() == GEQ || (orig.getKind() == NOT && atom.getKind() == LEQ));
-
- TNode left = atom[0];
- TNode right = atom[1];
- const Rational& c = right.getConst<Rational>();
-
- 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<Rational>();
- 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<Rational>();
- 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<Rational>();
- 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());
-}
+++ /dev/null
-/********************* */
-/*! \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 <algorithm>
-#include <vector>
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-class ArithUnatePropagator {
-private:
- /** Index of assertions. */
- context::CDList<Node> d_assertions;
-
- /** Index of the last assertion in d_assertions to be asserted. */
- context::CDO<unsigned int> 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<Node> 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<Node>& buffer);
-
- void enqueueEqualityImplications(TNode original, std::vector<Node>& buffer);
- void enqueueLowerBoundImplications(TNode atom, TNode original, std::vector<Node>& 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<Node>& 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<PropagatorEqListID, OrderedBoundsList*, ListCleanupStrategy> PropagatorEqList;
-
-struct PropagatorGeqListID {};
-typedef expr::Attribute<PropagatorGeqListID, OrderedBoundsList*, ListCleanupStrategy> PropagatorGeqList;
-
-struct PropagatorLeqListID {};
-typedef expr::Attribute<PropagatorLeqListID, OrderedBoundsList*, ListCleanupStrategy> PropagatorLeqList;
-
-
-struct PropagatorMarkedID {};
-typedef expr::CDAttribute<PropagatorMarkedID, bool> PropagatorMarked;
-
-struct PropagatorExplanationID {};
-typedef expr::CDAttribute<PropagatorExplanationID, Node> PropagatorExplanation;
-}/* CVC4::theory::arith::propagator */
-
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__ARITH__THEORY_ARITH_H */
--- /dev/null
+#include <set>
+#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<Rational>();
+ const Rational& c2 = rh2.getConst<Rational>();
+ int cmpRes = c1.cmp(c2);
+ return cmpRes < 0;
+ }
+};
+
+typedef std::set<Node, RightHandRationalLT> 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 */
#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"
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()
{}
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);
}
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;
}
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;
}
Node assertion = get();
- d_propagator.assertLiteral(assertion);
+ //d_propagator.assertLiteral(assertion);
bool conflictDuringAnAssert = assertionCases(assertion);
if(conflictDuringAnAssert){
// All the implication
Node impClosure = NodeBuilder<3>(kind::AND) << imp1 << imp2 << imp3;
+ ++(d_statistics.d_statDisequalitySplits);
d_out->lemma(lemma.andNode(impClosure));
}
}
}
void TheoryArith::explain(TNode n, Effort e) {
- Node explanation = d_propagator.explain(n);
- Debug("arith") << "arith::explain("<<explanation<<")->"
- << explanation << endl;
- d_out->explanation(explanation, true);
+ // Node explanation = d_propagator.explain(n);
+ // Debug("arith") << "arith::explain("<<explanation<<")->"
+ // << explanation << endl;
+ // d_out->explanation(explanation, true);
}
void TheoryArith::propagate(Effort e) {
- if(quickCheckOrMore(e)){
- std::vector<Node> implied = d_propagator.getImpliedLiterals();
- for(std::vector<Node>::iterator i = implied.begin();
- i != implied.end();
- ++i){
- d_out->propagate(*i);
- }
- }
+ // if(quickCheckOrMore(e)){
+ // std::vector<Node> implied = d_propagator.getImpliedLiterals();
+ // for(std::vector<Node>::iterator i = implied.begin();
+ // i != implied.end();
+ // ++i){
+ // d_out->propagate(*i);
+ // }
+ // }
}
Node TheoryArith::getValue(TNode n, TheoryEngine* engine) {
#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"
class Statistics {
public:
IntStat d_statUserVariables, d_statSlackVariables;
+ IntStat d_statDisequalitySplits;
+ IntStat d_statDisequalityConflicts;
Statistics();
~Statistics();
--- /dev/null
+/********************* */
+/*! \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 <list>
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::arith;
+
+using namespace CVC4::kind;
+
+using namespace std;
+
+struct PropagatorLeqSetID {};
+typedef expr::Attribute<PropagatorLeqSetID, OrderedSet*, SetCleanupStrategy> PropagatorLeqSet;
+
+struct PropagatorEqSetID {};
+typedef expr::Attribute<PropagatorEqSetID, OrderedSet*, SetCleanupStrategy> PropagatorEqSet;
+
+struct PropagatorGeqSetID {};
+typedef expr::Attribute<PropagatorGeqSetID, OrderedSet*, SetCleanupStrategy> 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<OrderedSet::iterator, bool> res = eqSet->insert(atom);
+ Assert(res.second);
+ addEqualityToEqualities(atom, eqSet, res.first);
+ addEqualityToLeqs(atom, leqSet);
+ addEqualityToGeqs(atom, geqSet);
+ break;
+ }
+ case LEQ:
+ {
+ pair<OrderedSet::iterator, bool> res = leqSet->insert(atom);
+ Assert(res.second);
+
+ addLeqToLeqs(atom, leqSet, res.first);
+ addLeqToEqualities(atom, eqSet);
+ addLeqToGeqs(atom, geqSet);
+ break;
+ }
+ case GEQ:
+ {
+ pair<OrderedSet::iterator, bool> 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<Rational>();
+ const Rational& qB = secondB.getConst<Rational>();
+
+ return qA == qB;
+}
+bool rightHandRationalIsLT(TNode a, TNode b){
+ TNode secondA = a[1];
+ TNode secondB = b[1];
+
+ const Rational& qA = secondA.getConst<Rational>();
+ const Rational& qB = secondB.getConst<Rational>();
+
+ 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);
+}
--- /dev/null
+/********************* */
+/*! \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<a) (x < b)), (=> (x<b) (x < c))}
+ ** If the order is changed to (x < a), (x < c), and (x < b), then
+ ** the final set of implications emitted is:
+ ** {(=> (x<a) (x < c)), (=> (x<a) (x < b)), (=> (x<b) (x < c))}
+ **
+ ** \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/output_channel.h"
+#include "theory/arith/ordered_set.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class ArithUnatePropagator {
+private:
+ /**
+ * OutputChannel for the theory of arithmetic.
+ * The propagator uses this to pass implications back to the SAT solver.
+ */
+ OutputChannel& d_arithOut;
+
+public:
+ ArithUnatePropagator(context::Context* cxt, OutputChannel& arith);
+
+ /**
+ * Adds an atom to the propagator.
+ * Any resulting lemmas will be output via d_arithOut.
+ */
+ void addAtom(TNode atom);
+
+private:
+ /** Sends an implication (=> 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 */
}
inline void newLemma(TNode node) {
- d_propEngine->assertLemma(preprocess(node));
+ d_propEngine->assertSafeLemma(preprocess(node));
}
/**
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));
return dis;
}
-// void testBasicConflict() {
-// Node x = d_nm->mkVar(*d_realType);
-// Node c = d_nm->mkConst<Rational>(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<Rational>(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<Rational>(d_zero);
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);
}
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);
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);
}
};
projects / cvc5.git / commitdiff