Add owner map to better manage QuantifiersModules. Initial infrastructure for cegqi.

16 files changed, 223 insertions, 83 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 908e3de6c..3e0831467 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -329,6 +329,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/quant_conflict_find.cpp \
 	theory/quantifiers/conjecture_generator.h \
 	theory/quantifiers/conjecture_generator.cpp \
+	theory/quantifiers/ce_guided_instantiation.h \
+	theory/quantifiers/ce_guided_instantiation.cpp \
 	theory/quantifiers/options_handlers.h \
 	theory/arith/theory_arith_type_rules.h \
 	theory/arith/type_enumerator.h \
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 366c76194..6fce26484 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1191,7 +1191,7 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
         PARSER_STATE->warning(ss.str());
       }
       // do nothing
-    } else if(attr == ":axiom" || attr == ":conjecture") {
+    } else if(attr==":axiom" || attr==":conjecture" || attr==":sygus" || attr==":synthesis") {
       if(hasValue) {
         std::stringstream ss;
         ss << "warning: Attribute " << attr << " does not take a value (ignoring)";
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
new file mode 100644
index 000000000..fec4255b2
--- /dev/null
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -0,0 +1,47 @@
+/*********************                                                        */
+/*! \file ce_guided_instantiation.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief counterexample guided instantiation class
+ **
+ **/
+
+#include "theory/quantifiers/ce_guided_instantiation.h"
+#include "theory/theory_engine.h"
+#include "theory/quantifiers/options.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/first_order_model.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace std;
+
+namespace CVC4 {
+
+CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ) {
+
+  
+}
+
+void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
+  //TODO
+}
+
+void CegInstantiation::registerQuantifier( Node q ) {
+  //TODO
+}
+
+void CegInstantiation::assertNode( Node n ) {
+  
+}
+  
+}
\ No newline at end of file
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
new file mode 100644
index 000000000..7861deffa
--- /dev/null
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -0,0 +1,46 @@
+/*********************                                                        */
+/*! \file ce_guided_instantiation.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief counterexample guided instantiation class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CE_GUIDED_INSTANTIATION_H
+#define CE_GUIDED_INSTANTIATION_H
+
+#include "context/cdhashmap.h"
+#include "context/cdchunk_list.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class CegInstantiation : public QuantifiersModule
+{
+public:
+  CegInstantiation( QuantifiersEngine * qe, context::Context* c );
+public:
+  /* Call during quantifier engine's check */
+  void check( Theory::Effort e, unsigned quant_e );
+  /* Called for new quantifiers */
+  void registerQuantifier( Node q );
+  void assertNode( Node n );
+  /** Identify this module (for debugging, dynamic configuration, etc..) */
+  std::string identify() const { return "CegInstantiation"; }
+};
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 25f15cd78..6a2bd5e2e 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -347,47 +347,3 @@ Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){
   Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta );
   return mkRationalNode(qmodel);
 }
-
-
-InstStrategyDatatypesValue::InstStrategyDatatypesValue( TheoryDatatypes* th, QuantifiersEngine* qe ) :
-  InstStrategy( qe ), d_th( th ){
-
-}
-
-bool InstStrategyDatatypesValue::calculateShouldProcess( Node f ){
-  //DO_THIS
-  return false;
-}
-
-void InstStrategyDatatypesValue::processResetInstantiationRound( Theory::Effort effort ){
-
-}
-
-int InstStrategyDatatypesValue::process( Node f, Theory::Effort effort, int e ){
-  Debug("quant-datatypes") << "Datatypes: Try to solve (" << e << ") for " << f << "... " << std::endl;
-  if( e<2 ){
-    return InstStrategy::STATUS_UNFINISHED;
-  }else if( e==2 ){
-    InstMatch m( f );
-    for( int j = 0; j<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){
-      Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
-      if( i.getType().isDatatype() ){
-        Node n = getValueFor( i );
-        Debug("quant-datatypes-debug") << "Value for " << i << " is " << n << std::endl;
-        m.setValue( j, n);
-      }
-    }
-    //d_quantEngine->addInstantiation( f, m );
-  }
-  return InstStrategy::STATUS_UNKNOWN;
-}
-
-Node InstStrategyDatatypesValue::getValueFor( Node n ){
-  //simply get the ground value for n in the current model, if it exists,
-  //  or return an arbitrary ground term otherwise
-  if( !TermDb::hasInstConstAttr(n) ){
-    return n;
-  }else{
-    return n;
-  }
-}
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 9196b9703..bfc0501dc 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -81,29 +81,6 @@ public:
 };
 
 
-class InstStrategyDatatypesValue : public InstStrategy
-{
-protected:
-  /** calculate if we should process this quantifier */
-  bool calculateShouldProcess( Node f );
-private:
-  /** reference to theory datatypes */
-  datatypes::TheoryDatatypes* d_th;
-  /** get value function */
-  Node getValueFor( Node n );
-public:
-  //constructor
-  InstStrategyDatatypesValue( datatypes::TheoryDatatypes* th, QuantifiersEngine* qe );
-  ~InstStrategyDatatypesValue(){}
-  /** reset instantiation */
-  void processResetInstantiationRound( Theory::Effort effort );
-  /** process method, returns a status */
-  int process( Node f, Theory::Effort effort, int e );
-  /** identify */
-  std::string identify() const { return std::string("InstStrategyDatatypesValue"); }
-
-};/* class InstStrategy */
-
 }
 }
 }
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 7207ceefb..9c3673bc2 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -215,7 +215,7 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
     for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
       Node n = d_quantEngine->getModel()->getAssertedQuantifier( i );
       //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
-      if( TermDb::isRewriteRule( n ) ){
+      if( !d_quantEngine->hasOwnership( n, this ) ){
         d_quant_active[n] = false;
       }else if( !d_quantEngine->getModel()->isQuantifierActive( n ) ){
         d_quant_active[n] = false;
@@ -300,7 +300,7 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
 }
 
 void InstantiationEngine::registerQuantifier( Node f ){
-  if( !TermDb::isRewriteRule( f ) ){
+  if( d_quantEngine->hasOwnership( f, this ) ){
     //Notice() << "do cbqi " << f << " ? " << std::endl;
     if( options::cbqi() ){
       Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 2c9a33388..cbff2b581 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -40,7 +40,7 @@ TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_curr_model( c, NULL ), d_qe
 }
 
 bool QModelBuilder::isQuantifierActive( Node f ) {
-  return !TermDb::isRewriteRule( f );
+  return d_qe->hasOwnership( f );
 }
 
 
@@ -382,8 +382,7 @@ QModelBuilderIG::Statistics::~Statistics(){
 }
 
 bool QModelBuilderIG::isQuantifierActive( Node f ){
-  return !TermDb::isRewriteRule( f ) &&
-         ( d_considerAxioms || !d_qe->getTermDatabase()->isQAttrAxiom( f ) ) && d_quant_sat.find( f )==d_quant_sat.end();
+  return d_qe->hasOwnership( f ) && ( d_considerAxioms || !d_qe->getTermDatabase()->isQAttrAxiom( f ) ) && d_quant_sat.find( f )==d_quant_sat.end();
 }
 
 bool QModelBuilderIG::isTermActive( Node n ){
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 872f270e7..5e3c66d9a 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -173,4 +173,8 @@ option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 0
  number of ground terms to generate for model filtering
 option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false
  more aggressive merging for universal equality engine, introduces terms
+ 
+option ceGuidedInst --cegqi bool :default false
+  counterexample guided quantifier instantiation
+ 
 endmodule
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index ee4464f87..060994379 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1702,7 +1702,7 @@ Node QuantConflictFind::mkEqNode( Node a, Node b ) {
 //-------------------------------------------------- registration

 

 void QuantConflictFind::registerQuantifier( Node q ) {

-  if( !TermDb::isRewriteRule( q ) ){

+  if( d_quantEngine->hasOwnership( q, this ) ){

     d_quants.push_back( q );

     d_quant_id[q] = d_quants.size();

     Trace("qcf-qregister") << "Register ";

@@ -1839,7 +1839,7 @@ bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) {
 //-------------------------------------------------- handling assertions / eqc

 

 void QuantConflictFind::assertNode( Node q ) {

-  if( !TermDb::isRewriteRule( q ) ){

+  if( d_quantEngine->hasOwnership( q, this ) ){

     Trace("qcf-proc") << "QCF : assertQuantifier : ";

     debugPrintQuant("qcf-proc", q);

     Trace("qcf-proc") << std::endl;

diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index f58e89c38..48608cb4e 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -33,6 +33,14 @@ void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n, s
     Trace("quant-attr-debug") << "Set conjecture " << n << std::endl;
     ConjectureAttribute ca;
     n.setAttribute( ca, true );
+  }else if( attr=="sygus" ){
+    Trace("quant-attr-debug") << "Set sygus " << n << std::endl;
+    SygusAttribute ca;
+    n.setAttribute( ca, true );
+  }else if( attr=="synthesis" ){
+    Trace("quant-attr-debug") << "Set synthesis " << n << std::endl;
+    SynthesisAttribute ca;
+    n.setAttribute( ca, true );
   }else if( attr=="quant-inst-max-level" ){
     Assert( node_values.size()==1 );
     uint64_t lvl = node_values[0].getConst<Rational>().getNumerator().getLong();
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index d142007c6..fb7ff679b 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1117,7 +1117,7 @@ Node QuantifiersRewriter::rewriteRewriteRule( Node r ) {
   NodeBuilder<> patternListB(kind::INST_PATTERN_LIST);
   //the entire rewrite rule is the first pattern
   if( options::quantRewriteRules() ){
-    patternListB << NodeManager::currentNM()->mkNode( INST_PATTERN, r );
+    patternListB << NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, r );
   }
   patternListB << static_cast<Node>(patternB);
   forallB << static_cast<Node>(patternListB);
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 7ec503016..405b3749d 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -21,6 +21,8 @@
 #include "theory/quantifiers/theory_quantifiers.h"
 #include "util/datatype.h"
 #include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/quantifiers/ce_guided_instantiation.h"
+#include "theory/quantifiers/rewrite_engine.h"
 
 using namespace std;
 using namespace CVC4;
@@ -991,6 +993,16 @@ void TermDb::computeAttributes( Node q ) {
           Trace("quant-attr") << "Attribute : conjecture : " << q << std::endl;
           d_qattr_conjecture[q] = true;
         }
+        if( avar.getAttribute(SygusAttribute()) ){
+          Trace("quant-attr") << "Attribute : sygus : " << q << std::endl;
+          d_qattr_sygus[q] = true;
+          d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() );
+        }
+        if( avar.getAttribute(SynthesisAttribute()) ){
+          Trace("quant-attr") << "Attribute : synthesis : " << q << std::endl;
+          d_qattr_synthesis[q] = true;
+          d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() );
+        }
         if( avar.hasAttribute(QuantInstLevelAttribute()) ){
           d_qattr_qinstLevel[q] = avar.getAttribute(QuantInstLevelAttribute());
           Trace("quant-attr") << "Attribute : quant inst level " << d_qattr_qinstLevel[q] << " : " << q << std::endl;
@@ -999,6 +1011,11 @@ void TermDb::computeAttributes( Node q ) {
           d_qattr_rr_priority[q] = avar.getAttribute(RrPriorityAttribute());
           Trace("quant-attr") << "Attribute : rr priority " << d_qattr_rr_priority[q] << " : " << q << std::endl;
         }
+        if( avar.getKind()==REWRITE_RULE ){
+          Assert( i==0 );
+          //set rewrite engine as owner
+          d_quantEngine->setOwner( q, d_quantEngine->getRewriteEngine() );
+        }
       }
     }
   }
@@ -1022,6 +1039,24 @@ bool TermDb::isQAttrAxiom( Node q ) {
   }
 }
 
+bool TermDb::isQAttrSygus( Node q ) {
+  std::map< Node, bool >::iterator it = d_qattr_sygus.find( q );
+  if( it==d_qattr_sygus.end() ){
+    return false;
+  }else{
+    return it->second;
+  }
+}
+
+bool TermDb::isQAttrSynthesis( Node q ) {
+  std::map< Node, bool >::iterator it = d_qattr_synthesis.find( q );
+  if( it==d_qattr_synthesis.end() ){
+    return false;
+  }else{
+    return it->second;
+  }
+}
+
 int TermDb::getQAttrQuantInstLevel( Node q ) {
   std::map< Node, int >::iterator it = d_qattr_qinstLevel.find( q );
   if( it==d_qattr_qinstLevel.end() ){
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index e9234bdfe..3bd0563b6 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -33,6 +33,14 @@ typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute;
 struct ConjectureAttributeId {};
 typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute;
   
+/** Attribute true for quantifiers that are SyGus conjectures */
+struct SygusAttributeId {};
+typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute;
+
+/** Attribute true for quantifiers that are synthesis conjectures */
+struct SynthesisAttributeId {};
+typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute;
+
 /** Attribute true for nodes that should not be used for matching */
 struct NoMatchAttributeId {};
 /** use the special for boolean flag */
@@ -297,6 +305,8 @@ public: //general queries concerning quantified formulas wrt modules
 private:
   std::map< Node, bool > d_qattr_conjecture;
   std::map< Node, bool > d_qattr_axiom;
+  std::map< Node, bool > d_qattr_sygus;
+  std::map< Node, bool > d_qattr_synthesis;
   std::map< Node, int > d_qattr_rr_priority;
   std::map< Node, int > d_qattr_qinstLevel;
   //record attributes
@@ -306,6 +316,10 @@ public:
   bool isQAttrConjecture( Node q );
   /** is axiom */
   bool isQAttrAxiom( Node q );
+  /** is sygus conjecture */
+  bool isQAttrSygus( Node q );
+  /** is synthesis conjecture */
+  bool isQAttrSynthesis( Node q );
   /** get instantiation level */
   int getQAttrQuantInstLevel( Node q );
   /** get rewrite rule priority */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 7ed5b2164..dfa17558d 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -31,6 +31,7 @@
 #include "theory/quantifiers/rewrite_engine.h"
 #include "theory/quantifiers/quant_conflict_find.h"
 #include "theory/quantifiers/conjecture_generator.h"
+#include "theory/quantifiers/ce_guided_instantiation.h"
 #include "theory/quantifiers/relevant_domain.h"
 #include "theory/uf/options.h"
 #include "theory/uf/theory_uf.h"
@@ -116,6 +117,12 @@ d_lemmas_produced_c(u){
   }else{
     d_rr_engine = NULL;
   }
+  if( options::ceGuidedInst() ){
+    d_ceg_inst = new quantifiers::CegInstantiation( this, c );
+    d_modules.push_back( d_ceg_inst );
+  }else{
+    d_ceg_inst = NULL;
+  }
 
   //options
   d_total_inst_count_debug = 0;
@@ -164,6 +171,30 @@ void QuantifiersEngine::finishInit(){
   }
 }
 
+QuantifiersModule * QuantifiersEngine::getOwner( Node q ) { 
+  std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q );
+  if( it==d_owner.end() ){
+    return NULL;
+  }else{
+    return it->second;
+  }
+}
+
+void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m ) {
+  QuantifiersModule * mo = getOwner( q );
+  if( mo!=m ){
+    if( mo!=NULL ){
+      Trace("quant-warn") << "WARNING: setting owner of " << q << " to " << m->identify() << ", but already has owner " << mo->identify() << "!" << std::endl;
+    }
+    d_owner[q] = m; 
+  }
+}
+
+bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) {
+  QuantifiersModule * mo = getOwner( q );
+  return mo==m || mo==NULL;
+}
+
 void QuantifiersEngine::check( Theory::Effort e ){
   CodeTimer codeTimer(d_time);
   bool needsCheck = false;
@@ -276,9 +307,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
 void QuantifiersEngine::registerQuantifier( Node f ){
   if( std::find( d_quants.begin(), d_quants.end(), f )==d_quants.end() ){
     Trace("quant") << "QuantifiersEngine : Register quantifier ";
-    if( d_term_db->isRewriteRule( f ) ){
-      Trace("quant") << " (rewrite rule)";
-    }
     Trace("quant") << " : " << f << std::endl;
     d_quants.push_back( f );
 
@@ -287,6 +315,10 @@ void QuantifiersEngine::registerQuantifier( Node f ){
     //make instantiation constants for f
     d_term_db->makeInstantiationConstantsFor( f );
     d_term_db->computeAttributes( f );
+    QuantifiersModule * qm = getOwner( f );
+    if( qm!=NULL ){
+      Trace("quant") << "   Owner : " << qm->identify() << std::endl;
+    }
     //register with quantifier relevance
     if( d_quant_rel ){
       d_quant_rel->registerQuantifier( f );
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index e84c4742e..d40277112 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -74,6 +74,7 @@ namespace quantifiers {
   class RewriteEngine;
   class RelevantDomain;
   class ConjectureGenerator;
+  class CegInstantiation;
 }/* CVC4::theory::quantifiers */
 
 namespace inst {
@@ -115,6 +116,8 @@ private:
   quantifiers::RewriteEngine * d_rr_engine;
   /** subgoal generator */
   quantifiers::ConjectureGenerator * d_sg_gen;
+  /** ceg instantiation */
+  quantifiers::CegInstantiation * d_ceg_inst;
 public: //effort levels
   enum {
     QEFFORT_CONFLICT,
@@ -160,10 +163,6 @@ public:
   /** get equality query object for the given type. The default is the
       generic one */
   EqualityQueryQuantifiersEngine* getEqualityQuery();
-  /** get instantiation engine */
-  quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
-  /** get model engine */
-  quantifiers::ModelEngine* getModelEngine() { return d_model_engine; }
   /** get default sat context for quantifiers engine */
   context::Context* getSatContext();
   /** get default sat context for quantifiers engine */
@@ -180,10 +179,31 @@ public:
   QuantPhaseReq* getPhaseRequirements( Node f ) { return d_phase_reqs.find( f )==d_phase_reqs.end() ? NULL : d_phase_reqs[f]; }
   /** get phase requirement terms */
   void getPhaseReqTerms( Node f, std::vector< Node >& nodes );
+public:  //modules
+  /** get instantiation engine */
+  quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
+  /** get model engine */
+  quantifiers::ModelEngine* getModelEngine() { return d_model_engine; }
   /** get bounded integers utility */
   quantifiers::BoundedIntegers * getBoundedIntegers() { return d_bint; }
   /** Conflict find mechanism for quantifiers */
   quantifiers::QuantConflictFind* getConflictFind() { return d_qcf; }
+  /** rewrite rules utility */
+  quantifiers::RewriteEngine * getRewriteEngine() { return d_rr_engine; }
+  /** subgoal generator */
+  quantifiers::ConjectureGenerator * getConjectureGenerator() { return d_sg_gen; }
+  /** ceg instantiation */
+  quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; }
+private:
+  /** owner of quantified formulas */
+  std::map< Node, QuantifiersModule * > d_owner;
+public:
+  /** get owner */
+  QuantifiersModule * getOwner( Node q );
+  /** set owner */
+  void setOwner( Node q, QuantifiersModule * m );
+  /** considers */
+  bool hasOwnership( Node q, QuantifiersModule * m = NULL );
 public:
   /** initialize */
   void finishInit();