diff options
author | Tim King <taking@cs.nyu.edu> | 2011-04-18 16:48:52 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-04-18 16:48:52 +0000 |
commit | abe849b486ea3707fd51a612c7982554f3d6581f (patch) | |
tree | 8f3967f644f9098079c778dd60cf9feb36e1ab2b /src/theory/arith/theory_arith.h | |
parent | b90081962840584bb9eeda368ea232a7d42a292b (diff) |
This commit merges the branch arithmetic/propagation-again into trunk.
- This adds code for bounds refinement, and conflict weakening.
- This adds util/boolean_simplification.h.
- This adds a propagation manager to theory of arithmetic.
- Propagation is disabled by default.
- Propagation can be enabled by the command line flag "--enable-arithmetic-propagation"
- Propagation interacts *heavily* with rewriting equalities, and will work best if the command line flag "--rewrite-arithmetic-equalities" is enabled.
Diffstat (limited to 'src/theory/arith/theory_arith.h')
-rw-r--r-- | src/theory/arith/theory_arith.h | 42 |
1 files changed, 16 insertions, 26 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 85f554849..9580a6c71 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -36,6 +36,8 @@ #include "theory/arith/unate_propagator.h" #include "theory/arith/simplex.h" #include "theory/arith/arith_static_learner.h" +#include "theory/arith/arith_prop_manager.h" +#include "theory/arith/arithvar_node_map.h" #include "util/stats.h" @@ -64,6 +66,8 @@ private: */ std::vector<Node> d_variables; + ArithVarNodeMap d_arithvarNodeMap; + /** * If ArithVar v maps to the node n in d_removednode, * then n = (= asNode(v) rhs) where rhs is a term that @@ -82,32 +86,7 @@ private: */ ArithVarSet d_userVariables; - /** - * Bidirectional map between Nodes and ArithVars. - */ - NodeToArithVarMap d_nodeToArithVarMap; - ArithVarToNodeMap d_arithVarToNodeMap; - - inline bool hasArithVar(TNode x) const { - return d_nodeToArithVarMap.find(x) != d_nodeToArithVarMap.end(); - } - - inline ArithVar asArithVar(TNode x) const{ - Assert(hasArithVar(x)); - Assert((d_nodeToArithVarMap.find(x))->second <= ARITHVAR_SENTINEL); - return (d_nodeToArithVarMap.find(x))->second; - } - inline Node asNode(ArithVar a) const{ - Assert(d_arithVarToNodeMap.find(a) != d_arithVarToNodeMap.end()); - return (d_arithVarToNodeMap.find(a))->second; - } - - inline void setArithVar(TNode x, ArithVar a){ - Assert(!hasArithVar(x)); - Assert(d_arithVarToNodeMap.find(a) == d_arithVarToNodeMap.end()); - d_arithVarToNodeMap[a] = x; - d_nodeToArithVarMap[x] = a; - } + /** * List of all of the inequalities asserted in the current context. @@ -141,6 +120,9 @@ private: Tableau d_smallTableauCopy; ArithUnatePropagator d_propagator; + + ArithPropManager d_propManager; + SimplexDecisionProcedure d_simplex; public: @@ -175,6 +157,9 @@ private: /** The constant zero. */ DeltaRational d_DELTA_ZERO; + /** propagates an arithvar */ + void propagateArithVar(bool upperbound, ArithVar var ); + /** * Using the simpleKind return the ArithVar associated with the * left hand side of assertion. @@ -228,6 +213,11 @@ private: */ void permanentlyRemoveVariable(ArithVar v); + bool isImpliedUpperBound(ArithVar var, Node exp); + bool isImpliedLowerBound(ArithVar var, Node exp); + + void internalExplain(TNode n, NodeBuilder<>& explainBuilder); + void asVectors(Polynomial& p, std::vector<Rational>& coeffs, |