diff options
author | Tim King <taking@cs.nyu.edu> | 2012-04-24 18:36:40 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-04-24 18:36:40 +0000 |
commit | c0f5194dd56c5127c5c6dab5e59997eccc2d78a5 (patch) | |
tree | 080d465b923832f14d67da4431642609d66b921b /src/theory/arith/constraint.cpp | |
parent | 5676b8bddcf001ba567ebb6d8e7b42dbd13ac9f3 (diff) |
This commit merges in the branch branches/arithmetic/congruence into trunk. Here are a summary of the changes:
- Adds CDMaybe and CDRaised in cdmaybe.h
- Add test for congruence over arithmetic terms and constants
- Renames DifferenceManager to CongruenceManager
- Changes a number of internal details for CongruenceManager
Diffstat (limited to 'src/theory/arith/constraint.cpp')
-rw-r--r-- | src/theory/arith/constraint.cpp | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index f78ecdddf..460877a23 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -444,14 +444,13 @@ Constraint ConstraintValue::makeNegation(ArithVar v, ConstraintType t, const Del } } -ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Context* userContext, const ArithVarNodeMap& av2nodeMap, - DifferenceManager& dm) +ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Context* userContext, const ArithVarNodeMap& av2nodeMap, ArithCongruenceManager& cm) : d_varDatabases(), d_toPropagate(satContext), d_proofs(satContext, false), d_watches(new Watches(satContext, userContext)), d_av2nodeMap(av2nodeMap), - d_differenceManager(dm), + d_congruenceManager(cm), d_satContext(satContext), d_satAllocationLevel(d_satContext->getLevel()) { @@ -997,12 +996,12 @@ Constraint ConstraintDatabase::getBestImpliedBound(ArithVar v, ConstraintType t, } Node ConstraintDatabase::eeExplain(const ConstraintValue* const c) const{ Assert(c->hasLiteral()); - return d_differenceManager.explain(c->getLiteral()); + return d_congruenceManager.explain(c->getLiteral()); } void ConstraintDatabase::eeExplain(const ConstraintValue* const c, NodeBuilder<>& nb) const{ Assert(c->hasLiteral()); - d_differenceManager.explain(c->getLiteral(), nb); + d_congruenceManager.explain(c->getLiteral(), nb); } bool ConstraintDatabase::variableDatabaseIsSetup(ArithVar v) const { |