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.h | |
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.h')
-rw-r--r-- | src/theory/arith/constraint.h | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index e1939159b..2e0a9d067 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -77,7 +77,7 @@ #include "theory/arith/arithvar_node_map.h" #include "theory/arith/delta_rational.h" -#include "theory/arith/difference_manager.h" +#include "theory/arith/congruence_manager.h" #include "theory/arith/constraint_forward.h" @@ -746,7 +746,7 @@ private: return d_av2nodeMap; } - DifferenceManager& d_differenceManager; + ArithCongruenceManager& d_congruenceManager; //Constraint allocateConstraintForLiteral(ArithVar v, Node literal); @@ -760,7 +760,7 @@ public: ConstraintDatabase( context::Context* satContext, context::Context* userContext, const ArithVarNodeMap& av2nodeMap, - DifferenceManager& dm); + ArithCongruenceManager& dm); ~ConstraintDatabase(); |