diff options
Diffstat (limited to 'src/theory/arith/constraint.h')
-rw-r--r-- | src/theory/arith/constraint.h | 25 |
1 files changed, 9 insertions, 16 deletions
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index e1c55f113..a5d64a652 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -72,12 +72,10 @@ #include "context/cdqueue.h" #include "theory/arith/arithvar.h" -#include "theory/arith/arithvar_node_map.h" #include "theory/arith/delta_rational.h" - #include "theory/arith/congruence_manager.h" - #include "theory/arith/constraint_forward.h" +#include "theory/arith/callbacks.h" #include <vector> #include <list> @@ -604,6 +602,8 @@ public: /** The node must have a proof already and be eligible for propagation! */ void propagate(); + bool satisfiedBy(const DeltaRational& dr) const; + private: /** * Marks the node as having a proof and being selfExplaining. @@ -620,11 +620,6 @@ private: void markAsTrue(Constraint a, Constraint b); void markAsTrue(const std::vector<Constraint>& b); -public: - - -private: - void debugPrint() const; /** @@ -776,20 +771,18 @@ private: static bool emptyDatabase(const std::vector<PerVariableDatabase>& vec); /** Map from nodes to arithvars. */ - const ArithVarNodeMap& d_av2nodeMap; + const ArithVariables& d_avariables; - const ArithVarNodeMap& getArithVarNodeMap() const{ - return d_av2nodeMap; + const ArithVariables& getArithVariables() const{ + return d_avariables; } ArithCongruenceManager& d_congruenceManager; - //Constraint allocateConstraintForLiteral(ArithVar v, Node literal); - const context::Context * const d_satContext; const int d_satAllocationLevel; - NodeCallBack& d_raiseConflict; + RaiseConflict d_raiseConflict; friend class ConstraintValue; @@ -797,9 +790,9 @@ public: ConstraintDatabase( context::Context* satContext, context::Context* userContext, - const ArithVarNodeMap& av2nodeMap, + const ArithVariables& variables, ArithCongruenceManager& dm, - NodeCallBack& conflictCallBack); + RaiseConflict conflictCallBack); ~ConstraintDatabase(); |