diff options
Diffstat (limited to 'src/theory/arith/constraint.cpp')
-rw-r--r-- | src/theory/arith/constraint.cpp | 34 |
1 files changed, 24 insertions, 10 deletions
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 28b999852..e26687bf1 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -371,8 +371,22 @@ void ConstraintValue::setAssertedToTheTheory(TNode witness) { d_database->pushAssertionOrderWatch(this, witness); } -// bool ConstraintValue::isPseudoConstraint() const { -// return d_proof == d_database->d_pseudoConstraintProof; +bool ConstraintValue::satisfiedBy(const DeltaRational& dr) const { + switch(getType()){ + case LowerBound: + return getValue() <= dr; + case Equality: + return getValue() == dr; + case UpperBound: + return getValue() >= dr; + case Disequality: + return getValue() != dr; + } + Unreachable(); +} + +// bool ConstraintValue::isPsuedoConstraint() const { +// return d_proof == d_database->d_psuedoConstraintProof; // } bool ConstraintValue::isSelfExplaining() const { @@ -394,7 +408,7 @@ bool ConstraintValue::sanityChecking(Node n) const { TNode left = pleft.getNode(); DeltaRational right = cmp.normalizedDeltaRational(); - const ArithVarNodeMap& av2node = d_database->getArithVarNodeMap(); + const ArithVariables& avariables = d_database->getArithVariables(); Debug("nf::tmp") << cmp.getNode() << endl; Debug("nf::tmp") << k << endl; @@ -402,13 +416,13 @@ bool ConstraintValue::sanityChecking(Node n) const { Debug("nf::tmp") << left << endl; Debug("nf::tmp") << right << endl; Debug("nf::tmp") << getValue() << endl; - Debug("nf::tmp") << av2node.hasArithVar(left) << endl; - Debug("nf::tmp") << av2node.asArithVar(left) << endl; + Debug("nf::tmp") << avariables.hasArithVar(left) << endl; + Debug("nf::tmp") << avariables.asArithVar(left) << endl; Debug("nf::tmp") << getVariable() << endl; - if(av2node.hasArithVar(left) && - av2node.asArithVar(left) == getVariable() && + if(avariables.hasArithVar(left) && + avariables.asArithVar(left) == getVariable() && getValue() == right){ switch(getType()){ case LowerBound: @@ -469,12 +483,12 @@ Constraint ConstraintValue::makeNegation(ArithVar v, ConstraintType t, const Del } } -ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Context* userContext, const ArithVarNodeMap& av2nodeMap, ArithCongruenceManager& cm, NodeCallBack& raiseConflict) +ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Context* userContext, const ArithVariables& avars, ArithCongruenceManager& cm, RaiseConflict raiseConflict) : d_varDatabases(), d_toPropagate(satContext), d_proofs(satContext, false), d_watches(new Watches(satContext, userContext)), - d_av2nodeMap(av2nodeMap), + d_avariables(avars), d_congruenceManager(cm), d_satContext(satContext), d_satAllocationLevel(d_satContext->getLevel()), @@ -670,7 +684,7 @@ Constraint ConstraintDatabase::addLiteral(TNode literal){ Polynomial nvp = posCmp.normalizedVariablePart(); Debug("nf::tmp") << "here " << nvp.getNode() << " " << endl; - ArithVar v = d_av2nodeMap.asArithVar(nvp.getNode()); + ArithVar v = d_avariables.asArithVar(nvp.getNode()); DeltaRational posDR = posCmp.normalizedDeltaRational(); |