summaryrefslogtreecommitdiff
path: root/src/theory/arith/theory_arith.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/theory_arith.h')
-rw-r--r--src/theory/arith/theory_arith.h10
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback