Split sygus template inference to its own file (#5388)

This splits techniques for inferring templates for functions-to-synthesize to their own file.

This is work towards cleaning up the single invocation utility, which will be undergoing some additions.

7 files changed, 299 insertions, 220 deletions

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 4b45072f7..ac7d6efc7 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -34,9 +34,8 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-CegSingleInv::CegSingleInv(QuantifiersEngine* qe, SynthConjecture* p)
+CegSingleInv::CegSingleInv(QuantifiersEngine* qe)
     : d_qe(qe),
-      d_parent(p),
       d_sip(new SingleInvocationPartition),
       d_sol(new CegSingleInvSol(qe)),
       d_isSolved(false),
@@ -61,20 +60,7 @@ void CegSingleInv::initialize(Node q)
   // infer single invocation-ness
 
   // get the variables
-  std::vector< Node > progs;
-  std::map< Node, std::vector< Node > > prog_vars;
-  for (const Node& sf : q[0])
-  {
-    progs.push_back( sf );
-    Node sfvl = CegGrammarConstructor::getSygusVarList(sf);
-    if (!sfvl.isNull())
-    {
-      for (const Node& sfv : sfvl)
-      {
-        prog_vars[sf].push_back(sfv);
-      }
-    }
-  }
+  std::vector<Node> progs(q[0].begin(), q[0].end());
   // compute single invocation partition
   Node qq;
   if (q[1].getKind() == NOT && q[1][0].getKind() == FORALL)
@@ -113,163 +99,8 @@ void CegSingleInv::initialize(Node q)
     if (options::cegqiSingleInvMode() != options::CegqiSingleInvMode::NONE)
     {
       d_single_invocation = true;
-      return;
-    }
-  }
-  // We are processing without single invocation techniques, now check if
-  // we should fix an invariant template (post-condition strengthening or
-  // pre-condition weakening).
-  options::SygusInvTemplMode tmode = options::sygusInvTemplMode();
-  if (tmode != options::SygusInvTemplMode::NONE)
-  {
-    // currently only works for single predicate synthesis
-    if (q[0].getNumChildren() > 1 || !q[0][0].getType().isPredicate())
-    {
-      tmode = options::SygusInvTemplMode::NONE;
-    }
-    else if (!options::sygusInvTemplWhenSyntax())
-    {
-      // only use invariant templates if no syntactic restrictions
-      if (CegGrammarConstructor::hasSyntaxRestrictions(q))
-      {
-        tmode = options::SygusInvTemplMode::NONE;
-      }
-    }
-  }
-
-  if (tmode == options::SygusInvTemplMode::NONE)
-  {
-    // not processing invariant templates
-    return;
-  }
-  // if we are doing invariant templates, then construct the template
-  Trace("sygus-si") << "- Do transition inference..." << std::endl;
-  d_ti[q].process(qq, q[0][0]);
-  Trace("cegqi-inv") << std::endl;
-  Node prog = d_ti[q].getFunction();
-  if (!d_ti[q].isComplete())
-  {
-    // the invariant could not be inferred
-    return;
-  }
-  Assert(prog == q[0][0]);
-  NodeManager* nm = NodeManager::currentNM();
-  // map the program back via non-single invocation map
-  std::vector<Node> prog_templ_vars;
-  d_ti[q].getVariables(prog_templ_vars);
-  d_trans_pre[prog] = d_ti[q].getPreCondition();
-  d_trans_post[prog] = d_ti[q].getPostCondition();
-  Trace("cegqi-inv") << "   precondition : " << d_trans_pre[prog] << std::endl;
-  Trace("cegqi-inv") << "  postcondition : " << d_trans_post[prog] << std::endl;
-  std::vector<Node> sivars;
-  d_sip->getSingleInvocationVariables(sivars);
-  Node invariant = d_sip->getFunctionInvocationFor(prog);
-  if (invariant.isNull())
-  {
-    // the conjecture did not have an instance of the invariant
-    // (e.g. it is trivially true/false).
-    return;
-  }
-  invariant = invariant.substitute(sivars.begin(),
-                                   sivars.end(),
-                                   prog_templ_vars.begin(),
-                                   prog_templ_vars.end());
-  Trace("cegqi-inv") << "      invariant : " << invariant << std::endl;
-
-  // store simplified version of quantified formula
-  d_simp_quant = d_sip->getFullSpecification();
-  std::vector<Node> new_bv;
-  for( const Node& v : sivars )
-  {
-    new_bv.push_back(nm->mkBoundVar(v.getType()));
-  }
-  d_simp_quant = d_simp_quant.substitute(
-      sivars.begin(), sivars.end(), new_bv.begin(), new_bv.end());
-  Assert(q[1].getKind() == NOT && q[1][0].getKind() == FORALL);
-  for (const Node& v : q[1][0][0])
-  {
-    new_bv.push_back(v);
-  }
-  d_simp_quant =
-      nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, new_bv), d_simp_quant)
-          .negate();
-  d_simp_quant = Rewriter::rewrite(d_simp_quant);
-  d_simp_quant = nm->mkNode(FORALL, q[0], d_simp_quant, q[2]);
-  Trace("sygus-si") << "Rewritten quantifier : " << d_simp_quant << std::endl;
-
-  // construct template argument
-  d_templ_arg[prog] = nm->mkSkolem("I", invariant.getType());
-
-  // construct template
-  Node templ;
-  if (options::sygusInvAutoUnfold())
-  {
-    if (d_ti[q].isComplete())
-    {
-      Trace("cegqi-inv-auto-unfold")
-          << "Automatic deterministic unfolding... " << std::endl;
-      // auto-unfold
-      DetTrace dt;
-      int init_dt = d_ti[q].initializeTrace(dt);
-      if (init_dt == 0)
-      {
-        Trace("cegqi-inv-auto-unfold") << "  Init : ";
-        dt.print("cegqi-inv-auto-unfold");
-        Trace("cegqi-inv-auto-unfold") << std::endl;
-        unsigned counter = 0;
-        unsigned status = 0;
-        while (counter < 100 && status == 0)
-        {
-          status = d_ti[q].incrementTrace(dt);
-          counter++;
-          Trace("cegqi-inv-auto-unfold") << "  #" << counter << " : ";
-          dt.print("cegqi-inv-auto-unfold");
-          Trace("cegqi-inv-auto-unfold")
-              << "...status = " << status << std::endl;
-        }
-        if (status == 1)
-        {
-          // we have a trivial invariant
-          templ = d_ti[q].constructFormulaTrace(dt);
-          Trace("cegqi-inv") << "By finite deterministic terminating trace, a "
-                                "solution invariant is : "
-                             << std::endl;
-          Trace("cegqi-inv") << "   " << templ << std::endl;
-          // this should be unnecessary
-          templ = nm->mkNode(AND, templ, d_templ_arg[prog]);
-        }
-      }
-      else
-      {
-        Trace("cegqi-inv-auto-unfold") << "...failed initialize." << std::endl;
-      }
-    }
-  }
-  Trace("cegqi-inv") << "Make the template... " << tmode << " " << templ
-                     << std::endl;
-  if (templ.isNull())
-  {
-    if (tmode == options::SygusInvTemplMode::PRE)
-    {
-      templ = nm->mkNode(OR, d_trans_pre[prog], d_templ_arg[prog]);
-    }
-    else
-    {
-      Assert(tmode == options::SygusInvTemplMode::POST);
-      templ = nm->mkNode(AND, d_trans_post[prog], d_templ_arg[prog]);
     }
   }
-  Trace("cegqi-inv") << "       template (pre-substitution) : " << templ
-                     << std::endl;
-  Assert(!templ.isNull());
-  // subsitute the template arguments
-  Assert(prog_templ_vars.size() == prog_vars[prog].size());
-  templ = templ.substitute(prog_templ_vars.begin(),
-                           prog_templ_vars.end(),
-                           prog_vars[prog].begin(),
-                           prog_vars[prog].end());
-  Trace("cegqi-inv") << "       template : " << templ << std::endl;
-  d_templ[prog] = templ;
 }
 
 void CegSingleInv::finishInit(bool syntaxRestricted)
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
index 642415935..0e1ddba1f 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
@@ -22,7 +22,6 @@
 #include "theory/quantifiers/inst_match_trie.h"
 #include "theory/quantifiers/single_inv_partition.h"
 #include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h"
-#include "theory/quantifiers/sygus/transition_inference.h"
 
 namespace CVC4 {
 namespace theory {
@@ -52,12 +51,8 @@ class CegSingleInv
  private:
   /** pointer to the quantifiers engine */
   QuantifiersEngine* d_qe;
-  /** the parent of this class */
-  SynthConjecture* d_parent;
   // single invocation inference utility
   SingleInvocationPartition* d_sip;
-  // transition inference module for each function to synthesize
-  std::map< Node, TransitionInference > d_ti;
   // solution reconstruction
   CegSingleInvSol* d_sol;
 
@@ -100,16 +95,9 @@ class CegSingleInv
   bool d_single_invocation;
   // single invocation portion of quantified formula
   Node d_single_inv;
-  // transition relation version per program
-  std::map< Node, Node > d_trans_pre;
-  std::map< Node, Node > d_trans_post;
-  // the template for each function to synthesize
-  std::map< Node, Node > d_templ;
-  // the template argument for each function to synthesize (occurs in exactly one position of its template)
-  std::map< Node, Node > d_templ_arg;
   
  public:
-  CegSingleInv(QuantifiersEngine* qe, SynthConjecture* p);
+  CegSingleInv(QuantifiersEngine* qe);
   ~CegSingleInv();
 
   // get simplified conjecture
@@ -144,35 +132,6 @@ class CegSingleInv
   /** preregister conjecture */
   void preregisterConjecture( Node q );
 
-  Node getTransPre(Node prog) const {
-    std::map<Node, Node>::const_iterator location = d_trans_pre.find(prog);
-    return location->second;
-  }
-
-  Node getTransPost(Node prog) const {
-    std::map<Node, Node>::const_iterator location = d_trans_post.find(prog);
-    return location->second;
-  }
-  // get template for program prog. This returns a term of the form t[x] where x is the template argument (see below)
-  Node getTemplate(Node prog) const {
-    std::map<Node, Node>::const_iterator tmpl = d_templ.find(prog);
-    if( tmpl!=d_templ.end() ){
-      return tmpl->second;
-    }else{
-      return Node::null();
-    }
-  }
-  // get the template argument for program prog.
-  // This is a variable which indicates the position of the function/predicate to synthesize.
-  Node getTemplateArg(Node prog) const {
-    std::map<Node, Node>::const_iterator tmpla = d_templ_arg.find(prog);
-    if( tmpla != d_templ_arg.end() ){
-      return tmpla->second;
-    }else{
-      return Node::null();
-    }
-  }
-
  private:
   /** solve trivial
    *
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index 33fce2e84..4549a0945 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -21,6 +21,7 @@
 #include "smt/smt_engine_scope.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/sygus/ce_guided_single_inv.h"
+#include "theory/quantifiers/sygus/transition_inference.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/smt_engine_subsolver.h"
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index c65ac9e65..2b4eba3b7 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -50,7 +50,8 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe,
       d_stats(s),
       d_tds(qe->getTermDatabaseSygus()),
       d_hasSolution(false),
-      d_ceg_si(new CegSingleInv(qe, this)),
+      d_ceg_si(new CegSingleInv(qe)),
+      d_templInfer(new SygusTemplateInfer),
       d_ceg_proc(new SynthConjectureProcess(qe)),
       d_ceg_gc(new CegGrammarConstructor(qe, this)),
       d_sygus_rconst(new SygusRepairConst(qe)),
@@ -116,15 +117,18 @@ void SynthConjecture::assign(Node q)
   {
     d_ceg_si->initialize(d_simp_quant);
     d_simp_quant = d_ceg_si->getSimplifiedConjecture();
+    if (!d_ceg_si->isSingleInvocation())
+    {
+      d_templInfer->initialize(d_simp_quant);
+    }
     // carry the templates
-    for (unsigned i = 0; i < q[0].getNumChildren(); i++)
+    for (const Node& v : q[0])
     {
-      Node v = q[0][i];
-      Node templ = d_ceg_si->getTemplate(v);
+      Node templ = d_templInfer->getTemplate(v);
       if (!templ.isNull())
       {
         templates[v] = templ;
-        templates_arg[v] = d_ceg_si->getTemplateArg(v);
+        templates_arg[v] = d_templInfer->getTemplateArg(v);
       }
     }
   }
@@ -1334,7 +1338,7 @@ bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
 
         // check if there was a template
         Node sf = d_quant[0][i];
-        Node templ = d_ceg_si->getTemplate(sf);
+        Node templ = d_templInfer->getTemplate(sf);
         if (!templ.isNull())
         {
           Trace("cegqi-inv-debug")
@@ -1342,7 +1346,7 @@ bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
           // if it was not embedded into the grammar
           if (!options::sygusTemplEmbedGrammar())
           {
-            TNode templa = d_ceg_si->getTemplateArg(sf);
+            TNode templa = d_templInfer->getTemplateArg(sf);
             // make the builtin version of the full solution
             sol = d_tds->sygusToBuiltin(sol, sol.getType());
             Trace("cegqi-inv") << "Builtin version of solution is : " << sol
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 5572032b6..7f499b1b3 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -33,6 +33,7 @@
 #include "theory/quantifiers/sygus/sygus_process_conj.h"
 #include "theory/quantifiers/sygus/sygus_repair_const.h"
 #include "theory/quantifiers/sygus/sygus_stats.h"
+#include "theory/quantifiers/sygus/template_infer.h"
 
 namespace CVC4 {
 namespace theory {
@@ -216,6 +217,8 @@ class SynthConjecture
   std::unique_ptr<DecisionStrategy> d_feasible_strategy;
   /** single invocation utility */
   std::unique_ptr<CegSingleInv> d_ceg_si;
+  /** template inference utility */
+  std::unique_ptr<SygusTemplateInfer> d_templInfer;
   /** utility for static preprocessing and analysis of conjectures */
   std::unique_ptr<SynthConjectureProcess> d_ceg_proc;
   /** grammar utility */
diff --git a/src/theory/quantifiers/sygus/template_infer.cpp b/src/theory/quantifiers/sygus/template_infer.cpp
new file mode 100644
index 000000000..2f6964f3a
--- /dev/null
+++ b/src/theory/quantifiers/sygus/template_infer.cpp
@@ -0,0 +1,205 @@
+/*********************                                                        */
+/*! \file template_infer.cpp 
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Mathias Preiner, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief utility for processing single invocation synthesis conjectures
+ **
+ **/
+#include "theory/quantifiers/sygus/template_infer.h"
+
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
+#include "theory/quantifiers/term_util.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+void SygusTemplateInfer::initialize(Node q)
+{
+  Assert(d_quant.isNull());
+  Assert(q.getKind() == FORALL);
+  d_quant = q;
+  // We are processing without single invocation techniques, now check if
+  // we should fix an invariant template (post-condition strengthening or
+  // pre-condition weakening).
+  options::SygusInvTemplMode tmode = options::sygusInvTemplMode();
+  if (tmode != options::SygusInvTemplMode::NONE)
+  {
+    // currently only works for single predicate synthesis
+    if (q[0].getNumChildren() > 1 || !q[0][0].getType().isPredicate())
+    {
+      tmode = options::SygusInvTemplMode::NONE;
+    }
+    else if (!options::sygusInvTemplWhenSyntax())
+    {
+      // only use invariant templates if no syntactic restrictions
+      if (CegGrammarConstructor::hasSyntaxRestrictions(q))
+      {
+        tmode = options::SygusInvTemplMode::NONE;
+      }
+    }
+  }
+
+  if (tmode == options::SygusInvTemplMode::NONE)
+  {
+    // not processing invariant templates
+    return;
+  }
+
+  Node qq;
+  if (q[1].getKind() == NOT && q[1][0].getKind() == FORALL)
+  {
+    qq = q[1][0][1];
+  }
+  else
+  {
+    qq = TermUtil::simpleNegate(q[1]);
+  }
+  if (qq.isConst())
+  {
+    // trivial, do not use transition inference
+    return;
+  }
+
+  // if we are doing invariant templates, then construct the template
+  Trace("sygus-si") << "- Do transition inference..." << std::endl;
+  d_ti.process(qq, q[0][0]);
+  Trace("cegqi-inv") << std::endl;
+  Node prog = d_ti.getFunction();
+  if (!d_ti.isComplete())
+  {
+    // the invariant could not be inferred
+    return;
+  }
+  Assert(prog == q[0][0]);
+  NodeManager* nm = NodeManager::currentNM();
+  // map the program back via non-single invocation map
+  std::vector<Node> prog_templ_vars;
+  d_ti.getVariables(prog_templ_vars);
+  d_trans_pre[prog] = d_ti.getPreCondition();
+  d_trans_post[prog] = d_ti.getPostCondition();
+  Trace("cegqi-inv") << "   precondition : " << d_trans_pre[prog] << std::endl;
+  Trace("cegqi-inv") << "  postcondition : " << d_trans_post[prog] << std::endl;
+
+  // construct template argument
+  TypeNode atn = prog.getType();
+  if (atn.isFunction())
+  {
+    atn = atn.getRangeType();
+  }
+  d_templ_arg[prog] = nm->mkSkolem("I", atn);
+
+  // construct template
+  Node templ;
+  if (options::sygusInvAutoUnfold())
+  {
+    if (d_ti.isComplete())
+    {
+      Trace("cegqi-inv-auto-unfold")
+          << "Automatic deterministic unfolding... " << std::endl;
+      // auto-unfold
+      DetTrace dt;
+      int init_dt = d_ti.initializeTrace(dt);
+      if (init_dt == 0)
+      {
+        Trace("cegqi-inv-auto-unfold") << "  Init : ";
+        dt.print("cegqi-inv-auto-unfold");
+        Trace("cegqi-inv-auto-unfold") << std::endl;
+        unsigned counter = 0;
+        unsigned status = 0;
+        while (counter < 100 && status == 0)
+        {
+          status = d_ti.incrementTrace(dt);
+          counter++;
+          Trace("cegqi-inv-auto-unfold") << "  #" << counter << " : ";
+          dt.print("cegqi-inv-auto-unfold");
+          Trace("cegqi-inv-auto-unfold")
+              << "...status = " << status << std::endl;
+        }
+        if (status == 1)
+        {
+          // we have a trivial invariant
+          templ = d_ti.constructFormulaTrace(dt);
+          Trace("cegqi-inv") << "By finite deterministic terminating trace, a "
+                                "solution invariant is : "
+                             << std::endl;
+          Trace("cegqi-inv") << "   " << templ << std::endl;
+          // this should be unnecessary
+          templ = nm->mkNode(AND, templ, d_templ_arg[prog]);
+        }
+      }
+      else
+      {
+        Trace("cegqi-inv-auto-unfold") << "...failed initialize." << std::endl;
+      }
+    }
+  }
+  Trace("cegqi-inv") << "Make the template... " << tmode << " " << templ
+                     << std::endl;
+  if (templ.isNull())
+  {
+    if (tmode == options::SygusInvTemplMode::PRE)
+    {
+      templ = nm->mkNode(OR, d_trans_pre[prog], d_templ_arg[prog]);
+    }
+    else
+    {
+      Assert(tmode == options::SygusInvTemplMode::POST);
+      templ = nm->mkNode(AND, d_trans_post[prog], d_templ_arg[prog]);
+    }
+  }
+  Trace("cegqi-inv") << "       template (pre-substitution) : " << templ
+                     << std::endl;
+  Assert(!templ.isNull());
+
+  // get the variables
+  Node sfvl = CegGrammarConstructor::getSygusVarList(prog);
+  if (!sfvl.isNull())
+  {
+    std::vector<Node> prog_vars(sfvl.begin(), sfvl.end());
+    // subsitute the template arguments
+    Trace("cegqi-inv") << "vars : " << prog_templ_vars << " " << prog_vars
+                       << std::endl;
+    Assert(prog_templ_vars.size() == prog_vars.size());
+    templ = templ.substitute(prog_templ_vars.begin(),
+                             prog_templ_vars.end(),
+                             prog_vars.begin(),
+                             prog_vars.end());
+  }
+  Trace("cegqi-inv") << "       template : " << templ << std::endl;
+  d_templ[prog] = templ;
+}
+
+Node SygusTemplateInfer::getTemplate(Node prog) const
+{
+  std::map<Node, Node>::const_iterator tmpl = d_templ.find(prog);
+  if (tmpl != d_templ.end())
+  {
+    return tmpl->second;
+  }
+  return Node::null();
+}
+
+Node SygusTemplateInfer::getTemplateArg(Node prog) const
+{
+  std::map<Node, Node>::const_iterator tmpla = d_templ_arg.find(prog);
+  if (tmpla != d_templ_arg.end())
+  {
+    return tmpla->second;
+  }
+  return Node::null();
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/sygus/template_infer.h b/src/theory/quantifiers/sygus/template_infer.h
new file mode 100644
index 000000000..97879dc22
--- /dev/null
+++ b/src/theory/quantifiers/sygus/template_infer.h
@@ -0,0 +1,76 @@
+/*********************                                                        */
+/*! \file template_infer.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief utility for inferring templates for invariant problems
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__TEMPLATE_INFER_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS__TEMPLATE_INFER_H
+
+#include <map>
+
+#include "expr/node.h"
+#include "theory/quantifiers/sygus/transition_inference.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/**
+ * This class infers templates for an invariant-to-synthesize based on the
+ * template mode. It uses the transition inference to choose a template.
+ */
+class SygusTemplateInfer
+{
+ public:
+  SygusTemplateInfer() {}
+  ~SygusTemplateInfer() {}
+  /**
+   * Initialize this class for synthesis conjecture q. If applicable, the
+   * templates for functions-to-synthesize for q are accessible by the
+   * calls below afterwards.
+   */
+  void initialize(Node q);
+  /**
+   * Get template for program prog. This returns a term of the form t[x] where
+   * x is the template argument (see below)
+   */
+  Node getTemplate(Node prog) const;
+  /**
+   * Get the template argument for program prog. This is a variable which
+   * indicates the position of the function/predicate to synthesize.
+   */
+  Node getTemplateArg(Node prog) const;
+
+ private:
+  /** The quantified formula we initialized with */
+  Node d_quant;
+  /** transition relation pre and post version per function to synthesize  */
+  std::map<Node, Node> d_trans_pre;
+  std::map<Node, Node> d_trans_post;
+  /** the template for each function to synthesize */
+  std::map<Node, Node> d_templ;
+  /**
+   * The template argument for each function to synthesize (occurs in exactly
+   * one position of its template)
+   */
+  std::map<Node, Node> d_templ_arg;
+  /** transition inference module */
+  TransitionInference d_ti;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+} /* namespace CVC4 */
+
+#endif