add relevant domain computation

1 files changed, 8 insertions, 0 deletions

diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 0678e230f..cb8cb8154 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -42,6 +42,11 @@ QuantifiersModule( qe ){
     d_builder = new QModelBuilderDefault( c, qe );
   }
 
+  if( options::fmfRelevantDomain() ){
+    d_rel_dom = new RelevantDomain( qe, qe->getModel() );
+  }else{
+    d_rel_dom = NULL;
+  }
 }
 
 void ModelEngine::check( Theory::Effort e ){
@@ -153,6 +158,9 @@ int ModelEngine::checkModel(){
     }
   }
   //relevant domain?
+  if( d_rel_dom ){
+    d_rel_dom->compute();
+  }
 
   d_triedLemmas = 0;
   d_addedLemmas = 0;