summaryrefslogtreecommitdiff
path: root/src/theory/arith/congruence_manager.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/congruence_manager.h')
-rw-r--r--src/theory/arith/congruence_manager.h4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index e70773030..a72989498 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -5,7 +5,6 @@
#pragma once
#include "theory/arith/arithvar.h"
-#include "theory/arith/arithvar_set.h"
#include "theory/arith/arithvar_node_map.h"
#include "theory/arith/constraint_forward.h"
@@ -18,6 +17,7 @@
#include "context/cdmaybe.h"
#include "util/stats.h"
+#include "util/dense_map.h"
namespace CVC4 {
namespace theory {
@@ -32,7 +32,7 @@ private:
* If this is 0 or cannot be 0, this can be signalled.
* The pair of terms for the congruence is stored in watched equalities.
*/
- PermissiveBackArithVarSet d_watchedVariables;
+ DenseSet d_watchedVariables;
/** d_watchedVariables |-> (= x y) */
ArithVarToNodeMap d_watchedEqualities;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback