diff options
author | Tim King <taking@cs.nyu.edu> | 2010-06-29 20:53:47 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-06-29 20:53:47 +0000 |
commit | e792bb8628ea7010fa9c452bf1aa7ba1b60291a3 (patch) | |
tree | ddc12f92092627b7aee2a63dca8dd66279b2970e /src/theory/arith | |
parent | e7e9c10006b5b243a73832ed97c5dec79df6c90a (diff) |
Merging the unate-propagator branch into the trunk. This is a big update so expect a little turbulence. This commit will not compile. There will be a second commit that fixes this in a moment. I am delaying a change to avoid svn whining about a conflict.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/Makefile.am | 3 | ||||
-rw-r--r-- | src/theory/arith/arith_propagator.cpp | 347 | ||||
-rw-r--r-- | src/theory/arith/arith_propagator.h | 111 | ||||
-rw-r--r-- | src/theory/arith/ordered_bounds_list.h | 212 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 93 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 7 |
6 files changed, 757 insertions, 16 deletions
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 83d44e285..37df73edd 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -15,10 +15,13 @@ libarith_la_SOURCES = \ delta_rational.cpp \ partial_model.h \ partial_model.cpp \ + ordered_bounds_list.h \ basic.h \ normal.h \ slack.h \ tableau.h \ + arith_propagator.h \ + arith_propagator.cpp \ theory_arith.h \ theory_arith.cpp diff --git a/src/theory/arith/arith_propagator.cpp b/src/theory/arith/arith_propagator.cpp new file mode 100644 index 000000000..e40575054 --- /dev/null +++ b/src/theory/arith/arith_propagator.cpp @@ -0,0 +1,347 @@ +#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(debugTagIsOn("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()); +} diff --git a/src/theory/arith/arith_propagator.h b/src/theory/arith/arith_propagator.h new file mode 100644 index 000000000..a623517fb --- /dev/null +++ b/src/theory/arith/arith_propagator.h @@ -0,0 +1,111 @@ + + +#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 */ diff --git a/src/theory/arith/ordered_bounds_list.h b/src/theory/arith/ordered_bounds_list.h new file mode 100644 index 000000000..d21283afa --- /dev/null +++ b/src/theory/arith/ordered_bounds_list.h @@ -0,0 +1,212 @@ + + +#include "cvc4_private.h" + + +#ifndef __CVC4__THEORY__ARITH__ORDERED_BOUNDS_LIST_H +#define __CVC4__THEORY__ARITH__ORDERED_BOUNDS_LIST_H + +#include "expr/node.h" +#include "util/rational.h" +#include "expr/kind.h" + +#include <vector> +#include <algorithm> + +namespace CVC4 { +namespace theory { +namespace arith { + +struct RightHandRationalLT +{ + bool operator()(TNode s1, TNode s2) const + { + Assert(s1.getNumChildren() >= 2); + Assert(s2.getNumChildren() >= 2); + + Assert(s1[1].getKind() == kind::CONST_RATIONAL); + Assert(s2[1].getKind() == kind::CONST_RATIONAL); + + TNode rh1 = s1[1]; + TNode rh2 = s2[1]; + const Rational& c1 = rh1.getConst<Rational>(); + const Rational& c2 = rh2.getConst<Rational>(); + return c1.cmp(c2) < 0; + } +}; + +struct RightHandRationalGT +{ + bool operator()(TNode s1, TNode s2) const + { + Assert(s1.getNumChildren() >= 2); + Assert(s2.getNumChildren() >= 2); + + Assert(s1[1].getKind() == kind::CONST_RATIONAL); + Assert(s2[1].getKind() == kind::CONST_RATIONAL); + + TNode rh1 = s1[1]; + TNode rh2 = s2[1]; + const Rational& c1 = rh1.getConst<Rational>(); + const Rational& c2 = rh2.getConst<Rational>(); + return c1.cmp(c2) > 0; + } +}; + +/** + * An OrderedBoundsList is a lazily sorted vector of Arithmetic constraints. + * The intended use is for a list of rewriting arithmetic atoms. + * An example of such a list would be [(<= x 5);(= y 78); (>= x 9)]. + * + * Nodes are required to have a CONST_RATIONAL child as their second node. + * Nodes are sorted in increasing order according to RightHandRationalLT. + * + * The lists are lazily sorted in the sense that the list is not sorted until + * an operation to access the element is attempted. + * + * An append() may make the list no longer sorted. + * After an append() operation all iterators for the list become invalid. + */ +class OrderedBoundsList { +private: + bool d_isSorted; + std::vector<Node> d_list; + +public: + typedef std::vector<Node>::const_iterator iterator; + typedef std::vector<Node>::const_reverse_iterator reverse_iterator; + + /** + * Constucts a new and empty OrderBoundsList. + * The empty list is initially sorted. + */ + OrderedBoundsList() : d_isSorted(true){} + + /** + * Appends a node onto the back of the list. + * The list may no longer be sorted. + */ + void append(TNode n){ + Assert(n.getNumChildren() >= 2); + Assert(n[1].getKind() == kind::CONST_RATIONAL); + d_isSorted = false; + d_list.push_back(n); + } + + /** returns the size of the list */ + unsigned int size(){ + return d_list.size(); + } + + /** returns the i'th element in the sort list. This may sort the list.*/ + TNode at(unsigned int idx){ + sortIfNeeded(); + return d_list.at(idx); + } + + /** returns true if the list is known to be sorted. */ + bool isSorted() const{ + return d_isSorted; + } + + /** sorts the list. */ + void sort(){ + d_isSorted = true; + std::sort(d_list.begin(), d_list.end(), RightHandRationalLT()); + } + + /** + * returns an iterator to the list that iterates in ascending order. + * This may sort the list. + */ + iterator begin(){ + sortIfNeeded(); + return d_list.begin(); + } + /** + * returns an iterator to the end of the list when interating in ascending order. + */ + iterator end() const{ + return d_list.end(); + } + + /** + * returns an iterator to the list that iterates in descending order. + * This may sort the list. + */ + reverse_iterator rbegin(){ + sortIfNeeded(); + return d_list.rend(); + } + /** + * returns an iterator to the end of the list when interating in descending order. + */ + reverse_iterator rend() const{ + return d_list.rend(); + } + + /** + * returns an iterator to the least strict upper bound of value. + * if the list is [(<= x 2);(>= x 80);(< y 70)] + * then *upper_bound((< z 70)) == (>= x 80) + * + * This may sort the list. + * see stl::upper_bound for more information. + */ + iterator upper_bound(TNode value){ + sortIfNeeded(); + return std::upper_bound(begin(), end(), value, RightHandRationalLT()); + } + /** + * returns an iterator to the greatest lower bound of value. + * This is bound is not strict. + * if the list is [(<= x 2);(>= x 80);(< y 70)] + * then *lower_bound((< z 70)) == (< y 70) + * + * This may sort the list. + * see stl::upper_bound for more information. + */ + iterator lower_bound(TNode value){ + sortIfNeeded(); + return std::lower_bound(begin(), end(), value, RightHandRationalLT()); + } + /** + * see OrderedBoundsList::upper_bound for more information. + * The difference is that the iterator goes in descending order. + */ + reverse_iterator reverse_upper_bound(TNode value){ + sortIfNeeded(); + return std::upper_bound(rbegin(), rend(), value, RightHandRationalGT()); + } + /** + * see OrderedBoundsList::lower_bound for more information. + * The difference is that the iterator goes in descending order. + */ + reverse_iterator reverse_lower_bound(TNode value){ + sortIfNeeded(); + return std::lower_bound(rbegin(), rend(), value, RightHandRationalGT()); + } + + /** + * This is an O(n) method for searching the array to check if it contains n. + */ + bool contains(TNode n) const { + for(std::vector<Node>::const_iterator i = d_list.begin(); i != d_list.end(); ++i){ + if(*i == n) return true; + } + return false; + } +private: + /** Sorts the list if it is not already sorted. */ + void sortIfNeeded(){ + if(!d_isSorted){ + sort(); + } + } +}; + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__ARITH__ORDERED_BOUNDS_LIST_H */ diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index b3b7f58be..bd35e0797 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -34,6 +34,7 @@ #include "theory/arith/basic.h" #include "theory/arith/arith_rewriter.h" +#include "theory/arith/arith_propagator.h" #include "theory/arith/theory_arith.h" #include <map> @@ -55,6 +56,7 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) : d_partialModel(c), d_diseq(c), d_rewriter(&d_constants), + d_propagator(c), d_statistics() { uint64_t ass_id = partial_model::Assignment::getId(); @@ -81,6 +83,15 @@ TheoryArith::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_statUpdateConflicts); } +TheoryArith::Statistics::~Statistics(){ + StatisticsRegistry::unregisterStat(&d_statPivots); + StatisticsRegistry::unregisterStat(&d_statUpdates); + StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts); + StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts); + StatisticsRegistry::unregisterStat(&d_statUpdateConflicts); +} + + bool isBasicSum(TNode n){ if(n.getKind() != kind::PLUS) return false; @@ -143,6 +154,8 @@ void TheoryArith::preRegisterTerm(TNode n) { Assert(isNormalAtom(n)); + d_propagator.addAtom(n); + TNode left = n[0]; TNode right = n[1]; if(left.getKind() == PLUS){ @@ -206,6 +219,10 @@ void TheoryArith::setupVariable(TNode x){ //lower bound. This is done to strongly enforce the notion that basic //variables should not be changed without begin checked. + //Strictly speaking checking x is unnessecary as it cannot have an upper or + //lower bound. This is done to strongly enforce the notion that basic + //variables should not be changed without begin checked. + } Debug("arithgc") << "setupVariable("<<x<<")"<<std::endl; }; @@ -682,41 +699,69 @@ void TheoryArith::check(Effort level){ Debug("arith") << "TheoryArith::check begun" << std::endl; while(!done()){ + Node original = get(); Node assertion = simulatePreprocessing(original); Debug("arith_assertions") << "arith assertion(" << original << " \\-> " << assertion << ")" << std::endl; + d_propagator.assertLiteral(original); bool conflictDuringAnAssert = assertionCases(original, assertion); + if(conflictDuringAnAssert){ - if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); } d_partialModel.revertAssignmentChanges(); - if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); } - return; } } - if(fullEffort(level)){ - if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); } + //TODO This must be done everytime for the time being + if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); } - Node possibleConflict = updateInconsistentVars(); - if(possibleConflict != Node::null()){ + Node possibleConflict = updateInconsistentVars(); + if(possibleConflict != Node::null()){ - d_partialModel.revertAssignmentChanges(); + d_partialModel.revertAssignmentChanges(); - d_out->conflict(possibleConflict, true); + if(debugTagIsOn("arith::print-conflict")) + Debug("arith_conflict") << (possibleConflict) << std::endl; - Debug("arith_conflict") <<"Found a conflict "<< possibleConflict << endl; - }else{ - d_partialModel.commitAssignmentChanges(); - } - if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); } + d_out->conflict(possibleConflict); + + Debug("arith_conflict") <<"Found a conflict "<< possibleConflict << endl; + }else{ + d_partialModel.commitAssignmentChanges(); } + if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); } + Debug("arith") << "TheoryArith::check end" << std::endl; + if(debugTagIsOn("arith::print_model")) { + Debug("arith::print_model") << "Model:" << endl; + + for (unsigned i = 0; i < d_variables.size(); ++ i) { + Debug("arith::print_model") << d_variables[i] << " : " << + d_partialModel.getAssignment(d_variables[i]); + if(isBasic(d_variables[i])) + Debug("arith::print_model") << " (basic)"; + Debug("arith::print_model") << endl; + } + } + if(debugTagIsOn("arith::print_assertions")) { + Debug("arith::print_assertions") << "Assertions:" << endl; + for (unsigned i = 0; i < d_variables.size(); ++ i) { + Node x = d_variables[i]; + if (x.hasAttribute(partial_model::LowerConstraint())) { + Node constr = d_partialModel.getLowerConstraint(x); + Debug("arith::print_assertions") << constr.toString() << endl; + } + if (x.hasAttribute(partial_model::UpperConstraint())) { + Node constr = d_partialModel.getUpperConstraint(x); + Debug("arith::print_assertions") << constr.toString() << endl; + } + } + } } /** @@ -750,3 +795,23 @@ void TheoryArith::checkTableau(){ Assert(sum == shouldBe); } } + + +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); +} + +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); + } + } +} diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index aff60f651..c76923bee 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -30,6 +30,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 "util/stats.h" @@ -96,6 +97,7 @@ private: */ ArithRewriter d_rewriter; + ArithUnatePropagator d_propagator; public: TheoryArith(context::Context* c, OutputChannel& out); @@ -115,8 +117,8 @@ public: void registerTerm(TNode n); void check(Effort e); - void propagate(Effort e) { Unimplemented(); } - void explain(TNode n, Effort e) { Unimplemented(); } + void propagate(Effort e); + void explain(TNode n, Effort e); void shutdown(){ } @@ -242,6 +244,7 @@ private: IntStat d_statAssertLowerConflicts, d_statUpdateConflicts; Statistics(); + ~Statistics(); }; Statistics d_statistics; |