11 files changed, 315 insertions, 104 deletions

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index fec4255b2..f4cdd1a60 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -27,21 +27,190 @@ using namespace std;
 
 namespace CVC4 {
 
-CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ) {
+CegInstantiation::CegConjecture::CegConjecture() {
+}
+
+void CegInstantiation::CegConjecture::assign( Node q ) {
+  Assert( d_quant.isNull() );
+  Assert( q.getKind()==FORALL );
+  d_quant = q;
+  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+    d_candidates.push_back( NodeManager::currentNM()->mkSkolem( "e", q[0][i].getType() ) );
+  }
+}
+void CegInstantiation::CegConjecture::initializeGuard( QuantifiersEngine * qe ){
+  if( d_guard.isNull() ){
+    d_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
+    //specify guard behavior
+    qe->getValuation().ensureLiteral( d_guard );
+    qe->getOutputChannel().requirePhase( d_guard, true );
+  }
+}
+
+CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ), d_conj_active( c, false ), d_conj_infeasible( c, false ), d_guard_assertions( c ) {
 
-  
+}
+
+bool CegInstantiation::needsCheck( Theory::Effort e ) {
+  return e>=Theory::EFFORT_LAST_CALL;
 }
 
 void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
-  //TODO
+  if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
+    Trace("cegqi-engine") << "---Countexample Guided Instantiation Engine---" << std::endl;
+    Trace("cegqi-debug") << "Current conjecture status : " << d_conj_active << " " << d_conj_infeasible << std::endl;
+    if( d_conj_active && !d_conj_infeasible ){
+      checkCegConjecture( &d_conj );
+    }
+    Trace("cegqi-engine") << "Finished Countexample Guided Instantiation engine." << std::endl;
+  }
 }
 
 void CegInstantiation::registerQuantifier( Node q ) {
-  //TODO
+  if( d_quantEngine->getOwner( q )==this ){
+    if( !d_conj.isAssigned() ){
+      Trace("cegqi") << "Register conjecture : " << q << std::endl;
+      d_conj.assign( q );
+      //construct base instantiation
+      d_conj.d_base_inst = Rewriter::rewrite( d_quantEngine->getInstantiation( q, d_conj.d_candidates ) );
+      Trace("cegqi") << "Base instantiation is : " << d_conj.d_base_inst << std::endl;
+      if( getTermDatabase()->isQAttrSygus( q ) ){
+        Assert( d_conj.d_base_inst.getKind()==NOT );
+        Assert( d_conj.d_base_inst[0].getKind()==FORALL );
+        for( unsigned j=0; j<d_conj.d_base_inst[0][0].getNumChildren(); j++ ){
+          d_conj.d_inner_vars.push_back( d_conj.d_base_inst[0][0][j] );
+        }
+      }else if( getTermDatabase()->isQAttrSynthesis( q ) ){
+        //add immediate lemma
+        Node lem = NodeManager::currentNM()->mkNode( OR, d_conj.d_guard.negate(), d_conj.d_base_inst );
+      }
+    }else{
+      Assert( d_conj.d_quant==q );
+    }
+  }
 }
 
 void CegInstantiation::assertNode( Node n ) {
-  
+  Trace("cegqi-debug") << "Cegqi : Assert : " << n << std::endl;
+  bool pol = n.getKind()!=NOT;
+  Node lit = n.getKind()==NOT ? n[0] : n;
+  if( lit==d_conj.d_guard ){
+    d_guard_assertions[lit] = pol;
+    d_conj_infeasible = !pol;
+  }
+  if( lit==d_conj.d_quant ){
+    d_conj_active = true;
+  }
+}
+
+Node CegInstantiation::getNextDecisionRequest() {
+  d_conj.initializeGuard( d_quantEngine );
+  bool value;
+  if( !d_quantEngine->getValuation().hasSatValue( d_conj.d_guard, value ) ) {
+    if( d_guard_assertions.find( d_conj.d_guard )==d_guard_assertions.end() ){
+      if( d_conj.d_guard_split.isNull() ){
+        Node lem = NodeManager::currentNM()->mkNode( OR, d_conj.d_guard.negate(), d_conj.d_guard );
+        d_quantEngine->getOutputChannel().lemma( lem );
+      }
+      Trace("cegqi-debug") << "Decide next on : " << d_conj.d_guard << "..." << std::endl;
+      return d_conj.d_guard;
+    }
+  }
+  return Node::null();
+}
+
+void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
+  Node q = conj->d_quant;
+  Trace("cegqi-engine-debug") << "Synthesis conjecture : " << q << std::endl;
+  Trace("cegqi-engine-debug") << "  * Candidate program/output : ";
+  for( unsigned i=0; i<conj->d_candidates.size(); i++ ){
+    Trace("cegqi-engine-debug") << conj->d_candidates[i] << " ";
+  }
+  Trace("cegqi-engine-debug") << std::endl;
+
+  if( getTermDatabase()->isQAttrSygus( q ) ){
+    Trace("cegqi-engine-debug") << "  * Values are : ";
+    bool success = true;
+    std::vector< Node > model_values;
+    for( unsigned i=0; i<conj->d_candidates.size(); i++ ){
+      Node v = getModelValue( conj->d_candidates[i] );
+      model_values.push_back( v );
+      Trace("cegqi-engine-debug") << v << " ";
+      if( v.isNull() ){
+        success = false;
+      }
+    }
+    Trace("cegqi-engine-debug") << std::endl;
+
+    if( success ){
+      //must get a counterexample to the value of the current candidate
+      Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() );
+      inst = Rewriter::rewrite( inst );
+      //body should be an existential
+      Assert( inst.getKind()==NOT );
+      Assert( inst[0].getKind()==FORALL );
+      //immediately skolemize
+      Node inst_sk = getTermDatabase()->getSkolemizedBody( inst[0] );
+      Trace("cegqi-lemma") << "Counterexample lemma : " << inst_sk << std::endl;
+      d_quantEngine->addLemma( NodeManager::currentNM()->mkNode( OR, q.negate(), inst_sk ) );
+
+      //candidate refinement : the next candidate must satisfy the counterexample found for the current model of the candidate
+      Assert( conj->d_inner_vars.size()==getTermDatabase()->d_skolem_constants[inst[0]].size() );
+      Node inst_ce_refine = conj->d_base_inst[0][1].substitute( conj->d_inner_vars.begin(), conj->d_inner_vars.end(),
+                                                                getTermDatabase()->d_skolem_constants[inst[0]].begin(), getTermDatabase()->d_skolem_constants[inst[0]].end() );
+      Node lem = NodeManager::currentNM()->mkNode( OR, conj->d_guard.negate(), inst_ce_refine.negate() );
+      Trace("cegqi-lemma") << "Candidate refinement lemma : " << lem << std::endl;
+      d_quantEngine->addLemma( lem );
+    }
+
+  }else if( getTermDatabase()->isQAttrSynthesis( q ) ){
+    std::vector< Node > model_terms;
+    for( unsigned i=0; i<conj->d_candidates.size(); i++ ){
+      Node t = getModelTerm( conj->d_candidates[i] );
+      model_terms.push_back( t );
+    }
+    d_quantEngine->addInstantiation( q, model_terms, false );
+  }
 }
-  
+
+Node CegInstantiation::getModelValue( Node n ) {
+  Trace("cegqi-mv") << "getModelValue for : " << n << std::endl;
+  //return d_quantEngine->getTheoryEngine()->getModelValue( n );
+  TypeNode tn = n.getType();
+  if( getEqualityEngine()->hasTerm( n ) ){
+    Node r = getRepresentative( n );
+    Node v;
+    eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );
+    while( !eqc_i.isFinished() ){
+      TNode nn = (*eqc_i);
+      if( nn.isConst() ){
+        Trace("cegqi-mv") << "..constant : " << nn << std::endl;
+        return nn;
+      }else if( nn.getKind()==APPLY_CONSTRUCTOR ){
+        v = nn;
+      }
+      ++eqc_i;
+    }
+    if( !v.isNull() ){
+      std::vector< Node > children;
+      if( v.hasOperator() ){
+        children.push_back( v.getOperator() );
+      }
+      for( unsigned i=0; i<v.getNumChildren(); i++ ){
+        children.push_back( getModelValue( v[i] ) );
+      }
+      Node vv = NodeManager::currentNM()->mkNode( v.getKind(), children );
+      Trace("cegqi-mv") << "...value : " << vv << std::endl;
+      return vv;
+    }
+  }
+  Node e = getTermDatabase()->getEnumerateTerm( tn, 0 );
+  Trace("cegqi-mv") << "...enumerate : " << e << std::endl;
+  return e;
+}
+
+Node CegInstantiation::getModelTerm( Node n ){
+  return getModelValue( 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
index 7861deffa..6139f8f59 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -25,16 +25,59 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+
+
 class CegInstantiation : public QuantifiersModule
 {
+  typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
+private:
+  class CegConjecture {
+  public:
+    CegConjecture();
+    /** quantified formula */
+    Node d_quant;
+    /** guard */
+    Node d_guard;
+    /** base instantiation */
+    Node d_base_inst;
+    /** guard split */
+    Node d_guard_split;
+    /** list of constants for quantified formula */
+    std::vector< Node > d_candidates;
+    /** list of variables on inner quantification */
+    std::vector< Node > d_inner_vars;
+    /** is assigned */
+    bool isAssigned() { return !d_quant.isNull(); }
+    /** assign */
+    void assign( Node q );
+    /** initialize guard */
+    void initializeGuard( QuantifiersEngine * qe );
+  };
+  /** the quantified formula stating the synthesis conjecture */
+  CegConjecture d_conj;
+  /** is conjecture active */
+  context::CDO< bool > d_conj_active;
+  /** is conjecture infeasible */
+  context::CDO< bool > d_conj_infeasible;
+  /** assertions for guards */
+  NodeBoolMap d_guard_assertions;
+private:
+  /** check conjecture */
+  void checkCegConjecture( CegConjecture * conj );
+  /** get model value */
+  Node getModelValue( Node n );
+  /** get model term */
+  Node getModelTerm( Node n );
 public:
   CegInstantiation( QuantifiersEngine * qe, context::Context* c );
 public:
+  bool needsCheck( Theory::Effort e );
   /* 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 );
+  Node getNextDecisionRequest();
   /** Identify this module (for debugging, dynamic configuration, etc..) */
   std::string identify() const { return "CegInstantiation"; }
 };
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index fe3c92323..f491adc7c 100755
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -280,33 +280,6 @@ TNode ConjectureGenerator::getUniversalRepresentative( TNode n, bool add ) {
   }

 }

 

-eq::EqualityEngine * ConjectureGenerator::getEqualityEngine() {

-  return d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();

-}

-

-bool ConjectureGenerator::areEqual( TNode n1, TNode n2 ) {

-  eq::EqualityEngine * ee = getEqualityEngine();

-  return n1==n2 || ( ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areEqual( n1, n2 ) );

-}

-

-bool ConjectureGenerator::areDisequal( TNode n1, TNode n2 ) {

-  eq::EqualityEngine * ee = getEqualityEngine();

-  return n1!=n2 && ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areDisequal( n1, n2, false );

-}

-

-TNode ConjectureGenerator::getRepresentative( TNode n ) {

-  eq::EqualityEngine * ee = getEqualityEngine();

-  if( ee->hasTerm( n ) ){

-    return ee->getRepresentative( n );

-  }else{

-    return n;

-  }

-}

-

-TermDb * ConjectureGenerator::getTermDatabase() {

-  return d_quantEngine->getTermDatabase();

-}

-

 Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) {

   Assert( !tn.isNull() );

   while( d_free_var[tn].size()<=i ){

@@ -1098,27 +1071,6 @@ int ConjectureGenerator::calculateGeneralizationDepth( TNode n, std::vector< TNo
   }

 }

 

-Node ConjectureGenerator::getEnumerateTerm( TypeNode tn, unsigned index ) {

-  std::map< TypeNode, unsigned >::iterator it = d_typ_enum_map.find( tn );

-  unsigned teIndex;

-  if( it==d_typ_enum_map.end() ){

-    teIndex = (int)d_typ_enum.size();

-    d_typ_enum_map[tn] = teIndex;

-    d_typ_enum.push_back( TypeEnumerator(tn) );

-  }else{

-    teIndex = it->second;

-  }

-  while( index>=d_enum_terms[tn].size() ){

-    if( d_typ_enum[teIndex].isFinished() ){

-      return Node::null();

-    }

-    d_enum_terms[tn].push_back( *d_typ_enum[teIndex] );

-    ++d_typ_enum[teIndex];

-  }

-  return d_enum_terms[tn][index];

-}

-

-

 Node ConjectureGenerator::getPredicateForType( TypeNode tn ) {

   std::map< TypeNode, Node >::iterator it = d_typ_pred.find( tn );

   if( it==d_typ_pred.end() ){

@@ -1149,7 +1101,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector<
         vec.push_back( size_limit );

       }else{

         //see if we can iterate current

-        if( vec_sum<size_limit && !getEnumerateTerm( n[index].getType(), vec[index]+1 ).isNull() ){

+        if( vec_sum<size_limit && !getTermDatabase()->getEnumerateTerm( n[index].getType(), vec[index]+1 ).isNull() ){

           vec[index]++;

           vec_sum++;

           vec.push_back( size_limit - vec_sum );

@@ -1164,7 +1116,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector<
       }

       if( success ){

         if( vec.size()==n.getNumChildren() ){

-          Node lc = getEnumerateTerm( n[vec.size()-1].getType(), vec[vec.size()-1] );

+          Node lc = getTermDatabase()->getEnumerateTerm( n[vec.size()-1].getType(), vec[vec.size()-1] );

           if( !lc.isNull() ){

             for( unsigned i=0; i<vec.size(); i++ ){

               Trace("sg-gt-enum-debug") << vec[i] << " ";

@@ -1177,7 +1129,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector<
             std::vector< Node > children;

             children.push_back( n.getOperator() );

             for( unsigned i=0; i<(vec.size()-1); i++ ){

-              Node nn = getEnumerateTerm( n[i].getType(), vec[i] );

+              Node nn = getTermDatabase()->getEnumerateTerm( n[i].getType(), vec[i] );

               Assert( !nn.isNull() );

               Assert( nn.getType()==n[i].getType() );

               children.push_back( nn );

diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 23e2b88ba..59d908fec 100755
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -357,13 +357,6 @@ public:  //for generalization
   // get generalization depth

   int calculateGeneralizationDepth( TNode n, std::vector< TNode >& fv );

 private:

-  //ground term enumeration

-  std::map< TypeNode, std::vector< Node > > d_enum_terms;

-  //type enumerators

-  std::map< TypeNode, unsigned > d_typ_enum_map;

-  std::vector< TypeEnumerator > d_typ_enum;

-  //get nth term for type

-  Node getEnumerateTerm( TypeNode tn, unsigned index );

   //predicate for type

   std::map< TypeNode, Node > d_typ_pred;

   //get predicate for type

@@ -389,12 +382,6 @@ public:  //for property enumeration
   std::map< TNode, std::vector< TNode > > d_subs_confirmWitnessDomain;

   //number of ground substitutions whose equality is unknown

   unsigned d_subs_unkCount;

-public:  //for ground equivalence classes

-  eq::EqualityEngine * getEqualityEngine();

-  bool areDisequal( TNode n1, TNode n2 );

-  bool areEqual( TNode n1, TNode n2 );

-  TNode getRepresentative( TNode n );

-  TermDb * getTermDatabase();

 private:  //information about ground equivalence classes

   TNode d_bool_eqc[2];

   std::map< TNode, Node > d_ground_eqc_map;

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 060994379..8136bf11e 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1851,27 +1851,6 @@ void QuantConflictFind::assertNode( Node q ) {
   }

 }

 

-eq::EqualityEngine * QuantConflictFind::getEqualityEngine() {

-  //return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getEqualityEngine();

-  return d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();

-}

-bool QuantConflictFind::areEqual( Node n1, Node n2 ) {

-  return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areEqual( n1,n2 );

-}

-bool QuantConflictFind::areDisequal( Node n1, Node n2 ) {

-  return n1!=n2 && getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areDisequal( n1,n2, false );

-}

-Node QuantConflictFind::getRepresentative( Node n ) {

-  if( getEqualityEngine()->hasTerm( n ) ){

-    return getEqualityEngine()->getRepresentative( n );

-  }else{

-    return n;

-  }

-}

-TermDb* QuantConflictFind::getTermDatabase() { 

-  return d_quantEngine->getTermDatabase();

-}

-

 Node QuantConflictFind::evaluateTerm( Node n ) {

   if( MatchGen::isHandledUfTerm( n ) ){

     Node f = MatchGen::getOperator( this, n );

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index d8f1c8e6f..81f31fa90 100755
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -187,11 +187,6 @@ private:
   NodeList d_qassert;

   std::map< Node, QuantInfo > d_qinfo;

 private:  //for equivalence classes

-  eq::EqualityEngine * getEqualityEngine();

-  bool areDisequal( Node n1, Node n2 );

-  bool areEqual( Node n1, Node n2 );

-  Node getRepresentative( Node n );

-  TermDb* getTermDatabase();

   // type -> list(eqc)

   std::map< TypeNode, std::vector< TNode > > d_eqcs;

   std::map< TypeNode, Node > d_model_basis;

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 405b3749d..9c1eeb9b4 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -751,6 +751,27 @@ Node TermDb::getSkolemizedBody( Node f ){
   return d_skolem_body[ f ];
 }
 
+Node TermDb::getEnumerateTerm( TypeNode tn, unsigned index ) {
+  std::map< TypeNode, unsigned >::iterator it = d_typ_enum_map.find( tn );
+  unsigned teIndex;
+  if( it==d_typ_enum_map.end() ){
+    teIndex = (int)d_typ_enum.size();
+    d_typ_enum_map[tn] = teIndex;
+    d_typ_enum.push_back( TypeEnumerator(tn) );
+  }else{
+    teIndex = it->second;
+  }
+  while( index>=d_enum_terms[tn].size() ){
+    if( d_typ_enum[teIndex].isFinished() ){
+      return Node::null();
+    }
+    d_enum_terms[tn].push_back( *d_typ_enum[teIndex] );
+    ++d_typ_enum[teIndex];
+  }
+  return d_enum_terms[tn][index];
+}
+
+
 Node TermDb::getFreeVariableForInstConstant( Node n ){
   TypeNode tn = n.getType();
   if( d_free_vars.find( tn )==d_free_vars.end() ){
@@ -983,6 +1004,7 @@ Node TermDb::getRewriteRule( Node q ) {
 void TermDb::computeAttributes( Node q ) {
   if( q.getNumChildren()==3 ){
     for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
+      Trace("quant-attr-debug") << "Check : " << q[2][i] << " " << q[2][i].getKind() << std::endl;
       if( q[2][i].getKind()==INST_ATTRIBUTE ){
         Node avar = q[2][i][0];
         if( avar.getAttribute(AxiomAttribute()) ){
@@ -994,13 +1016,22 @@ void TermDb::computeAttributes( Node q ) {
           d_qattr_conjecture[q] = true;
         }
         if( avar.getAttribute(SygusAttribute()) ){
+          //should be nested existential
+          Assert( q[1].getKind()==NOT );
+          Assert( q[1][0].getKind()==FORALL );
           Trace("quant-attr") << "Attribute : sygus : " << q << std::endl;
           d_qattr_sygus[q] = true;
+          if( d_quantEngine->getCegInstantiation()==NULL ){
+            Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl;
+          }
           d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() );
         }
         if( avar.getAttribute(SynthesisAttribute()) ){
           Trace("quant-attr") << "Attribute : synthesis : " << q << std::endl;
           d_qattr_synthesis[q] = true;
+          if( d_quantEngine->getCegInstantiation()==NULL ){
+            Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl;
+          }
           d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() );
         }
         if( avar.hasAttribute(QuantInstLevelAttribute()) ){
@@ -1012,7 +1043,11 @@ void TermDb::computeAttributes( Node q ) {
           Trace("quant-attr") << "Attribute : rr priority " << d_qattr_rr_priority[q] << " : " << q << std::endl;
         }
         if( avar.getKind()==REWRITE_RULE ){
+          Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl;
           Assert( i==0 );
+          if( d_quantEngine->getRewriteEngine()==NULL ){
+            Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : " << q << std::endl;
+          }
           //set rewrite engine as owner
           d_quantEngine->setOwner( q, d_quantEngine->getRewriteEngine() );
         }
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 3bd0563b6..25ef9c81c 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -19,6 +19,7 @@
 
 #include "expr/attribute.h"
 #include "theory/theory.h"
+#include "theory/type_enumerator.h"
 
 #include <map>
 
@@ -241,6 +242,8 @@ public:
 public:
   //get bound variables in n
   static void getBoundVars( Node n, std::vector< Node >& bvs);
+  
+  
 //for skolem
 private:
   /** map from universal quantifiers to their skolemized body */
@@ -253,7 +256,20 @@ public:
                                 std::vector< Node >& sk, Node& sub, std::vector< unsigned >& sub_vars );
   /** get the skolemized body */
   Node getSkolemizedBody( Node f);
-
+  /** is induction variable */
+  static bool isInductionTerm( Node n );
+  
+//for ground term enumeration
+private:  
+  /** ground terms enumerated for types */
+  std::map< TypeNode, std::vector< Node > > d_enum_terms;
+  //type enumerators
+  std::map< TypeNode, unsigned > d_typ_enum_map;
+  std::vector< TypeEnumerator > d_typ_enum;
+public:
+  //get nth term for type
+  Node getEnumerateTerm( TypeNode tn, unsigned index );  
+  
 //miscellaneous
 public:
   /** map from universal quantifiers to the list of variables */
@@ -289,11 +305,7 @@ public:
   int isInstanceOf( Node n1, Node n2 );
   /** filter all nodes that have instances */
   void filterInstances( std::vector< Node >& nodes );
-  
-public: //for induction
-  /** is induction variable */
-  static bool isInductionTerm( Node n );
-  
+
   
 public: //general queries concerning quantified formulas wrt modules
   /** is quantifier treated as a rewrite rule? */
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index e71489fc5..f7c4c745f 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -42,6 +42,8 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output
   d_baseDecLevel = -1;
   out.handleUserAttribute( "axiom", this );
   out.handleUserAttribute( "conjecture", this );
+  out.handleUserAttribute( "sygus", this );
+  out.handleUserAttribute( "synthesis", this );
   out.handleUserAttribute( "quant-inst-max-level", this );
   out.handleUserAttribute( "rr-priority", this );
 }
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index dfa17558d..d17899cf2 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -43,6 +43,34 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::inst;
 
+
+eq::EqualityEngine * QuantifiersModule::getEqualityEngine() {
+  return d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
+}
+
+bool QuantifiersModule::areEqual( TNode n1, TNode n2 ) {
+  eq::EqualityEngine * ee = getEqualityEngine();
+  return n1==n2 || ( ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->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 );
+}
+
+TNode QuantifiersModule::getRepresentative( TNode n ) {
+  eq::EqualityEngine * ee = getEqualityEngine();
+  if( ee->hasTerm( n ) ){
+    return ee->getRepresentative( n );
+  }else{
+    return n;
+  }
+}
+
+quantifiers::TermDb * QuantifiersModule::getTermDatabase() {
+  return d_quantEngine->getTermDatabase();
+}
+
 QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te):
 d_te( te ),
 d_lemmas_produced_c(u){
@@ -184,7 +212,7 @@ 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;
+      Trace("quant-warn") << "WARNING: setting owner of " << q << " to " << ( m ? m->identify() : "null" ) << ", but already has owner " << mo->identify() << "!" << std::endl;
     }
     d_owner[q] = m; 
   }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index d40277112..b5a02df60 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -37,6 +37,10 @@ namespace theory {
 
 class QuantifiersEngine;
 
+namespace quantifiers {
+  class TermDb;
+}
+
 class QuantifiersModule {
 protected:
   QuantifiersEngine* d_quantEngine;
@@ -61,10 +65,15 @@ public:
   virtual Node explain(TNode n) { return TNode::null(); }
   /** Identify this module (for debugging, dynamic configuration, etc..) */
   virtual std::string identify() const = 0;
+public:
+  eq::EqualityEngine * getEqualityEngine();
+  bool areDisequal( TNode n1, TNode n2 );
+  bool areEqual( TNode n1, TNode n2 );
+  TNode getRepresentative( TNode n );
+  quantifiers::TermDb * getTermDatabase();
 };/* class QuantifiersModule */
 
 namespace quantifiers {
-  class TermDb;
   class FirstOrderModel;
   //modules
   class InstantiationEngine;