This commit merges the branch arithmetic/propagation-again into trunk.

[cvc5.git] / src / theory / arith / theory_arith.h

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 85f55484962ad3de096b02ae93e32c33cd0a3660..9580a6c711dc9c2175ddabed2f34e4784daa1cc4 100644 (file)
--- 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,