1 /********************* */
2 /*! \file sygus_datatype_utils.h
4 ** Top contributors (to current version):
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
12 ** \brief Util functions for sygus datatypes
15 #include "cvc4_private.h"
17 #ifndef CVC4__THEORY__STRINGS__SYGUS_DATATYPE_UTILS_H
18 #define CVC4__THEORY__STRINGS__SYGUS_DATATYPE_UTILS_H
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"
30 // ----------------------- sygus datatype attributes
32 struct SygusVarNumAttributeId
35 typedef expr::Attribute
<SygusVarNumAttributeId
, uint64_t> SygusVarNumAttribute
;
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.
43 struct SygusSymBreakOkAttributeId
46 typedef expr::Attribute
<SygusSymBreakOkAttributeId
, bool>
47 SygusSymBreakOkAttribute
;
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.
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.
64 * This attribute is used to compute applySygusArgs below.
66 struct SygusVarFreeAttributeId
69 typedef expr::Attribute
<SygusVarFreeAttributeId
, Node
> SygusVarFreeAttribute
;
70 // ----------------------- end sygus datatype attributes
76 /** get operator kind for sygus builtin
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.
82 Kind
getOperatorKindForSygusBuiltin(Node op
);
84 * Returns the total version of Kind k if it is a partial operator, or
87 Kind
getEliminateKind(Kind k
);
89 * Returns a version of n where all partial functions such as bvudiv
90 * have been replaced by their total versions like bvudiv_total.
92 Node
eliminatePartialOperators(Node n
);
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
100 * If isExternal is true, then the returned term respects the original grammar
101 * that was provided. This includes the use of defined functions.
103 Node
mkSygusTerm(const DType
& dt
,
105 const std::vector
<Node
>& children
,
106 bool doBetaReduction
= true,
107 bool isExternal
= false);
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().
112 Node
mkSygusTerm(Node op
,
113 const std::vector
<Node
>& children
,
114 bool doBetaReduction
= true);
116 * n is a builtin term that is a (rewritten) application of operator op.
118 * This returns an n' such that (eval n args) is n', where n' is a instance of
119 * n for the appropriate substitution.
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 } )
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.
142 Node
applySygusArgs(const DType
& dt
,
145 const std::vector
<Node
>& args
);
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
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.
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).
162 Node
sygusToBuiltin(Node n
, bool isExternal
= false);
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
170 Node
builtinVarToSygus(Node v
);
172 /** Sygus to builtin eval
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.
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
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.
193 Node
sygusToBuiltinEval(Node n
, const std::vector
<Node
>& args
);
195 /** Get free symbols in a sygus datatype type
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
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.
204 void getFreeSymbolsSygusType(TypeNode sdt
,
205 std::unordered_set
<Node
, NodeHashFunction
>& syms
);
207 /** Substitute and generalize a sygus datatype type
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.
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.
216 * The variables in vars of type BOUND_VARIABLE are added to the
217 * formal argument list of t. Other symbols are not.
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'.
228 * This method traverses the type definition of the datatype corresponding to
231 TypeNode
substituteAndGeneralizeSygusType(TypeNode sdt
,
232 const std::vector
<Node
>& syms
,
233 const std::vector
<Node
>& vars
);
235 // ------------------------ end sygus utils
238 } // namespace datatypes
239 } // namespace theory