diff options
Diffstat (limited to 'src/theory/arith/theory_arith.h')
-rw-r--r-- | src/theory/arith/theory_arith.h | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 4a5c398bd..3ed1d1941 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -38,7 +38,7 @@ #include "theory/arith/arith_static_learner.h" #include "theory/arith/arithvar_node_map.h" #include "theory/arith/dio_solver.h" -#include "theory/arith/difference_manager.h" +#include "theory/arith/congruence_manager.h" #include "theory/arith/constraint.h" @@ -241,14 +241,8 @@ private: */ Tableau d_smallTableauCopy; - /** - * The atom database keeps track of the atoms that have been preregistered. - * Used to add unate propagations. - */ - //ArithAtomDatabase d_atomDatabase; - /** This keeps track of difference equalities. Mostly for sharing. */ - DifferenceManager d_differenceManager; + ArithCongruenceManager d_congruenceManager; /** This implements the Simplex decision procedure. */ SimplexDecisionProcedure d_simplex; |