Sample based on sygus grammar by default (#1558)

1 files changed, 69 insertions, 15 deletions

diff --git a/src/theory/quantifiers/term_database_sygus.h b/src/theory/quantifiers/term_database_sygus.h
index 586ef0777..af1ef50b6 100644
--- a/src/theory/quantifiers/term_database_sygus.h
+++ b/src/theory/quantifiers/term_database_sygus.h
@@ -68,6 +68,56 @@ class TermDbSygus {
   SygusExplain* getExplain() { return d_syexp.get(); }
   /** get the extended rewrite utility */
   ExtendedRewriter* getExtRewriter() { return d_ext_rw.get(); }
+  //-----------------------------conversion from sygus to builtin
+  /** get free variable
+   *
+   * This class caches a list of free variables for each type, which are
+   * used, for instance, for constructing canonical forms of terms with free
+   * variables. This function returns the i^th free variable for type tn.
+   * If useSygusType is true, then this function returns a variable of the
+   * analog type for sygus type tn (see d_fv for details).
+   */
+  TNode getFreeVar(TypeNode tn, int i, bool useSygusType = false);
+  /** get free variable and increment
+   *
+   * This function returns the next free variable for type tn, and increments
+   * the counter in var_count for that type.
+   */
+  TNode getFreeVarInc(TypeNode tn,
+                      std::map<TypeNode, int>& var_count,
+                      bool useSygusType = false);
+  /** returns true if n is a cached free variable (in d_fv). */
+  bool isFreeVar(Node n) { return d_fv_stype.find(n) != d_fv_stype.end(); }
+  /** returns the index of n in the free variable cache (d_fv). */
+  int getVarNum(Node n) { return d_fv_num[n]; }
+  /** returns true if n has a cached free variable (in d_fv). */
+  bool hasFreeVar(Node n);
+  /** make generic
+   *
+   * This function returns a builtin term f( t1, ..., tn ) where f is the
+   * builtin op of the sygus datatype constructor specified by arguments
+   * dt and c. The mapping pre maps child indices to the term for that index
+   * in the term we are constructing. That is, for each i = 1,...,n:
+   *   If i is in the domain of pre, then ti = pre[i].
+   *   If i is not in the domain of pre, then ti = d_fv[1][ var_count[Ti ] ],
+   *     and var_count[Ti] is incremented.
+   */
+  Node mkGeneric(const Datatype& dt,
+                 int c,
+                 std::map<TypeNode, int>& var_count,
+                 std::map<int, Node>& pre);
+  /** same as above, but with empty var_count */
+  Node mkGeneric(const Datatype& dt, int c, std::map<int, Node>& pre);
+  /** sygus to builtin
+   *
+   * Given a sygus datatype term n of type tn, this function returns its analog,
+   * that is, the term that n encodes.
+   */
+  Node sygusToBuiltin(Node n, TypeNode tn);
+  /** same as above, but without tn */
+  Node sygusToBuiltin(Node n) { return sygusToBuiltin(n, n.getType()); }
+  //-----------------------------end conversion from sygus to builtin
+
  private:
   /** reference to the quantifiers engine */
   QuantifiersEngine* d_quantEngine;
@@ -88,23 +138,31 @@ class TermDbSygus {
    */
   std::map<Node, Node> d_enum_to_active_guard;
 
+  //-----------------------------conversion from sygus to builtin
+  /** cache for sygusToBuiltin */
+  std::map<TypeNode, std::map<Node, Node> > d_sygus_to_builtin;
+  /** a cache of fresh variables for each type
+   *
+   * We store two versions of this list:
+   *   index 0: mapping from builtin types to fresh variables of that type,
+   *   index 1: mapping from sygus types to fresh varaibles of the type they
+   *            encode.
+   */
+  std::map<TypeNode, std::vector<Node> > d_fv[2];
+  /** Maps free variables to the domain type they are associated with in d_fv */
+  std::map<Node, TypeNode> d_fv_stype;
+  /** Maps free variables to their index in d_fv. */
+  std::map<Node, int> d_fv_num;
+  /** recursive helper for hasFreeVar, visited stores nodes we have visited. */
+  bool hasFreeVar(Node n, std::map<Node, bool>& visited);
+  //-----------------------------end conversion from sygus to builtin
+
   // TODO :issue #1235 : below here needs refactor
 
  public:
   Node d_true;
   Node d_false;
 
- private:
-  std::map< TypeNode, std::vector< Node > > d_fv[2];
-  std::map< Node, TypeNode > d_fv_stype;
-  std::map< Node, int > d_fv_num;
-  bool hasFreeVar( Node n, std::map< Node, bool >& visited );
-public:
-  TNode getFreeVar( TypeNode tn, int i, bool useSygusType = false );
-  TNode getFreeVarInc( TypeNode tn, std::map< TypeNode, int >& var_count, bool useSygusType = false );
-  bool isFreeVar( Node n ) { return d_fv_stype.find( n )!=d_fv_stype.end(); }
-  int getVarNum( Node n ) { return d_fv_num[n]; }
-  bool hasFreeVar( Node n );
 private:
   void computeMinTypeDepthInternal( TypeNode root_tn, TypeNode tn, unsigned type_depth );
   bool involvesDivByZero( Node n, std::map< Node, bool >& visited );
@@ -122,7 +180,6 @@ private:
   std::map<TypeNode, std::map<Node, Node> > d_semantic_skolem;
   // normalized map
   std::map<TypeNode, std::map<Node, Node> > d_normalized;
-  std::map<TypeNode, std::map<Node, Node> > d_sygus_to_builtin;
   // grammar information
   // root -> type -> _
   std::map<TypeNode, std::map<TypeNode, unsigned> > d_min_type_depth;
@@ -165,9 +222,6 @@ private:
   bool isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 );
 
   TypeNode getSygusTypeForVar( Node v );
-  Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre );
-  Node sygusToBuiltin( Node n, TypeNode tn );
-  Node sygusToBuiltin( Node n ) { return sygusToBuiltin( n, n.getType() ); }
   Node sygusSubstituted( TypeNode tn, Node n, std::vector< Node >& args );
   Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs );
   Node getNormalized(TypeNode t, Node prog);