src/theory/datatypes/sygus_datatype_utils.h

   1 /*********************                                                        */
   2 /*! \file sygus_datatype_utils.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Util functions for sygus datatypes
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__STRINGS__SYGUS_DATATYPE_UTILS_H
  18 #define CVC4__THEORY__STRINGS__SYGUS_DATATYPE_UTILS_H
  19
  20 #include <vector>
  21
  22 #include "expr/dtype.h"
  23 #include "expr/node.h"
  24 #include "expr/node_manager_attributes.h"
  25 #include "theory/datatypes/theory_datatypes_utils.h"
  26
  27 namespace CVC4 {
  28 namespace theory {
  29
  30 // ----------------------- sygus datatype attributes
  31 /** sygus var num */
  32 struct SygusVarNumAttributeId
  33 {
  34 };
  35 typedef expr::Attribute<SygusVarNumAttributeId, uint64_t> SygusVarNumAttribute;
  36
  37 /**
  38  * Attribute true for enumerators whose current model values were registered by
  39  * the datatypes sygus solver, and were not excluded by sygus symmetry breaking.
  40  * This is set by the datatypes sygus solver during LAST_CALL effort checks for
  41  * each active sygus enumerator.
  42  */
  43 struct SygusSymBreakOkAttributeId
  44 {
  45 };
  46 typedef expr::Attribute<SygusSymBreakOkAttributeId, bool>
  47     SygusSymBreakOkAttribute;
  48
  49 /** sygus var free
  50  *
  51  * This attribute is used to mark whether sygus operators have free occurrences
  52  * of variables from the formal argument list of the function-to-synthesize.
  53  *
  54  * We store three possible cases for sygus operators op:
  55  * (1) op.getAttribute(SygusVarFreeAttribute())==Node::null()
  56  * In this case, op has no free variables from the formal argument list of the
  57  * function-to-synthesize.
  58  * (2) op.getAttribute(SygusVarFreeAttribute())==v, where v is a bound variable.
  59  * In this case, op has exactly one free variable, v.
  60  * (3) op.getAttribute(SygusVarFreeAttribute())==op
  61  * In this case, op has an arbitrary set (cardinality >1) of free variables from
  62  * the formal argument list of the function to synthesize.
  63  *
  64  * This attribute is used to compute applySygusArgs below.
  65  */
  66 struct SygusVarFreeAttributeId
  67 {
  68 };
  69 typedef expr::Attribute<SygusVarFreeAttributeId, Node> SygusVarFreeAttribute;
  70 // ----------------------- end sygus datatype attributes
  71
  72 namespace datatypes {
  73 namespace utils {
  74
  75
  76 /** get operator kind for sygus builtin
  77  *
  78  * This returns the Kind corresponding to applications of the operator op
  79  * when building the builtin version of sygus terms. This is used by the
  80  * function mkSygusTerm.
  81  */
  82 Kind getOperatorKindForSygusBuiltin(Node op);
  83 /**
  84  * Returns the total version of Kind k if it is a partial operator, or
  85  * otherwise k itself.
  86  */
  87 Kind getEliminateKind(Kind k);
  88 /**
  89  * Returns a version of n where all partial functions such as bvudiv
  90  * have been replaced by their total versions like bvudiv_total.
  91  */
  92 Node eliminatePartialOperators(Node n);
  93 /** make sygus term
  94  *
  95  * This function returns a builtin term f( children[0], ..., children[n] )
  96  * where f is the builtin op that the i^th constructor of sygus datatype dt
  97  * encodes. If doBetaReduction is true, then lambdas are eagerly eliminated
  98  * via beta reduction.
  99  *
 100  * If isExternal is true, then the returned term respects the original grammar
 101  * that was provided. This includes the use of defined functions.
 102  */
 103 Node mkSygusTerm(const DType& dt,
 104                  unsigned i,
 105                  const std::vector<Node>& children,
 106                  bool doBetaReduction = true,
 107                  bool isExternal = false);
 108 /**
 109  * Same as above, but we already have the sygus operator op. The above method
 110  * is syntax sugar for calling this method on dt[i].getSygusOp().
 111  */
 112 Node mkSygusTerm(Node op,
 113                  const std::vector<Node>& children,
 114                  bool doBetaReduction = true);
 115 /**
 116  * n is a builtin term that is a (rewritten) application of operator op.
 117  *
 118  * This returns an n' such that (eval n args) is n', where n' is a instance of
 119  * n for the appropriate substitution.
 120  *
 121  * For example, given a function-to-synthesize with formal argument list (x,y),
 122  * say we have grammar:
 123  *   A -> A+A | A+x | A+(x+y) | y
 124  * These lead to constructors with sygus ops:
 125  *   C1 / L1 where L1 is (lambda w1 w2. w1+w2)
 126  *   C2 / L2 where L2 is (lambda w1. w1+x)
 127  *   C3 / L3 where L3 is (lambda w1. w1+(x+y))
 128  *   C4 / L4 where L4 is y
 129  * Examples of calling this function:
 130  *   applySygusArgs( dt, L1, (APPLY_UF L1 t1 t2), { 3, 5 } )
 131  *     ... returns (APPLY_UF (lambda w1 w2. w1+w2) t1 t2).
 132  *   applySygusArgs( dt, L2, (APPLY_UF L2 t1), { 3, 5 } )
 133  *     ... returns (APPLY_UF (lambda w1. w1+3) t1).
 134  *   applySygusArgs( dt, L3, (APPLY_UF L3 t1), { 3, 5 } )
 135  *     ... returns (APPLY_UF (lambda w1. w1+(3+5)) t1).
 136  *   applySygusArgs( dt, L4, L4, { 3, 5 } )
 137  *     ... returns 5.
 138  * Notice the attribute SygusVarFreeAttribute is applied to C1, C2, C3, C4,
 139  * to cache the results of whether the evaluation of this constructor needs
 140  * a substitution over the formal argument list of the function-to-synthesize.
 141  */
 142 Node applySygusArgs(const DType& dt,
 143                     Node op,
 144                     Node n,
 145                     const std::vector<Node>& args);
 146 /** Sygus to builtin
 147  *
 148  * This method converts a term n of SyGuS datatype type to its builtin
 149  * equivalent. For example, given input C_*( C_x(), C_y() ), this method returns
 150  * x*y, assuming C_+, C_x, and C_y have sygus operators *, x, and y
 151  * respectively.
 152  *
 153  * If isExternal is true, then the returned term respects the original grammar
 154  * that was provided. This includes the use of defined functions. This argument
 155  * should typically be false, unless we are e.g. exporting the value of the
 156  * term as a final solution.
 157  *
 158  * If n is not constant, then its non-constant subterms that have sygus
 159  * datatype types are replaced by fresh variables (of the same name, if that
 160  * subterm is a variable, and having arbitrary name otherwise).
 161  */
 162 Node sygusToBuiltin(Node n, bool isExternal = false);
 163
 164 /**
 165  * Builtin variable to sygus. Converts from builtin variables introduced by
 166  * the method above to their source, which is a sygus variable. It should
 167  * be the case that v is a variable introduced by the above method, or otherwise
 168  * null is returned.
 169  */
 170 Node builtinVarToSygus(Node v);
 171
 172 /** Sygus to builtin eval
 173  *
 174  * This method returns the rewritten form of (DT_SYGUS_EVAL n args). Notice that
 175  * n does not necessarily need to be a constant.
 176  *
 177  * It does so by (1) converting constant subterms of n to builtin terms and
 178  * evaluating them on the arguments args, (2) unfolding non-constant
 179  * applications of sygus constructors in n with respect to args and (3)
 180  * converting all other non-constant subterms of n to applications of
 181  * DT_SYGUS_EVAL.
 182  *
 183  * For example, if
 184  *   n = C_+( C_*( C_x(), C_y() ), n' ), and args = { 3, 4 }
 185  * where n' is a variable, then this method returns:
 186  *   12 + (DT_SYGUS_EVAL n' 3 4)
 187  * Notice that the subterm C_*( C_x(), C_y() ) is converted to its builtin
 188  * equivalent x*y and evaluated under the substition { x -> 3, y -> 4 } giving
 189  * 12. The subterm n' is non-constant and thus we return its evaluation under
 190  * 3,4, giving the term (DT_SYGUS_EVAL n' 3 4). Since the top-level constructor
 191  * is C_+, these terms are added together to give the result.
 192  */
 193 Node sygusToBuiltinEval(Node n, const std::vector<Node>& args);
 194
 195 /** Get free symbols in a sygus datatype type
 196  *
 197  * Add the free symbols (expr::getSymbols) in terms that can be generated by
 198  * sygus datatype sdt to the set syms. For example, given sdt encodes the
 199  * grammar:
 200  *   G -> a | +( b, G ) | c | e
 201  * We have that { a, b, c, e } are added to syms. Notice that expr::getSymbols
 202  * excludes variables whose kind is BOUND_VARIABLE.
 203  */
 204 void getFreeSymbolsSygusType(TypeNode sdt,
 205                              std::unordered_set<Node, NodeHashFunction>& syms);
 206
 207 /** Substitute and generalize a sygus datatype type
 208  *
 209  * This transforms a sygus datatype sdt into another one sdt' that generates
 210  * terms t such that t * { vars -> syms } is generated by sdt.
 211  *
 212  * The arguments syms and vars should be vectors of the same size and types.
 213  * It is recommended that the arguments in syms and vars should be variables
 214  * (return true for .isVar()) but this is not required.
 215  *
 216  * The variables in vars of type BOUND_VARIABLE are added to the
 217  * formal argument list of t. Other symbols are not.
 218  *
 219  * For example, given sdt encodes the grammar:
 220  *   G -> a | +( b, G ) | c | e
 221  * Let syms = { a, b, c } and vars = { x_a, x_b, d }, where x_a and x_b have
 222  * type BOUND_VARIABLE and d does not.
 223  * The returned type encodes the grammar:
 224  *   G' -> x_a | +( x_b, G' ) | d | e
 225  * Additionally, x_a and x_b are treated as formal arguments of a function
 226  * to synthesize whose syntax restrictions are specified by G'.
 227  *
 228  * This method traverses the type definition of the datatype corresponding to
 229  * the argument sdt.
 230  */
 231 TypeNode substituteAndGeneralizeSygusType(TypeNode sdt,
 232                                           const std::vector<Node>& syms,
 233                                           const std::vector<Node>& vars);
 234
 235 // ------------------------ end sygus utils
 236
 237 }  // namespace utils
 238 }  // namespace datatypes
 239 }  // namespace theory
 240 }  // namespace CVC4
 241
 242 #endif