path: root/src/theory/quantifiers/ce_guided_pbe.h

/*********************                                                        */
/*! \file ce_guided_pbe.h
 ** \verbatim
 ** Top contributors (to current version):
 **   Andrew Reynolds
 ** This file is part of the CVC4 project.
 ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
 ** in the top-level source directory) and their institutional affiliations.
 ** All rights reserved.  See the file COPYING in the top-level source
 ** directory for licensing information.\endverbatim
 **
 ** \brief utility for processing programming by examples synthesis conjectures
 **/

#include "cvc4_private.h"

#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_PBE_H
#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_PBE_H

#include "context/cdhashmap.h"
#include "theory/quantifiers_engine.h"

namespace CVC4 {
namespace theory {
namespace quantifiers {

/** roles for enumerators
 *
 * This indicates the role of an enumerator that is allocated by approaches
 * for synthesis-by-unification (see details below).
 *   io : the enumerator should enumerate values that are overall solutions
 *        for the function-to-synthesize,
 *   ite_condition : the enumerator should enumerate values that are useful
 *                   in ite conditions in the ITE strategy,
 *   concat_term : the enumerator should enumerate values that are used as
 *                 components of string concatenation solutions.
 */
enum EnumRole
{
  enum_invalid,
  enum_io,
  enum_ite_condition,
  enum_concat_term,
};
std::ostream& operator<<(std::ostream& os, EnumRole r);

/** roles for strategy nodes
 *
 * This indicates the role of a strategy node, which is a subprocedure of
 * CegConjecturePbe::constructSolution (see details below).
 *   equal : the node constructed must be equal to the overall solution for
 *           the function-to-synthesize,
 *   string_prefix/suffix : the node constructed must be a prefix/suffix
 *                          of the function-to-synthesize,
 *   ite_condition : the node constructed must be a condition that makes some
 *                   active input examples true and some input examples false.
 */
enum NodeRole
{
  role_invalid,
  role_equal,
  role_string_prefix,
  role_string_suffix,
  role_ite_condition,
};
std::ostream& operator<<(std::ostream& os, NodeRole r);

/** enumerator role for node role */
EnumRole getEnumeratorRoleForNodeRole(NodeRole r);

/** strategy types
 *
 * This indicates a strategy for synthesis-by-unification (see details below).
 *   ITE : strategy for constructing if-then-else solutions via decision
 *         tree learning techniques,
 *   CONCAT_PREFIX/SUFFIX : strategy for constructing string concatenation
 *         solutions via a divide and conquer approach,
 *   ID : identity strategy used for calling strategies on child type through
 *        an identity function.
 */
enum StrategyType
{
  strat_INVALID,
  strat_ITE,
  strat_CONCAT_PREFIX,
  strat_CONCAT_SUFFIX,
  strat_ID,
};
std::ostream& operator<<(std::ostream& os, StrategyType st);

class CegConjecture;

/** CegConjecturePbe
*
* This class implements optimizations that target synthesis conjectures
* that are in Programming-By-Examples (PBE) form.
*
* [EX#1] An example of a synthesis conjecture in PBE form is :
* exists f. forall x.
* ( x = 0 => f( x ) = 2 ) ^ ( x = 5 => f( x ) = 7 ) ^ ( x = 6 => f( x ) = 8 )
*
* We say that the above conjecture has I/O examples (0)->2, (5)->7, (6)->8.
*
* Internally, this class does the following for SyGuS inputs:
*
* (1) Infers whether the input conjecture is in PBE form or not.
* (2) Based on this information and on the syntactic restrictions, it
*     devises a strategy for enumerating terms and construction solutions,
*     which is inspired by Alur et al. "Scaling Enumerative Program Synthesis
*     via Divide and Conquer" TACAS 2017. In particular, it may consider
*     strategies for constructing decision trees when the grammar permits ITEs
*     and a strategy for divide-and-conquer string synthesis when the grammar
*     permits string concatenation. This is stored in a set of data structures
*     within d_cinfo.
* (3) It makes (possibly multiple) calls to
*     TermDatabaseSygus::registerMeasuredTerm(...) based
*     on the strategy, which inform the rest of the system to enumerate values
*     of particular types in the grammar through use of fresh variables which
*     we call "enumerators".
*
* Points (1)-(3) happen within a call to CegConjecturePbe::initialize(...).
*
* Notice that each enumerator is associated with a single
* function-to-synthesize, but a function-to-sythesize may be mapped to multiple 
* enumerators. Some public functions of this class expect an enumerator as 
* input, which we map to a function-to-synthesize via 
* TermDatabaseSygus::getSynthFunFor(e).
*
* An enumerator is initially "active" but may become inactive if the enumeration
* exhausts all possible values in the datatype corresponding to syntactic
* restrictions for it. The search may continue unless all enumerators become 
* inactive.
*
* (4) During search, the extension of quantifier-free datatypes procedure for
*     SyGuS datatypes may ask this class whether current candidates can be
*     discarded based on
*     inferring when two candidate solutions are equivalent up to examples.
*     For example, the candidate solutions:
*     f = \x ite( x<0, x+1, x ) and f = \x x
*     are equivalent up to examples on the above conjecture, since they have the
*     same value on the points x = 0,5,6. Hence, we need only consider one of
*     them. The interface for querying this is
*       CegConjecturePbe::addSearchVal(...).
*     For details, see Reynolds et al. SYNT 2017.
*
* (5) When the extension of quantifier-free datatypes procedure for SyGuS
*     datatypes terminates with a model, the parent of this class calls
*     CegConjecturePbe::getCandidateList(...), where this class returns the list
*     of active enumerators.
* (6) The parent class subsequently calls
*     CegConjecturePbe::constructValues(...), which
*     informs this class that new values have been enumerated for active
*     enumerators, as indicated by the current model. This call also requests
*     that based on these
*     newly enumerated values, whether this class is now able to construct a
*     solution based on the high-level strategy (stored in d_c_info).
*
* This class is not designed to work in incremental mode, since there is no way
* to specify incremental problems in SyguS.
*/
class CegConjecturePbe {
 public:
  CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p);
  ~CegConjecturePbe();

  /** initialize this class
  *
  * n is the "base instantiation" of the deep-embedding version of
  *   the synthesis conjecture under "candidates".
  *   (see CegConjecture::d_base_inst)
  *
  * This function may add lemmas to the vector lemmas corresponding
  * to initial lemmas regarding static analysis of enumerators it
  * introduced. For example, we may say that the top-level symbol
  * of an enumerator is not ITE if it is being used to construct
  * return values for decision trees.
  */
  void initialize(Node n,
                  std::vector<Node>& candidates,
                  std::vector<Node>& lemmas);
  /** get candidate list
  * Adds all active enumerators associated with functions-to-synthesize in
  * candidates to clist.
  */
  void getCandidateList(std::vector<Node>& candidates,
                        std::vector<Node>& clist);
  /** construct candidates
  * (1) Indicates that the list of enumerators in "enums" currently have model
  *     values "enum_values".
  * (2) Asks whether based on these new enumerated values, we can construct a
  *     solution for
  *     the functions-to-synthesize in "candidates". If so, this function
  *     returns "true" and
  *     adds solutions for candidates into "candidate_values".
  * During this class, this class may add auxiliary lemmas to "lems", which the
  * caller should send on the output channel via lemma(...).
  */
  bool constructCandidates(std::vector<Node>& enums,
                           std::vector<Node>& enum_values,
                           std::vector<Node>& candidates,
                           std::vector<Node>& candidate_values,
                           std::vector<Node>& lems);
  /** is PBE enabled for any enumerator? */
  bool isPbe() { return d_is_pbe; }
  /** is the enumerator e associated with I/O example pairs? */
  bool hasExamples(Node e);
  /** get number of I/O example pairs for enumerator e */
  unsigned getNumExamples(Node e);
  /** get the input arguments for i^th I/O example for e, which is added to the
   * vector ex */
  void getExample(Node e, unsigned i, std::vector<Node>& ex);
  /** get the output value of the i^th I/O example for enumerator e */
  Node getExampleOut(Node e, unsigned i);

  /** add the search val
  * This function is called by the extension of quantifier-free datatypes
  * procedure for SyGuS datatypes when we are considering a value of
  * enumerator e of sygus type tn whose analog in the signature of builtin
  * theory is bvr.
  *
  * For example, bvr = x + 1 when e is the datatype value Plus( x(), One() ) and
  * tn is a sygus datatype that encodes a subsignature of the integers.
  *
  * This returns either:
  * - A SyGuS term whose analog is equivalent to bvr up to examples
  *   In the above example,
  *   it may return a term t of the form Plus( One(), x() ), such that this
  *   function was previously called with t as input.
  * - e, indicating that no previous terms are equivalent to e up to examples.
  */
  Node addSearchVal(TypeNode tn, Node e, Node bvr);
  /** evaluate builtin
  * This returns the evaluation of bn on the i^th example for the
  * function-to-synthesis
  * associated with enumerator e. If there are not at least i examples, it
  * returns the rewritten form of bn.
  * For example, if bn = x+5, e is an enumerator for f in the above example
  * [EX#1], then
  *   evaluateBuiltin( tn, bn, e, 0 ) = 7
  *   evaluateBuiltin( tn, bn, e, 1 ) = 9
  *   evaluateBuiltin( tn, bn, e, 2 ) = 10
  */
  Node evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i);

 private:
  /** quantifiers engine associated with this class */
  QuantifiersEngine* d_qe;
  /** sygus term database of d_qe */
  quantifiers::TermDbSygus * d_tds;
  /** true and false nodes */
  Node d_true;
  Node d_false;
  /** A reference to the conjecture that owns this class. */
  CegConjecture* d_parent;
  /** is this a PBE conjecture for any function? */
  bool d_is_pbe;
  /** for each candidate variable f (a function-to-synthesize), whether the
  * conjecture is purely PBE for that variable
  * In other words, all occurrences of f are guarded by equalities that
  * constraint its arguments to constants.
  */
  std::map< Node, bool > d_examples_invalid;
  /** for each candidate variable (function-to-synthesize), whether the
  * conjecture is purely PBE for that variable.
  * An example of a conjecture for which d_examples_invalid is false but
  * d_examples_out_invalid is true is:
  *   exists f. forall x. ( x = 0 => f( x ) > 2 )
  * another example is:
  *   exists f. forall x. ( ( x = 0 => f( x ) = 2 ) V ( x = 3 => f( x ) = 3 ) )
  * since the formula is not a conjunction (the example values are not
  * entailed).
  * However, the domain of f in both cases is finite, which can be used for
  * search space pruning.
  */
  std::map< Node, bool > d_examples_out_invalid;
  /** for each candidate variable (function-to-synthesize), input of I/O
   * examples */
  std::map< Node, std::vector< std::vector< Node > > > d_examples;
  /** for each candidate variable (function-to-synthesize), output of I/O
   * examples */
  std::map< Node, std::vector< Node > > d_examples_out;
  /** the list of example terms
   * For the example [EX#1] above, this is f( 0 ), f( 5 ), f( 6 )
   */
  std::map< Node, std::vector< Node > > d_examples_term;
  /** collect the PBE examples in n
  * This is called on the input conjecture, and will populate the above vectors.
  *   hasPol/pol denote the polarity of n in the conjecture.
  */
  void collectExamples( Node n, std::map< Node, bool >& visited, bool hasPol, bool pol );

  //--------------------------------- PBE search values
  /** this class is an index of candidate solutions for PBE synthesis */
  class PbeTrie {
   public:
    PbeTrie() {}
    ~PbeTrie() {}
    Node d_lazy_child;
    std::map<Node, PbeTrie> d_children;
    void clear() { d_children.clear(); }
    Node addPbeExample(TypeNode etn, Node e, Node b, CegConjecturePbe* cpbe,
                       unsigned index, unsigned ntotal);

   private:
    Node addPbeExampleEval(TypeNode etn, Node e, Node b, std::vector<Node>& ex,
                           CegConjecturePbe* cpbe, unsigned index,
                           unsigned ntotal);
  };
  /** trie of candidate solutions tried
  * This stores information for each (enumerator, type),
  * where type is a type in the grammar of the space of solutions for a subterm
  * of e. This is used for symmetry breaking in quantifier-free reasoning
  * about SyGuS datatypes.
  */
  std::map<Node, std::map<TypeNode, PbeTrie> > d_pbe_trie;
  //--------------------------------- end PBE search values

  // -------------------------------- decision tree learning
  // index filter
  class IndexFilter {
  public:
    IndexFilter(){}
    void mk( std::vector< Node >& vals, bool pol = true );
    std::map< unsigned, unsigned > d_next;
    unsigned start();
    unsigned next( unsigned i );
    void clear() { d_next.clear(); }
    bool isEq( std::vector< Node >& vs, Node v );
  };
  // subsumption trie
  class SubsumeTrie {
  public:
    SubsumeTrie(){}
    // adds term to the trie, removes based on subsumption
    Node addTerm( CegConjecturePbe * pbe, Node t, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed, IndexFilter * f = NULL );
    // adds condition to the trie (does not do subsumption)
    Node addCond( CegConjecturePbe * pbe, Node c, std::vector< Node >& vals, bool pol, IndexFilter * f = NULL );
    // returns the set of terms that are subsets of vals
    void getSubsumed( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed, IndexFilter * f = NULL );
    // returns the set of terms that are supersets of vals
    void getSubsumedBy( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed_by, IndexFilter * f = NULL );
    // v[-1,1,0] -> children always false, always true, both
    void getLeaves( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::map< int, std::vector< Node > >& v, IndexFilter * f = NULL );
    /** is this trie empty? */
    bool isEmpty() { return d_term.isNull() && d_children.empty(); }
    /** clear this trie */
    void clear() {
      d_term = Node::null();
      d_children.clear(); 
    }

   private:
    /** the term at this node */
    Node d_term;
    /** the children nodes of this trie */
    std::map<Node, SubsumeTrie> d_children;
    /** helper function for above functions */
    Node addTermInternal(CegConjecturePbe* pbe,
                         Node t,
                         std::vector<Node>& vals,
                         bool pol,
                         std::vector<Node>& subsumed,
                         bool spol,
                         IndexFilter* f,
                         unsigned index,
                         int status,
                         bool checkExistsOnly,
                         bool checkSubsume);
    /** helper function for above functions */
    void getLeavesInternal(CegConjecturePbe* pbe,
                           std::vector<Node>& vals,
                           bool pol,
                           std::map<int, std::vector<Node> >& v,
                           IndexFilter* f,
                           unsigned index,
                           int status);
  };
  // -------------------------------- end decision tree learning

  //------------------------------ representation of a enumeration strategy

  /** information about an enumerator
   *
   * We say an enumerator is a master enumerator if it is the variable that
   * we use to enumerate values for its sort. Master enumerators may have
   * (possibly multiple) slave enumerators, stored in d_enum_slave,
   */
  class EnumInfo {
  public:
    EnumInfo() : d_role( enum_io ){}
    /** initialize this class
    * c is the parent function-to-synthesize
    * role is the "role" the enumerator plays in the high-level strategy,
    *   which is one of enum_* above.
    */
    void initialize(Node c, EnumRole role);
    bool isTemplated() { return !d_template.isNull(); }
    void addEnumValue(CegConjecturePbe* pbe,
                      Node v,
                      std::vector<Node>& results);
    void setSolved(Node slv);
    bool isSolved() { return !d_enum_solved.isNull(); }
    Node getSolved() { return d_enum_solved; }
    EnumRole getRole() { return d_role; }
    Node d_parent_candidate;
    // for template
    Node d_template;
    Node d_template_arg;
    
    Node d_active_guard;
    std::vector< Node > d_enum_slave;
    /** values we have enumerated */
    std::vector< Node > d_enum_vals;
    /**
     * This either stores the values of f( I ) for inputs
     * or the value of f( I ) = O if d_role==enum_io
     */
    std::vector< std::vector< Node > > d_enum_vals_res;
    std::vector< Node > d_enum_subsume;
    std::map< Node, unsigned > d_enum_val_to_index;
    SubsumeTrie d_term_trie;

   private:
    /** whether an enumerated value for this conjecture has solved the entire
     * conjecture */
    Node d_enum_solved;
    /** the role of this enumerator (one of enum_* above). */
    EnumRole d_role;
  };
  /** maps enumerators to the information above */
  std::map< Node, EnumInfo > d_einfo;

  class CandidateInfo;

  /** represents a strategy for a SyGuS datatype type
   *
   * This represents a possible strategy to apply when processing a strategy
   * node in constructSolution. When applying the strategy represented by this
   * class, we may make recursive calls to the children of the strategy,
   * given in d_cenum. If all recursive calls to constructSolution are
   * successful, say:
   *   constructSolution( c, d_cenum[1], ... ) = t1,
   *    ...,
   *   constructSolution( c, d_cenum[n], ... ) = tn,
   * Then, the solution returned by this strategy is
   *   d_sol_templ * { d_sol_templ_args -> (t1,...,tn) }
   */
  class EnumTypeInfoStrat {
   public:
    /** the type of strategy this represents */
    StrategyType d_this;
    /** the sygus datatype constructor that induced this strategy
     *
     * For example, this may be a sygus datatype whose sygus operator is ITE,
     * if the strategy type above is strat_ITE.
     */
    Node d_cons;
    /** children of this strategy */
    std::vector<std::pair<Node, NodeRole> > d_cenum;
    /** the arguments for the (templated) solution */
    std::vector<Node> d_sol_templ_args;
    /** the template for the solution */
    Node d_sol_templ;
  };

  /** represents a node in the strategy graph
   *
   * It contains a list of possible strategies which are tried during calls
   * to constructSolution.
   */
  class StrategyNode
  {
   public:
    StrategyNode() {}
    ~StrategyNode();
    /** the set of strategies to try at this node in the strategy graph */
    std::vector<EnumTypeInfoStrat*> d_strats;
  };

  /** stores enumerators and strategies for a SyGuS datatype type */
  class EnumTypeInfo {
  public:
    EnumTypeInfo() : d_parent( NULL ){}
    /** the parent candidate info (see below) */
    CandidateInfo * d_parent;
    /** the type that this information is for */
    TypeNode d_this_type;
    /** map from enum roles to enumerators for this type */
    std::map<EnumRole, Node> d_enum;
    /** map from node roles to strategy nodes */
    std::map<NodeRole, StrategyNode> d_snodes;
  };

  /** stores strategy and enumeration information for a function-to-synthesize
   */
  class CandidateInfo {
  public:
    CandidateInfo() : d_check_sol( false ), d_cond_count( 0 ){}
    Node d_this_candidate;
    /**
     * The root sygus datatype for the function-to-synthesize,
     * which encodes the overall syntactic restrictions on the space
     * of solutions.
     */
    TypeNode d_root;
    /** Info for sygus datatype type occurring in a field of d_root */
    std::map< TypeNode, EnumTypeInfo > d_tinfo;
    /** list of all enumerators for the function-to-synthesize */
    std::vector< Node > d_esym_list;
    /**
     * Maps sygus datatypes to their search enumerator. This is the (single)
     * enumerator of that type that we enumerate values for.
     */
    std::map< TypeNode, Node > d_search_enum;
    bool d_check_sol;
    unsigned d_cond_count;
    Node d_solution;
    void initialize( Node c );
    void initializeType( TypeNode tn );
    Node getRootEnumerator();
    bool isNonTrivial();
  };
  /** maps a function-to-synthesize to the above information */
  std::map< Node, CandidateInfo > d_cinfo;

  //------------------------------ representation of an enumeration strategy
  /** add enumerated value */
  void addEnumeratedValue( Node x, Node v, std::vector< Node >& lems );
  bool getExplanationForEnumeratorExclude( Node c, Node x, Node v, std::vector< Node >& results, EnumInfo& ei, std::vector< Node >& exp );

  //------------------------------ strategy registration
  /** collect enumerator types
   *
   * This builds the strategy for enumerated values of type tn for the given
   * role of nrole, for solutions to function-to-synthesize c.
   */
  void collectEnumeratorTypes(Node c, TypeNode tn, NodeRole nrole);
  /** register enumerator
   *
   * This registers that et is an enumerator for function-to-synthesize c
   * of type tn, having enumerator role enum_role.
   *
   * inSearch is whether we will enumerate values based on this enumerator.
   * A strategy node is represented by a (enumerator, node role) pair. Hence,
   * we may use enumerators for which this flag is false to represent strategy
   * nodes that have child strategies.
   */
  void registerEnumerator(
      Node et, Node c, TypeNode tn, EnumRole enum_role, bool inSearch);
  /** infer template */
  bool inferTemplate(unsigned k,
                     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 c, and stores these into lemmas.
   */
  void staticLearnRedundantOps(Node c, std::vector<Node>& lemmas);
  /** helper for static learn redundant operators
   *
   * (e, nrole) specify the strategy node in the graph we are currently
   * analyzing, visited stores the nodes we have already visited.
   *
   * 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).
   */
  void staticLearnRedundantOps(
      Node c,
      Node e,
      NodeRole nrole,
      std::map<Node, std::map<NodeRole, bool> >& visited,
      std::map<Node, std::map<unsigned, bool> >& needs_cons,
      int ind);
  //------------------------------ end strategy registration

  //------------------------------ constructing solutions
  class UnifContext {
  public:
   UnifContext() : d_has_string_pos(role_invalid) {}
   /** this intiializes this context for function-to-synthesize c */
   void initialize(CegConjecturePbe* pbe, Node c);

   //----------for ITE strategy
   /** the value of the context conditional
    *
    * This stores a list of Boolean constants that is the same length of the
    * number of input/output example pairs we are considering. For each i,
    * if d_vals[i] = true, i/o pair #i is active according to this context
    * if d_vals[i] = false, i/o pair #i is inactive according to this context
    */
   std::vector<Node> d_vals;
   /** update the examples
    *
    * if pol=true, this method updates d_vals to d_vals & vals
    * if pol=false, this method updates d_vals to d_vals & ( ~vals )
    */
   bool updateContext(CegConjecturePbe* pbe, std::vector<Node>& vals, bool pol);
   //----------end for ITE strategy

   //----------for CONCAT strategies
   /** the position in the strings
    *
    * For each i/o example pair, this stores the length of the current solution
    * for the input of the pair, where the solution for that input is a prefix
    * or
    * suffix of the output of the pair. For example, if our i/o pairs are:
    *   f( "abcd" ) = "abcdcd"
    *   f( "aa" ) = "aacd"
    * If the solution we have currently constructed is str.++( x1, "c", ... ),
    * then d_str_pos = ( 5, 3 ), where notice that
    *   str.++( "abc", "c" ) is a prefix of "abcdcd" and
    *   str.++( "aa", "c" ) is a prefix of "aacd".
    */
   std::vector<unsigned> d_str_pos;
   /** has string position
    *
    * Whether the solution positions indicate a prefix or suffix of the output
    * examples. If this is role_invalid, then we have not updated the string
    * position.
    */
   NodeRole d_has_string_pos;
   /** update the string examples
    *
    * This method updates d_str_pos to d_str_pos + pos.
    */
   bool updateStringPosition(CegConjecturePbe* pbe, std::vector<unsigned>& pos);
   /** get current strings
    *
    * This returns the prefix/suffix of the string constants stored in vals
    * of size d_str_pos, and stores the result in ex_vals. For example, if vals
    * is (abcdcd", "aacde") and d_str_pos = ( 5, 3 ), then we add
    * "d" and "de" to ex_vals.
    */
   void getCurrentStrings(CegConjecturePbe* pbe,
                          const std::vector<Node>& vals,
                          std::vector<String>& ex_vals);
   /** get string increment
    *
    * If this method returns true, then inc and tot are updated such that
    *   for all active indices i,
    *      vals[i] is a prefix (or suffix if isPrefix=false) of ex_vals[i], and
    *      inc[i] = str.len(vals[i])
    *   for all inactive indices i, inc[i] = 0
    * We set tot to the sum of inc[i] for i=1,...,n. This indicates the total
    * number of characters incremented across all examples.
    */
   bool getStringIncrement(CegConjecturePbe* pbe,
                           bool isPrefix,
                           const std::vector<String>& ex_vals,
                           const std::vector<Node>& vals,
                           std::vector<unsigned>& inc,
                           unsigned& tot);
   /** returns true if ex_vals[i] = vals[i] for all active indices i. */
   bool isStringSolved(CegConjecturePbe* pbe,
                       const std::vector<String>& ex_vals,
                       const std::vector<Node>& vals);
   //----------end for CONCAT strategies

   /** is return value modified?
    *
    * This returns true if we are currently in a state where the return value
    * of the solution has been modified, e.g. by a previous node that solved
    * for a prefix.
    */
   bool isReturnValueModified();
   /** returns true if argument is valid strategy in this context */
   bool isValidStrategy(EnumTypeInfoStrat* etis);
   /** visited role
    *
    * This is the current set of enumerator/node role pairs we are currently
    * visiting. This set is cleared when the context is updated.
    */
   std::map<Node, std::map<NodeRole, bool> > d_visit_role;

   /** unif context enumerator information */
   class UEnumInfo
   {
    public:
     UEnumInfo() {}
     /** map from conditions and branch positions to a solved node
      *
      * For example, if we have:
      *   f( 1 ) = 2 ^ f( 3 ) = 4 ^ f( -1 ) = 1
      * Then, valid entries in this map is:
      *   d_look_ahead_sols[x>0][1] = x+1
      *   d_look_ahead_sols[x>0][2] = 1
      * For the first entry, notice that  for all input examples such that x>0
      * evaluates to true, which are (1) and (3), we have that their output
      * values for x+1 under the substitution that maps x to the input value,
      * resulting in 2 and 4, are equal to the output value for the respective
      * pairs.
      */
     std::map<Node, std::map<unsigned, Node> > d_look_ahead_sols;
    };
    /** map from enumerators to the above info class */
    std::map< Node, UEnumInfo > d_uinfo;
  };

  /** construct solution
   *
   * This method tries to construct a solution for function-to-synthesize c
   * based on the strategy stored for c in d_cinfo, which may include
   * synthesis-by-unification approaches for ite and string concatenation terms.
   * These approaches include the work of Alur et al. TACAS 2017.
   * If it cannot construct a solution, it returns the null node.
   */
  Node constructSolution( Node c );
  /** helper function for construct solution.
   *
   * Construct a solution based on enumerator e for function-to-synthesize c
   * with node role nrole in context x.
   *
   * ind is the term depth of the context (for debugging).
   */
  Node constructSolution(
      Node c, Node e, NodeRole nrole, UnifContext& x, int ind);
  /** Heuristically choose the best solved term from solved in context x,
   * currently return the first. */
  Node constructBestSolvedTerm( std::vector< Node >& solved, UnifContext& x );
  /** Heuristically choose the best solved string term  from solved in context
   * x, currently  return the first. */
  Node constructBestStringSolvedTerm( std::vector< Node >& solved, UnifContext& x );
  /** Heuristically choose the best solved conditional term  from solved in
   * context x, currently random */
  Node constructBestSolvedConditional( std::vector< Node >& solved, UnifContext& x );
  /** Heuristically choose the best conditional term  from conds in context x,
   * currently random */
  Node constructBestConditional( std::vector< Node >& conds, UnifContext& x );
  /** Heuristically choose the best string to concatenate from strs to the
  * solution in context x, currently random
  * incr stores the vector of indices that are incremented by this solution in
  * example outputs.
  * total_inc[x] is the sum of incr[x] for each x in strs.
  */
  Node constructBestStringToConcat( std::vector< Node > strs,
                                    std::map< Node, unsigned > total_inc, 
                                    std::map< Node, std::vector< unsigned > > incr,
                                    UnifContext& x );
  //------------------------------ end constructing solutions
};

}/* namespace CVC4::theory::quantifiers */
}/* namespace CVC4::theory */
}/* namespace CVC4 */

#endif