diff options
Diffstat (limited to 'src/theory/quantifiers/quant_util.cpp')
-rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 23 |
1 files changed, 17 insertions, 6 deletions
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 6d28c574a..01f362d25 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -30,27 +30,38 @@ QuantifiersModule::QEffort QuantifiersModule::needsModel(Theory::Effort e) return QEFFORT_NONE; } -eq::EqualityEngine * QuantifiersModule::getEqualityEngine() { +eq::EqualityEngine* QuantifiersModule::getEqualityEngine() const +{ return d_quantEngine->getActiveEqualityEngine(); } -bool QuantifiersModule::areEqual( TNode n1, TNode n2 ) { +bool QuantifiersModule::areEqual(TNode n1, TNode n2) const +{ return d_quantEngine->getEqualityQuery()->areEqual( n1, n2 ); } -bool QuantifiersModule::areDisequal( TNode n1, TNode n2 ) { +bool QuantifiersModule::areDisequal(TNode n1, TNode n2) const +{ return d_quantEngine->getEqualityQuery()->areDisequal( n1, n2 ); } -TNode QuantifiersModule::getRepresentative( TNode n ) { +TNode QuantifiersModule::getRepresentative(TNode n) const +{ return d_quantEngine->getEqualityQuery()->getRepresentative( n ); } -quantifiers::TermDb * QuantifiersModule::getTermDatabase() { +QuantifiersEngine* QuantifiersModule::getQuantifiersEngine() const +{ + return d_quantEngine; +} + +quantifiers::TermDb* QuantifiersModule::getTermDatabase() const +{ return d_quantEngine->getTermDatabase(); } -quantifiers::TermUtil * QuantifiersModule::getTermUtil() { +quantifiers::TermUtil* QuantifiersModule::getTermUtil() const +{ return d_quantEngine->getTermUtil(); } |