summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/inst_match.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/inst_match.cpp')
-rw-r--r--src/theory/quantifiers/inst_match.cpp12
1 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index dcd7a1b79..85a96f90a 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -103,12 +103,12 @@ void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){
}
}
-void InstMatch::makeInternalRepresentative( QuantifiersEngine* qe ){
- EqualityQueryQuantifiersEngine* eqqe = (EqualityQueryQuantifiersEngine*)qe->getEqualityQuery();
- for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
- d_map[ it->first ] = eqqe->getInternalRepresentative( it->second );
- }
-}
+//void InstMatch::makeInternalRepresentative( QuantifiersEngine* qe ){
+// EqualityQueryQuantifiersEngine* eqqe = (EqualityQueryQuantifiersEngine*)qe->getEqualityQuery();
+// for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
+// d_map[ it->first ] = eqqe->getInternalRepresentative( it->second );
+// }
+//}
void InstMatch::makeRepresentative( QuantifiersEngine* qe ){
for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback