From 09f164674497e70044cc7759b00c6477db90b7be Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 3 May 2018 19:54:28 -0500
Subject: Document datatypes sygus (#1818)

---
 src/theory/datatypes/datatypes_sygus.cpp           | 167 ++++--------
 src/theory/datatypes/datatypes_sygus.h             | 280 ++++++++++++++++++---
 src/theory/datatypes/kinds                         |   6 -
 src/theory/datatypes/theory_datatypes_type_rules.h |  22 --
 4 files changed, 300 insertions(+), 175 deletions(-)

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 4d3584596..6f660642e 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -40,7 +40,6 @@ SygusSymBreakNew::SygusSymBreakNew(TheoryDatatypes* td,
     : d_td(td),
       d_tds(tds),
       d_testers(c),
-      d_is_const(c),
       d_testers_exp(c),
       d_active_terms(c),
       d_currTermSize(c) {
@@ -100,21 +99,15 @@ void SygusSymBreakNew::assertTester( int tindex, TNode n, Node exp, std::vector<
 }
 
 void SygusSymBreakNew::assertFact( Node n, bool polarity, std::vector< Node >& lemmas ) {
-  if( n.getKind()==kind::DT_SYGUS_TERM_ORDER ){
-    if( polarity ){
-      Trace("sygus-sb-torder") << "Sygus term order : " << n[0] << " < " << n[1] << std::endl;
-      Node comm_sb = getTermOrderPredicate( n[0], n[1] );
-      Node comm_lem = NodeManager::currentNM()->mkNode( kind::OR, n.negate(), comm_sb );
-      lemmas.push_back( comm_lem );
-    }
-  }else if( n.getKind()==kind::DT_SYGUS_BOUND ){
+  if (n.getKind() == kind::DT_SYGUS_BOUND)
+  {
     Node m = n[0];
     Trace("sygus-fair") << "Have sygus bound : " << n << ", polarity=" << polarity << " on measure " << m << std::endl;
     registerMeasureTerm( m );
     if( options::sygusFair()==SYGUS_FAIR_DT_SIZE ){
       std::map< Node, SearchSizeInfo * >::iterator its = d_szinfo.find( m );
       Assert( its!=d_szinfo.end() );
-      Node mt = its->second->getOrMkSygusMeasureTerm( lemmas );
+      Node mt = its->second->getOrMkMeasureValue(lemmas);
       //it relates the measure term to arithmetic
       Node blem = n.eqNode( NodeManager::currentNM()->mkNode( kind::LEQ, mt, n[1] ) );
       lemmas.push_back( blem );
@@ -123,57 +116,12 @@ void SygusSymBreakNew::assertFact( Node n, bool polarity, std::vector< Node >& l
       unsigned s = n[1].getConst<Rational>().getNumerator().toUnsignedInt();
       notifySearchSize( m, s, n, lemmas );
     }
-  }else if( n.getKind() == kind::DT_SYGUS_IS_CONST ){
-    assertIsConst( n[0], polarity, lemmas );
   }else if( n.getKind() == kind::DT_HEIGHT_BOUND || n.getKind()==DT_SIZE_BOUND ){
     //reduce to arithmetic TODO ?
 
   }
 }
 
-void SygusSymBreakNew::assertIsConst( Node n, bool polarity, std::vector< Node >& lemmas ) {
-  if( d_active_terms.find( n )!=d_active_terms.end() ) {
-    // what kind of constructor is n?
-    IntMap::const_iterator itt = d_testers.find( n );
-    Assert( itt!=d_testers.end() );
-    int tindex = (*itt).second;
-    TypeNode tn = n.getType();
-    const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype();
-    Node lem;
-    if( dt[tindex].getNumArgs()==0 ){
-      // is this a constant?
-      Node sygus_op = Node::fromExpr( dt[tindex].getSygusOp() );
-      if( sygus_op.isConst()!=polarity ){
-        lem = NodeManager::currentNM()->mkNode( kind::DT_SYGUS_IS_CONST, n );
-        if( polarity ){
-          lem.negate();
-        }
-      }
-    }else{
-      // reduce
-      std::vector< Node > child_conj;
-      for( unsigned j=0; j<dt[tindex].getNumArgs(); j++ ){
-        Node sel = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[tindex].getSelectorInternal( tn.toType(), j ) ), n );
-        child_conj.push_back( NodeManager::currentNM()->mkNode( kind::DT_SYGUS_IS_CONST, sel ) );
-      }
-      lem = child_conj.size()==1 ? child_conj[0] : NodeManager::currentNM()->mkNode( kind::AND, child_conj );
-      // only an implication (TODO : strengthen?)
-      lem = NodeManager::currentNM()->mkNode( kind::OR, lem.negate(), NodeManager::currentNM()->mkNode( kind::DT_SYGUS_IS_CONST, n ) );
-    }
-    if( !lem.isNull() ){
-      Trace("sygus-isc") << "Sygus is-const lemma : " << lem << std::endl;
-      Node rlv = getRelevancyCondition( n );
-      if( !rlv.isNull() ){
-        lem = NodeManager::currentNM()->mkNode( kind::OR, rlv.negate(), lem );
-      }
-      lemmas.push_back( lem );
-    }
-  }else{
-    // lazy
-    d_is_const[n] = polarity ? 1 : -1;
-  }
-}
-
 Node SygusSymBreakNew::getTermOrderPredicate( Node n1, Node n2 ) {
   NodeManager* nm = NodeManager::currentNM();
   std::vector< Node > comm_disj;
@@ -269,13 +217,6 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std:
   d_active_terms.insert( n );
   Trace("sygus-sb-debug2") << "Sygus : activate term : " << n << " : " << exp << std::endl;  
   
-  /* TODO
-  IntMap::const_iterator itisc = d_is_const.find( n );
-  if( itisc != d_is_const.end() ){
-    assertIsConst( n, (*itisc).second==1, lemmas );
-  }
-  */
-  
   TypeNode ntn = n.getType();
   const Datatype& dt = ((DatatypeType)ntn.toType()).getDatatype();
   
@@ -502,21 +443,8 @@ Node SygusSymBreakNew::getSimpleSymBreakPred( TypeNode tn, int tindex, unsigned
             if( quantifiers::TermUtil::isComm( nk ) ){
               if( children.size()==2 ){
                 if( children[0].getType()==children[1].getType() ){
-  #if 0
-                  Node order_pred = NodeManager::currentNM()->mkNode( DT_SYGUS_TERM_ORDER, children[0], children[1] );
-                  sbp_conj.push_back( order_pred );
-                  Node child11 = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[tindex].getSelectorInternal( tn.toType(), 1 ) ), children[0] );
-                  Assert( child11.getType()==children[1].getType() );
-                  //chainable
-                  if( children[0].getType()==tn ){
-                    Node order_pred_trans = NodeManager::currentNM()->mkNode( OR, DatatypesRewriter::mkTester( children[0], tindex, dt ).negate(),
-                                                                              NodeManager::currentNM()->mkNode( DT_SYGUS_TERM_ORDER, child11, children[1] ) );
-                    sbp_conj.push_back( order_pred_trans );
-                  }
-  #else   
                   Node order_pred = getTermOrderPredicate( children[0], children[1] );
                   sbp_conj.push_back( order_pred );
-  #endif
                 }
               }
             }
@@ -672,23 +600,6 @@ TNode SygusSymBreakNew::getFreeVar( TypeNode tn ) {
   return d_tds->getFreeVar(tn, 0);
 }
 
-unsigned SygusSymBreakNew::processSelectorChain( Node n, std::map< TypeNode, Node >& top_level, std::map< Node, unsigned >& tdepth, std::vector< Node >& lemmas ) {
-  unsigned ret = 0;
-  if( n.getKind()==APPLY_SELECTOR_TOTAL ){
-    ret = processSelectorChain( n[0], top_level, tdepth, lemmas );
-  }
-  TypeNode tn = n.getType();
-  if( top_level.find( tn )==top_level.end() ){
-    top_level[tn] = n;
-    //tdepth[n] = ret;
-    registerSearchTerm( tn, ret, n, true, lemmas );
-  }else{
-    registerSearchTerm( tn, ret, n, false, lemmas );
-  }
-  tdepth[n] = ret;
-  return ret+1;
-}
-
 void SygusSymBreakNew::registerSearchTerm( TypeNode tn, unsigned d, Node n, bool topLevel, std::vector< Node >& lemmas ) {
   //register this term
   std::unordered_map<Node, Node, NodeHashFunction>::iterator ita =
@@ -1001,21 +912,17 @@ void SygusSymBreakNew::registerSizeTerm( Node e, std::vector< Node >& lemmas ) {
           if( options::sygusFair()==SYGUS_FAIR_DT_SIZE ){
             // update constraints on the measure term
             if( options::sygusFairMax() ){
-              if( options::sygusFair()==SYGUS_FAIR_DT_SIZE ){
-                Node ds = NodeManager::currentNM()->mkNode( kind::DT_SIZE, e );
-                Node slem = NodeManager::currentNM()->mkNode( kind::LEQ, ds, d_szinfo[m]->getOrMkSygusMeasureTerm( lemmas ) );
-                lemmas.push_back( slem );
-              }
+              Node ds = NodeManager::currentNM()->mkNode(kind::DT_SIZE, e);
+              Node slem = NodeManager::currentNM()->mkNode(
+                  kind::LEQ, ds, d_szinfo[m]->getOrMkMeasureValue(lemmas));
+              lemmas.push_back(slem);
             }else{
-              Node mt = d_szinfo[m]->getOrMkSygusActiveMeasureTerm( lemmas );
-              Node new_mt = NodeManager::currentNM()->mkSkolem( "mt", NodeManager::currentNM()->integerType() );
-              lemmas.push_back( NodeManager::currentNM()->mkNode( kind::GEQ, new_mt, d_zero ) );
-              if( options::sygusFair()==SYGUS_FAIR_DT_SIZE ){
-                Node ds = NodeManager::currentNM()->mkNode( kind::DT_SIZE, e );
-                lemmas.push_back( mt.eqNode( NodeManager::currentNM()->mkNode( kind::PLUS, new_mt, ds ) ) );
-                //lemmas.push_back( NodeManager::currentNM()->mkNode( kind::GEQ, ds, d_zero ) );
-              }
-              d_szinfo[m]->d_sygus_measure_term_active = new_mt;
+              Node mt = d_szinfo[m]->getOrMkActiveMeasureValue(lemmas);
+              Node new_mt =
+                  d_szinfo[m]->getOrMkActiveMeasureValue(lemmas, true);
+              Node ds = NodeManager::currentNM()->mkNode(kind::DT_SIZE, e);
+              lemmas.push_back(mt.eqNode(
+                  NodeManager::currentNM()->mkNode(kind::PLUS, new_mt, ds)));
             }
           }
         }else{
@@ -1166,7 +1073,8 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) {
         Trace("dt-sygus") << ss.str() << std::endl;
       }
       // TODO : remove this step (ensure there is no way a sygus term cannot be assigned a tester before this point)
-      if( !debugTesters( prog, progv, 0, lemmas ) ){
+      if (!checkTesters(prog, progv, 0, lemmas))
+      {
         Trace("sygus-sb") << "  SygusSymBreakNew::check: ...WARNING: considered missing split for " << prog << "." << std::endl;
         // this should not happen generally, it is caused by a sygus term not being assigned a tester
         //Assert( false );
@@ -1221,7 +1129,11 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) {
   }
 }
 
-bool SygusSymBreakNew::debugTesters( Node n, Node vn, int ind, std::vector< Node >& lemmas ) {
+bool SygusSymBreakNew::checkTesters(Node n,
+                                    Node vn,
+                                    int ind,
+                                    std::vector<Node>& lemmas)
+{
   Assert( vn.getKind()==kind::APPLY_CONSTRUCTOR );
   if( Trace.isOn("sygus-sb-warn") ){
     Node prog_sz = NodeManager::currentNM()->mkNode( kind::DT_SIZE, n );
@@ -1249,7 +1161,8 @@ bool SygusSymBreakNew::debugTesters( Node n, Node vn, int ind, std::vector< Node
   }
   for( unsigned i=0; i<vn.getNumChildren(); i++ ){
     Node sel = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex].getSelectorInternal( tn.toType(), i ) ), n );
-    if( !debugTesters( sel, vn[i], ind+1, lemmas ) ){
+    if (!checkTesters(sel, vn[i], ind + 1, lemmas))
+    {
       return false;
     }
   }
@@ -1278,19 +1191,37 @@ Node SygusSymBreakNew::getCurrentTemplate( Node n, std::map< TypeNode, int >& va
   }
 }
 
-Node SygusSymBreakNew::SearchSizeInfo::getOrMkSygusMeasureTerm( std::vector< Node >& lemmas ) {
-  if( d_sygus_measure_term.isNull() ){
-    d_sygus_measure_term = NodeManager::currentNM()->mkSkolem( "mt", NodeManager::currentNM()->integerType() );
-    lemmas.push_back( NodeManager::currentNM()->mkNode( kind::GEQ, d_sygus_measure_term, NodeManager::currentNM()->mkConst( Rational(0) ) ) );
+Node SygusSymBreakNew::SearchSizeInfo::getOrMkMeasureValue(
+    std::vector<Node>& lemmas)
+{
+  if (d_measure_value.isNull())
+  {
+    d_measure_value = NodeManager::currentNM()->mkSkolem(
+        "mt", NodeManager::currentNM()->integerType());
+    lemmas.push_back(NodeManager::currentNM()->mkNode(
+        kind::GEQ,
+        d_measure_value,
+        NodeManager::currentNM()->mkConst(Rational(0))));
   }
-  return d_sygus_measure_term;
+  return d_measure_value;
 }
 
-Node SygusSymBreakNew::SearchSizeInfo::getOrMkSygusActiveMeasureTerm( std::vector< Node >& lemmas ) {
-  if( d_sygus_measure_term_active.isNull() ){
-    d_sygus_measure_term_active = getOrMkSygusMeasureTerm( lemmas );
+Node SygusSymBreakNew::SearchSizeInfo::getOrMkActiveMeasureValue(
+    std::vector<Node>& lemmas, bool mkNew)
+{
+  if (mkNew)
+  {
+    Node new_mt = NodeManager::currentNM()->mkSkolem(
+        "mt", NodeManager::currentNM()->integerType());
+    lemmas.push_back(NodeManager::currentNM()->mkNode(
+        kind::GEQ, new_mt, NodeManager::currentNM()->mkConst(Rational(0))));
+    d_measure_value_active = new_mt;
+  }
+  else if (d_measure_value_active.isNull())
+  {
+    d_measure_value_active = getOrMkMeasureValue(lemmas);
   }
-  return d_sygus_measure_term_active;
+  return d_measure_value_active;
 }
 
 Node SygusSymBreakNew::SearchSizeInfo::getFairnessLiteral( unsigned s, TheoryDatatypes * d, std::vector< Node >& lemmas ) {
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index 2936c1561..e0b29efd2 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -40,6 +40,17 @@ namespace datatypes {
 
 class TheoryDatatypes;
 
+/**
+ * This is the sygus extension of the decision procedure for quantifier-free
+ * inductive datatypes. At a high level, this class takes as input a
+ * set of asserted testers is-C1( x ), is-C2( x.1 ), is-C3( x.2 ), and
+ * generates lemmas that restrict the models of x, if x is a "sygus enumerator"
+ * (see TermDbSygus::registerEnumerator).
+ *
+ * Some of these techniques are described in these papers:
+ * "Refutation-Based Synthesis in SMT", Reynolds et al 2017.
+ * "Sygus Techniques in the Core of an SMT Solver", Reynolds et al 2017.
+ */
 class SygusSymBreakNew
 {
   typedef context::CDHashMap< Node, int, NodeHashFunction > IntMap;
@@ -52,11 +63,53 @@ class SygusSymBreakNew
                    quantifiers::TermDbSygus* tds,
                    context::Context* c);
   ~SygusSymBreakNew();
-  /** add tester */
+  /**
+   * Notify this class that tester for constructor tindex has been asserted for
+   * n. Exp is the literal corresponding to this tester. This method may add
+   * lemmas to the vector lemmas, for details see assertTesterInternal below.
+   * These lemmas are sent out on the output channel of datatypes by the caller.
+   */
   void assertTester(int tindex, TNode n, Node exp, std::vector<Node>& lemmas);
+  /**
+   * Notify this class that literal n has been asserted with the given
+   * polarity. This method may add lemmas to the vector lemmas, for instance
+   * based on inferring consequences of (not) n. One example is if n is
+   * (DT_SIZE_BOUND x n), we add the lemma:
+   *   (DT_SIZE_BOUND x n) <=> ((DT_SIZE x) <= n )
+   */
   void assertFact(Node n, bool polarity, std::vector<Node>& lemmas);
+  /** pre-register term n
+   *
+   * This is called when n is pre-registered with the theory of datatypes.
+   * If n is a sygus enumerator, then we may add lemmas to the vector lemmas
+   * that are used to enforce fairness regarding the size of n.
+   */
   void preRegisterTerm(TNode n, std::vector<Node>& lemmas);
+  /** check
+   *
+   * This is called at last call effort, when the current model assignment is
+   * satisfiable according to the quantifier-free decision procedures and a
+   * model is built. This method may add lemmas to the vector lemmas based
+   * on dynamic symmetry breaking techniques, based on the model values of
+   * all preregistered enumerators.
+   */
   void check(std::vector<Node>& lemmas);
+  /** get next decision request
+   *
+   * This function has the same interface as Theory::getNextDecisionRequest.
+   *
+   * The decisions returned by this method are of one of two forms:
+   * (1) Positive decisions on the active guards G of enumerators e registered
+   * to this class. These assert "there are more values to enumerate for e".
+   * (2) Positive bounds (DT_SYGUS_BOUND m n) for "measure terms" m (see below),
+   * where n is a non-negative integer. This asserts "the measure of terms
+   * we are enumerating for enumerators whose measure term m is at most n",
+   * where measure is commonly term size, but can also be height.
+   *
+   * We prioritize decisions of form (1) before (2). For both decisions,
+   * we set the priority argument to "1", indicating that the decision is
+   * critical for solution completeness.
+   */
   Node getNextDecisionRequest(unsigned& priority, std::vector<Node>& lemmas);
 
  private:
@@ -64,11 +117,33 @@ class SygusSymBreakNew
   TheoryDatatypes* d_td;
   /** Pointer to the sygus term database */
   quantifiers::TermDbSygus* d_tds;
+  /**
+   * Map from terms to the index of the tester that is asserted for them in
+   * the current SAT context. In other words, if d_testers[n] = 2, then the
+   * tester is-C_2(n) is asserted in this SAT context.
+   */
   IntMap d_testers;
-  IntMap d_is_const;
+  /**
+   * Map from terms to the tester asserted for them. In the example above,
+   * d_testers[n] = is-C_2(n).
+   */
   NodeMap d_testers_exp;
+  /**
+   * The set of (selector chain) terms that are active in the current SAT
+   * context. A selector chain term S_n( ... S_1( x )... ) is active if either:
+   * (1) n=0 and x is a sygus enumerator,
+   *   or:
+   * (2.1) S_{n-1}( ... S_1( x )) is active,
+   * (2.2) is-C( S_{n-1}( ... S_1( x )) ) is asserted in this SAT context, and
+   * (2.3) S_n is a selector for constructor C.
+   */
   NodeSet d_active_terms;
+  /**
+   * Map from enumerators to a lower bound on their size in the current SAT
+   * context.
+   */
   IntMap d_currTermSize;
+  /** zero */
   Node d_zero;
   /**
    * Map from terms (selector chains) to their anchors. The anchor of a
@@ -96,7 +171,6 @@ class SygusSymBreakNew
    *   S4 : T1 -> T3
    * Then, x, S1( x ), and S4( S3( S2( S1( x ) ) ) ) are top-level terms,
    * whereas S2( S1( x ) ) and S3( S2( S1( x ) ) ) are not.
-   *
    */
   std::unordered_map<Node, bool, NodeHashFunction> d_is_top_level;
   /**
@@ -330,59 +404,207 @@ private:
 
   /** Get the canonical free variable for type tn */
   TNode getFreeVar( TypeNode tn );
+  /** get term order predicate
+   *
+   * Assuming that n1 and n2 are children of a commutative operator, this
+   * returns a symmetry breaking predicate that can be instantiated for n1 and
+   * n2 while preserving satisfiability. By default, this is the predicate
+   *   ( DT_SIZE n1 ) >= ( DT_SIZE n2 )
+   */
   Node getTermOrderPredicate( Node n1, Node n2 );
-private:
- /**
-  * Map from registered variables to whether they are a sygus enumerator.
-  *
-  * This should be user context-dependent if sygus is updated to work in
-  * incremental mode.
-  */
- std::map<Node, bool> d_register_st;
- void registerSizeTerm(Node e, std::vector<Node>& lemmas);
- class SearchSizeInfo
- {
-  public:
+
+ private:
+  /**
+   * Map from registered variables to whether they are a sygus enumerator.
+   *
+   * This should be user context-dependent if sygus is updated to work in
+   * incremental mode.
+   */
+  std::map<Node, bool> d_register_st;
+  //----------------------search size information
+  /**
+   * Checks whether e is a sygus enumerator, that is, a term for which this
+   * class will track size for.
+   *
+   * We associate each sygus enumerator e with a "measure term", which is used
+   * for bounding the size of terms for the models of e. The measure term for a
+   * sygus enumerator may be e itself (if e has an active guard), or an
+   * arbitrary sygus variable otherwise. A measure term m is one for which our
+   * decision strategy decides on literals of the form (DT_SYGUS_BOUND m n).
+   *
+   * After determining the measure term m for e, if applicable, we initialize
+   * SearchSizeInfo for m below. This may result in lemmas
+   */
+  void registerSizeTerm(Node e, std::vector<Node>& lemmas);
+  /** information for each measure term allocated by this class */
+  class SearchSizeInfo
+  {
+   public:
     SearchSizeInfo( Node t, context::Context* c ) : d_this( t ), d_curr_search_size(0), d_curr_lit( c, 0 ) {}
+    /** the measure term */
     Node d_this;
+    /**
+     * For each size n, an explanation for why this measure term has size at
+     * most n. This is typically the literal (DT_SYGUS_BOUND m n), which
+     * we call the (n^th) "fairness literal" for m.
+     */
     std::map< unsigned, Node > d_search_size_exp;
+    /**
+     * For each size, whether we have called SygusSymBreakNew::notifySearchSize.
+     */
     std::map< unsigned, bool > d_search_size;
+    /**
+     * The current search size. This corresponds to the number of times
+     * incrementCurrentSearchSize has been called for this measure term.
+     */
     unsigned d_curr_search_size;
-    Node d_sygus_measure_term;
-    Node d_sygus_measure_term_active;
+    /** the list of all enumerators whose measure term is this */
     std::vector< Node > d_anchors;
-    Node getOrMkSygusMeasureTerm( std::vector< Node >& lemmas );
-    Node getOrMkSygusActiveMeasureTerm( std::vector< Node >& lemmas );
-  public:
-    /** current cardinality */
+    /** get or make the measure value
+     *
+     * The measure value is an integer variable v that is a (symbolic) integer
+     * value that is constrained to be less than or equal to the current search
+     * size. For example, if we are using the fairness strategy
+     * SYGUS_FAIR_DT_SIZE (see options/datatype_options.h), then we constrain:
+     *   (DT_SYGUS_BOUND m n) <=> (v <= n)
+     * for all asserted fairness literals. Then, if we are enforcing fairness
+     * based on the maximum size, we assert:
+     *   (DT_SIZE e) <= v
+     * for all enumerators e.
+     */
+    Node getOrMkMeasureValue(std::vector<Node>& lemmas);
+    /** get or make the active measure value
+     *
+     * The active measure value av is an integer variable that corresponds to
+     * the (symbolic) value of the sum of enumerators that are yet to be
+     * registered. This is to enforce the "sum of measures" strategy. For
+     * example, if we are using the fairness strategy SYGUS_FAIR_DT_SIZE,
+     * then initially av is equal to the measure value v, and the constraints
+     *   (DT_SYGUS_BOUND m n) <=> (v <= n)
+     * are added as before. When an enumerator e is registered, we add the
+     * lemma:
+     *   av = (DT_SIZE e) + av'
+     * and update the active measure value to av'. This ensures that the sum
+     * of sizes of active enumerators is at most n.
+     *
+     * If the flag mkNew is set to true, then we return a fresh variable and
+     * update the active measure value.
+     */
+    Node getOrMkActiveMeasureValue(std::vector<Node>& lemmas,
+                                   bool mkNew = false);
+    /**
+     * The current search size literal for this measure term. This corresponds
+     * to the minimial n such that (DT_SYGUS_BOUND d_this n) is asserted in
+     * this SAT context.
+     */
     context::CDO< unsigned > d_curr_lit;
+    /**
+     * Map from integers n to the fairness literal, for each n such that this
+     * literal has been allocated (by getFairnessLiteral below).
+     */
     std::map< unsigned, Node > d_lits;
+    /**
+     * Returns the s^th fairness literal for this measure term. This adds a
+     * split on this literal to lemmas.
+     */
     Node getFairnessLiteral( unsigned s, TheoryDatatypes * d, std::vector< Node >& lemmas );
+    /** get the current fairness literal */
     Node getCurrentFairnessLiteral( TheoryDatatypes * d, std::vector< Node >& lemmas ) { 
       return getFairnessLiteral( d_curr_lit.get(), d, lemmas ); 
     }
     /** increment current term size */
     void incrementCurrentLiteral() { d_curr_lit.set( d_curr_lit.get() + 1 ); }
+
+   private:
+    /** the measure value */
+    Node d_measure_value;
+    /** the sygus measure value */
+    Node d_measure_value_active;
   };
+  /** the above information for each registered measure term */
   std::map< Node, SearchSizeInfo * > d_szinfo;
+  /** map from enumerators (anchors) to their associated measure term */
   std::map< Node, Node > d_anchor_to_measure_term;
+  /** map from enumerators (anchors) to their active guard*/
   std::map< Node, Node > d_anchor_to_active_guard;
+  /** generic measure term
+   *
+   * This is a global term that is used as the measure term for all sygus
+   * enumerators that do not have active guards. This class enforces that
+   * all enumerators have size at most n, where n is the minimal integer
+   * such that (DT_SYGUS_BOUND d_generic_measure_term n) is asserted.
+   */
   Node d_generic_measure_term;
+  /**
+   * This increments the current search size for measure term m. This may
+   * cause lemmas to be added to lemmas based on the fact that symmetry
+   * breaking lemmas are now relevant for new search terms, see discussion
+   * of how search size affects which lemmas are relevant above
+   * addSymBreakLemmasFor.
+   */
   void incrementCurrentSearchSize( Node m, std::vector< Node >& lemmas );
+  /**
+   * Notify this class that we are currently searching for terms of size at
+   * most s as model values for measure term m. Literal exp corresponds to the
+   * explanation of why the measure term has size at most n. This calls
+   * incrementSearchSize above, until the total number of times we have called
+   * incrementSearchSize so far is at least s.
+   */
   void notifySearchSize( Node m, unsigned s, Node exp, std::vector< Node >& lemmas );
+  /** Allocates a SearchSizeInfo object in d_szinfo. */
   void registerMeasureTerm( Node m );
+  /**
+   * Return the current search size for arbitrary term n. This is the current
+   * search size of the anchor of n.
+   */
   unsigned getSearchSizeFor( Node n );
-  unsigned getSearchSizeForAnchor( Node n );
+  /** return the current search size for enumerator (anchor) e */
+  unsigned getSearchSizeForAnchor(Node e);
+  /** Get the current search size for measure term m in this SAT context. */
   unsigned getSearchSizeForMeasureTerm(Node m);
-
- private:
-  unsigned processSelectorChain( Node n, std::map< TypeNode, Node >& top_level, 
-                                 std::map< Node, unsigned >& tdepth, std::vector< Node >& lemmas );
-  bool debugTesters( Node n, Node vn, int ind, std::vector< Node >& lemmas );
+  /** get current template
+   *
+   * For debugging. This returns a term that corresponds to the current
+   * inferred shape of n. For example, if the testers
+   *   is-C1( n ) and is-C2( n.1 )
+   * have been asserted where C1 and C2 are binary constructors, then this
+   * method may return a term of the form:
+   *   C1( C2( x1, x2 ), x3 )
+   * for fresh variables x1, x2, x3. The map var_count maintains the variable
+   * count for generating these fresh variables.
+   */
   Node getCurrentTemplate( Node n, std::map< TypeNode, int >& var_count );
+  //----------------------end search size information
+  /** check testers
+   *
+   * This is called when we have a model assignment vn for n, where n is
+   * a selector chain applied to an enumerator (a search term). This function
+   * ensures that testers have been asserted for each subterm of vn. This is
+   * critical for ensuring that the proper steps have been taken by this class
+   * regarding whether or not vn is a legal value for n (not greater than the
+   * current search size and not a value that can be blocked by symmetry
+   * breaking).
+   *
+   * For example, if vn = +( x(), x() ), then we ensure that the testers
+   *   is-+( n ), is-x( n.1 ), is-x( n.2 )
+   * have been asserted to this class. If a tester is not asserted for some
+   * relevant selector chain S( n ) of n, then we add a lemma L for that
+   * selector chain to lemmas, where L is the "splitting lemma" for S( n ), that
+   * states that the top symbol of S( n ) must be one of the constructors of
+   * its type.
+   *
+   * Notice that this function is a sanity check. Typically, it should be the
+   * case that testers are asserted for all subterms of vn, and hence this
+   * method should not ever add anything to lemmas. However, due to its
+   * importance, we check this regardless.
+   */
+  bool checkTesters(Node n, Node vn, int ind, std::vector<Node>& lemmas);
+  /**
+   * Get the current SAT status of the guard g.
+   * In particular, this returns 1 if g is asserted true, -1 if it is asserted
+   * false, and 0 if it is not asserted.
+   */
   int getGuardStatus( Node g );
-private:
-  void assertIsConst( Node n, bool polarity, std::vector< Node >& lemmas );
 };
 
 }
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 3ce416b40..65f258de1 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -114,10 +114,4 @@ typerule DT_SIZE_BOUND ::CVC4::theory::datatypes::DtBoundTypeRule
 operator DT_SYGUS_BOUND 2 "datatypes sygus bound"
 typerule DT_SYGUS_BOUND ::CVC4::theory::datatypes::DtSygusBoundTypeRule
 
-operator DT_SYGUS_TERM_ORDER 2 "datatypes sygus term order"
-typerule DT_SYGUS_TERM_ORDER ::CVC4::theory::datatypes::DtSygusPredTypeRule
-
-operator DT_SYGUS_IS_CONST 1 "datatypes sygus is constant"
-typerule DT_SYGUS_IS_CONST ::CVC4::theory::datatypes::DtSygusPredTypeRule
-
 endtheory
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index d6045404d..6ba64d8dd 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -359,28 +359,6 @@ class DtSygusBoundTypeRule {
   }
 }; /* class DtSygusBoundTypeRule */
 
-
-class DtSygusPredTypeRule {
- public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check) {
-    if (check) {
-      TypeNode tn = n[0].getType();
-      if (!tn.isDatatype() || !((DatatypeType)tn.toType()).getDatatype().isSygus()) {
-        throw TypeCheckingExceptionPrivate(
-            n, "datatype sygus predicate expecting terms of sygus type");
-      }
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        if (tn!=n[i].getType()) {
-          throw TypeCheckingExceptionPrivate(
-              n, "datatype sygus predicate expecting two terms of the same type");
-        }
-      }
-    }
-    return nodeManager->booleanType();
-  }
-}; /* class DtSygusPredTypeRule */
-
 } /* CVC4::theory::datatypes namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
-- 
cgit v1.2.3


From 3fe18c9d3b15e1c4a7bf23d54bf92e2ae27c6a80 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 3 May 2018 21:11:18 -0500
Subject: Initialize cegis unif strategy (#1861)

---
 src/theory/quantifiers/sygus/cegis_unif.cpp       |  20 +-
 src/theory/quantifiers/sygus/sygus_unif.cpp       |   2 +-
 src/theory/quantifiers/sygus/sygus_unif_io.cpp    |   2 +
 src/theory/quantifiers/sygus/sygus_unif_rl.cpp    | 150 ++++++++++--
 src/theory/quantifiers/sygus/sygus_unif_rl.h      |  46 +++-
 src/theory/quantifiers/sygus/sygus_unif_strat.cpp | 271 +++++++++++++---------
 src/theory/quantifiers/sygus/sygus_unif_strat.h   |  70 ++++--
 7 files changed, 407 insertions(+), 154 deletions(-)

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index ee8fb6f12..cc477fa62 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -14,7 +14,9 @@
 
 #include "theory/quantifiers/sygus/cegis_unif.h"
 
+#include "options/base_options.h"
 #include "options/quantifiers_options.h"
+#include "printer/printer.h"
 #include "theory/quantifiers/sygus/ce_guided_conjecture.h"
 #include "theory/quantifiers/sygus/sygus_unif_rl.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
@@ -55,6 +57,12 @@ bool CegisUnif::initialize(Node n,
       unif_candidates.push_back(c);
     }
   }
+  for (const Node& e : d_cond_enums)
+  {
+    Node g = d_tds->getActiveGuardForEnumerator(e);
+    Assert(!g.isNull());
+    d_enum_to_active_guard[e] = g;
+  }
   // initialize the enumeration manager
   d_u_enum_manager.initialize(unif_candidates);
   return true;
@@ -73,6 +81,8 @@ void CegisUnif::getTermList(const std::vector<Node>& candidates,
     Valuation& valuation = d_qe->getValuation();
     for (const Node& e : d_cond_enums)
     {
+      Trace("cegis-unif-debug")
+          << "Check conditional enumerator : " << e << std::endl;
       Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end());
       Node g = d_enum_to_active_guard[e];
       /* Get whether the active guard for this enumerator is set. If so, then
@@ -109,8 +119,14 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
     {
       continue;
     }
-    Trace("cegis-unif-enum") << "  " << enums[i] << " -> " << enum_values[i]
-                             << std::endl;
+    if (Trace.isOn("cegis-unif-enum"))
+    {
+      Trace("cegis-unif-enum") << "  " << enums[i] << " -> ";
+      std::stringstream ss;
+      Printer::getPrinter(options::outputLanguage())
+          ->toStreamSygus(ss, enum_values[i]);
+      Trace("cegis-unif-enum") << ss.str() << std::endl;
+    }
     unsigned sz = d_tds->getSygusTermSize(enum_values[i]);
     if (i == 0 || sz < min_term_size)
     {
diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp
index dc927388e..23b04aa4d 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif.cpp
@@ -41,7 +41,7 @@ void SygusUnif::initialize(QuantifiersEngine* qe,
   {
     d_candidates.push_back(f);
     // initialize the strategy
-    d_strategy[f].initialize(qe, f, enums, lemmas);
+    d_strategy[f].initialize(qe, f, enums);
   }
 }
 
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index eb607d2c3..8f2038d31 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -477,6 +477,8 @@ void SygusUnifIo::initialize(QuantifiersEngine* qe,
   d_ecache.clear();
   d_candidate = funs[0];
   SygusUnif::initialize(qe, funs, enums, lemmas);
+  // learn redundant operators based on the strategy
+  d_strategy[d_candidate].staticLearnRedundantOps(lemmas);
 }
 
 void SygusUnifIo::addExample(const std::vector<Node>& input, Node output)
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 3b7cef4b9..2cf751927 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -31,11 +31,17 @@ void SygusUnifRl::initialize(QuantifiersEngine* qe,
                              std::vector<Node>& lemmas)
 {
   d_ecache.clear();
-  d_cand_to_cond_enum.clear();
   d_cand_to_pt_enum.clear();
-  /* TODO populate d_unif_candidates and remove lemmas cleaning */
-  SygusUnif::initialize(qe, funs, enums, lemmas);
-  lemmas.clear();
+  // initialize
+  std::vector<Node> all_enums;
+  SygusUnif::initialize(qe, funs, all_enums, lemmas);
+  // based on the strategy inferred for each function, determine if we are
+  // using a unification strategy that is compatible our approach.
+  for (const Node& f : funs)
+  {
+    registerStrategy(f);
+  }
+  enums.insert(enums.end(), d_cond_enums.begin(), d_cond_enums.end());
   /* Copy candidates and check whether CegisUnif for any of them */
   for (const Node& c : d_unif_candidates)
   {
@@ -73,23 +79,28 @@ Node SygusUnifRl::purifyLemma(Node n,
   /* Recurse */
   unsigned size = n.getNumChildren();
   Kind k = n.getKind();
-  /* Whether application of a function-to-synthesize */
-  bool fapp = k == APPLY_UF && size > 0;
-  Assert(std::find(d_candidates.begin(), d_candidates.end(), n[0])
-         == d_candidates.end());
-  /* Whether application of a (non-)unification function-to-synthesize */
-  bool u_fapp = fapp && usingUnif(n[0]);
-  bool nu_fapp = fapp && !usingUnif(n[0]);
   /* We retrive model value now because purified node may not have a value */
   Node nv = n;
-  /* get model value of non-top level applications of functions-to-synthesize
-     occurring under a unification function-to-synthesize */
-  if (ensureConst && fapp)
+  /* Whether application of a function-to-synthesize */
+  bool fapp = k == APPLY_UF && size > 0;
+  bool u_fapp = false;
+  bool nu_fapp = false;
+  if (fapp)
   {
-    nv = d_parent->getModelValue(n);
-    Assert(n != nv);
-    Trace("sygus-unif-rl-purify") << "PurifyLemma : model value for " << n
-                                  << " is " << nv << "\n";
+    Assert(std::find(d_candidates.begin(), d_candidates.end(), n[0])
+           != d_candidates.end());
+    /* Whether application of a (non-)unification function-to-synthesize */
+    u_fapp = usingUnif(n[0]);
+    nu_fapp = !usingUnif(n[0]);
+    /* get model value of non-top level applications of functions-to-synthesize
+      occurring under a unification function-to-synthesize */
+    if (ensureConst)
+    {
+      nv = d_parent->getModelValue(n);
+      Assert(n != nv);
+      Trace("sygus-unif-rl-purify")
+          << "PurifyLemma : model value for " << n << " is " << nv << "\n";
+    }
   }
   /* Travese to purify */
   bool childChanged = false;
@@ -210,6 +221,7 @@ void SygusUnifRl::initializeConstructSol() {}
 void SygusUnifRl::initializeConstructSolFor(Node f) {}
 bool SygusUnifRl::constructSolution(std::vector<Node>& sols)
 {
+  initializeConstructSol();
   for (const Node& c : d_candidates)
   {
     if (!usingUnif(c))
@@ -221,7 +233,16 @@ bool SygusUnifRl::constructSolution(std::vector<Node>& sols)
     }
     else
     {
-      return false;
+      initializeConstructSolFor(c);
+      Node v =
+          constructSol(c, d_strategy[c].getRootEnumerator(), role_equal, 0);
+      if (v.isNull())
+      {
+        return false;
+      }
+      Trace("sygus-unif-rl-sol")
+          << "Adding solution " << v << " to unif candidate " << c << "\n";
+      sols.push_back(v);
     }
   }
   return true;
@@ -229,6 +250,20 @@ bool SygusUnifRl::constructSolution(std::vector<Node>& sols)
 
 Node SygusUnifRl::constructSol(Node f, Node e, NodeRole nrole, int ind)
 {
+  indent("sygus-unif-sol", ind);
+  Trace("sygus-unif-sol") << "ConstructSol: SygusRL : " << e << std::endl;
+  // is there a decision tree strategy?
+  if (nrole == role_equal)
+  {
+    std::map<Node, DecisionTreeInfo>::iterator itd = d_enum_to_dt.find(e);
+    if (itd != d_enum_to_dt.end())
+    {
+      indent("sygus-unif-sol", ind);
+      Trace("sygus-unif-sol")
+          << "...it has a decision tree strategy." << std::endl;
+    }
+  }
+
   return Node::null();
 }
 
@@ -237,6 +272,83 @@ bool SygusUnifRl::usingUnif(Node f)
   return d_unif_candidates.find(f) != d_unif_candidates.end();
 }
 
+void SygusUnifRl::registerStrategy(Node f)
+{
+  if (Trace.isOn("sygus-unif-rl-strat"))
+  {
+    Trace("sygus-unif-rl-strat")
+        << "Strategy for " << f << " is : " << std::endl;
+    d_strategy[f].debugPrint("sygus-unif-rl-strat");
+  }
+  Trace("sygus-unif-rl-strat") << "Register..." << std::endl;
+  Node e = d_strategy[f].getRootEnumerator();
+  std::map<Node, std::map<NodeRole, bool> > visited;
+  registerStrategyNode(f, e, role_equal, visited);
+}
+
+void SygusUnifRl::registerStrategyNode(
+    Node f,
+    Node e,
+    NodeRole nrole,
+    std::map<Node, std::map<NodeRole, bool> >& visited)
+{
+  Trace("sygus-unif-rl-strat") << "  register node " << e << std::endl;
+  if (visited[e].find(nrole) != visited[e].end())
+  {
+    return;
+  }
+  visited[e][nrole] = true;
+  TypeNode etn = e.getType();
+  EnumTypeInfo& tinfo = d_strategy[f].getEnumTypeInfo(etn);
+  StrategyNode& snode = tinfo.getStrategyNode(nrole);
+  for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++)
+  {
+    EnumTypeInfoStrat* etis = snode.d_strats[j];
+    StrategyType strat = etis->d_this;
+    // is this a simple recursive ITE strategy?
+    if (strat == strat_ITE && nrole == role_equal)
+    {
+      bool success = true;
+      for (unsigned c = 1; c <= 2; c++)
+      {
+        std::pair<Node, NodeRole> child = etis->d_cenum[c];
+        if (child.first != e || child.second != nrole)
+        {
+          success = false;
+          break;
+        }
+      }
+      if (success)
+      {
+        Node cond = etis->d_cenum[0].first;
+        Assert(etis->d_cenum[0].second == role_ite_condition);
+        Trace("sygus-unif-rl-strat")
+            << "  ...detected recursive ITE strategy, condition enumerator : "
+            << cond << std::endl;
+        // indicate that we will be enumerating values for cond
+        registerConditionalEnumerator(f, e, cond);
+      }
+    }
+    // TODO: recurse? for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
+  }
+}
+
+void SygusUnifRl::registerConditionalEnumerator(Node f, Node e, Node cond)
+{
+  // we will do unification for this candidate
+  d_unif_candidates.insert(f);
+  // add to the list of all conditional enumerators
+  if (std::find(d_cond_enums.begin(), d_cond_enums.end(), cond)
+      == d_cond_enums.end())
+  {
+    d_cond_enums.push_back(cond);
+    // register the conditional enumerator
+    d_tds->registerEnumerator(cond, f, d_parent, true);
+  }
+  // register that this enumerator has a decision tree construction
+  d_enum_to_dt[e].d_cond_enum = cond;
+}
+
 } /* CVC4::theory::quantifiers namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index dc1b14641..b8ead4986 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -73,8 +73,6 @@ class SygusUnifRl : public SygusUnif
   CegConjecture* d_parent;
   /* Functions-to-synthesize (a.k.a. candidates) with unification strategies */
   std::unordered_set<Node, NodeHashFunction> d_unif_candidates;
-  /* Maps unif candidates to their conditonal enumerators */
-  std::map<Node, Node> d_cand_to_cond_enum;
   /**
    * This class stores information regarding an enumerator, including: a
    * database
@@ -151,6 +149,50 @@ class SygusUnifRl : public SygusUnif
                    bool ensureConst,
                    std::vector<Node>& model_guards,
                    BoolNodePairMap& cache);
+  /*
+    --------------------------------------------------------------
+        Strategy information
+    --------------------------------------------------------------
+  */
+  /**
+   * This class stores the necessary information for building a decision tree
+   * for a particular node in the strategy tree of a candidate variable f.
+   */
+  class DecisionTreeInfo
+  {
+   public:
+    /**
+     * The enumerator in the strategy tree that stores conditions of the
+     * decision tree.
+     */
+    Node d_cond_enum;
+  };
+  /** map from enumerators in the strategy trees to the above data */
+  std::map<Node, DecisionTreeInfo> d_enum_to_dt;
+  /** all conditional enumerators */
+  std::vector<Node> d_cond_enums;
+  /** register strategy
+   *
+   * Initialize the above data for the relevant enumerators in the strategy tree
+   * of candidate variable f.
+   */
+  void registerStrategy(Node f);
+  /** register strategy node
+   *
+   * Called while traversing the strategy tree of f. The arguments e and nrole
+   * indicate the current node in the tree we are traversing, and visited
+   * indicates the nodes we have already visited.
+   */
+  void registerStrategyNode(Node f,
+                            Node e,
+                            NodeRole nrole,
+                            std::map<Node, std::map<NodeRole, bool>>& visited);
+  /** register conditional enumerator
+   *
+   * Registers that cond is a conditional enumerator for building a (recursive)
+   * decision tree at strategy node e within the strategy tree of f.
+   */
+  void registerConditionalEnumerator(Node f, Node e, Node cond);
 };
 
 } /* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
index 86efffd1f..d3a5d6c23 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -80,8 +80,7 @@ std::ostream& operator<<(std::ostream& os, StrategyType st)
 
 void SygusUnifStrategy::initialize(QuantifiersEngine* qe,
                                    Node f,
-                                   std::vector<Node>& enums,
-                                   std::vector<Node>& lemmas)
+                                   std::vector<Node>& enums)
 {
   Assert(d_candidate.isNull());
   d_candidate = f;
@@ -92,8 +91,10 @@ void SygusUnifStrategy::initialize(QuantifiersEngine* qe,
   collectEnumeratorTypes(d_root, role_equal);
   // add the enumerators
   enums.insert(enums.end(), d_esym_list.begin(), d_esym_list.end());
-  // learn redundant ops
-  staticLearnRedundantOps(lemmas);
+  // finish the initialization of the strategy
+  // this computes if each node is conditional
+  std::map<Node, std::map<NodeRole, bool> > visited;
+  finishInit(getRootEnumerator(), role_equal, visited, false);
 }
 
 void SygusUnifStrategy::initializeType(TypeNode tn)
@@ -101,10 +102,13 @@ void SygusUnifStrategy::initializeType(TypeNode tn)
   d_tinfo[tn].d_this_type = tn;
 }
 
-Node SygusUnifStrategy::getRootEnumerator()
+Node SygusUnifStrategy::getRootEnumerator() const
 {
-  std::map<EnumRole, Node>::iterator it = d_tinfo[d_root].d_enum.find(enum_io);
-  Assert(it != d_tinfo[d_root].d_enum.end());
+  std::map<TypeNode, EnumTypeInfo>::const_iterator itt = d_tinfo.find(d_root);
+  Assert(itt != d_tinfo.end());
+  std::map<EnumRole, Node>::const_iterator it =
+      itt->second.d_enum.find(enum_io);
+  Assert(it != itt->second.d_enum.end());
   return it->second;
 }
 
@@ -702,10 +706,10 @@ void SygusUnifStrategy::staticLearnRedundantOps(std::vector<Node>& lemmas)
   Trace("sygus-unif") << std::endl;
   Trace("sygus-unif") << "Strategy for candidate " << d_candidate
                       << " is : " << std::endl;
+  debugPrint("sygus-unif");
   std::map<Node, std::map<NodeRole, bool> > visited;
   std::map<Node, std::map<unsigned, bool> > needs_cons;
-  staticLearnRedundantOps(
-      getRootEnumerator(), role_equal, visited, needs_cons, 0, false);
+  staticLearnRedundantOps(getRootEnumerator(), role_equal, visited, needs_cons);
   // now, check the needs_cons map
   for (std::pair<const Node, std::map<unsigned, bool> >& nce : needs_cons)
   {
@@ -730,124 +734,181 @@ void SygusUnifStrategy::staticLearnRedundantOps(std::vector<Node>& lemmas)
   }
 }
 
+void SygusUnifStrategy::debugPrint(const char* c)
+{
+  if (Trace.isOn(c))
+  {
+    std::map<Node, std::map<NodeRole, bool> > visited;
+    debugPrint(c, getRootEnumerator(), role_equal, visited, 0);
+  }
+}
+
 void SygusUnifStrategy::staticLearnRedundantOps(
     Node e,
     NodeRole nrole,
     std::map<Node, std::map<NodeRole, bool> >& visited,
-    std::map<Node, std::map<unsigned, bool> >& needs_cons,
-    int ind,
-    bool isCond)
+    std::map<Node, std::map<unsigned, bool> >& needs_cons)
 {
-  std::map<Node, EnumInfo>::iterator itn = d_einfo.find(e);
-  Assert(itn != d_einfo.end());
-
-  if (visited[e].find(nrole) == visited[e].end()
-      || (isCond && !itn->second.isConditional()))
+  if (visited[e].find(nrole) != visited[e].end())
+  {
+    return;
+  }
+  visited[e][nrole] = true;
+  EnumInfo& ei = getEnumInfo(e);
+  if (ei.isTemplated())
   {
-    visited[e][nrole] = true;
-    // if conditional
-    if (isCond)
+    return;
+  }
+  TypeNode etn = e.getType();
+  EnumTypeInfo& tinfo = getEnumTypeInfo(etn);
+  StrategyNode& snode = tinfo.getStrategyNode(nrole);
+  if (snode.d_strats.empty())
+  {
+    return;
+  }
+  std::map<unsigned, bool> needs_cons_curr;
+  // various strategies
+  for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++)
+  {
+    EnumTypeInfoStrat* etis = snode.d_strats[j];
+    int cindex = Datatype::indexOf(etis->d_cons.toExpr());
+    Assert(cindex != -1);
+    needs_cons_curr[static_cast<unsigned>(cindex)] = false;
+    for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
     {
-      itn->second.setConditional();
+      staticLearnRedundantOps(cec.first, cec.second, visited, needs_cons);
     }
-    indent("sygus-unif", ind);
-    Trace("sygus-unif") << e << " :: node role : " << nrole;
-    Trace("sygus-unif")
-        << ", type : "
-        << ((DatatypeType)e.getType().toType()).getDatatype().getName();
-    if (isCond)
+  }
+  // get the master enumerator for the type of this enumerator
+  std::map<TypeNode, Node>::iterator itse = d_master_enum.find(etn);
+  if (itse == d_master_enum.end())
+  {
+    return;
+  }
+  Node em = itse->second;
+  Assert(!em.isNull());
+  // get the current datatype
+  const Datatype& dt = static_cast<DatatypeType>(etn.toType()).getDatatype();
+  // all constructors that are not a part of a strategy are needed
+  for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++)
+  {
+    if (needs_cons_curr.find(j) == needs_cons_curr.end())
     {
-      Trace("sygus-unif") << ", conditional";
+      needs_cons_curr[j] = true;
     }
-    Trace("sygus-unif") << ", enum role : " << itn->second.getRole();
-
-    if (itn->second.isTemplated())
+  }
+  // update the constructors that the master enumerator needs
+  if (needs_cons.find(em) == needs_cons.end())
+  {
+    needs_cons[em] = needs_cons_curr;
+  }
+  else
+  {
+    for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++)
     {
-      Trace("sygus-unif") << ", templated : (lambda "
-                          << itn->second.d_template_arg << " "
-                          << itn->second.d_template << ")" << std::endl;
+      needs_cons[em][j] = needs_cons[em][j] || needs_cons_curr[j];
     }
-    else
+  }
+}
+
+void SygusUnifStrategy::finishInit(
+    Node e,
+    NodeRole nrole,
+    std::map<Node, std::map<NodeRole, bool> >& visited,
+    bool isCond)
+{
+  EnumInfo& ei = getEnumInfo(e);
+  if (visited[e].find(nrole) != visited[e].end()
+      && (!isCond || ei.isConditional()))
+  {
+    return;
+  }
+  visited[e][nrole] = true;
+  // set conditional
+  if (isCond)
+  {
+    ei.setConditional();
+  }
+  if (ei.isTemplated())
+  {
+    return;
+  }
+  TypeNode etn = e.getType();
+  EnumTypeInfo& tinfo = getEnumTypeInfo(etn);
+  StrategyNode& snode = tinfo.getStrategyNode(nrole);
+  for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++)
+  {
+    EnumTypeInfoStrat* etis = snode.d_strats[j];
+    StrategyType strat = etis->d_this;
+    bool newIsCond = isCond || strat == strat_ITE;
+    for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
     {
-      Trace("sygus-unif") << std::endl;
-      TypeNode etn = e.getType();
+      finishInit(cec.first, cec.second, visited, newIsCond);
+    }
+  }
+}
 
-      // enumerator type info
-      std::map<TypeNode, EnumTypeInfo>::iterator itt = d_tinfo.find(etn);
-      Assert(itt != d_tinfo.end());
-      EnumTypeInfo& tinfo = itt->second;
+void SygusUnifStrategy::debugPrint(
+    const char* c,
+    Node e,
+    NodeRole nrole,
+    std::map<Node, std::map<NodeRole, bool> >& visited,
+    int ind)
+{
+  if (visited[e].find(nrole) != visited[e].end())
+  {
+    indent(c, ind);
+    Trace(c) << e << " :: node role : " << nrole << std::endl;
+    return;
+  }
+  visited[e][nrole] = true;
+  EnumInfo& ei = getEnumInfo(e);
 
-      // strategy info
-      std::map<NodeRole, StrategyNode>::iterator itsn =
-          tinfo.d_snodes.find(nrole);
-      Assert(itsn != tinfo.d_snodes.end());
-      StrategyNode& snode = itsn->second;
+  TypeNode etn = e.getType();
 
-      if (snode.d_strats.empty())
-      {
-        return;
-      }
-      std::map<unsigned, bool> needs_cons_curr;
-      // various strategies
-      for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++)
-      {
-        EnumTypeInfoStrat* etis = snode.d_strats[j];
-        StrategyType strat = etis->d_this;
-        bool newIsCond = isCond || strat == strat_ITE;
-        indent("sygus-unif", ind + 1);
-        Trace("sygus-unif") << "Strategy : " << strat
-                            << ", from cons : " << etis->d_cons << std::endl;
-        int cindex = Datatype::indexOf(etis->d_cons.toExpr());
-        Assert(cindex != -1);
-        needs_cons_curr[static_cast<unsigned>(cindex)] = false;
-        for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
-        {
-          // recurse
-          staticLearnRedundantOps(
-              cec.first, cec.second, visited, needs_cons, ind + 2, newIsCond);
-        }
-      }
-      // get the master enumerator for the type of this enumerator
-      std::map<TypeNode, Node>::iterator itse = d_master_enum.find(etn);
-      if (itse == d_master_enum.end())
-      {
-        return;
-      }
-      Node em = itse->second;
-      Assert(!em.isNull());
-      // get the current datatype
-      const Datatype& dt =
-          static_cast<DatatypeType>(etn.toType()).getDatatype();
-      // all constructors that are not a part of a strategy are needed
-      for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++)
-      {
-        if (needs_cons_curr.find(j) == needs_cons_curr.end())
-        {
-          needs_cons_curr[j] = true;
-        }
-      }
-      // update the constructors that the master enumerator needs
-      if (needs_cons.find(em) == needs_cons.end())
-      {
-        needs_cons[em] = needs_cons_curr;
-      }
-      else
-      {
-        for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++)
-        {
-          needs_cons[em][j] = needs_cons[em][j] || needs_cons_curr[j];
-        }
-      }
-    }
+  indent(c, ind);
+  Trace(c) << e << " :: node role : " << nrole;
+  Trace(c) << ", type : "
+           << static_cast<DatatypeType>(etn.toType()).getDatatype().getName();
+  if (ei.isConditional())
+  {
+    Trace(c) << ", conditional";
   }
-  else
+  Trace(c) << ", enum role : " << ei.getRole();
+
+  if (ei.isTemplated())
+  {
+    Trace(c) << ", templated : (lambda " << ei.d_template_arg << " "
+             << ei.d_template << ")";
+  }
+  Trace(c) << std::endl;
+
+  EnumTypeInfo& tinfo = getEnumTypeInfo(etn);
+  StrategyNode& snode = tinfo.getStrategyNode(nrole);
+  for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++)
   {
-    indent("sygus-unif", ind);
-    Trace("sygus-unif") << e << " :: node role : " << nrole << std::endl;
+    EnumTypeInfoStrat* etis = snode.d_strats[j];
+    StrategyType strat = etis->d_this;
+    indent(c, ind + 1);
+    Trace(c) << "Strategy : " << strat << ", from cons : " << etis->d_cons
+             << std::endl;
+    for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
+    {
+      // recurse
+      debugPrint(c, cec.first, cec.second, visited, ind + 2);
+    }
   }
 }
 
 void EnumInfo::initialize(EnumRole role) { d_role = role; }
+
+StrategyNode& EnumTypeInfo::getStrategyNode(NodeRole nrole)
+{
+  std::map<NodeRole, StrategyNode>::iterator it = d_snodes.find(nrole);
+  Assert(it != d_snodes.end());
+  return it->second;
+}
+
 bool EnumTypeInfoStrat::isValid(UnifContext& x)
 {
   if ((x.getCurrentRole() == role_string_prefix
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h
index 0ab7ea1d6..8f9adefb9 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h
@@ -198,6 +198,8 @@ class EnumTypeInfo
   std::map<EnumRole, Node> d_enum;
   /** map from node roles to strategy nodes */
   std::map<NodeRole, StrategyNode> d_snodes;
+  /** get strategy node for node role */
+  StrategyNode& getStrategyNode(NodeRole nrole);
 };
 
 /** represents a strategy for a SyGuS datatype type
@@ -253,18 +255,10 @@ class SygusUnifStrategy
    *
    * This call constructs a set of enumerators for the relevant subfields of
    * the grammar of f and adds them to enums.
-   *
-   * This also may result in lemmas being added to lemmas,
-   * which correspond to static symmetry breaking predicates (for example,
-   * those that exclude ITE from enumerators whose role is enum_io when the
-   * strategy is ITE_strat).
    */
-  void initialize(QuantifiersEngine* qe,
-                  Node f,
-                  std::vector<Node>& enums,
-                  std::vector<Node>& lemmas);
+  void initialize(QuantifiersEngine* qe, Node f, std::vector<Node>& enums);
   /** Get the root enumerator for this class */
-  Node getRootEnumerator();
+  Node getRootEnumerator() const;
   /**
    * Get the enumerator info for enumerator e, where e must be an enumerator
    * initialized by this class (in enums after a call to initialize).
@@ -276,6 +270,20 @@ class SygusUnifStrategy
    */
   EnumTypeInfo& getEnumTypeInfo(TypeNode tn);
 
+  /** static learn redundant operators
+   *
+   * This learns static lemmas for pruning enumerative space based on the
+   * strategy for the function-to-synthesize of this class, and stores these
+   * into lemmas.
+   *
+   * These may correspond to static symmetry breaking predicates (for example,
+   * those that exclude ITE from enumerators whose role is enum_io when the
+   * strategy is ITE_strat).
+   */
+  void staticLearnRedundantOps(std::vector<Node>& lemmas);
+  /** debug print this strategy on Trace c */
+  void debugPrint(const char* c);
+
  private:
   /** reference to quantifier engine */
   QuantifiersEngine* d_qe;
@@ -332,13 +340,6 @@ class SygusUnifStrategy
                      Node n,
                      std::map<Node, unsigned>& templ_var_index,
                      std::map<unsigned, unsigned>& templ_injection);
-  /** static learn redundant operators
-   *
-   * This learns static lemmas for pruning enumerative space based on the
-   * strategy for the function-to-synthesize of this class, and stores these
-   * into lemmas.
-   */
-  void staticLearnRedundantOps(std::vector<Node>& lemmas);
   /** helper for static learn redundant operators
    *
    * (e, nrole) specify the strategy node in the graph we are currently
@@ -346,19 +347,38 @@ class SygusUnifStrategy
    *
    * This method builds the mapping needs_cons, which maps (master) enumerators
    * to a map from the constructors that it needs.
-   *
-   * ind is the depth in the strategy graph we are at (for debugging).
-   *
-   * isCond is whether the current enumerator is conditional (beneath a
-   * conditional of an strat_ITE strategy).
    */
   void staticLearnRedundantOps(
       Node e,
       NodeRole nrole,
       std::map<Node, std::map<NodeRole, bool> >& visited,
-      std::map<Node, std::map<unsigned, bool> >& needs_cons,
-      int ind,
-      bool isCond);
+      std::map<Node, std::map<unsigned, bool> >& needs_cons);
+  /** finish initialization of the strategy tree
+   *
+   * (e, nrole) specify the strategy node in the graph we are currently
+   * analyzing, visited stores the nodes we have already visited.
+   *
+   * isCond is whether the current enumerator is conditional (beneath a
+   * conditional of an strat_ITE strategy).
+   */
+  void finishInit(Node e,
+                  NodeRole nrole,
+                  std::map<Node, std::map<NodeRole, bool> >& visited,
+                  bool isCond);
+  /** helper for debug print
+   *
+   * Prints the node e with role nrole on Trace(c).
+   *
+   * (e, nrole) specify the strategy node in the graph we are currently
+   * analyzing, visited stores the nodes we have already visited.
+   *
+   * ind is the current level of indentation (for debugging)
+   */
+  void debugPrint(const char* c,
+                  Node e,
+                  NodeRole nrole,
+                  std::map<Node, std::map<NodeRole, bool> >& visited,
+                  int ind);
   //------------------------------ end strategy registration
 };
 
-- 
cgit v1.2.3


From b35ed9dd0e1c8361338ba11d2b1532301f540945 Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Thu, 3 May 2018 21:40:30 -0500
Subject: Move Lazy trie datastructure to its own file (#1871)

Preparation for further developing CegisUnif
---
 src/Makefile.am                          |   2 +
 src/theory/quantifiers/lazy_trie.cpp     |  65 ++++++++++++++++++++
 src/theory/quantifiers/lazy_trie.h       | 101 +++++++++++++++++++++++++++++++
 src/theory/quantifiers/sygus_sampler.cpp |  43 +------------
 src/theory/quantifiers/sygus_sampler.h   |  73 +---------------------
 5 files changed, 170 insertions(+), 114 deletions(-)
 create mode 100644 src/theory/quantifiers/lazy_trie.cpp
 create mode 100644 src/theory/quantifiers/lazy_trie.h

diff --git a/src/Makefile.am b/src/Makefile.am
index 6cb179b1d..168e1e3b8 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -431,6 +431,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/inst_propagator.h \
 	theory/quantifiers/inst_strategy_enumerative.cpp \
 	theory/quantifiers/inst_strategy_enumerative.h \
+	theory/quantifiers/lazy_trie.cpp \
+	theory/quantifiers/lazy_trie.h \
 	theory/quantifiers/local_theory_ext.cpp \
 	theory/quantifiers/local_theory_ext.h \
 	theory/quantifiers/macros.cpp \
diff --git a/src/theory/quantifiers/lazy_trie.cpp b/src/theory/quantifiers/lazy_trie.cpp
new file mode 100644
index 000000000..5a63024b8
--- /dev/null
+++ b/src/theory/quantifiers/lazy_trie.cpp
@@ -0,0 +1,65 @@
+/*********************                                                        */
+/*! \file lazy_trie.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 Implementation of lazy trie
+ **/
+
+#include "theory/quantifiers/lazy_trie.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+Node LazyTrie::add(Node n,
+                   LazyTrieEvaluator* ev,
+                   unsigned index,
+                   unsigned ntotal,
+                   bool forceKeep)
+{
+  LazyTrie* lt = this;
+  while (lt != NULL)
+  {
+    if (index == ntotal)
+    {
+      // lazy child holds the leaf data
+      if (lt->d_lazy_child.isNull() || forceKeep)
+      {
+        lt->d_lazy_child = n;
+      }
+      return lt->d_lazy_child;
+    }
+    std::vector<Node> ex;
+    if (lt->d_children.empty())
+    {
+      if (lt->d_lazy_child.isNull())
+      {
+        // no one has been here, we are done
+        lt->d_lazy_child = n;
+        return lt->d_lazy_child;
+      }
+      // evaluate the lazy child
+      Node e_lc = ev->evaluate(lt->d_lazy_child, index);
+      // store at next level
+      lt->d_children[e_lc].d_lazy_child = lt->d_lazy_child;
+      // replace
+      lt->d_lazy_child = Node::null();
+    }
+    // recurse
+    Node e = ev->evaluate(n, index);
+    lt = &lt->d_children[e];
+    index = index + 1;
+  }
+  return Node::null();
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/lazy_trie.h b/src/theory/quantifiers/lazy_trie.h
new file mode 100644
index 000000000..b114f55df
--- /dev/null
+++ b/src/theory/quantifiers/lazy_trie.h
@@ -0,0 +1,101 @@
+/*********************                                                        */
+/*! \file lazy_trie.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 lazy trie
+ **/
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H
+#define __CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** abstract evaluator class
+ *
+ * This class is used for the LazyTrie data structure below.
+ */
+class LazyTrieEvaluator
+{
+ public:
+  virtual ~LazyTrieEvaluator() {}
+  virtual Node evaluate(Node n, unsigned index) = 0;
+};
+
+/** LazyTrie
+ *
+ * This is a trie where terms are added in a lazy fashion. This data structure
+ * is useful, for instance, when we are only interested in when two terms
+ * map to the same node in the trie but we need not care about computing
+ * exactly where they are.
+ *
+ * In other words, when a term n is added to this trie, we do not insist
+ * that n is placed at the maximal depth of the trie. Instead, we place n at a
+ * minimal depth node that has no children. In this case we say n is partially
+ * evaluated in this trie.
+ *
+ * This class relies on an abstract evaluator interface above, which evaluates
+ * nodes for indices.
+ *
+ * For example, say we have terms a, b, c and an evaluator ev where:
+ *   ev->evaluate( a, 0,1,2 ) = 0, 5, 6
+ *   ev->evaluate( b, 0,1,2 ) = 1, 3, 0
+ *   ev->evaluate( c, 0,1,2 ) = 1, 3, 2
+ * After adding a to the trie, we get:
+ *   root: a
+ * After adding b to the resulting trie, we get:
+ *   root: null
+ *     d_children[0]: a
+ *     d_children[1]: b
+ * After adding c to the resulting trie, we get:
+ *   root: null
+ *     d_children[0]: a
+ *     d_children[1]: null
+ *       d_children[3]: null
+ *         d_children[0] : b
+ *         d_children[2] : c
+ * Notice that we need not call ev->evalute( a, 1 ) and ev->evalute( a, 2 ).
+ */
+class LazyTrie
+{
+ public:
+  LazyTrie() {}
+  ~LazyTrie() {}
+  /** the data at this node, which may be partially evaluated */
+  Node d_lazy_child;
+  /** the children of this node */
+  std::map<Node, LazyTrie> d_children;
+  /** clear the trie */
+  void clear() { d_children.clear(); }
+  /** add n to the trie
+   *
+   * This function returns a node that is mapped to the same node in the trie
+   * if one exists, or n otherwise.
+   *
+   * ev is an evaluator which determines where n is placed in the trie
+   * index is the depth of this node
+   * ntotal is the maximal depth of the trie
+   * forceKeep is whether we wish to force that n is chosen as a representative
+   */
+  Node add(Node n,
+           LazyTrieEvaluator* ev,
+           unsigned index,
+           unsigned ntotal,
+           bool forceKeep);
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H */
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 757256fc3..fb4f7e831 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -17,6 +17,7 @@
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
+#include "theory/quantifiers/lazy_trie.h"
 #include "util/bitvector.h"
 #include "util/random.h"
 
@@ -24,48 +25,6 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-Node LazyTrie::add(Node n,
-                   LazyTrieEvaluator* ev,
-                   unsigned index,
-                   unsigned ntotal,
-                   bool forceKeep)
-{
-  LazyTrie* lt = this;
-  while (lt != NULL)
-  {
-    if (index == ntotal)
-    {
-      // lazy child holds the leaf data
-      if (lt->d_lazy_child.isNull() || forceKeep)
-      {
-        lt->d_lazy_child = n;
-      }
-      return lt->d_lazy_child;
-    }
-    std::vector<Node> ex;
-    if (lt->d_children.empty())
-    {
-      if (lt->d_lazy_child.isNull())
-      {
-        // no one has been here, we are done
-        lt->d_lazy_child = n;
-        return lt->d_lazy_child;
-      }
-      // evaluate the lazy child
-      Node e_lc = ev->evaluate(lt->d_lazy_child, index);
-      // store at next level
-      lt->d_children[e_lc].d_lazy_child = lt->d_lazy_child;
-      // replace
-      lt->d_lazy_child = Node::null();
-    }
-    // recurse
-    Node e = ev->evaluate(n, index);
-    lt = &lt->d_children[e];
-    index = index + 1;
-  }
-  return Node::null();
-}
-
 SygusSampler::SygusSampler()
     : d_tds(nullptr), d_use_sygus_type(false), d_is_valid(false)
 {
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index b741b60d4..5e0a24dd2 100644
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -19,84 +19,13 @@
 
 #include <map>
 #include "theory/quantifiers/dynamic_rewrite.h"
+#include "theory/quantifiers/lazy_trie.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-/** abstract evaluator class
- *
- * This class is used for the LazyTrie data structure below.
- */
-class LazyTrieEvaluator
-{
- public:
-  virtual ~LazyTrieEvaluator() {}
-  virtual Node evaluate(Node n, unsigned index) = 0;
-};
-
-/** LazyTrie
- *
- * This is a trie where terms are added in a lazy fashion. This data structure
- * is useful, for instance, when we are only interested in when two terms
- * map to the same node in the trie but we need not care about computing
- * exactly where they are.
- *
- * In other words, when a term n is added to this trie, we do not insist
- * that n is placed at the maximal depth of the trie. Instead, we place n at a
- * minimal depth node that has no children. In this case we say n is partially
- * evaluated in this trie.
- *
- * This class relies on an abstract evaluator interface above, which evaluates
- * nodes for indices.
- *
- * For example, say we have terms a, b, c and an evaluator ev where:
- *   ev->evaluate( a, 0,1,2 ) = 0, 5, 6
- *   ev->evaluate( b, 0,1,2 ) = 1, 3, 0
- *   ev->evaluate( c, 0,1,2 ) = 1, 3, 2
- * After adding a to the trie, we get:
- *   root: a
- * After adding b to the resulting trie, we get:
- *   root: null
- *     d_children[0]: a
- *     d_children[1]: b
- * After adding c to the resulting trie, we get:
- *   root: null
- *     d_children[0]: a
- *     d_children[1]: null
- *       d_children[3]: null
- *         d_children[0] : b
- *         d_children[2] : c
- * Notice that we need not call ev->evalute( a, 1 ) and ev->evalute( a, 2 ).
- */
-class LazyTrie
-{
- public:
-  LazyTrie() {}
-  ~LazyTrie() {}
-  /** the data at this node, which may be partially evaluated */
-  Node d_lazy_child;
-  /** the children of this node */
-  std::map<Node, LazyTrie> d_children;
-  /** clear the trie */
-  void clear() { d_children.clear(); }
-  /** add n to the trie
-   *
-   * This function returns a node that is mapped to the same node in the trie
-   * if one exists, or n otherwise.
-   *
-   * ev is an evaluator which determines where n is placed in the trie
-   * index is the depth of this node
-   * ntotal is the maximal depth of the trie
-   * forceKeep is whether we wish to force that n is chosen as a representative
-   */
-  Node add(Node n,
-           LazyTrieEvaluator* ev,
-           unsigned index,
-           unsigned ntotal,
-           bool forceKeep);
-};
 
 /** SygusSampler
  *
-- 
cgit v1.2.3