From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 23 Aug 2019 19:44:14 +0000 (-0500)
Subject: Document transition inference utility (#3207)
X-Git-Tag: cvc5-1.0.0~3996
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c11154240248592b5446f1de4743d78ed2fb97bd;p=cvc5.git

Document transition inference utility (#3207)
---

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 16feace50..c75e5576f 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -591,6 +591,8 @@ libcvc4_add_sources(
   theory/quantifiers/sygus/synth_engine.h
   theory/quantifiers/sygus/term_database_sygus.cpp
   theory/quantifiers/sygus/term_database_sygus.h
+  theory/quantifiers/sygus/transition_inference.cpp
+  theory/quantifiers/sygus/transition_inference.h
   theory/quantifiers/sygus_sampler.cpp
   theory/quantifiers/sygus_sampler.h
   theory/quantifiers/term_database.cpp
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index a6eed127b..4289fc815 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -14,7 +14,6 @@
  **/
 #include "theory/quantifiers/sygus/ce_guided_single_inv.h"
 
-#include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
@@ -146,19 +145,18 @@ void CegSingleInv::initialize(Node q)
   Trace("cegqi-si") << "- Do transition inference..." << std::endl;
   d_ti[q].process(qq);
   Trace("cegqi-inv") << std::endl;
-  if (d_ti[q].d_func.isNull())
+  Node prog = d_ti[q].getFunction();
+  if (prog.isNull())
   {
     // the invariant could not be inferred
     return;
   }
   NodeManager* nm = NodeManager::currentNM();
   // map the program back via non-single invocation map
-  Node prog = d_ti[q].d_func;
   std::vector<Node> prog_templ_vars;
-  prog_templ_vars.insert(
-      prog_templ_vars.end(), d_ti[q].d_vars.begin(), d_ti[q].d_vars.end());
-  d_trans_pre[prog] = d_ti[q].getComponent(1);
-  d_trans_post[prog] = d_ti[q].getComponent(-1);
+  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;
@@ -604,447 +602,5 @@ Node CegSingleInv::reconstructToSyntax(Node s,
 }
 
 void CegSingleInv::preregisterConjecture(Node q) { d_orig_conjecture = q; }
-
-bool DetTrace::DetTraceTrie::add( Node loc, std::vector< Node >& val, unsigned index ){
-  if( index==val.size() ){
-    if( d_children.empty() ){
-      d_children[loc].clear();
-      return true;
-    }else{
-      return false;
-    }
-  }else{
-    return d_children[val[index]].add( loc, val, index+1 );
-  }
-}
-
-Node DetTrace::DetTraceTrie::constructFormula( std::vector< Node >& vars, unsigned index ){
-  if( index==vars.size() ){
-    return NodeManager::currentNM()->mkConst( true );    
-  }else{
-    std::vector< Node > disj;
-    for( std::map< Node, DetTraceTrie >::iterator it = d_children.begin(); it != d_children.end(); ++it ){
-      Node eq = vars[index].eqNode( it->first );
-      if( index<vars.size()-1 ){
-        Node conc = it->second.constructFormula( vars, index+1 );
-        disj.push_back( NodeManager::currentNM()->mkNode( kind::AND, eq, conc ) );
-      }else{
-        disj.push_back( eq );
-      }
-    }
-    Assert( !disj.empty() );
-    return disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj );
-  }
-}
-
-bool DetTrace::increment( Node loc, std::vector< Node >& vals ){
-  if( d_trie.add( loc, vals ) ){
-    for( unsigned i=0; i<vals.size(); i++ ){
-      d_curr[i] = vals[i];
-    }
-    return true;
-  }else{
-    return false;
-  }
-}
-
-Node DetTrace::constructFormula( std::vector< Node >& vars ) {
-  return d_trie.constructFormula( vars );
-}
-
-
-void DetTrace::print( const char* c ) {
-  for( unsigned i=0; i<d_curr.size(); i++ ){
-    Trace(c) << d_curr[i] << " ";
-  }
-}
-
-void TransitionInference::initialize( Node f, std::vector< Node >& vars ) {
-  Assert( d_vars.empty() );
-  d_func = f;
-  d_vars.insert( d_vars.end(), vars.begin(), vars.end() );
-}
-
-
-void TransitionInference::getConstantSubstitution( std::vector< Node >& vars, std::vector< Node >& disjuncts, std::vector< Node >& const_var, std::vector< Node >& const_subs, bool reqPol ) {
-  for( unsigned j=0; j<disjuncts.size(); j++ ){
-    Node sn;
-    if( !const_var.empty() ){
-      sn = disjuncts[j].substitute( const_var.begin(), const_var.end(), const_subs.begin(), const_subs.end() );
-      sn = Rewriter::rewrite( sn );
-    }else{
-      sn = disjuncts[j];
-    }
-    bool slit_pol = sn.getKind()!=NOT;
-    Node slit = sn.getKind()==NOT ? sn[0] : sn;
-    if( slit.getKind()==EQUAL && slit_pol==reqPol ){
-      // check if it is a variable equality
-      TNode v;
-      Node s;
-      for (unsigned r = 0; r < 2; r++)
-      {
-        if (std::find(vars.begin(), vars.end(), slit[r]) != vars.end())
-        {
-          if (!expr::hasSubterm(slit[1 - r], slit[r]))
-          {
-            v = slit[r];
-            s = slit[1 - r];
-            break;
-          }
-        }
-      }
-      if( v.isNull() ){
-        //solve for var
-        std::map< Node, Node > msum;
-        if (ArithMSum::getMonomialSumLit(slit, msum))
-        {
-          for (std::map<Node, Node>::iterator itm = msum.begin();
-               itm != msum.end();
-               ++itm)
-          {
-            if (std::find(vars.begin(), vars.end(), itm->first) != vars.end())
-            {
-              Node veq_c;
-              Node val;
-              int ires =
-                  ArithMSum::isolate(itm->first, msum, veq_c, val, EQUAL);
-              if (ires != 0 && veq_c.isNull()
-                  && !expr::hasSubterm(val, itm->first))
-              {
-                v = itm->first;
-                s = val;
-              }
-            }
-          }
-        }
-      }
-      if( !v.isNull() ){
-        TNode ts = s;
-        for( unsigned k=0; k<const_subs.size(); k++ ){
-          const_subs[k] = Rewriter::rewrite( const_subs[k].substitute( v, ts ) );
-        }
-        Trace("cegqi-inv-debug2") << "...substitution : " << v << " -> " << s << std::endl;
-        const_var.push_back( v );
-        const_subs.push_back( s );
-      }
-    }
-  }
-}
-
-void TransitionInference::process( Node n ) {
-  NodeManager* nm = NodeManager::currentNM();
-  d_complete = true;
-  std::vector< Node > n_check;
-  if( n.getKind()==AND ){
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      n_check.push_back( n[i] );
-    }
-  }else{
-    n_check.push_back( n );
-  }
-  for( unsigned i=0; i<n_check.size(); i++ ){
-    Node nn = n_check[i];
-    std::map<bool, std::map<Node, bool> > visited;
-    std::map< bool, Node > terms;
-    std::vector< Node > disjuncts;
-    Trace("cegqi-inv") << "TransitionInference : Process disjunct : " << nn << std::endl;
-    if( processDisjunct( nn, terms, disjuncts, visited, true ) ){
-      if( !terms.empty() ){
-        Node curr;
-        int comp_num;
-        std::map< bool, Node >::iterator itt = terms.find( false );
-        if( itt!=terms.end() ){
-          curr = itt->second;
-          if( terms.find( true )!=terms.end() ){
-            comp_num = 0;
-          }else{
-            comp_num = -1;
-          }
-        }else{
-          curr = terms[true];
-          comp_num = 1;
-        }
-        Trace("cegqi-inv-debug2")
-            << "  normalize based on " << curr << std::endl;
-        std::vector<Node> vars;
-        std::vector<Node> svars;
-        getNormalizedSubstitution(curr, d_vars, vars, svars, disjuncts);
-        for( unsigned j=0; j<disjuncts.size(); j++ ){
-          Trace("cegqi-inv-debug2") << "  apply " << disjuncts[j] << std::endl;
-          disjuncts[j] = Rewriter::rewrite(disjuncts[j].substitute(
-              vars.begin(), vars.end(), svars.begin(), svars.end()));
-          Trace("cegqi-inv-debug2") << "  ..." << disjuncts[j] << std::endl;
-        }
-        std::vector< Node > const_var;
-        std::vector< Node > const_subs;
-        if( comp_num==0 ){
-          //transition
-          Assert( terms.find( true )!=terms.end() );
-          Node next = terms[true];
-          next = Rewriter::rewrite(next.substitute(
-              vars.begin(), vars.end(), svars.begin(), svars.end()));
-          Trace("cegqi-inv-debug") << "transition next predicate : " << next << std::endl;
-          // make the primed variables if we have not already
-          if (d_prime_vars.empty())
-          {
-            for (unsigned j = 0, nchild = next.getNumChildren(); j < nchild;
-                 j++)
-            {
-              Node v = nm->mkSkolem(
-                  "ir", next[j].getType(), "template inference rev argument");
-              d_prime_vars.push_back( v );
-            }
-          }
-          // normalize the other direction
-          Trace("cegqi-inv-debug2") << "  normalize based on " << next << std::endl;
-          std::vector<Node> rvars;
-          std::vector<Node> rsvars;
-          getNormalizedSubstitution(
-              next, d_prime_vars, rvars, rsvars, disjuncts);
-          Assert(rvars.size() == rsvars.size());
-          for( unsigned j=0; j<disjuncts.size(); j++ ){
-            Trace("cegqi-inv-debug2")
-                << "  apply " << disjuncts[j] << std::endl;
-            disjuncts[j] = Rewriter::rewrite(disjuncts[j].substitute(
-                rvars.begin(), rvars.end(), rsvars.begin(), rsvars.end()));
-            Trace("cegqi-inv-debug2") << "  ..." << disjuncts[j] << std::endl;
-          }
-          getConstantSubstitution( d_prime_vars, disjuncts, const_var, const_subs, false );
-        }else{
-          getConstantSubstitution( d_vars, disjuncts, const_var, const_subs, false );
-        }
-        Node res;
-        if( disjuncts.empty() ){
-          res = NodeManager::currentNM()->mkConst( false );
-        }else if( disjuncts.size()==1 ){
-          res = disjuncts[0];
-        }else{
-          res = NodeManager::currentNM()->mkNode( kind::OR, disjuncts );
-        }
-        if (!expr::hasBoundVar(res))
-        {
-          Trace("cegqi-inv") << "*** inferred " << ( comp_num==1 ? "pre" : ( comp_num==-1 ? "post" : "trans" ) ) << "-condition : " << res << std::endl;
-          d_com[comp_num].d_conjuncts.push_back( res );
-          if( !const_var.empty() ){
-            bool has_const_eq = const_var.size()==d_vars.size();
-            Trace("cegqi-inv") << "    with constant substitution, complete = " << has_const_eq << " : " << std::endl;
-            for( unsigned i=0; i<const_var.size(); i++ ){
-              Trace("cegqi-inv") << "      " << const_var[i] << " -> " << const_subs[i] << std::endl;
-              if( has_const_eq ){
-                d_com[comp_num].d_const_eq[res][const_var[i]] = const_subs[i];
-              }
-            }
-            Trace("cegqi-inv") << "...size = " << const_var.size() << ", #vars = " << d_vars.size() << std::endl;
-          }
-        }else{
-          Trace("cegqi-inv-debug2") << "...failed, free variable." << std::endl;
-          d_complete = false;
-        }
-      }
-    }else{
-      d_complete = false;
-    }
-  }
-  
-  // finalize the components
-  for( int i=-1; i<=1; i++ ){
-    Node ret;
-    if( d_com[i].d_conjuncts.empty() ){
-      ret = NodeManager::currentNM()->mkConst( true );
-    }else if( d_com[i].d_conjuncts.size()==1 ){
-      ret = d_com[i].d_conjuncts[0];
-    }else{
-      ret = NodeManager::currentNM()->mkNode( kind::AND, d_com[i].d_conjuncts );
-    }
-    if( i==0 || i==1 ){
-      // pre-condition and transition are negated
-      ret = TermUtil::simpleNegate( ret );
-    }
-    d_com[i].d_this = ret;
-  }
-}
-void TransitionInference::getNormalizedSubstitution(
-    Node curr,
-    const std::vector<Node>& pvars,
-    std::vector<Node>& vars,
-    std::vector<Node>& subs,
-    std::vector<Node>& disjuncts)
-{
-  for (unsigned j = 0, nchild = curr.getNumChildren(); j < nchild; j++)
-  {
-    if (curr[j].getKind() == BOUND_VARIABLE)
-    {
-      // if the argument is a bound variable, add to the renaming
-      vars.push_back(curr[j]);
-      subs.push_back(pvars[j]);
-    }
-    else
-    {
-      // otherwise, treat as a constraint on the variable
-      // For example, this transforms e.g. a precondition clause
-      // I( 0, 1 ) to x1 != 0 OR x2 != 1 OR I( x1, x2 ).
-      Node eq = curr[j].eqNode(pvars[j]);
-      disjuncts.push_back(eq.negate());
-    }
-  }
-}
-
-bool TransitionInference::processDisjunct(
-    Node n,
-    std::map<bool, Node>& terms,
-    std::vector<Node>& disjuncts,
-    std::map<bool, std::map<Node, bool> >& visited,
-    bool topLevel)
-{
-  if (visited[topLevel].find(n) == visited[topLevel].end())
-  {
-    visited[topLevel][n] = true;
-    bool childTopLevel = n.getKind()==OR && topLevel;
-    //if another part mentions UF or a free variable, then fail
-    bool lit_pol = n.getKind()!=NOT;
-    Node lit = n.getKind()==NOT ? n[0] : n;
-    if( lit.getKind()==APPLY_UF ){
-      Node op = lit.getOperator();
-      if( d_func.isNull() ){
-        d_func = op;
-        Trace("cegqi-inv-debug") << "Use " << op << " with args ";
-        for( unsigned i=0; i<lit.getNumChildren(); i++ ){
-          Node v = NodeManager::currentNM()->mkSkolem( "i", lit[i].getType(), "template inference argument" );
-          d_vars.push_back( v );
-          Trace("cegqi-inv-debug") << v << " ";
-        }
-        Trace("cegqi-inv-debug") << std::endl;
-      }
-      if( op!=d_func ){
-        Trace("cegqi-inv-debug") << "...failed, free function : " << n << std::endl;
-        return false;
-      }else if( topLevel ){
-        if( terms.find( lit_pol )==terms.end() ){
-          terms[lit_pol] = lit;
-          return true;
-        }else{
-          Trace("cegqi-inv-debug") << "...failed, repeated inv-app : " << lit << std::endl;
-          return false;
-        }
-      }else{
-        Trace("cegqi-inv-debug") << "...failed, non-entailed inv-app : " << lit << std::endl;
-        return false;
-      }
-    }else if( topLevel && !childTopLevel ){
-      disjuncts.push_back( n );
-    }
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( !processDisjunct( n[i], terms, disjuncts, visited, childTopLevel ) ){
-        return false;
-      }
-    }
-  }
-  return true;
-}
-
-Node TransitionInference::getComponent( int i ) {
-  return d_com[i].d_this;
-}
-
-int TransitionInference::initializeTrace( DetTrace& dt, Node loc, bool fwd ) {
-  int index = fwd ? 1 : -1;
-  Assert( d_com[index].has( loc ) );
-  std::map< Node, std::map< Node, Node > >::iterator it = d_com[index].d_const_eq.find( loc );
-  if( it!=d_com[index].d_const_eq.end() ){
-    std::vector< Node > next;
-    for( unsigned i=0; i<d_vars.size(); i++ ){
-      Node v = d_vars[i];
-      Assert( it->second.find( v )!=it->second.end() );
-      next.push_back( it->second[v] );
-      dt.d_curr.push_back( it->second[v] );
-    }
-    Trace("cegqi-inv-debug2") << "dtrace : initial increment" << std::endl;
-    bool ret = dt.increment( loc, next );
-    AlwaysAssert( ret );
-    return 0;
-  }
-  return -1;
-}
-  
-int TransitionInference::incrementTrace( DetTrace& dt, Node loc, bool fwd ) {
-  Assert( d_com[0].has( loc ) );
-  // check if it satisfies the pre/post condition
-  int check_index = fwd ? -1 : 1;
-  Node cc = getComponent( check_index );
-  Assert( !cc.isNull() );
-  Node ccr = Rewriter::rewrite( cc.substitute( d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end() ) );
-  if( ccr.isConst() ){
-    if( ccr.getConst<bool>()==( fwd ? false : true ) ){
-      Trace("cegqi-inv-debug2") << "dtrace : counterexample" << std::endl;
-      return 2;
-    }
-  }
-
-
-  // terminates?
-  Node c = getComponent( 0 );
-  Assert( !c.isNull() );
-
-  Assert( d_vars.size()==dt.d_curr.size() );
-  Node cr = Rewriter::rewrite( c.substitute( d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end() ) );
-  if( cr.isConst() ){
-    if( !cr.getConst<bool>() ){
-      Trace("cegqi-inv-debug2") << "dtrace : terminated" << std::endl;
-      return 1;
-    }else{
-      return -1;
-    }
-  }
-  if( fwd ){
-    Component& cm = d_com[0];
-    std::map<Node, std::map<Node, Node> >::iterator it =
-        cm.d_const_eq.find(loc);
-    if (it != cm.d_const_eq.end())
-    {
-      std::vector< Node > next;
-      for( unsigned i=0; i<d_prime_vars.size(); i++ ){
-        Node pv = d_prime_vars[i];
-        Assert( it->second.find( pv )!=it->second.end() );
-        Node pvs = it->second[pv];
-        Assert( d_vars.size()==dt.d_curr.size() );
-        Node pvsr = Rewriter::rewrite( pvs.substitute( d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end() ) );
-        next.push_back( pvsr );
-      }
-      if( dt.increment( loc, next ) ){
-        Trace("cegqi-inv-debug2") << "dtrace : success increment" << std::endl;
-        return 0;
-      }else{
-        // looped
-        Trace("cegqi-inv-debug2") << "dtrace : looped" << std::endl;
-        return 1;
-      }
-    }
-  }else{
-    //TODO
-  }
-  return -1;
-}
-
-int TransitionInference::initializeTrace( DetTrace& dt, bool fwd ) {
-  Trace("cegqi-inv-debug2") << "Initialize trace" << std::endl;
-  int index = fwd ? 1 : -1;
-  if( d_com[index].d_conjuncts.size()==1 ){
-    return initializeTrace( dt, d_com[index].d_conjuncts[0], fwd );
-  }else{
-    return -1;
-  }
-}
-
-int TransitionInference::incrementTrace( DetTrace& dt, bool fwd ) {
-  if( d_com[0].d_conjuncts.size()==1 ){
-    return incrementTrace( dt, d_com[0].d_conjuncts[0], fwd );
-  }else{
-    return -1;
-  }
-}
-
-Node TransitionInference::constructFormulaTrace( DetTrace& dt ) {
-  return dt.constructFormula( d_vars );
-}
   
 } //namespace CVC4
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
index fb216ce0b..00e3639f8 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
@@ -18,10 +18,11 @@
 #define CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
 
 #include "context/cdlist.h"
-#include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h"
-#include "theory/quantifiers/inst_match_trie.h"
 #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
+#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 {
@@ -29,121 +30,6 @@ namespace quantifiers {
 
 class SynthConjecture;
 
-class DetTrace {
-private:
-  class DetTraceTrie {
-  public:
-    std::map< Node, DetTraceTrie > d_children;
-    bool add( Node loc, std::vector< Node >& val, unsigned index = 0 );
-    void clear() { d_children.clear(); }
-    Node constructFormula( std::vector< Node >& vars, unsigned index = 0 );
-  };
-  DetTraceTrie d_trie;
-public:
-  std::vector< Node > d_curr;
-  bool increment( Node loc, std::vector< Node >& vals );
-  Node constructFormula( std::vector< Node >& vars );
-  void print( const char* c );
-};
-
-/**
- * This class is used for inferring that an arbitrary synthesis conjecture
- * corresponds to an invariant synthesis problem for some predicate (d_func).
- *
- * The invariant-to-synthesize can either be explicitly given, via a call
- * to initialize( f, vars ), or otherwise inferred if this method is not called.
- */
-class TransitionInference {
- private:
-  /** process disjunct
-   *
-   * The purpose of this function is to infer pre/post/transition conditions
-   * for a (possibly unknown) invariant-to-synthesis, given a conjunct from
-   * an arbitrary synthesis conjecture.
-   *
-   * Assume our negated synthesis conjecture is of the form:
-   *    forall f. exists x. (and (or F11 ... F1{m_1}) ... (or Fn1 ... Fn{m_n}))
-   * This method is called on each (or Fi1 ... Fi{m_i}), where topLevel is true
-   * for each of Fi1...F1{m_i} and false otherwise. It adds each of Fi1..Fi{m_i}
-   * to disjuncts.
-   *
-   * If this method returns true, then (1) all applications of free function
-   * symbols have operator d_func. Note this function may set d_func to a
-   * function symbol in n if d_func was null prior to this call. In other words,
-   * this method may infer the subject of the invariant synthesis problem;
-   * (2) all occurrences of d_func are "top-level", that is, each Fij may be
-   * of the form (not) <d_func>( tj ), but otherwise d_func does not occur in
-   * (or Fi1 ... Fi{m_i}); (3) there exists at most one occurrence of
-   * <d_func>( tj ), and (not <d_func>( tk )).
-   *
-   * If the above conditions are met, then terms[true] is set to <d_func>( tj )
-   * if Fij is <d_func>( tj ) for some j, and likewise terms[false]
-   * is set to <d_func>( tk ) if Fik is (not <d_func>( tk )) for some k.
-   *
-   * The argument visited caches the results of this function for (topLevel, n).
-   */
-  bool processDisjunct(Node n,
-                       std::map<bool, Node>& terms,
-                       std::vector<Node>& disjuncts,
-                       std::map<bool, std::map<Node, bool> >& visited,
-                       bool topLevel);
-  void getConstantSubstitution( std::vector< Node >& vars, std::vector< Node >& disjuncts, std::vector< Node >& const_var, std::vector< Node >& const_subs, bool reqPol );
-  bool d_complete;
-  /** get normalized substitution
-   *
-   * This method takes as input a node curr of the form I( t1, ..., tn ) and
-   * a vector of variables pvars, where pvars.size()=n. For each ti that is
-   * a variable, it adds ti to vars, and pvars[i] to subs. For each ti that is
-   * not a variable, it adds the disequality ti != pvars[i] to disjuncts.
-   *
-   * This function is used for instance to normalize an arbitrary application of
-   * I so that is over arguments pvars. For instance if curr is I(3,5,y) and
-   * pvars = { x1,x2,x3 }, then the formula:
-   *   I(3,5,y) ^ P(y)
-   * is equivalent to:
-   *   x1 != 3 V x2 != 5 V I(x1,x2,x3) V P( y ) { y -> x3 }
-   * Here, we add y and x3 to vars and subs respectively, and x1!=3 and x2!=5
-   * to disjuncts.
-   */
-  void getNormalizedSubstitution(Node curr,
-                                 const std::vector<Node>& pvars,
-                                 std::vector<Node>& vars,
-                                 std::vector<Node>& subs,
-                                 std::vector<Node>& disjuncts);
-
- public:
-  TransitionInference() : d_complete( false ) {}
-  std::vector< Node > d_vars;
-  std::vector< Node > d_prime_vars;
-  /**
-   * The function (predicate) that is the subject of the invariant synthesis
-   * problem we are inferring.
-   */
-  Node d_func;
-  
-  class Component {
-  public:
-    Component(){}
-    Node d_this;
-    std::vector< Node > d_conjuncts;
-    std::map< Node, std::map< Node, Node > > d_const_eq;
-    bool has( Node c ) { return std::find( d_conjuncts.begin(), d_conjuncts.end(), c )!=d_conjuncts.end(); }
-  };
-  std::map< int, Component > d_com;
-  
-  void initialize( Node f, std::vector< Node >& vars );
-  void process( Node n );
-  Node getComponent( int i );
-  bool isComplete() { return d_complete; }
-  
-  // 0 : success, 1 : terminated, 2 : counterexample, -1 : invalid
-  int initializeTrace( DetTrace& dt, Node loc, bool fwd = true );
-  int incrementTrace( DetTrace& dt, Node loc, bool fwd = true );
-  int initializeTrace( DetTrace& dt, bool fwd = true );
-  int incrementTrace( DetTrace& dt, bool fwd = true );
-  Node constructFormulaTrace( DetTrace& dt );
-};
-
 // this class infers whether a conjecture is single invocation (Reynolds et al CAV 2015), and sets up the
 // counterexample-guided quantifier instantiation utility (d_cinst), and methods for solution
 // reconstruction (d_sol).
diff --git a/src/theory/quantifiers/sygus/transition_inference.cpp b/src/theory/quantifiers/sygus/transition_inference.cpp
new file mode 100644
index 000000000..88ffe84b2
--- /dev/null
+++ b/src/theory/quantifiers/sygus/transition_inference.cpp
@@ -0,0 +1,579 @@
+/*********************                                                        */
+/*! \file transition_inference.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 Implmentation of utility for inferring whether a synthesis conjecture
+ ** encodes a transition system.
+ **
+ **/
+#include "theory/quantifiers/sygus/transition_inference.h"
+
+#include "expr/node_algorithm.h"
+#include "theory/arith/arith_msum.h"
+#include "theory/quantifiers/term_util.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+bool DetTrace::DetTraceTrie::add(Node loc, const std::vector<Node>& val)
+{
+  DetTraceTrie* curr = this;
+  for (const Node& v : val)
+  {
+    curr = &(curr->d_children[v]);
+  }
+  if (curr->d_children.empty())
+  {
+    curr->d_children[loc].clear();
+    return true;
+  }
+  return false;
+}
+
+Node DetTrace::DetTraceTrie::constructFormula(const std::vector<Node>& vars,
+                                              unsigned index)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  if (index == vars.size())
+  {
+    return nm->mkConst(true);
+  }
+  std::vector<Node> disj;
+  for (std::pair<const Node, DetTraceTrie>& p : d_children)
+  {
+    Node eq = vars[index].eqNode(p.first);
+    if (index < vars.size() - 1)
+    {
+      Node conc = p.second.constructFormula(vars, index + 1);
+      disj.push_back(nm->mkNode(AND, eq, conc));
+    }
+    else
+    {
+      disj.push_back(eq);
+    }
+  }
+  Assert(!disj.empty());
+  return disj.size() == 1 ? disj[0] : nm->mkNode(OR, disj);
+}
+
+bool DetTrace::increment(Node loc, std::vector<Node>& vals)
+{
+  if (d_trie.add(loc, vals))
+  {
+    for (unsigned i = 0, vsize = vals.size(); i < vsize; i++)
+    {
+      d_curr[i] = vals[i];
+    }
+    return true;
+  }
+  return false;
+}
+
+Node DetTrace::constructFormula(const std::vector<Node>& vars)
+{
+  return d_trie.constructFormula(vars);
+}
+
+void DetTrace::print(const char* c) const
+{
+  for (const Node& n : d_curr)
+  {
+    Trace(c) << n << " ";
+  }
+}
+
+Node TransitionInference::getFunction() const { return d_func; }
+
+void TransitionInference::getVariables(std::vector<Node>& vars) const
+{
+  vars.insert(vars.end(), d_vars.begin(), d_vars.end());
+}
+
+Node TransitionInference::getPreCondition() const { return d_pre.d_this; }
+Node TransitionInference::getPostCondition() const { return d_post.d_this; }
+Node TransitionInference::getTransitionRelation() const
+{
+  return d_trans.d_this;
+}
+
+void TransitionInference::getConstantSubstitution(
+    const std::vector<Node>& vars,
+    const std::vector<Node>& disjuncts,
+    std::vector<Node>& const_var,
+    std::vector<Node>& const_subs,
+    bool reqPol)
+{
+  for (const Node& d : disjuncts)
+  {
+    Node sn;
+    if (!const_var.empty())
+    {
+      sn = d.substitute(const_var.begin(),
+                        const_var.end(),
+                        const_subs.begin(),
+                        const_subs.end());
+      sn = Rewriter::rewrite(sn);
+    }
+    else
+    {
+      sn = d;
+    }
+    bool slit_pol = sn.getKind() != NOT;
+    Node slit = sn.getKind() == NOT ? sn[0] : sn;
+    if (slit.getKind() == EQUAL && slit_pol == reqPol)
+    {
+      // check if it is a variable equality
+      TNode v;
+      Node s;
+      for (unsigned r = 0; r < 2; r++)
+      {
+        if (std::find(vars.begin(), vars.end(), slit[r]) != vars.end())
+        {
+          if (!expr::hasSubterm(slit[1 - r], slit[r]))
+          {
+            v = slit[r];
+            s = slit[1 - r];
+            break;
+          }
+        }
+      }
+      if (v.isNull())
+      {
+        // solve for var
+        std::map<Node, Node> msum;
+        if (ArithMSum::getMonomialSumLit(slit, msum))
+        {
+          for (std::pair<const Node, Node>& m : msum)
+          {
+            if (std::find(vars.begin(), vars.end(), m.first) != vars.end())
+            {
+              Node veq_c;
+              Node val;
+              int ires = ArithMSum::isolate(m.first, msum, veq_c, val, EQUAL);
+              if (ires != 0 && veq_c.isNull()
+                  && !expr::hasSubterm(val, m.first))
+              {
+                v = m.first;
+                s = val;
+              }
+            }
+          }
+        }
+      }
+      if (!v.isNull())
+      {
+        TNode ts = s;
+        for (unsigned k = 0, csize = const_subs.size(); k < csize; k++)
+        {
+          const_subs[k] = Rewriter::rewrite(const_subs[k].substitute(v, ts));
+        }
+        Trace("cegqi-inv-debug2")
+            << "...substitution : " << v << " -> " << s << std::endl;
+        const_var.push_back(v);
+        const_subs.push_back(s);
+      }
+    }
+  }
+}
+
+void TransitionInference::process(Node n)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  d_complete = true;
+  std::vector<Node> n_check;
+  if (n.getKind() == AND)
+  {
+    for (const Node& nc : n)
+    {
+      n_check.push_back(nc);
+    }
+  }
+  else
+  {
+    n_check.push_back(n);
+  }
+  for (const Node& nn : n_check)
+  {
+    std::map<bool, std::map<Node, bool> > visited;
+    std::map<bool, Node> terms;
+    std::vector<Node> disjuncts;
+    Trace("cegqi-inv") << "TransitionInference : Process disjunct : " << nn
+                       << std::endl;
+    if (!processDisjunct(nn, terms, disjuncts, visited, true))
+    {
+      d_complete = false;
+      continue;
+    }
+    if (terms.empty())
+    {
+      continue;
+    }
+    Node curr;
+    // The component that this disjunct contributes to, where
+    // 1 : pre-condition, -1 : post-condition, 0 : transition relation
+    int comp_num;
+    std::map<bool, Node>::iterator itt = terms.find(false);
+    if (itt != terms.end())
+    {
+      curr = itt->second;
+      if (terms.find(true) != terms.end())
+      {
+        comp_num = 0;
+      }
+      else
+      {
+        comp_num = -1;
+      }
+    }
+    else
+    {
+      curr = terms[true];
+      comp_num = 1;
+    }
+    Trace("cegqi-inv-debug2") << "  normalize based on " << curr << std::endl;
+    std::vector<Node> vars;
+    std::vector<Node> svars;
+    getNormalizedSubstitution(curr, d_vars, vars, svars, disjuncts);
+    for (unsigned j = 0, dsize = disjuncts.size(); j < dsize; j++)
+    {
+      Trace("cegqi-inv-debug2") << "  apply " << disjuncts[j] << std::endl;
+      disjuncts[j] = Rewriter::rewrite(disjuncts[j].substitute(
+          vars.begin(), vars.end(), svars.begin(), svars.end()));
+      Trace("cegqi-inv-debug2") << "  ..." << disjuncts[j] << std::endl;
+    }
+    std::vector<Node> const_var;
+    std::vector<Node> const_subs;
+    if (comp_num == 0)
+    {
+      // transition
+      Assert(terms.find(true) != terms.end());
+      Node next = terms[true];
+      next = Rewriter::rewrite(next.substitute(
+          vars.begin(), vars.end(), svars.begin(), svars.end()));
+      Trace("cegqi-inv-debug")
+          << "transition next predicate : " << next << std::endl;
+      // make the primed variables if we have not already
+      if (d_prime_vars.empty())
+      {
+        for (unsigned j = 0, nchild = next.getNumChildren(); j < nchild; j++)
+        {
+          Node v = nm->mkSkolem(
+              "ir", next[j].getType(), "template inference rev argument");
+          d_prime_vars.push_back(v);
+        }
+      }
+      // normalize the other direction
+      Trace("cegqi-inv-debug2") << "  normalize based on " << next << std::endl;
+      std::vector<Node> rvars;
+      std::vector<Node> rsvars;
+      getNormalizedSubstitution(next, d_prime_vars, rvars, rsvars, disjuncts);
+      Assert(rvars.size() == rsvars.size());
+      for (unsigned j = 0, dsize = disjuncts.size(); j < dsize; j++)
+      {
+        Trace("cegqi-inv-debug2") << "  apply " << disjuncts[j] << std::endl;
+        disjuncts[j] = Rewriter::rewrite(disjuncts[j].substitute(
+            rvars.begin(), rvars.end(), rsvars.begin(), rsvars.end()));
+        Trace("cegqi-inv-debug2") << "  ..." << disjuncts[j] << std::endl;
+      }
+      getConstantSubstitution(
+          d_prime_vars, disjuncts, const_var, const_subs, false);
+    }
+    else
+    {
+      getConstantSubstitution(d_vars, disjuncts, const_var, const_subs, false);
+    }
+    Node res;
+    if (disjuncts.empty())
+    {
+      res = nm->mkConst(false);
+    }
+    else if (disjuncts.size() == 1)
+    {
+      res = disjuncts[0];
+    }
+    else
+    {
+      res = nm->mkNode(OR, disjuncts);
+    }
+    if (expr::hasBoundVar(res))
+    {
+      Trace("cegqi-inv-debug2") << "...failed, free variable." << std::endl;
+      d_complete = false;
+      continue;
+    }
+    Trace("cegqi-inv") << "*** inferred "
+                       << (comp_num == 1 ? "pre"
+                                         : (comp_num == -1 ? "post" : "trans"))
+                       << "-condition : " << res << std::endl;
+    Component& c =
+        (comp_num == 1 ? d_pre : (comp_num == -1 ? d_post : d_trans));
+    c.d_conjuncts.push_back(res);
+    if (!const_var.empty())
+    {
+      bool has_const_eq = const_var.size() == d_vars.size();
+      Trace("cegqi-inv") << "    with constant substitution, complete = "
+                         << has_const_eq << " : " << std::endl;
+      for (unsigned i = 0, csize = const_var.size(); i < csize; i++)
+      {
+        Trace("cegqi-inv") << "      " << const_var[i] << " -> "
+                           << const_subs[i] << std::endl;
+        if (has_const_eq)
+        {
+          c.d_const_eq[res][const_var[i]] = const_subs[i];
+        }
+      }
+      Trace("cegqi-inv") << "...size = " << const_var.size()
+                         << ", #vars = " << d_vars.size() << std::endl;
+    }
+  }
+
+  // finalize the components
+  for (int i = -1; i <= 1; i++)
+  {
+    Component& c = (i == 1 ? d_pre : (i == -1 ? d_post : d_trans));
+    Node ret;
+    if (c.d_conjuncts.empty())
+    {
+      ret = nm->mkConst(true);
+    }
+    else if (c.d_conjuncts.size() == 1)
+    {
+      ret = c.d_conjuncts[0];
+    }
+    else
+    {
+      ret = nm->mkNode(AND, c.d_conjuncts);
+    }
+    if (i == 0 || i == 1)
+    {
+      // pre-condition and transition are negated
+      ret = TermUtil::simpleNegate(ret);
+    }
+    c.d_this = ret;
+  }
+}
+void TransitionInference::getNormalizedSubstitution(
+    Node curr,
+    const std::vector<Node>& pvars,
+    std::vector<Node>& vars,
+    std::vector<Node>& subs,
+    std::vector<Node>& disjuncts)
+{
+  for (unsigned j = 0, nchild = curr.getNumChildren(); j < nchild; j++)
+  {
+    if (curr[j].getKind() == BOUND_VARIABLE)
+    {
+      // if the argument is a bound variable, add to the renaming
+      vars.push_back(curr[j]);
+      subs.push_back(pvars[j]);
+    }
+    else
+    {
+      // otherwise, treat as a constraint on the variable
+      // For example, this transforms e.g. a precondition clause
+      // I( 0, 1 ) to x1 != 0 OR x2 != 1 OR I( x1, x2 ).
+      Node eq = curr[j].eqNode(pvars[j]);
+      disjuncts.push_back(eq.negate());
+    }
+  }
+}
+
+bool TransitionInference::processDisjunct(
+    Node n,
+    std::map<bool, Node>& terms,
+    std::vector<Node>& disjuncts,
+    std::map<bool, std::map<Node, bool> >& visited,
+    bool topLevel)
+{
+  if (visited[topLevel].find(n) != visited[topLevel].end())
+  {
+    return true;
+  }
+  visited[topLevel][n] = true;
+  bool childTopLevel = n.getKind() == OR && topLevel;
+  // if another part mentions UF or a free variable, then fail
+  bool lit_pol = n.getKind() != NOT;
+  Node lit = n.getKind() == NOT ? n[0] : n;
+  if (lit.getKind() == APPLY_UF)
+  {
+    Node op = lit.getOperator();
+    if (d_func.isNull())
+    {
+      d_func = op;
+      Trace("cegqi-inv-debug") << "Use " << op << " with args ";
+      NodeManager* nm = NodeManager::currentNM();
+      for (const Node& l : lit)
+      {
+        Node v = nm->mkSkolem("i", l.getType(), "template inference argument");
+        d_vars.push_back(v);
+        Trace("cegqi-inv-debug") << v << " ";
+      }
+      Trace("cegqi-inv-debug") << std::endl;
+    }
+    if (op != d_func)
+    {
+      Trace("cegqi-inv-debug")
+          << "...failed, free function : " << n << std::endl;
+      return false;
+    }
+    else if (topLevel)
+    {
+      if (terms.find(lit_pol) == terms.end())
+      {
+        terms[lit_pol] = lit;
+        return true;
+      }
+      else
+      {
+        Trace("cegqi-inv-debug")
+            << "...failed, repeated inv-app : " << lit << std::endl;
+        return false;
+      }
+    }
+    Trace("cegqi-inv-debug")
+        << "...failed, non-entailed inv-app : " << lit << std::endl;
+    return false;
+  }
+  else if (topLevel && !childTopLevel)
+  {
+    disjuncts.push_back(n);
+  }
+  for (const Node& nc : n)
+  {
+    if (!processDisjunct(nc, terms, disjuncts, visited, childTopLevel))
+    {
+      return false;
+    }
+  }
+  return true;
+}
+
+TraceIncStatus TransitionInference::initializeTrace(DetTrace& dt,
+                                                    Node loc,
+                                                    bool fwd)
+{
+  Component& c = fwd ? d_pre : d_post;
+  Assert(c.has(loc));
+  std::map<Node, std::map<Node, Node> >::iterator it = c.d_const_eq.find(loc);
+  if (it != c.d_const_eq.end())
+  {
+    std::vector<Node> next;
+    for (const Node& v : d_vars)
+    {
+      Assert(it->second.find(v) != it->second.end());
+      next.push_back(it->second[v]);
+      dt.d_curr.push_back(it->second[v]);
+    }
+    Trace("cegqi-inv-debug2") << "dtrace : initial increment" << std::endl;
+    bool ret = dt.increment(loc, next);
+    AlwaysAssert(ret);
+    return TRACE_INC_SUCCESS;
+  }
+  return TRACE_INC_INVALID;
+}
+
+TraceIncStatus TransitionInference::incrementTrace(DetTrace& dt,
+                                                   Node loc,
+                                                   bool fwd)
+{
+  Assert(d_trans.has(loc));
+  // check if it satisfies the pre/post condition
+  Node cc = fwd ? getPostCondition() : getPreCondition();
+  Assert(!cc.isNull());
+  Node ccr = Rewriter::rewrite(cc.substitute(
+      d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end()));
+  if (ccr.isConst())
+  {
+    if (ccr.getConst<bool>() == (fwd ? false : true))
+    {
+      Trace("cegqi-inv-debug2") << "dtrace : counterexample" << std::endl;
+      return TRACE_INC_CEX;
+    }
+  }
+
+  // terminates?
+  Node c = getTransitionRelation();
+  Assert(!c.isNull());
+
+  Assert(d_vars.size() == dt.d_curr.size());
+  Node cr = Rewriter::rewrite(c.substitute(
+      d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end()));
+  if (cr.isConst())
+  {
+    if (!cr.getConst<bool>())
+    {
+      Trace("cegqi-inv-debug2") << "dtrace : terminated" << std::endl;
+      return TRACE_INC_TERMINATE;
+    }
+    return TRACE_INC_INVALID;
+  }
+  if (!fwd)
+  {
+    // only implemented in forward direction
+    Assert(false);
+    return TRACE_INC_INVALID;
+  }
+  Component& cm = d_trans;
+  std::map<Node, std::map<Node, Node> >::iterator it = cm.d_const_eq.find(loc);
+  if (it == cm.d_const_eq.end())
+  {
+    return TRACE_INC_INVALID;
+  }
+  std::vector<Node> next;
+  for (const Node& pv : d_prime_vars)
+  {
+    Assert(it->second.find(pv) != it->second.end());
+    Node pvs = it->second[pv];
+    Assert(d_vars.size() == dt.d_curr.size());
+    Node pvsr = Rewriter::rewrite(pvs.substitute(
+        d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end()));
+    next.push_back(pvsr);
+  }
+  if (dt.increment(loc, next))
+  {
+    Trace("cegqi-inv-debug2") << "dtrace : success increment" << std::endl;
+    return TRACE_INC_SUCCESS;
+  }
+  // looped
+  Trace("cegqi-inv-debug2") << "dtrace : looped" << std::endl;
+  return TRACE_INC_TERMINATE;
+}
+
+TraceIncStatus TransitionInference::initializeTrace(DetTrace& dt, bool fwd)
+{
+  Trace("cegqi-inv-debug2") << "Initialize trace" << std::endl;
+  Component& c = fwd ? d_pre : d_post;
+  if (c.d_conjuncts.size() == 1)
+  {
+    return initializeTrace(dt, c.d_conjuncts[0], fwd);
+  }
+  return TRACE_INC_INVALID;
+}
+
+TraceIncStatus TransitionInference::incrementTrace(DetTrace& dt, bool fwd)
+{
+  if (d_trans.d_conjuncts.size() == 1)
+  {
+    return incrementTrace(dt, d_trans.d_conjuncts[0], fwd);
+  }
+  return TRACE_INC_INVALID;
+}
+
+Node TransitionInference::constructFormulaTrace(DetTrace& dt) const
+{
+  return dt.constructFormula(d_vars);
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/sygus/transition_inference.h b/src/theory/quantifiers/sygus/transition_inference.h
new file mode 100644
index 000000000..b4fb220db
--- /dev/null
+++ b/src/theory/quantifiers/sygus/transition_inference.h
@@ -0,0 +1,324 @@
+/*********************                                                        */
+/*! \file transition_inference.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 whether a synthesis conjecture encodes a
+ ** transition system.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H
+#define CVC4__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H
+
+#include <map>
+#include <vector>
+
+#include "expr/node.h"
+
+#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
+#include "theory/quantifiers/inst_match_trie.h"
+#include "theory/quantifiers/single_inv_partition.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/**
+ * Utility for storing a deterministic trace of a transition system. A trace
+ * is stored as a collection of vectors of values that have been taken by
+ * the variables of transition system. For example, say we have a transition
+ * system with variables x,y,z. Say the precondition constrains these variables
+ * to x=1,y=2,z=3, and say that the transition relation admits the single
+ * trace: [1,2,3], [2,3,4], [3,4,5]. We store these three vectors of variables
+ * in the trie within this class.
+ *
+ * This utility is used for determining whether a transition system has a
+ * deterministic terminating trace and hence a trivial invariant.
+ */
+class DetTrace
+{
+ public:
+  /** The current value of the trace */
+  std::vector<Node> d_curr;
+  /**
+   * Increment the trace: index the current values, if successful (they are
+   * not a duplicate of a previous value), update the current values to vals.
+   * Returns true if the increment was successful.
+   */
+  bool increment(Node loc, std::vector<Node>& vals);
+  /**
+   * Construct the formula that this trace represents with respect to variables
+   * in vars. For details, see DetTraceTrie::constructFormula below.
+   */
+  Node constructFormula(const std::vector<Node>& vars);
+  /** Debug print this trace on trace message c */
+  void print(const char* c) const;
+
+ private:
+  /**
+   * A trie of value vectors for the variables of a transition system. Nodes
+   * are stored as data in tries with no children at the leaves of this trie.
+   */
+  class DetTraceTrie
+  {
+   public:
+    /** the children of this trie */
+    std::map<Node, DetTraceTrie> d_children;
+    /** Add data loc to this trie, indexed by val. */
+    bool add(Node loc, const std::vector<Node>& val);
+    /** clear the trie */
+    void clear() { d_children.clear(); }
+    /**
+     * Construct the formula corresponding to this trie with respect to
+     * variables in vars. For example, if we have indexed [1,2,3] and [2,3,4]
+     * and vars is [x,y,z], then this method returns:
+     *   ( x=1 ^ y=2 ^ z=3 ) V ( x=2 ^ y=3 ^ z=4 ).
+     */
+    Node constructFormula(const std::vector<Node>& vars, unsigned index = 0);
+  };
+  /** The above trie data structure for this class */
+  DetTraceTrie d_trie;
+};
+
+/**
+ * Trace increment status, used for incrementTrace below.
+ */
+enum TraceIncStatus
+{
+  // the trace was successfully incremented to a new value
+  TRACE_INC_SUCCESS,
+  // the trace terminated
+  TRACE_INC_TERMINATE,
+  // the trace encountered a bad state (violating the post-condition)
+  TRACE_INC_CEX,
+  // the trace was invalid
+  TRACE_INC_INVALID
+};
+
+/**
+ * This class is used for inferring that an arbitrary synthesis conjecture
+ * corresponds to an invariant synthesis problem for some predicate (d_func).
+ *
+ * The invariant-to-synthesize can either be explicitly given, via a call
+ * to initialize( f, vars ), or otherwise inferred if this method is not called.
+ */
+class TransitionInference
+{
+ public:
+  TransitionInference() : d_complete(false) {}
+  /** Process the conjecture n
+   *
+   * This initializes this class with information related to viewing it as a
+   * transition system. This means we infer a function, the state variables,
+   * the pre/post condition and transition relation.
+   *
+   * The node n should be the inner body of the negated synthesis conjecture,
+   * prior to generating the deep embedding. That is, given:
+   *   forall f. ~forall x. P( f, x ),
+   * this method expects n to be P( f, x ).
+   */
+  void process(Node n);
+  /**
+   * Get the function that is the subject of the synthesis problem we are
+   * analyzing.
+   */
+  Node getFunction() const;
+  /**
+   * Get the variables that the function is applied to. These are the free
+   * variables of the pre/post condition, and transition relation. These are
+   * fresh (Skolem) variables allocated by this class.
+   */
+  void getVariables(std::vector<Node>& vars) const;
+  /**
+   * Get the pre/post condition, or transition relation that was inferred by
+   * this class.
+   */
+  Node getPreCondition() const;
+  Node getPostCondition() const;
+  Node getTransitionRelation() const;
+  /**
+   * Was the analysis of the conjecture complete?
+   *
+   * If this is false, then the system we have inferred does not take into
+   * account all of the synthesis conjecture. This is the case when process(...)
+   * was called on formula that does not have the shape of a transition system.
+   */
+  bool isComplete() const { return d_complete; }
+
+  /**
+   * The following two functions are used for computing whether this transition
+   * relation is deterministic and terminating.
+   *
+   * The argument fwd is whether we are going in the forward direction of the
+   * transition system (starting from the precondition).
+   *
+   * If fwd is true, the initializeTrace method returns TRACE_INC_SUCCESS if the
+   * precondition consists of a single conjunct of the form
+   *   ( x1 = t1 ^ ... ^ xn = tn )
+   * where x1...xn are the state variables of the transition system. Otherwise
+   * it returns TRACE_INC_INVALID.
+   */
+  TraceIncStatus initializeTrace(DetTrace& dt, bool fwd = true);
+  /**
+   * Increment the trace dt in direction fwd.
+   *
+   * If fwd is true, the incrementTrace method returns TRACE_INC_INVALID if the
+   * transition relation is not of the form
+   *   ( x1' = t1[X] ^ ... ^ xn' = tn[X] ^ Q[X] ^ P(x1...xn) ) => P( x1'...xn' )
+   * Otherwise, it returns TRACE_INC_TERMINATE if the values of
+   * x1' = t1[dt.d_curr] ^ ... ^ xn' = tn[dt.d_curr] have already been executed
+   * on trace dt (the trace has looped), or if
+   * x1' = t1[dt.d_curr] ^ ... ^ xn' = tn[dt.d_curr] ^ Q[dt.d_curr] is unsat
+   * (the trace has terminated). It returns TRACE_INC_CEX if the postcondition
+   * is false for the values t1[dt.d_curr] ^ ... ^ tn[dt.d_curr]. Otherwise,
+   * it returns TRACE_INC_SUCCESS.
+   */
+  TraceIncStatus incrementTrace(DetTrace& dt, bool fwd = true);
+  /**
+   * Constructs the formula corresponding to trace dt with respect to the
+   * variables of this class.
+   */
+  Node constructFormulaTrace(DetTrace& dt) const;
+
+ private:
+  /**
+   * The function (predicate) that is the subject of the invariant synthesis
+   * problem we are inferring.
+   */
+  Node d_func;
+  /** The variables that the function is applied to */
+  std::vector<Node> d_vars;
+  /**
+   * The variables that the function is applied to in the next state of the
+   * inferred transition relation.
+   */
+  std::vector<Node> d_prime_vars;
+  /**
+   * Was the analysis of the synthesis conjecture passed to the process method
+   * of this class complete?
+   */
+  bool d_complete;
+
+  /** process disjunct
+   *
+   * The purpose of this function is to infer pre/post/transition conditions
+   * for a (possibly unknown) invariant-to-synthesis, given a conjunct from
+   * an arbitrary synthesis conjecture.
+   *
+   * Assume our negated synthesis conjecture is of the form:
+   *    forall f. exists x. (and (or F11 ... F1{m_1}) ... (or Fn1 ... Fn{m_n}))
+   * This method is called on each (or Fi1 ... Fi{m_i}), where topLevel is true
+   * for each of Fi1...F1{m_i} and false otherwise. It adds each of Fi1..Fi{m_i}
+   * to disjuncts.
+   *
+   * If this method returns true, then (1) all applications of free function
+   * symbols have operator d_func. Note this function may set d_func to a
+   * function symbol in n if d_func was null prior to this call. In other words,
+   * this method may infer the subject of the invariant synthesis problem;
+   * (2) all occurrences of d_func are "top-level", that is, each Fij may be
+   * of the form (not) <d_func>( tj ), but otherwise d_func does not occur in
+   * (or Fi1 ... Fi{m_i}); (3) there exists at most one occurrence of
+   * <d_func>( tj ), and (not <d_func>( tk )).
+   *
+   * If the above conditions are met, then terms[true] is set to <d_func>( tj )
+   * if Fij is <d_func>( tj ) for some j, and likewise terms[false]
+   * is set to <d_func>( tk ) if Fik is (not <d_func>( tk )) for some k.
+   *
+   * The argument visited caches the results of this function for (topLevel, n).
+   */
+  bool processDisjunct(Node n,
+                       std::map<bool, Node>& terms,
+                       std::vector<Node>& disjuncts,
+                       std::map<bool, std::map<Node, bool> >& visited,
+                       bool topLevel);
+  /**
+   * This method infers if the conjunction of disjuncts is equivalent to a
+   * conjunction of the form
+   *   (~) const_var[1] = const_subs[1] ... (~) const_var[n] = const_subs[n]
+   * where the above equalities are negated iff reqPol is false, and
+   *   const_var[1] ... const_var[n]
+   * are distinct members of vars
+   */
+  void getConstantSubstitution(const std::vector<Node>& vars,
+                               const std::vector<Node>& disjuncts,
+                               std::vector<Node>& const_var,
+                               std::vector<Node>& const_subs,
+                               bool reqPol);
+  /** get normalized substitution
+   *
+   * This method takes as input a node curr of the form I( t1, ..., tn ) and
+   * a vector of variables pvars, where pvars.size()=n. For each ti that is
+   * a variable, it adds ti to vars, and pvars[i] to subs. For each ti that is
+   * not a variable, it adds the disequality ti != pvars[i] to disjuncts.
+   *
+   * This function is used for instance to normalize an arbitrary application of
+   * I so that is over arguments pvars. For instance if curr is I(3,5,y) and
+   * pvars = { x1,x2,x3 }, then the formula:
+   *   I(3,5,y) ^ P(y)
+   * is equivalent to:
+   *   x1 != 3 V x2 != 5 V I(x1,x2,x3) V P( y ) { y -> x3 }
+   * Here, we add y and x3 to vars and subs respectively, and x1!=3 and x2!=5
+   * to disjuncts.
+   */
+  void getNormalizedSubstitution(Node curr,
+                                 const std::vector<Node>& pvars,
+                                 std::vector<Node>& vars,
+                                 std::vector<Node>& subs,
+                                 std::vector<Node>& disjuncts);
+  /**
+   * Stores one of the components of the inferred form of the synthesis
+   * conjecture (precondition, postcondition, or transition relation).
+   */
+  class Component
+  {
+   public:
+    Component() {}
+    /** The formula that was inferred for this component */
+    Node d_this;
+    /** The list of conjuncts of the above formula */
+    std::vector<Node> d_conjuncts;
+    /**
+     * Maps formulas to the constant equality substitution that it entails.
+     * For example, the formula (x=4 ^ y=x+5) may map to { x -> 4, y -> 9 }.
+     */
+    std::map<Node, std::map<Node, Node> > d_const_eq;
+    /** Does this component have conjunct c? */
+    bool has(Node c) const
+    {
+      return std::find(d_conjuncts.begin(), d_conjuncts.end(), c)
+             != d_conjuncts.end();
+    }
+  };
+  /** Components for the pre/post condition and transition relation. */
+  Component d_pre;
+  Component d_post;
+  Component d_trans;
+  /**
+   * Initialize trace dt, loc is a node to identify the trace, fwd is whether
+   * we are going in the forward direction of the transition system (starting
+   * from the precondition).
+   *
+   * The argument loc is a conjunct of transition relation that entails that the
+   * trace dt has executed in its last step to its current value. For example,
+   * if the transition relation is ( x'=x+1 ^ P( x ) ) => P(x'), and our trace's
+   * current value was last updated [x:=1] -> [x:=2] based on x'=x+1, then loc
+   * is the node x'=x+1.
+   */
+  TraceIncStatus initializeTrace(DetTrace& dt, Node loc, bool fwd = true);
+  /** Same as above, for incrementing the trace dt */
+  TraceIncStatus incrementTrace(DetTrace& dt, Node loc, bool fwd = true);
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+} /* namespace CVC4 */
+
+#endif