Add option --sygus-inv-templ for synthesizing strengthening/weakening of pre/post conditions. Dump synth by default in sygus, update regressions. Set better defaults for induction. Fix bug in related to IFF and EQUAL in sygus grammar.

8 files changed, 357 insertions, 81 deletions

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 045407bf0..e10ba0fef 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -37,14 +37,25 @@ CegConjecture::CegConjecture( context::Context* c ) : d_active( c, false ), d_in
 void CegConjecture::assign( QuantifiersEngine * qe, Node q ) {
   Assert( d_quant.isNull() );
   Assert( q.getKind()==FORALL );
+  d_assert_quant = q;
+  //register with single invocation if applicable
+  if( qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) && options::cegqiSingleInv() ){
+    d_ceg_si->initialize( qe, q );
+    if( q!=d_ceg_si->d_quant ){
+      //Node red_lem = NodeManager::currentNM()->mkNode( OR, q.negate(), d_cegqi_si->d_quant );
+      //may have rewritten quantified formula (for invariant synthesis)
+      q = d_ceg_si->d_quant;
+    }
+  }
   d_quant = q;
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
     d_candidates.push_back( NodeManager::currentNM()->mkSkolem( "e", q[0][i].getType() ) );
   }
+  Trace("cegqi") << "Base quantified fm is : " << q << std::endl;
   //construct base instantiation
   d_base_inst = Rewriter::rewrite( qe->getInstantiation( q, d_candidates ) );
   Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl;
-  if( qe->getTermDatabase()->isQAttrSygus( q ) ){
+  if( qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) ){
     CegInstantiation::collectDisjuncts( d_base_inst, d_base_disj );
     Trace("cegqi") << "Conjecture has " << d_base_disj.size() << " disjuncts." << std::endl;
     //store the inner variables for each disjunct
@@ -59,10 +70,7 @@ void CegConjecture::assign( QuantifiersEngine * qe, Node q ) {
       }
     }
     d_syntax_guided = true;
-    if( options::cegqiSingleInv() ){
-      d_ceg_si->initialize( qe, q );
-    }
-  }else if( qe->getTermDatabase()->isQAttrSynthesis( q ) ){
+  }else if( qe->getTermDatabase()->isQAttrSynthesis( d_assert_quant ) ){
     d_syntax_guided = false;
   }else{
     Assert( false );
@@ -211,7 +219,7 @@ void CegInstantiation::assertNode( Node n ) {
     //d_guard_assertions[lit] = pol;
     d_conj->d_infeasible = !pol;
   }
-  if( lit==d_conj->d_quant ){
+  if( lit==d_conj->d_assert_quant ){
     d_conj->d_active = true;
   }
 }
@@ -229,7 +237,7 @@ Node CegInstantiation::getNextDecisionRequest() {
       Trace("cegqi-debug") << "CEGQI : Decide next on : " << d_conj->d_guard << "..." << std::endl;
       return d_conj->d_guard;
     }
-    
+
     if( d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){
       Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
       if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) {
@@ -251,6 +259,7 @@ Node CegInstantiation::getNextDecisionRequest() {
 
 void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
   Node q = conj->d_quant;
+  Node aq = conj->d_assert_quant;
   Trace("cegqi-engine-debug") << "Synthesis conjecture : " << q << std::endl;
   Trace("cegqi-engine-debug") << "  * Candidate program/output symbol : ";
   for( unsigned i=0; i<conj->d_candidates.size(); i++ ){
@@ -263,7 +272,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
 
   if( conj->d_ce_sk.empty() ){
     Trace("cegqi-engine") << "  *** Check candidate phase..." << std::endl;
-    if( getTermDatabase()->isQAttrSygus( q ) ){
+    if( conj->d_syntax_guided ){
       if( conj->d_ceg_si ){
         std::vector< Node > lems;
         conj->d_ceg_si->check( lems );
@@ -303,7 +312,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
           conj->d_ce_sk.push_back( std::vector< Node >() );
         }
         std::vector< Node > ic;
-        ic.push_back( q.negate() );
+        ic.push_back( aq.negate() );
         std::vector< Node > d;
         collectDisjuncts( inst, d );
         Assert( d.size()==conj->d_base_disj.size() );
@@ -334,7 +343,8 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
         Trace("cegqi-engine") << "  ...find counterexample." << std::endl;
       }
 
-    }else if( getTermDatabase()->isQAttrSynthesis( q ) ){
+    }else{
+      Assert( aq==q );
       std::vector< Node > model_terms;
       if( getModelValues( conj, conj->d_candidates, model_terms ) ){
         d_quantEngine->addInstantiation( q, model_terms, false );
@@ -497,11 +507,12 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
     //  out << "Solution:" << std::endl;
     //}
     for( unsigned i=0; i<d_conj->d_candidates.size(); i++ ){
+      Node prog = d_conj->d_quant[0][i];
       std::stringstream ss;
-      ss << d_conj->d_quant[0][i];
+      ss << prog;
       std::string f(ss.str());
       f.erase(f.begin());
-      TypeNode tn = d_conj->d_quant[0][i].getType();
+      TypeNode tn = prog.getType();
       Assert( datatypes::DatatypesRewriter::isTypeDatatype( tn ) );
       const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
       Assert( dt.isSygus() );
@@ -514,7 +525,34 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
       }else{
         if( !d_conj->d_candidate_inst[i].empty() ){
           sol = d_conj->d_candidate_inst[i].back();
-          status = 1;
+          //check if this was based on a template, if so, we must do reconstruction
+          if( d_conj->d_assert_quant!=d_conj->d_quant ){
+            Trace("cegqi-inv") << "Sygus version of solution is : " << sol << ", type : " << sol.getType() << std::endl;
+            sol = getTermDatabase()->getTermDatabaseSygus()->sygusToBuiltin( sol, sol.getType() );
+            Trace("cegqi-inv") << "Builtin version of solution is : " << sol << ", type : " << sol.getType() << std::endl;
+            std::vector< Node > subs;
+            Expr svl = dt.getSygusVarList();
+            for( unsigned j=0; j<svl.getNumChildren(); j++ ){
+              subs.push_back( Node::fromExpr( svl[j] ) );
+            }
+            if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){
+              Node pre = d_conj->d_ceg_si->d_trans_pre[prog];
+              pre = pre.substitute( d_conj->d_ceg_si->d_prog_templ_vars[prog].begin(), d_conj->d_ceg_si->d_prog_templ_vars[prog].end(),
+                                    subs.begin(), subs.end() );
+              sol = NodeManager::currentNM()->mkNode( OR, sol, pre );
+            }else if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST ){
+              Node post = d_conj->d_ceg_si->d_trans_post[prog];
+              post = post.substitute( d_conj->d_ceg_si->d_prog_templ_vars[prog].begin(), d_conj->d_ceg_si->d_prog_templ_vars[prog].end(),
+                                      subs.begin(), subs.end() );
+              sol = NodeManager::currentNM()->mkNode( AND, sol, post );
+            }
+            Trace("cegqi-inv-debug") << "With template : " << sol << std::endl;
+            sol = Rewriter::rewrite( sol );
+            Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl;
+            sol = d_conj->d_ceg_si->reconstructToSyntax( sol, tn, status );
+          }else{
+            status = 1;
+          }
         }
       }
       if( !(Trace.isOn("cegqi-stats")) ){
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 5f393626c..af3a19d62 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -35,7 +35,9 @@ public:
   context::CDO< bool > d_active;
   /** is conjecture infeasible */
   context::CDO< bool > d_infeasible;
-  /** quantified formula */
+  /** quantified formula asserted */
+  Node d_assert_quant;
+  /** quantified formula (after processing) */
   Node d_quant;
   /** guard */
   Node d_guard;
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index b7bbf8a93..ef2e3005e 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -810,6 +810,7 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
   }
   //collect information about conjunctions
   bool singleInvocation = false;
+  bool invExtractPrePost = false;
   if( analyzeSygusConjunct( Node::null(), q[1], children, prog_invoke, progs, contains, true ) ){
     singleInvocation = true;
     //try to phrase as single invocation property
@@ -826,7 +827,6 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
           for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){
             if( it2->second.size()>1 ){
               singleInvocation = false;
-              break;
             }else if( it2->second.size()==1 ){
               Node prog = it2->first;
               Node inv = it2->second[0];
@@ -840,15 +840,26 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
                   single_invoke_args[prog][k-1].push_back( arg );
                 }
               }
+              if( inv.getType().isBoolean() ){
+                //conjunct defines pre and/or post conditions
+                if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){
+                  invExtractPrePost = true;
+                }
+              }
             }
           }
         }
       }
     }
-    if( singleInvocation ){
+    if( singleInvocation || invExtractPrePost ){
+      //no value in extracting pre/post if we are single invocation
+      if( singleInvocation ){
+        invExtractPrePost = false;
+      }
       Trace("cegqi-si") << "Property is single invocation with : " << std::endl;
       std::vector< Node > pbvs;
       std::vector< Node > new_vars;
+      std::map< Node, std::vector< Node > > prog_vars;
       std::map< Node, std::vector< Node > > new_assumptions;
       for( std::map< Node, std::vector< Node > >::iterator it = invocations.begin(); it != invocations.end(); ++it ){
         Assert( !it->second.empty() );
@@ -868,12 +879,14 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
           Assert( !single_invoke_args[prog][k-1].empty() );
           if( single_invoke_args[prog][k-1].size()==1 && single_invoke_args[prog][k-1][0].getKind()==BOUND_VARIABLE ){
             invc.push_back( single_invoke_args[prog][k-1][0] );
+            prog_vars[prog].push_back( single_invoke_args[prog][k-1][0] );
           }else{
             //introduce fresh variable, assign all
             Node v = NodeManager::currentNM()->mkSkolem( "a", single_invoke_args[prog][k-1][0].getType(), "single invocation arg" );
             new_vars.push_back( v );
             invc.push_back( v );
             d_single_inv_arg_sk.push_back( v );
+            prog_vars[prog].push_back( v );
 
             for( unsigned i=0; i<single_invoke_args[prog][k-1].size(); i++ ){
               Node arg = single_invoke_args[prog][k-1][i];
@@ -897,7 +910,6 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
       }
       //construct the single invocation version of the property
       Trace("cegqi-si") << "Single invocation formula conjuncts are : " << std::endl;
-      //std::vector< Node > si_conj;
       Node pbvl;
       if( !pbvs.empty() ){
         pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs );
@@ -906,6 +918,8 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
         //should hold since we prevent miniscoping
         Assert( d_single_inv.isNull() );
         std::vector< Node > conjuncts;
+        std::vector< Node > conjuncts_si_progs;
+        std::vector< Node > conjuncts_si_invokes;
         for( unsigned i=0; i<it->second.size(); i++ ){
           Node c = it->second[i];
           std::vector< Node > disj;
@@ -917,17 +931,32 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
           if( itp!=prog_invoke.end() ){
             std::vector< Node > terms;
             std::vector< Node > subs;
+            std::vector< Node > progs;
             for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){
-              if( !it2->second.empty() ){
+              if( it2->second.size()==1 ){
                 Node prog = it2->first;
                 Node inv = it2->second[0];
                 Assert( it2->second.size()==1 );
                 terms.push_back( inv );
                 subs.push_back( d_single_inv_map[prog] );
+                progs.push_back( prog );
                 Trace("cegqi-si-debug2") << "subs : " << inv << " -> var for " << prog << " : " << d_single_inv_map[prog] << std::endl;
               }
             }
-            cr = c.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
+            if( singleInvocation ){
+              cr = c.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
+            }else{
+              cr = c;
+              if( invExtractPrePost ){
+                if( terms.size()==1 ){
+                  conjuncts_si_progs.push_back( progs[0] );
+                  conjuncts_si_invokes.push_back( terms[0] );
+                }else if( terms.size()>1 ){
+                  //abort when mixing multiple invariants?  TODO
+                  invExtractPrePost = false;
+                }
+              }
+            }
           }else{
             cr = c;
           }
@@ -941,6 +970,10 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
           Node curr = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj );
           curr = TermDb::simpleNegate( curr );
           Trace("cegqi-si") << "    " << curr;
+          if( invExtractPrePost && conjuncts.size()==conjuncts_si_progs.size() ){
+            conjuncts_si_progs.push_back( Node::null() );
+            conjuncts_si_invokes.push_back( Node::null() );
+          }
           conjuncts.push_back( curr );
           if( !it->first.isNull() ){
             Trace("cegqi-si-debug") << " under " << it->first;
@@ -948,75 +981,163 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
           Trace("cegqi-si") << std::endl;
         }
         Assert( !conjuncts.empty() );
-        //make the skolems for the existential
-        if( !it->first.isNull() ){
-          std::vector< Node > vars;
-          std::vector< Node > sks;
-          for( unsigned j=0; j<it->first.getNumChildren(); j++ ){
-            std::stringstream ss;
-            ss << "a_" << it->first[j];
-            Node v = NodeManager::currentNM()->mkSkolem( ss.str(), it->first[j].getType(), "single invocation skolem" );
-            vars.push_back( it->first[j] );
-            sks.push_back( v );
+        //CASE 1 : rewrite based on a template for invariants
+        if( invExtractPrePost ){
+          //for invariant synthesis
+          std::map< Node, bool > has_inv;
+          std::map< Node, std::vector< Node > > inv_pre_post[2];
+          for( unsigned c=0; c<conjuncts.size(); c++ ){
+            Node inv = conjuncts_si_invokes[c];
+            Node prog = conjuncts_si_progs[c];
+            Trace("cegqi-si-inv-debug") << "Conjunct #" << c << ": " << conjuncts[c] << std::endl;
+            if( !prog.isNull() ){
+              Trace("cegqi-si-inv-debug") << "...has program " << prog << " invoked once: " << inv << std::endl;
+              std::vector< Node > curr_disj;
+              //find the polarity of the invocation : this determines pre vs. post
+              int pol = extractInvariantPolarity( conjuncts[c], inv, curr_disj, true );
+              Trace("cegqi-si-inv-debug") << "...polarity is " << pol << std::endl;
+              if( ( pol==1 && !curr_disj.empty() ) || pol==0 ){
+                //conjunct is part of pre/post condition : will add to template of invariant
+                Node nc = curr_disj.empty() ? NodeManager::currentNM()->mkConst( true ) :
+                           ( curr_disj.size()==1 ? curr_disj[0] : NodeManager::currentNM()->mkNode( AND, curr_disj ) );
+                nc = pol==0 ? nc : TermDb::simpleNegate( nc );
+                Trace("cegqi-si-inv-debug") << "  -> " << nc << " is " << ( pol==0 ? "pre" : "post" ) << "condition of invariant " << prog << "." << std::endl;
+                inv_pre_post[pol][prog].push_back( nc );
+                has_inv[prog] = true;
+              }
+            }
           }
-          //substitute conjunctions
-          for( unsigned i=0; i<conjuncts.size(); i++ ){
-            conjuncts[i] = conjuncts[i].substitute( vars.begin(), vars.end(), sks.begin(), sks.end() );
+          Trace("cegqi-si-inv") << "Constructing invariant templates..." << std::endl;
+          //now, contruct the template for the invariant(s)
+          std::map< Node, Node > prog_templ;
+          for( std::map< Node, bool >::iterator iti = has_inv.begin(); iti != has_inv.end(); ++iti ){
+            Node prog = iti->first;
+            Trace("cegqi-si-inv") << "...for " << prog << "..." << std::endl;
+            Trace("cegqi-si-inv") << "   args : ";
+            for( unsigned j=0; j<prog_vars[prog].size(); j++ ){
+              Node v = NodeManager::currentNM()->mkBoundVar( prog_vars[prog][j].getType() );
+              d_prog_templ_vars[prog].push_back( v );
+              Trace("cegqi-si-inv") << v << " ";
+            }
+            Trace("cegqi-si-inv") << std::endl;
+            Node pre = inv_pre_post[0][prog].empty() ? NodeManager::currentNM()->mkConst( false ) :
+                       ( inv_pre_post[0][prog].size()==1 ? inv_pre_post[0][prog][0] : NodeManager::currentNM()->mkNode( OR, inv_pre_post[0][prog] ) );
+            d_trans_pre[prog] = pre.substitute( prog_vars[prog].begin(), prog_vars[prog].end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() );
+            Node post = inv_pre_post[1][prog].empty() ? NodeManager::currentNM()->mkConst( true ) :
+                        ( inv_pre_post[1][prog].size()==1 ? inv_pre_post[1][prog][0] : NodeManager::currentNM()->mkNode( AND, inv_pre_post[1][prog] ) );
+            d_trans_post[prog] = post.substitute( prog_vars[prog].begin(), prog_vars[prog].end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() );
+            Trace("cegqi-si-inv") << "   precondition : " << d_trans_pre[prog] << std::endl;
+            Trace("cegqi-si-inv") << "  postcondition : " << d_trans_post[prog] << std::endl;
+            Node invariant = d_single_inv_app_map[prog];
+            invariant = invariant.substitute( prog_vars[prog].begin(), prog_vars[prog].end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() );
+            Trace("cegqi-si-inv") << "      invariant : " << invariant << std::endl;
+            //construct template
+            Node templ;
+            if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){
+              //templ = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], invariant ), d_trans_post[prog] );
+              templ = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], invariant );
+            }else{
+              Assert( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST );
+              //templ = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], invariant ) );
+              templ = NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], invariant );
+            }
+            Trace("cegqi-si-inv") << "       template : " << templ << std::endl;
+            prog_templ[prog] = templ;
           }
-          d_single_inv_arg_sk.insert( d_single_inv_arg_sk.end(), sks.begin(), sks.end() );
-          //substitute single invocation applications
-          for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){
-            Node n = itam->second;
-            d_single_inv_app_map[itam->first] = n.substitute( vars.begin(), vars.end(), sks.begin(), sks.end() );
+          Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts );
+          Trace("cegqi-si-inv") << "           body : " << bd << std::endl;
+          bd = substituteInvariantTemplates( bd, prog_templ, d_prog_templ_vars );
+          Trace("cegqi-si-inv-debug") << "     templ-subs body : " << bd << std::endl;
+          //make inner existential
+          std::vector< Node > new_var_bv;
+          for( unsigned j=0; j<new_vars.size(); j++ ){
+            new_var_bv.push_back( NodeManager::currentNM()->mkBoundVar( new_vars[j].getType() ) );
           }
-        }
-        //ensure that this is a ground property
-        for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){
-          Node n = itam->second;
-          //check if all variables are arguments of this
-          std::vector< Node > n_args;
-          for( unsigned i=1; i<n.getNumChildren(); i++ ){
-            n_args.push_back( n[i] );
+          bd = bd.substitute( new_vars.begin(), new_vars.end(), new_var_bv.begin(), new_var_bv.end() );
+          for( unsigned j=0; j<q[1][0][0].getNumChildren(); j++ ){
+            new_var_bv.push_back( q[1][0][0][j] );
           }
-          for( int i=0; i<(int)d_single_inv_arg_sk.size(); i++ ){
-            if( std::find( n_args.begin(), n_args.end(), d_single_inv_arg_sk[i] )==n_args.end() ){
-              Trace("cegqi-si") << "...property is not ground: program invocation " << n << " does not contain variable " << d_single_inv_arg_sk[i] << "." << std::endl;
-              //try to do variable elimination on d_single_inv_arg_sk[i]
-              if( doVariableElimination( d_single_inv_arg_sk[i], conjuncts ) ){
-                Trace("cegqi-si") << "...did variable elimination on " << d_single_inv_arg_sk[i] << std::endl;
-                d_single_inv_arg_sk.erase( d_single_inv_arg_sk.begin() + i, d_single_inv_arg_sk.begin() + i + 1 );
-                i--;
-              }else{
-                singleInvocation = false;
-                //exit( 57 );
+          if( !new_var_bv.empty() ){
+            Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, new_var_bv );
+            bd = NodeManager::currentNM()->mkNode( FORALL, bvl, TermDb::simpleNegate( bd ) ).negate();
+          }
+          //make outer universal
+          bd = NodeManager::currentNM()->mkNode( FORALL, q[0], bd );
+          bd = Rewriter::rewrite( bd );
+          Trace("cegqi-si-inv") << "  rtempl-subs body : " << bd << std::endl;
+          d_quant = bd;
+        //CASE 2 : rewrite based on single invocation
+        }else{
+          //make the skolems for the existential
+          if( !it->first.isNull() ){
+            std::vector< Node > vars;
+            std::vector< Node > sks;
+            for( unsigned j=0; j<it->first.getNumChildren(); j++ ){
+              std::stringstream ss;
+              ss << "a_" << it->first[j];
+              Node v = NodeManager::currentNM()->mkSkolem( ss.str(), it->first[j].getType(), "single invocation skolem" );
+              vars.push_back( it->first[j] );
+              sks.push_back( v );
+            }
+            //substitute conjunctions
+            for( unsigned i=0; i<conjuncts.size(); i++ ){
+              conjuncts[i] = conjuncts[i].substitute( vars.begin(), vars.end(), sks.begin(), sks.end() );
+            }
+            d_single_inv_arg_sk.insert( d_single_inv_arg_sk.end(), sks.begin(), sks.end() );
+            //substitute single invocation applications
+            for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){
+              Node n = itam->second;
+              d_single_inv_app_map[itam->first] = n.substitute( vars.begin(), vars.end(), sks.begin(), sks.end() );
+            }
+          }
+          //ensure that this is a ground property
+          for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){
+            Node n = itam->second;
+            //check if all variables are arguments of this
+            std::vector< Node > n_args;
+            for( unsigned i=1; i<n.getNumChildren(); i++ ){
+              n_args.push_back( n[i] );
+            }
+            for( int i=0; i<(int)d_single_inv_arg_sk.size(); i++ ){
+              if( std::find( n_args.begin(), n_args.end(), d_single_inv_arg_sk[i] )==n_args.end() ){
+                Trace("cegqi-si") << "...property is not ground: program invocation " << n << " does not contain variable " << d_single_inv_arg_sk[i] << "." << std::endl;
+                //try to do variable elimination on d_single_inv_arg_sk[i]
+                if( doVariableElimination( d_single_inv_arg_sk[i], conjuncts ) ){
+                  Trace("cegqi-si") << "...did variable elimination on " << d_single_inv_arg_sk[i] << std::endl;
+                  d_single_inv_arg_sk.erase( d_single_inv_arg_sk.begin() + i, d_single_inv_arg_sk.begin() + i + 1 );
+                  i--;
+                }else{
+                  singleInvocation = false;
+                  //exit( 57 );
+                }
+                break;
               }
-              break;
             }
           }
-        }
 
-        if( singleInvocation ){
-          Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts );
-          if( pbvl.isNull() ){
-            d_single_inv = bd;
-          }else{
-            d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd );
-          }
-          Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl;
-          /*
-          if( options::eMatching() && options::eMatching.wasSetByUser() ){
-            Node bd = d_qe->getTermDatabase()->getInstConstantBody( d_single_inv );
-            std::vector< Node > patTerms;
-            std::vector< Node > exclude;
-            inst::Trigger::collectPatTerms( d_qe, d_single_inv, bd, patTerms, inst::Trigger::TS_ALL, exclude );
-            if( !patTerms.empty() ){
-              Trace("cegqi-si-em") << "Triggers : " << std::endl;
-              for( unsigned i=0; i<patTerms.size(); i++ ){
-                Trace("cegqi-si-em") << "   " << patTerms[i] << std::endl;
+          if( singleInvocation ){
+            Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts );
+            if( pbvl.isNull() ){
+              d_single_inv = bd;
+            }else{
+              d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd );
+            }
+            Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl;
+            /*
+            if( options::eMatching() && options::eMatching.wasSetByUser() ){
+              Node bd = d_qe->getTermDatabase()->getInstConstantBody( d_single_inv );
+              std::vector< Node > patTerms;
+              std::vector< Node > exclude;
+              inst::Trigger::collectPatTerms( d_qe, d_single_inv, bd, patTerms, inst::Trigger::TS_ALL, exclude );
+              if( !patTerms.empty() ){
+                Trace("cegqi-si-em") << "Triggers : " << std::endl;
+                for( unsigned i=0; i<patTerms.size(); i++ ){
+                  Trace("cegqi-si-em") << "   " << patTerms[i] << std::endl;
+                }
               }
             }
+            */
           }
-          */
         }
       }
     }
@@ -1146,9 +1267,66 @@ bool CegConjectureSingleInv::getVariableEliminationTerm( bool pol, bool hasPol,
   return false;
 }
 
+int CegConjectureSingleInv::extractInvariantPolarity( Node n, Node inv, std::vector< Node >& curr_disj, bool pol ) {
+  if( n.getKind()==NOT ){
+    return extractInvariantPolarity( n[0], inv, curr_disj, !pol );
+  }else if( ( n.getKind()==AND && pol ) || ( n.getKind()==OR && !pol ) ){
+    int curr_pol = -1;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      int eipc = extractInvariantPolarity( n[i], inv, curr_disj, pol );
+      if( eipc!=-1 ){
+        if( curr_pol==-1 ){
+          curr_pol = eipc;
+        }else{
+          return -1;
+        }
+      }else{
+        curr_disj.push_back( pol ? n[i] : TermDb::simpleNegate( n[i] ) );
+      }
+    }
+    return curr_pol;
+  }else if( n==inv ){
+    return pol ? 1 : 0;
+  }else{
+    return -1;
+  }
+}
+
+Node CegConjectureSingleInv::substituteInvariantTemplates( Node n, std::map< Node, Node >& prog_templ, std::map< Node, std::vector< Node > >& prog_templ_vars ) {
+  if( n.getKind()==APPLY_UF && n.getNumChildren()>0 ){
+    std::map< Node, Node >::iterator it = prog_templ.find( n[0] );
+    if( it!=prog_templ.end() ){
+      std::vector< Node > children;
+      for( unsigned i=1; i<n.getNumChildren(); i++ ){
+        children.push_back( n[i] );
+      }
+      std::map< Node, std::vector< Node > >::iterator itv = prog_templ_vars.find( n[0] );
+      Assert( itv!=prog_templ_vars.end() );
+      Assert( children.size()==itv->second.size() );
+      Node newc = it->second.substitute( itv->second.begin(), itv->second.end(), children.begin(), children.end() );
+      return newc;
+    }
+  }
+  bool childChanged = false;
+  std::vector< Node > children;
+  for( unsigned i=0; i<n.getNumChildren(); i++ ){
+    Node nn = substituteInvariantTemplates( n[i], prog_templ, prog_templ_vars );
+    children.push_back( nn );
+    childChanged = childChanged || ( nn!=n[i] );
+  }
+  if( childChanged ){
+    if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+      children.insert( children.begin(), n.getOperator() );
+    }
+    return NodeManager::currentNM()->mkNode( n.getKind(), children );
+  }else{
+    return n;
+  }
+}
+
 bool CegConjectureSingleInv::analyzeSygusConjunct( Node p, Node n, std::map< Node, std::vector< Node > >& children,
-                                                            std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke,
-                                                            std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol ) {
+                                                   std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke,
+                                                   std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol ) {
   if( ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND ) ){
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
       if( !analyzeSygusConjunct( p, n[i], children, prog_invoke, progs, contains, pol ) ){
@@ -1371,7 +1549,12 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int&
   Trace("csi-sol") << "Solution (pre-simplification): " << d_orig_solution << std::endl;
   s = d_sol->simplifySolution( s, stn );
   Trace("csi-sol") << "Solution (post-simplification): " << s << std::endl;
+  return reconstructToSyntax( s, stn, reconstructed );
+}
+
+Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& reconstructed ) {
   d_solution = s;
+  const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
 
   //reconstruct the solution into sygus if necessary
   reconstructed = 0;
@@ -1429,4 +1612,5 @@ bool CegConjectureSingleInv::needsCheck() {
   return true;
 }
 
+
 }
\ No newline at end of file
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index f8e3879ac..f0d00b61c 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -111,6 +111,9 @@ private:
   bool processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals );
   bool doVariableElimination( Node v, std::vector< Node >& conjuncts );
   bool getVariableEliminationTerm( bool pol, bool active, Node v, Node n, TNode& s, int& status );
+  //for recognizing templates for invariant synthesis
+  int extractInvariantPolarity( Node n, Node inv, std::vector< Node >& curr_disj, bool pol );
+  Node substituteInvariantTemplates( Node n, std::map< Node, Node >& prog_templ, std::map< Node, std::vector< Node > >& prog_templ_vars );
   //presolve
   void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq );
   void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms, std::map< Node, std::vector< Node > >& teq, Node n, std::vector< Node >& conj );
@@ -141,7 +144,7 @@ private:
 public:
   //lemmas produced
   std::vector< Node > d_lemmas_produced;
-  std::vector< std::vector< Node > > d_inst; 
+  std::vector< std::vector< Node > > d_inst;
 private:
   std::vector< Node > d_curr_lemmas;
   //add instantiation
@@ -156,6 +159,10 @@ public:
   Node d_quant;
   // single invocation version of quant
   Node d_single_inv;
+  // transition relation version per program
+  std::map< Node, Node > d_trans_pre;
+  std::map< Node, Node > d_trans_post;
+  std::map< Node, std::vector< Node > > d_prog_templ_vars;
 public:
   //get the single invocation lemma
   Node getSingleInvLemma( Node guard );
@@ -165,6 +172,8 @@ public:
   void check( std::vector< Node >& lems );
   //get solution
   Node getSolution( unsigned sol_index, TypeNode stn, int& reconstructed );
+  //reconstruct to syntax
+  Node reconstructToSyntax( Node s, TypeNode stn, int& reconstructed );
   // has ites
   bool hasITEs() { return d_has_ites; }
   // is single invocation
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index 97ad3e8ea..af2d88e94 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -152,6 +152,15 @@ typedef enum {
   ITE_LIFT_QUANT_MODE_ALL,
 } IteLiftQuantMode;
 
+typedef enum {
+  /** synthesize I( x ) */
+  SYGUS_INV_TEMPL_MODE_NONE,
+  /** synthesize ( pre( x ) V I( x ) ) */
+  SYGUS_INV_TEMPL_MODE_PRE,
+  /** synthesize ( post( x ) ^ I( x ) ) */
+  SYGUS_INV_TEMPL_MODE_POST,
+} SygusInvTemplMode;
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index ab0526471..5cb9062e4 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -32,7 +32,7 @@ option iteLiftQuant --ite-lift-quant=MODE CVC4::theory::quantifiers::IteLiftQuan
  ite lifting mode for quantified formulas
 option iteCondVarSplitQuant --ite-cond-var-split-quant bool :default true
  split variables occurring as conditions of ITE in quantifiers
-option iteDtTesterSplitQuant --ite-dtt-split-quant bool :default false
+option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default false
  split ites with dt testers as conditions
 # Whether to CNF quantifier bodies
 # option cnfQuant --cnf-quant bool :default false
@@ -240,6 +240,9 @@ option sygusNormalFormGlobalArg --sygus-nf-sym-arg bool :default true
 option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true
   generalize based on content in global search space narrowing
   
+option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToSygusInvTemplMode :handler-include "theory/quantifiers/options_handlers.h"
+  template mode for sygus invariant synthesis
+
 # approach applied to general quantified formulas
 option cbqi --cbqi bool :read-write :default false
  turns on counterexample-based quantifier instantiation
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index c518813a0..4d2276621 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -217,6 +217,19 @@ none \n\
 + Lift if-then-else in quantified formulas. \n\
 \n\
 ";
+static const std::string sygusInvTemplHelp = "\
+Template modes for sygus invariant synthesis, supported by --sygus-inv-templ:\n\
+\n\
+none  \n\
++ Synthesize invariant directly.\n\
+\n\
+pre  \n\
++ Synthesize invariant based on weakening of precondition .\n\
+\n\
+post \n\
++ Synthesize invariant based on strengthening of postcondition. \n\
+\n\
+";
 
 inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
   if(optarg == "pre-full") {
@@ -443,6 +456,22 @@ inline IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string
   }
 }
 
+inline SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg == "none" ) {
+    return SYGUS_INV_TEMPL_MODE_NONE;
+  } else if(optarg == "pre") {
+    return SYGUS_INV_TEMPL_MODE_PRE;
+  } else if(optarg == "post") {
+    return SYGUS_INV_TEMPL_MODE_POST;
+  } else if(optarg ==  "help") {
+    puts(sygusInvTemplHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --sygus-inv-templ: `") +
+                          optarg + "'.  Try --sygus-inv-templ help.");
+  }
+}
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index fa0e211b3..c6115195d 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -781,6 +781,7 @@ Node TermDb::getCounterexampleLiteral( Node f ){
 }
 
 Node TermDb::getInstConstantNode( Node n, Node f ){
+  Assert( d_inst_constants.find( f )!=d_inst_constants.end() );
   return convertNodeToPattern(n,f,d_vars[f],d_inst_constants[ f ]);
 }
 
@@ -1754,6 +1755,7 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int
 Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) {
   std::map< Node, Node >::iterator it = d_sygus_to_builtin[tn].find( n );
   if( it==d_sygus_to_builtin[tn].end() ){
+    Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n << ", type = " << tn << std::endl;
     Assert( n.getKind()==APPLY_CONSTRUCTOR );
     const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
     unsigned i = Datatype::indexOf( n.getOperator().toExpr() );