#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"
*/
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
*/
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.
Tableau d_smallTableauCopy;
ArithUnatePropagator d_propagator;
+
+ ArithPropManager d_propManager;
+
SimplexDecisionProcedure d_simplex;
public:
/** 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.
*/
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,