diff options
author | Tim King <taking@cs.nyu.edu> | 2011-11-29 21:11:45 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-11-29 21:11:45 +0000 |
commit | e9198d9b99c6037165362870436b45826674303f (patch) | |
tree | b5e8d01a53d38d353dae7c16351ff9206e1f96c6 /src/theory/arith/difference_manager.h | |
parent | 8b202bab8442c927e9ac18a35c71a82444acf63b (diff) |
Merging the branch branches/arithmetic/shared-terms into trunk. Arithmetic now supports propagating equalities when a slack variable corresponding to a difference of shared terms must be 0. Similarly disequalities are propagated when these variables cannot be zero.
Diffstat (limited to 'src/theory/arith/difference_manager.h')
-rw-r--r-- | src/theory/arith/difference_manager.h | 95 |
1 files changed, 95 insertions, 0 deletions
diff --git a/src/theory/arith/difference_manager.h b/src/theory/arith/difference_manager.h new file mode 100644 index 000000000..01f42dcfe --- /dev/null +++ b/src/theory/arith/difference_manager.h @@ -0,0 +1,95 @@ + + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H +#define __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H + +#include "theory/arith/arith_utilities.h" +#include "theory/uf/equality_engine.h" +#include "context/cdo.h" +#include "context/cdlist.h" +#include "context/context.h" +#include "util/stats.h" +#include "theory/arith/arith_prop_manager.h" + +namespace CVC4 { +namespace theory { +namespace arith { + +class DifferenceManager { +private: + struct Difference { + bool isSlack; + TNode x; + TNode y; + Difference() : isSlack(false), x(TNode::null()), y(TNode::null()){} + Difference(TNode a, TNode b) : isSlack(true), x(a), y(b) { + Assert(x < y); + } + }; + + + class DifferenceNotifyClass { + private: + DifferenceManager& d_dm; + public: + DifferenceNotifyClass(DifferenceManager& dm): d_dm(dm) {} + + bool notify(TNode propagation) { + Debug("arith::differences") << "DifferenceNotifyClass::notify(" << propagation << ")" << std::endl; + // Just forward to dm + d_dm.propagate(propagation); + return true; + } + + void notify(TNode t1, TNode t2) { + Debug("arith::differences") << "DifferenceNotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl; + Node equality = t1.eqNode(t2); + d_dm.propagate(equality); + } + }; + + std::vector< Difference > d_differences; + + context::CDList<Node> d_reasons; + PropManager& d_queue; + + + DifferenceNotifyClass d_notify; + theory::uf::EqualityEngine<DifferenceNotifyClass> d_ee; + + void propagate(TNode x); + void explain(TNode literal, std::vector<TNode>& assumptions); + + Node d_false; + +public: + + DifferenceManager(context::Context*, PropManager&); + + Node explain(TNode literal); + + void addDifference(ArithVar s, Node x, Node y); + + inline bool isDifferenceSlack(ArithVar s) const{ + if(s < d_differences.size()){ + return d_differences[s].isSlack; + }else{ + return false; + } + } + + void differenceIsZero(ArithVar s, TNode reason); + + void differenceCannotBeZero(ArithVar s, TNode reason); + + void addSharedTerm(Node x); +};/* class DifferenceManager */ + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H */ + |