More work on inst propagate. Optimization for qcf to check instances eagerly. Improvements to equality query for disequalities.

1 files changed, 3 insertions, 10 deletions

diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 3b7787a20..437f1bddf 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -33,22 +33,15 @@ eq::EqualityEngine * QuantifiersModule::getEqualityEngine() {
 }
 
 bool QuantifiersModule::areEqual( TNode n1, TNode n2 ) {
-  eq::EqualityEngine * ee = getEqualityEngine();
-  return n1==n2 || ( ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areEqual( n1, n2 ) );
+  return d_quantEngine->getEqualityQuery()->areEqual( n1, n2 );
 }
 
 bool QuantifiersModule::areDisequal( TNode n1, TNode n2 ) {
-  eq::EqualityEngine * ee = getEqualityEngine();
-  return n1!=n2 && ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areDisequal( n1, n2, false );
+  return d_quantEngine->getEqualityQuery()->areDisequal( n1, n2 );
 }
 
 TNode QuantifiersModule::getRepresentative( TNode n ) {
-  eq::EqualityEngine * ee = getEqualityEngine();
-  if( ee->hasTerm( n ) ){
-    return ee->getRepresentative( n );
-  }else{
-    return n;
-  }
+  return d_quantEngine->getEqualityQuery()->getRepresentative( n );
 }
 
 quantifiers::TermDb * QuantifiersModule::getTermDatabase() {