From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sun, 15 May 2016 17:34:51 +0000 (-0500)
Subject: Work on --sygus-direct-eval. Minor optimizations, updates to casc scripts. Enable... 
X-Git-Tag: cvc5-1.0.0~6049^2~47
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f58c881034d3b0193dfee8fabf451cc0e9ea20ab;p=cvc5.git

Work on --sygus-direct-eval. Minor optimizations, updates to casc scripts. Enable e-matching when --strings-exp is enabled.
---

diff --git a/contrib/run-script-cascj8-fof b/contrib/run-script-cascj8-fof
index f8d79b1de..fe18c3ed0 100644
--- a/contrib/run-script-cascj8-fof
+++ b/contrib/run-script-cascj8-fof
@@ -30,18 +30,19 @@ function finishwith {
 }
 
 # designed for 300 seconds
-trywith 20 --relevant-triggers --full-saturate-quant 
+trywith 20 --relational-triggers --full-saturate-quant 
 trywith 20 --no-e-matching --full-saturate-quant 
-trywith 20 --finite-model-find --mbqi=abs
+trywith 15 --finite-model-find --mbqi=abs
 trywith 5 --multi-trigger-when-single --full-saturate-quant 
 trywith 5 --trigger-sel=max --full-saturate-quant
-trywith 5 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant 
-trywith 5 --relational-triggers --full-saturate-quant 
-trywith 15 --term-db-mode=relevant --full-saturate-quant
-trywith 15 --pre-quant=none --full-saturate-quant
-trywith 15 --finite-model-find --uf-ss=no-minimal
-trywith 30 --decision=internal --full-saturate-quant
+trywith 5 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant  
+trywith 10 --finite-model-find --uf-ss=no-minimal --sort-inference --uf-ss-fair
+trywith 10 --term-db-mode=relevant --full-saturate-quant
+trywith 15 --prenex-quant=none --full-saturate-quant
+trywith 15 --decision=internal --full-saturate-quant
+trywith 30 --relevant-triggers --full-saturate-quant 
+trywith 30 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair
 trywith 30 --fs-inst --full-saturate-quant
 trywith 30 --no-quant-cf --full-saturate-quant 
-finishwith --relational-triggers --full-saturate-quant 
+finishwith --qcf-vo-exp --full-saturate-quant 
 # echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/run-script-cascj8-tfa b/contrib/run-script-cascj8-tfa
index a7a97a44d..da4056466 100644
--- a/contrib/run-script-cascj8-tfa
+++ b/contrib/run-script-cascj8-tfa
@@ -31,10 +31,10 @@ function finishwith {
 
 trywith 10 --decision=internal --full-saturate-quant
 trywith 10 --finite-model-find --decision=internal
-trywith 10 ---purify-quant --full-saturate-quant
-trywith 10 ---partial-triggers --full-saturate-quant
-trywith 10 ---no-e-matching --full-saturate-quant
+trywith 10 --purify-quant --full-saturate-quant
+trywith 10 --partial-triggers --full-saturate-quant
+trywith 10 --no-e-matching --full-saturate-quant
 trywith 30 --cbqi-all --purify-triggers --full-saturate-quant 
-trywith 60 --cbqi-all ---fs-inst --full-saturate-quant
+trywith 60 --cbqi-all --fs-inst --full-saturate-quant
 finishwith --full-saturate-quant
 # echo "% SZS status" "GaveUp for $filename"
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 7d41ae862..cbef7109f 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -390,7 +390,7 @@ uf-dt-size \n\
 + Enforce fairness using an uninterpreted function for datatypes size.\n\
 \n\
 default | dt-size \n\
-+ Default, enforce fairness using size theory operator.\n\
++ Default, enforce fairness using size operator.\n\
 \n\
 dt-height-bound \n\
 + Enforce fairness by height bound predicate.\n\
@@ -657,6 +657,8 @@ theory::quantifiers::CegqiFairMode OptionsHandler::stringToCegqiFairMode(std::st
     return theory::quantifiers::CEGQI_FAIR_DT_SIZE;
   } else if(optarg == "dt-height-bound" ){
     return theory::quantifiers::CEGQI_FAIR_DT_HEIGHT_PRED;
+  //} else if(optarg == "dt-size-bound" ){
+  //  return theory::quantifiers::CEGQI_FAIR_DT_SIZE_PRED;
   } else if(optarg == "none") {
     return theory::quantifiers::CEGQI_FAIR_NONE;
   } else if(optarg ==  "help") {
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index b4b9abdaf..38308c9dc 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -131,6 +131,8 @@ enum CegqiFairMode {
   CEGQI_FAIR_DT_SIZE,
   /** enforce fairness by datatypes height bound */
   CEGQI_FAIR_DT_HEIGHT_PRED,
+  /** enforce fairness by datatypes size bound */
+  CEGQI_FAIR_DT_SIZE_PRED,
   /** do not use fair strategy for CEGQI */
   CEGQI_FAIR_NONE,
 };
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 19d6885b7..34f399f45 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -144,7 +144,7 @@ option fmfOneInstPerRound --mbqi-one-inst-per-round bool :read-write :default fa
 option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false
  only add instantiations for one quantifier per round for mbqi
 
-option fmfInstEngine --fmf-inst-engine bool :default false
+option fmfInstEngine --fmf-inst-engine bool :default false :read-write
  use instantiation engine in conjunction with finite model finding
 option fmfInstGen --fmf-inst-gen bool :default true
  enable Inst-Gen instantiation techniques for finite model finding 
@@ -258,8 +258,8 @@ option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true
 option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToSygusInvTemplMode
   template mode for sygus invariant synthesis
 
-option sygusEagerUnfold --sygus-eager-unfold bool :default false
-  eager unfold evaluation functions
+option sygusDirectEval --sygus-direct-eval bool :default false
+  direct unfolding of evaluation functions
   
 # approach applied to general quantified formulas
 option cbqiSplx --cbqi-splx bool :read-write :default false
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 78975bbe6..41428ed89 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -802,6 +802,8 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
         //since we enforce satisfaction completeness, immediately convert to total version
         if( k==CVC4::kind::BITVECTOR_UDIV ){
           k = CVC4::kind::BITVECTOR_UDIV_TOTAL;
+        }else if( k==CVC4::kind::BITVECTOR_UREM ){
+          k = CVC4::kind::BITVECTOR_UREM_TOTAL;
         }
         sgt.d_name = kind::kindToString(k);
         sgt.d_gterm_type = SygusGTerm::gterm_op;
@@ -837,6 +839,8 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
           k = PARSER_STATE->getOperatorKind(name);
           if( k==CVC4::kind::BITVECTOR_UDIV ){
             k = CVC4::kind::BITVECTOR_UDIV_TOTAL;
+          }else if( k==CVC4::kind::BITVECTOR_UREM ){
+            k = CVC4::kind::BITVECTOR_UREM_TOTAL;
           }
           sgt.d_name = kind::kindToString(k);
           sgt.d_gterm_type = SygusGTerm::gterm_op;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3a138e4b7..54deba78c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1343,6 +1343,10 @@ void SmtEngine::setDefaults() {
       options::fmfBoundInt.set( true );
       Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
     }
+    if(! options::fmfInstEngine.wasSetByUser()) {
+      options::fmfInstEngine.set( true );
+      Trace("smt") << "turning on fmf-inst-engine, for strings-exp" << std::endl;
+    }
     /*
     if(! options::rewriteDivk.wasSetByUser()) {
       options::rewriteDivk.set( true );
@@ -3895,7 +3899,6 @@ void SmtEnginePrivate::processAssertions() {
 
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
-
   dumpAssertions("pre-constrain-subtypes", d_assertions);
   {
     // Any variables of subtype types need to be constrained properly.
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index d035f0fa7..3338e5f31 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -105,7 +105,7 @@ typerule RECORD_UPDATE ::CVC4::theory::datatypes::RecordUpdateTypeRule
 operator DT_SIZE 1 "datatypes size"
 typerule DT_SIZE ::CVC4::theory::datatypes::DtSizeTypeRule
 
-operator DT_HEIGHT_BOUND 1 "datatypes height bound"
+operator DT_HEIGHT_BOUND 2 "datatypes height bound"
 typerule DT_HEIGHT_BOUND ::CVC4::theory::datatypes::DtHeightBoundTypeRule
 
 endtheory
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 5a3645691..9c8387958 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -299,11 +299,10 @@ public:
         throw TypeCheckingExceptionPrivate(n, "datatype height bound must be non-negative");
       }
     }
-    return nodeManager->integerType();
+    return nodeManager->booleanType();
   }
 };/* class DtHeightBoundTypeRule */
 
-
 }/* CVC4::theory::datatypes namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index ad900ee82..cae3e730e 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -131,14 +131,18 @@ Node CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) {
       qe->getOutputChannel().lemma( lem );
       qe->getOutputChannel().requirePhase( lit, true );
 
-      if( getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED ){
+      if( getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED || getCegqiFairMode()==CEGQI_FAIR_DT_SIZE_PRED ){
         //implies height bounds on each candidate variable
         std::vector< Node > lem_c;
         for( unsigned j=0; j<d_candidates.size(); j++ ){
-          lem_c.push_back( NodeManager::currentNM()->mkNode( DT_HEIGHT_BOUND, d_candidates[j], c ) );
+          if( getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED ){
+            lem_c.push_back( NodeManager::currentNM()->mkNode( DT_HEIGHT_BOUND, d_candidates[j], c ) );
+          }else{
+            //lem_c.push_back( NodeManager::currentNM()->mkNode( DT_SIZE_BOUND, d_candidates[j], c ) );
+          }
         }
         Node hlem = NodeManager::currentNM()->mkNode( OR, lit.negate(), lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c ) );
-        Trace("cegqi-lemma") << "Cegqi::Lemma : Fairness expansion (dt-height-pred) : " << hlem << std::endl;
+        Trace("cegqi-lemma") << "Cegqi::Lemma : Fairness expansion (pred) : " << hlem << std::endl;
         qe->getOutputChannel().lemma( hlem );
       }
       return lit;
@@ -258,8 +262,28 @@ void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
   }
 }
 
+void CegInstantiation::preRegisterQuantifier( Node q ) {
+  if( options::sygusDirectEval() ){
+    if( q.getNumChildren()==3 && q[2].getKind()==INST_PATTERN_LIST && q[2][0].getKind()==INST_PATTERN ){  
+      //check whether it is an evaluation axiom
+      Node pat = q[2][0][0];
+      if( pat.getKind()==APPLY_UF ){
+        TypeNode tn = pat[0].getType();
+        if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){
+          const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+          if( dt.isSygus() ){
+            //take ownership of this quantified formula (will use direct evaluation instead of instantiation)
+            d_quantEngine->setOwner( q, this );
+            d_eval_axioms[q] = true;
+          }
+        }
+      }
+    }
+  }  
+}
+
 void CegInstantiation::registerQuantifier( Node q ) {
-  if( d_quantEngine->getOwner( q )==this ){
+  if( d_quantEngine->getOwner( q )==this && d_eval_axioms.find( q )==d_eval_axioms.end() ){
     if( !d_conj->isAssigned() ){
       Trace("cegqi") << "Register conjecture : " << q << std::endl;
       d_conj->assign( q );
@@ -279,7 +303,7 @@ void CegInstantiation::registerQuantifier( Node q ) {
             if( it!=d_uf_measure.end() ){
               mc.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, it->second, d_conj->d_candidates[j] ) );
             }
-          }else if( d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED ){
+          }else if( d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED || d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_SIZE_PRED  ){
             //measure term is a fresh constant
             mc.push_back( NodeManager::currentNM()->mkSkolem( "K", NodeManager::currentNM()->integerType() ) );
           }
@@ -353,6 +377,11 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
     Trace("cegqi-engine-debug") << conj->d_candidates[i] << " ";
   }
   Trace("cegqi-engine-debug") << std::endl;
+  Trace("cegqi-engine-debug") << "  * Candidate ce skolems : ";
+  for( unsigned i=0; i<conj->d_ce_sk.size(); i++ ){
+    Trace("cegqi-engine-debug") << conj->d_ce_sk[i] << " ";
+  }
+  Trace("cegqi-engine-debug") << std::endl;
   if( conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){
     Trace("cegqi-engine") << "  * Current term size : " << conj->d_curr_lit.get() << std::endl;
   }
@@ -377,6 +406,19 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
       }
       std::vector< Node > model_values;
       if( getModelValues( conj, conj->d_candidates, model_values ) ){
+        if( options::sygusDirectEval() ){
+          std::vector< Node > eager_eval_lem;
+          for( unsigned j=0; j<conj->d_candidates.size(); j++ ){
+            d_quantEngine->getTermDatabaseSygus()->registerModelValue( conj->d_candidates[j], model_values[j], eager_eval_lem );
+          }
+          if( !eager_eval_lem.empty() ){
+            for( unsigned j=0; j<eager_eval_lem.size(); j++ ){
+              Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << eager_eval_lem[j] << std::endl;
+              d_quantEngine->addLemma( eager_eval_lem[j] );
+            }
+            return;
+          }
+        }
         //check if we must apply fairness lemmas
         if( conj->getCegqiFairMode()==CEGQI_FAIR_UF_DT_SIZE ){
           std::vector< Node > lems;
@@ -425,18 +467,28 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
         Node lem = NodeManager::currentNM()->mkNode( OR, ic );
         lem = Rewriter::rewrite( lem );
         d_last_inst_si = false;
+        //eagerly unfold applications of evaluation function
+        if( options::sygusDirectEval() ){
+          Trace("cegqi-eager") << "pre-unfold counterexample : " << lem << std::endl;
+          std::map< Node, Node > visited_n;
+          lem = getEagerUnfold( lem, visited_n );
+        }
+
         Trace("cegqi-lemma") << "Cegqi::Lemma : counterexample : " << lem << std::endl;
-        d_quantEngine->addLemma( lem );
-        ++(d_statistics.d_cegqi_lemmas_ce);
-        Trace("cegqi-engine") << "  ...find counterexample." << std::endl;
-        //optimization : eagerly unfold applications of evaluation function
-        if( options::sygusEagerUnfold() ){
-          std::vector< Node > eager_lems;
-          std::map< Node, bool > visited;
-          getEagerUnfoldLemmas( eager_lems, lem, visited );        
-          for( unsigned i=0; i<eager_lems.size(); i++ ){
-            Trace("cegqi-lemma") << "Cegqi::Lemma : eager unfold : " << eager_lems[i] << std::endl;
-            d_quantEngine->addLemma( eager_lems[i] );
+        if( d_quantEngine->addLemma( lem ) ){
+          ++(d_statistics.d_cegqi_lemmas_ce);
+          Trace("cegqi-engine") << "  ...find counterexample." << std::endl;
+        }else{
+          //this may happen if we eagerly unfold, simplify to true
+          if( !options::sygusDirectEval() ){
+            Trace("cegqi-engine") << "  ...FAILED to add candidate!" << std::endl;
+          }else{
+            Trace("cegqi-engine-debug") << "  ...FAILED to add candidate!" << std::endl;
+          }
+          if( conj->d_refine_count==0  ){
+            //immediately go to refine candidate
+            checkCegConjecture( conj );
+            return;
           }
         }
       }
@@ -602,16 +654,17 @@ void CegInstantiation::getMeasureLemmas( Node n, Node v, std::vector< Node >& le
   }
 }
 
-void CegInstantiation::getEagerUnfoldLemmas( std::vector< Node >& lems, Node n, std::map< Node, bool >& visited ) {
-  if( visited.find( n )==visited.end() ){
-    Trace("cegqi-eager-debug") << "getEagerUnfoldLemmas " << n << std::endl;
-    visited[n] = true;
+Node CegInstantiation::getEagerUnfold( Node n, std::map< Node, Node >& visited ) {
+  std::map< Node, Node >::iterator itv = visited.find( n );
+  if( itv==visited.end() ){
+    Trace("cegqi-eager-debug") << "getEagerUnfold " << n << std::endl;
+    Node ret;
     if( n.getKind()==APPLY_UF ){
       TypeNode tn = n[0].getType();
       Trace("cegqi-eager-debug") << "check " << n[0].getType() << std::endl;
       if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){
         const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-        if( dt.isSygus() ){
+        if( dt.isSygus() ){ 
           Trace("cegqi-eager") << "Unfold eager : " << n << std::endl;
           Node bTerm = d_quantEngine->getTermDatabaseSygus()->sygusToBuiltin( n[0], tn );
           Trace("cegqi-eager") << "Built-in term : " << bTerm << std::endl;
@@ -623,12 +676,13 @@ void CegInstantiation::getEagerUnfoldLemmas( std::vector< Node >& lems, Node n,
             vars.push_back( var_list[j] );
           }
           for( unsigned j=1; j<n.getNumChildren(); j++ ){
+            Node nc = getEagerUnfold( n[j], visited );
             if( var_list[j-1].getType().isBoolean() ){   
               //TODO: remove this case when boolean term conversion is eliminated
               Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
-              subs.push_back( n[j].eqNode( c ) );
+              subs.push_back( nc.eqNode( c ) );
             }else{
-              subs.push_back( n[j] );
+              subs.push_back( nc );
             }
             Assert( subs[j-1].getType()==var_list[j-1].getType() );
           }
@@ -636,16 +690,34 @@ void CegInstantiation::getEagerUnfoldLemmas( std::vector< Node >& lems, Node n,
           Trace("cegqi-eager") << "Built-in term after subs : " << bTerm << std::endl;
           Trace("cegqi-eager-debug") << "Types : " << bTerm.getType() << " " << n.getType() << std::endl;
           Assert( n.getType()==bTerm.getType() );
-          Node lem = Rewriter::rewrite( NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, n, bTerm ) ); 
-          lems.push_back( lem );
+          ret = bTerm; 
         }
       }
     }
-    if( n.getKind()!=FORALL ){
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        getEagerUnfoldLemmas( lems, n[i], visited );
+    if( ret.isNull() ){
+      if( n.getKind()!=FORALL ){
+        bool childChanged = false;
+        std::vector< Node > children;
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          Node nc = getEagerUnfold( n[i], visited );
+          childChanged = childChanged || n[i]!=nc;
+          children.push_back( nc );
+        }
+        if( childChanged ){
+          if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+            children.insert( children.begin(), n.getOperator() );
+          }
+          ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+        }
+      }
+      if( ret.isNull() ){
+        ret = n;
       }
     }
+    visited[n] = ret;
+    return ret;
+  }else{
+    return itv->second;
   }
 }
 
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 81f70d600..c8b41c035 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -126,6 +126,8 @@ private:
   CegConjecture * d_conj;
   /** last instantiation by single invocation module? */
   bool d_last_inst_si;
+  /** evaluation axioms */
+  std::map< Node, bool > d_eval_axioms;
 private: //for enforcing fairness
   /** measure functions */
   std::map< TypeNode, Node > d_uf_measure;
@@ -140,7 +142,7 @@ private: //for enforcing fairness
   /** get measure lemmas */
   void getMeasureLemmas( Node n, Node v, std::vector< Node >& lems );
   /** get eager unfolding */
-  void getEagerUnfoldLemmas( std::vector< Node >& lems, Node n, std::map< Node, bool >& visited );
+  Node getEagerUnfold( Node n, std::map< Node, Node >& visited );
 private:
   /** check conjecture */
   void checkCegConjecture( CegConjecture * conj );
@@ -158,6 +160,7 @@ public:
   /* Call during quantifier engine's check */
   void check( Theory::Effort e, unsigned quant_e );
   /* Called for new quantifiers */
+  void preRegisterQuantifier( Node q );
   void registerQuantifier( Node q );
   void assertNode( Node n );
   Node getNextDecisionRequest();
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 149330c61..d2637a555 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -692,8 +692,10 @@ CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
 
 void InstStrategyCegqi::registerQuantifier( Node q ) {
   if( options::cbqiPreRegInst() ){
-    //just get the instantiator
-    getInstantiator( q );
+    if( doCbqi( q ) ){
+      //just get the instantiator
+      getInstantiator( q );
+    }
   }
 }
 
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 9450c5daa..bac2aa35c 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -219,7 +219,6 @@ void QuantInfo::flatten( Node n, bool beneathQuant ) {
     if( n.getKind()==BOUND_VARIABLE ){
       d_inMatchConstraint[n] = true;
     }
-    //if( MatchGen::isHandledUfTerm( n ) || n.getKind()==ITE ){
     if( d_var_num.find( n )==d_var_num.end() ){
       Trace("qcf-qregister-debug2") << "Add FLATTEN VAR : " << n << std::endl;
       d_var_num[n] = d_vars.size();
@@ -987,26 +986,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar )
   if( isVar ){
     Assert( qi->d_var_num.find( n )!=qi->d_var_num.end() );
     if( n.getKind()==ITE ){
-  /*
-      d_type = typ_ite_var;
-      d_type_not = false;
-      d_n = n;
-      d_children.push_back( MatchGen( qi, d_n[0] ) );
-      if( d_children[0].isValid() ){
-        d_type = typ_ite_var;
-        for( unsigned i=1; i<=2; i++ ){
-          Node nn = n.eqNode( n[i] );
-          d_children.push_back( MatchGen( qi, nn ) );
-          d_children[d_children.size()-1].d_qni_bound_except.push_back( 0 );
-          if( !d_children[d_children.size()-1].isValid() ){
-            setInvalid();
-            break;
-          }
-        }
-      }else{
-*/
-        d_type = typ_invalid;
-     //}
+      d_type = typ_invalid;
     }else{
       d_type = isHandledUfTerm( n ) ? typ_var : typ_tsym;
       d_qni_var_num[0] = qi->getVarNum( n );
@@ -1049,26 +1029,6 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar )
               break;
             }
           }
-          /*
-          else if( isTop && n.getKind()==OR && d_children[d_children.size()-1].d_type==typ_var_eq ){
-            Trace("qcf-qregister-debug") << "Remove child, make built-in constraint" << std::endl;
-            //if variable equality/disequality at top level, remove immediately
-            bool cIsNot = d_children[d_children.size()-1].d_type_not;
-            Node cn = d_children[d_children.size()-1].d_n;
-            Assert( cn.getKind()==EQUAL );
-            Assert( p->d_qinfo[q].isVar( cn[0] ) || p->d_qinfo[q].isVar( cn[1] ) );
-            //make it a built-in constraint instead
-            for( unsigned i=0; i<2; i++ ){
-              if( p->d_qinfo[q].isVar( cn[i] ) ){
-                int v = p->d_qinfo[q].getVarNum( cn[i] );
-                Node cno = cn[i==0 ? 1 : 0];
-                p->d_qinfo[q].d_var_constraint[ cIsNot ? 0 : 1 ][v].push_back( cno );
-                break;
-              }
-            }
-            d_children.pop_back();
-          }
-          */
         }
       }else{
         d_type = typ_invalid;
@@ -1104,20 +1064,6 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar )
       d_type = typ_ground;
       qi->setGroundSubterm( d_n );
     }
-    //if( d_type!=typ_invalid ){
-      //determine an efficient children ordering
-      //if( !d_children.empty() ){
-        //for( unsigned i=0; i<d_children.size(); i++ ){
-        //  d_children_order.push_back( i );
-        //}
-        //if( !d_n.isNull() && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF ) ){
-          //sort based on the type of the constraint : ground comes first, then literals, then others
-          //MatchGenSort mgs;
-          //mgs.d_mg = this;
-          //std::sort( d_children_order.begin(), d_children_order.end(), mgs );
-        //}
-      //}
-    //}
   }
   Trace("qcf-qregister-debug")  << "Done make match gen " << n << ", type = ";
   debugPrintType( "qcf-qregister-debug", d_type, true );
@@ -1201,22 +1147,21 @@ void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars
       //add to children order
       d_children_order.push_back( min_score_index );
       assigned[min_score_index] = true;
-      //if( vb_count[min_score_index]==0 ){
-      //  d_independent.push_back( min_score_index );
-      //}
       //determine order internal to children
       d_children[min_score_index].determineVariableOrder( qi, bvars );
       Trace("qcf-qregister-debug")  << "...bind variables" << std::endl;
       //now, make it a bound variable
-      for( unsigned i=0; i<c_to_vars[min_score_index].size(); i++ ){
-        int v = c_to_vars[min_score_index][i];
-        if( std::find( bvars.begin(), bvars.end(), v )==bvars.end() ){
-          for( unsigned j=0; j<vars_to_c[v].size(); j++ ){
-            int vc = vars_to_c[v][j];
-            vu_count[vc]--;
-            vb_count[vc]++;
+      if( vu_count[min_score_index]>0 ){
+        for( unsigned i=0; i<c_to_vars[min_score_index].size(); i++ ){
+          int v = c_to_vars[min_score_index][i];
+          if( std::find( bvars.begin(), bvars.end(), v )==bvars.end() ){
+            for( unsigned j=0; j<vars_to_c[v].size(); j++ ){
+              int vc = vars_to_c[v][j];
+              vu_count[vc]--;
+              vb_count[vc]++;
+            }
+            bvars.push_back( v );
           }
-          bvars.push_back( v );
         }
       }
       Trace("qcf-qregister-debug") << "...done assign child " << min_score_index << std::endl;
@@ -1908,7 +1853,7 @@ void MatchGen::setInvalid() {
 }
 
 bool MatchGen::isHandledBoolConnective( TNode n ) {
-  return n.getType().isBoolean() && TermDb::isBoolConnective( n.getKind() );
+  return TermDb::isBoolConnective( n.getKind() ) && ( n.getKind()!=ITE || n.getType().isBoolean() );
 }
 
 bool MatchGen::isHandledUfTerm( TNode n ) {
@@ -1964,28 +1909,31 @@ void QuantConflictFind::registerQuantifier( Node q ) {
   if( d_quantEngine->hasOwnership( q, this ) ){
     d_quants.push_back( q );
     d_quant_id[q] = d_quants.size();
-    Trace("qcf-qregister") << "Register ";
-    debugPrintQuant( "qcf-qregister", q );
-    Trace("qcf-qregister") << " : " << q << std::endl;
+    if( Trace.isOn("qcf-qregister") ){
+      Trace("qcf-qregister") << "Register ";
+      debugPrintQuant( "qcf-qregister", q );
+      Trace("qcf-qregister") << " : " << q << std::endl;
+    }
     //make QcfNode structure
     Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;
     d_qinfo[q].initialize( this, q, q[1] );
 
     //debug print
-    Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;
-    Trace("qcf-qregister") << "    ";
-    debugPrintQuantBody( "qcf-qregister", q, q[1] );
-    Trace("qcf-qregister") << std::endl;
-    if( d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){
-      Trace("qcf-qregister") << "  with additional constraints : " << std::endl;
-      for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){
-        Trace("qcf-qregister") << "    ?x" << j << " = ";
-        debugPrintQuantBody( "qcf-qregister", q, d_qinfo[q].d_vars[j], false );
-        Trace("qcf-qregister") << std::endl;
-      }
-    }
-    
-    Trace("qcf-qregister") << "Done registering quantifier." << std::endl;
+    if( Trace.isOn("qcf-qregister") ){
+      Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;
+      Trace("qcf-qregister") << "    ";
+      debugPrintQuantBody( "qcf-qregister", q, q[1] );
+      Trace("qcf-qregister") << std::endl;
+      if( d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){
+        Trace("qcf-qregister") << "  with additional constraints : " << std::endl;
+        for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){
+          Trace("qcf-qregister") << "    ?x" << j << " = ";
+          debugPrintQuantBody( "qcf-qregister", q, d_qinfo[q].d_vars[j], false );
+          Trace("qcf-qregister") << std::endl;
+        }
+      }
+      Trace("qcf-qregister") << "Done registering quantifier." << std::endl;
+    }
   }
 }
 
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 7b4719878..eff641736 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -90,7 +90,7 @@ TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine*
   d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
   d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
   if( options::ceGuidedInst() ){
-    d_sygus_tdb = new TermDbSygus;
+    d_sygus_tdb = new TermDbSygus( c, qe );
   }else{
     d_sygus_tdb = NULL;
   }
@@ -170,6 +170,10 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi
           Node op = getMatchOperator( n );
           d_op_map[op].push_back( n );
           added.insert( n );
+          
+          if( d_sygus_tdb ){
+            d_sygus_tdb->registerEvalTerm( n );
+          }
 
           if( options::eagerInstQuant() ){
             for( unsigned i=0; i<n.getNumChildren(); i++ ){
@@ -537,7 +541,7 @@ bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
         return qy->getEngine()->getRepresentative( n1 ) == ( pol ? d_true : d_false );
       }
     }
-  }else if( n.getKind()==FORALL ){
+  }else if( n.getKind()==FORALL && !pol ){
     return isEntailed2( n[1], subs, subsRep, hasSubs, pol, qy );
   }
   return false;
@@ -1576,7 +1580,7 @@ struct sortTermOrder {
 //this function makes a canonical representation of a term (
 //  - orders variables left to right
 //  - if apply_torder, then sort direct subterms of commutative operators
-Node TermDb::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder ) {
+Node TermDb::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder, std::map< TNode, Node >& visited ) {
   Trace("canon-term-debug") << "Get canonical term for " << n << std::endl;
   if( n.getKind()==BOUND_VARIABLE ){
     std::map< TNode, TNode >::iterator it = subs.find( n );
@@ -1593,32 +1597,38 @@ Node TermDb::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_coun
       return it->second;
     }
   }else if( n.getNumChildren()>0 ){
-    //collect children
-    Trace("canon-term-debug") << "Collect children" << std::endl;
-    std::vector< Node > cchildren;
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      cchildren.push_back( n[i] );
-    }
-    //if applicable, first sort by term order
-    if( apply_torder && isComm( n.getKind() ) ){
-      Trace("canon-term-debug") << "Sort based on commutative operator " << n.getKind() << std::endl;
-      sortTermOrder sto;
-      sto.d_tdb = this;
-      std::sort( cchildren.begin(), cchildren.end(), sto );
-    }
-    //now make canonical
-    Trace("canon-term-debug") << "Make canonical children" << std::endl;
-    for( unsigned i=0; i<cchildren.size(); i++ ){
-      cchildren[i] = getCanonicalTerm( cchildren[i], var_count, subs, apply_torder );
-    }
-    if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-      Trace("canon-term-debug") << "Insert operator " << n.getOperator() << std::endl;
-      cchildren.insert( cchildren.begin(), n.getOperator() );
-    }
-    Trace("canon-term-debug") << "...constructing for " << n << "." << std::endl;
-    Node ret = NodeManager::currentNM()->mkNode( n.getKind(), cchildren );
-    Trace("canon-term-debug") << "...constructed " << ret << " for " << n << "." << std::endl;
-    return ret;
+    std::map< TNode, Node >::iterator it = visited.find( n );
+    if( it!=visited.end() ){
+      return it->second;
+    }else{
+      //collect children
+      Trace("canon-term-debug") << "Collect children" << std::endl;
+      std::vector< Node > cchildren;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        cchildren.push_back( n[i] );
+      }
+      //if applicable, first sort by term order
+      if( apply_torder && isComm( n.getKind() ) ){
+        Trace("canon-term-debug") << "Sort based on commutative operator " << n.getKind() << std::endl;
+        sortTermOrder sto;
+        sto.d_tdb = this;
+        std::sort( cchildren.begin(), cchildren.end(), sto );
+      }
+      //now make canonical
+      Trace("canon-term-debug") << "Make canonical children" << std::endl;
+      for( unsigned i=0; i<cchildren.size(); i++ ){
+        cchildren[i] = getCanonicalTerm( cchildren[i], var_count, subs, apply_torder, visited );
+      }
+      if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+        Trace("canon-term-debug") << "Insert operator " << n.getOperator() << std::endl;
+        cchildren.insert( cchildren.begin(), n.getOperator() );
+      }
+      Trace("canon-term-debug") << "...constructing for " << n << "." << std::endl;
+      Node ret = NodeManager::currentNM()->mkNode( n.getKind(), cchildren );
+      Trace("canon-term-debug") << "...constructed " << ret << " for " << n << "." << std::endl;
+      visited[n] = ret;
+      return ret;
+    }
   }else{
     Trace("canon-term-debug") << "...return 0-child term." << std::endl;
     return n;
@@ -1628,7 +1638,8 @@ Node TermDb::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_coun
 Node TermDb::getCanonicalTerm( TNode n, bool apply_torder ){
   std::map< TypeNode, unsigned > var_count;
   std::map< TNode, TNode > subs;
-  return getCanonicalTerm( n, var_count, subs, apply_torder );
+  std::map< TNode, Node > visited;
+  return getCanonicalTerm( n, var_count, subs, apply_torder, visited );
 }
 
 void TermDb::getVtsTerms( std::vector< Node >& t, bool isFree, bool create, bool inc_delta ) {
@@ -2249,11 +2260,15 @@ bool TermDb::isQAttrQuantElimPartial( Node q ) {
   }
 }
 
-TermDbSygus::TermDbSygus(){
+TermDbSygus::TermDbSygus( context::Context* c, QuantifiersEngine* qe ) : d_quantEngine( qe ){
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
 }
 
+bool TermDbSygus::reset( Theory::Effort e ) { 
+  return true;  
+}
+
 TNode TermDbSygus::getVar( TypeNode tn, int i ) {
   while( i>=(int)d_fv[tn].size() ){
     std::stringstream ss;
@@ -3184,3 +3199,69 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
     out << n;
   }
 }
+
+void TermDbSygus::registerEvalTerm( Node n ) {
+  if( options::sygusDirectEval() ){
+    if( n.getKind()==APPLY_UF ){
+      Trace("sygus-eager") << "TermDbSygus::eager: Register eval term : " << n << std::endl;
+      TypeNode tn = n[0].getType();
+      if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){
+        const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+        if( dt.isSygus() ){
+          Node f = n.getOperator();
+          Trace("sygus-eager") << "...the evaluation function is : " << f << std::endl;
+          Assert( n[0].getKind()!=APPLY_CONSTRUCTOR );
+          d_evals[n[0]].push_back( n );
+          TypeNode tn = n[0].getType();
+          Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
+          const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+          Node var_list = Node::fromExpr( dt.getSygusVarList() );
+          Assert( dt.isSygus() );
+          d_eval_args[n[0]].push_back( std::vector< Node >() );
+          for( unsigned j=1; j<n.getNumChildren(); j++ ){
+            if( var_list[j-1].getType().isBoolean() ){
+              //TODO: remove this case when boolean term conversion is eliminated
+              Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
+              d_eval_args[n[0]].back().push_back( n[j].eqNode( c ) );
+            }else{
+              d_eval_args[n[0]].back().push_back( n[j] );
+            }
+          }
+
+        }
+      }    
+    }
+  }
+}
+
+void TermDbSygus::registerModelValue( Node n, Node v, std::vector< Node >& lems ) {
+  std::map< Node, std::vector< std::vector< Node > > >::iterator it = d_eval_args.find( n );
+  if( it!=d_eval_args.end() && !it->second.empty() ){
+    unsigned start = d_node_mv_args_proc[n][v];
+    Node antec = n.eqNode( v ).negate();
+    TypeNode tn = n.getType();
+    Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
+    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+    Assert( dt.isSygus() );
+    Trace("sygus-eager") << "TermDbSygus::eager: Register model value : " << v << " for " << n << std::endl;
+    Trace("sygus-eager") << "...it has " << it->second.size() << " evaluations, already processed " << start << "." << std::endl;
+    Node bTerm = d_quantEngine->getTermDatabaseSygus()->sygusToBuiltin( v, tn );
+    Trace("sygus-eager") << "Built-in term : " << bTerm << std::endl;
+    std::vector< Node > vars;
+    Node var_list = Node::fromExpr( dt.getSygusVarList() );
+    for( unsigned j=0; j<var_list.getNumChildren(); j++ ){
+      vars.push_back( var_list[j] );
+    }
+    //for each evaluation
+    for( unsigned i=start; i<it->second.size(); i++ ){
+      Assert( vars.size()==it->second[i].size() );
+      Node sBTerm = bTerm.substitute( vars.begin(), vars.end(), it->second[i].begin(), it->second[i].end() );
+      Node lem = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, d_evals[n][i], sBTerm ); 
+      lem = NodeManager::currentNM()->mkNode( OR, antec, lem );
+      Trace("sygus-eager") << "Lemma : " << lem << std::endl;
+      lems.push_back( lem );
+    }
+    d_node_mv_args_proc[n][v] = it->second.size();
+  }
+}
+
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 684b6cf83..4291587a4 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -419,7 +419,8 @@ private:
   //free variables
   std::map< TypeNode, std::vector< Node > > d_cn_free_var;
   // get canonical term, return null if it contains a term apart from handled signature
-  Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder );
+  Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder, 
+                         std::map< TNode, Node >& visited );
 public:
   /** get id for operator */
   int getIdForOperator( Node op );
@@ -541,6 +542,8 @@ public:
 
 class TermDbSygus {
 private:
+  /** reference to the quantifiers engine */
+  QuantifiersEngine* d_quantEngine;
   std::map< TypeNode, std::vector< Node > > d_fv;
   std::map< Node, TypeNode > d_fv_stype;
   std::map< Node, int > d_fv_num;
@@ -581,7 +584,11 @@ private:
   std::map< TypeNode, std::map< Node, Node > > d_sygus_to_builtin;
   std::map< TypeNode, std::map< Node, Node > > d_builtin_const_to_sygus;
 public:
-  TermDbSygus();
+  TermDbSygus( context::Context* c, QuantifiersEngine* qe );
+  ~TermDbSygus(){}
+  bool reset( Theory::Effort e );
+  std::string identify() const { return "TermDbSygus"; }
+  
   bool isRegistered( TypeNode tn );
   TypeNode sygusToBuiltinType( TypeNode tn );
   int getKindArg( TypeNode tn, Kind k );
@@ -633,6 +640,15 @@ public:
   static Kind getOperatorKind( Node op );
   /** print sygus term */
   static void printSygusTerm( std::ostream& out, Node n, std::vector< Node >& lvs );
+  
+//for eager instantiation
+private:
+  std::map< Node, std::vector< Node > > d_evals;
+  std::map< Node, std::vector< std::vector< Node > > > d_eval_args;
+  std::map< Node, std::map< Node, unsigned > > d_node_mv_args_proc;
+public:
+  void registerEvalTerm( Node n );
+  void registerModelValue( Node n, Node v, std::vector< Node >& lems );
 };
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index efe40aaa8..7ad13b3a8 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -72,8 +72,11 @@ void TheoryQuantifiers::notifyEq(TNode lhs, TNode rhs) {
 
 void TheoryQuantifiers::preRegisterTerm(TNode n) {
   Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl;
-  if( n.getKind()==FORALL && !TermDb::hasInstConstAttr(n) ){
-    getQuantifiersEngine()->registerQuantifier( n );
+  if( n.getKind()==FORALL ){
+    if( !options::cbqi() || options::recurseCbqi() || !TermDb::hasInstConstAttr(n) ){
+      getQuantifiersEngine()->registerQuantifier( n );
+      Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() done " << n << endl;
+    }
   }
 }
 
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 7522c633b..1f4a04218 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -295,9 +295,9 @@ private:
   bool removeInstantiationInternal( Node q, std::vector< Node >& terms );
   /** set instantiation level attr */
   static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level );
+public:
   /** flush lemmas */
   void flushLemmas();
-public:
   /** get instantiation */
   Node getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false );
   /** get instantiation */