summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2012-08-14 17:52:54 +0000
committerTim King <taking@cs.nyu.edu>2012-08-14 17:52:54 +0000
commit8d6589fee6583ee7036c83a25d7e71471f6f5fd5 (patch)
tree2a9a0654bd1420ab5f3f15f9ff3fbd066b04275a
parentb43f87e90aec85a18b5b8c34f6111a9aacaa42ba (diff)
Switched TheoryModel assertEqualityEngine to use const Equality Engine pointers.
-rw-r--r--src/theory/model.cpp2
-rw-r--r--src/theory/model.h2
2 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 882a3034a..2260e86d3 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -256,7 +256,7 @@ void TheoryModel::assertPredicate( Node a, bool polarity ){
}
/** assert equality engine */
-void TheoryModel::assertEqualityEngine( eq::EqualityEngine* ee ){
+void TheoryModel::assertEqualityEngine( const eq::EqualityEngine* ee ){
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
while( !eqcs_i.isFinished() ){
Node eqc = (*eqcs_i);
diff --git a/src/theory/model.h b/src/theory/model.h
index 940a2f527..4a4bf48c9 100644
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -123,7 +123,7 @@ public:
/** assert predicate holds in the model */
void assertPredicate( Node a, bool polarity );
/** assert all equalities/predicates in equality engine hold in the model */
- void assertEqualityEngine( eq::EqualityEngine* ee );
+ void assertEqualityEngine( const eq::EqualityEngine* ee );
public:
/** general queries */
bool hasTerm( Node a );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback