Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Gereon Kremer
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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.
11 : : * ****************************************************************************
12 : : *
13 : : * sygus explanations
14 : : */
15 : :
16 : : #include "cvc5_private.h"
17 : :
18 : : #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H
19 : : #define CVC5__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H
20 : :
21 : : #include <vector>
22 : :
23 : : #include "expr/node.h"
24 : : #include "smt/env_obj.h"
25 : :
26 : : namespace cvc5::internal {
27 : : namespace theory {
28 : : namespace quantifiers {
29 : :
30 : : class SygusInvarianceTest;
31 : : class TermDbSygus;
32 : :
33 : : /** Recursive term builder
34 : : *
35 : : * This is a utility used to generate variants
36 : : * of a term n, where subterms of n can be replaced
37 : : * by others via calls to replaceChild(...).
38 : : *
39 : : * This class maintains a "context", which indicates
40 : : * a position in term n. Below, we call the subterm of
41 : : * the initial term n at this position the "active term".
42 : : *
43 : : */
44 : : class TermRecBuild
45 : : {
46 : : public:
47 : 26298 : TermRecBuild(NodeManager* nm) : d_nm(nm) {}
48 : : /** set the initial term to n
49 : : *
50 : : * The context initially empty, that is,
51 : : * the active term is initially n.
52 : : */
53 : : void init(Node n);
54 : :
55 : : /** push the context
56 : : *
57 : : * This updates the context so that the
58 : : * active term is updated to curr[p], where
59 : : * curr is the previously active term.
60 : : */
61 : : void push(unsigned p);
62 : :
63 : : /** pop the context */
64 : : void pop();
65 : : /** indicates that the i^th child of the active
66 : : * term should be replaced by r in calls to build().
67 : : */
68 : : void replaceChild(unsigned i, Node r);
69 : : /** get the i^th child of the active term */
70 : : Node getChild(unsigned i);
71 : : /** build the (modified) version of the term
72 : : * we initialized via the call to init().
73 : : */
74 : : Node build(unsigned p = 0);
75 : :
76 : : private:
77 : : /** Pointer to the node manager */
78 : : NodeManager* d_nm;
79 : : /** stack of active terms */
80 : : std::vector<Node> d_term;
81 : : /** stack of children of active terms
82 : : * Notice that these may be modified with calls to replaceChild(...).
83 : : */
84 : : std::vector<std::vector<Node> > d_children;
85 : : /** stack the kind of active terms */
86 : : std::vector<Kind> d_kind;
87 : : /** stack of whether the active terms had an operator */
88 : : std::vector<bool> d_has_op;
89 : : /** stack of positions that were pushed via calls to push(...) */
90 : : std::vector<unsigned> d_pos;
91 : : /** add term to the context stack */
92 : : void addTerm(Node n);
93 : : };
94 : :
95 : : /*The SygusExplain utility
96 : : *
97 : : * This class is used to produce explanations for refinement lemmas
98 : : * in the counterexample-guided inductive synthesis (CEGIS) loop.
99 : : *
100 : : * When given an invariance test T traverses the AST of a given term,
101 : : * uses TermRecBuild to replace various subterms by fresh variables and
102 : : * recheck whether the invariant, as specified by T still holds.
103 : : * If it does, then we may exclude the explanation for that subterm.
104 : : *
105 : : * For example, say we have that the current value of
106 : : * (datatype) sygus term n is:
107 : : * (if (gt x 0) 0 0)
108 : : * where if, gt, x, 0 are datatype constructors.
109 : : * The explanation returned by getExplanationForEquality
110 : : * below for n and the above term is:
111 : : * { ((_ is if) n), ((_ is geq) n.0),
112 : : * ((_ is x) n.0.0), ((_ is 0) n.0.1),
113 : : * ((_ is 0) n.1), ((_ is 0) n.2) }
114 : : *
115 : : * This class can also return more precise
116 : : * explanations based on a property that holds for
117 : : * variants of n. For instance,
118 : : * say we find that n's builtin analog rewrites to 0:
119 : : * ite( x>0, 0, 0 ) ----> 0
120 : : * and we would like to find the minimal explanation for
121 : : * why the builtin analog of n rewrites to 0.
122 : : * We use the invariance test EquivSygusInvarianceTest
123 : : * (see sygus_invariance.h) for doing this.
124 : : * Using the SygusExplain::getExplanationFor method below,
125 : : * this will invoke the invariant test to check, e.g.
126 : : * ite( x>0, 0, y1 ) ----> 0 ? fail
127 : : * ite( x>0, y2, 0 ) ----> 0 ? fail
128 : : * ite( y3, 0, 0 ) ----> 0 ? success
129 : : * where y1, y2, y3 are fresh variables.
130 : : * Hence the explanation for the condition x>0 is irrelevant.
131 : : * This gives us the explanation:
132 : : * { ((_ is if) n), ((_ is 0) n.1), ((_ is 0) n.2) }
133 : : * indicating that all terms of the form:
134 : : * (if _ 0 0) have a builtin equivalent that rewrites to 0.
135 : : *
136 : : * For details, see Reynolds et al SYNT 2017.
137 : : *
138 : : * Below, we let [[exp]]_n denote the term induced by
139 : : * the explanation exp for n.
140 : : * For example:
141 : : * exp = { ((_ is plus) n), ((_ is y) n.1) }
142 : : * is such that:
143 : : * [[exp]]_n = (plus w y)
144 : : * where w is a fresh variable.
145 : : */
146 : : class SygusExplain : protected EnvObj
147 : : {
148 : : public:
149 : : SygusExplain(Env& env, TermDbSygus* tdb);
150 : 14895 : ~SygusExplain() {}
151 : : /** get explanation for equality
152 : : *
153 : : * This function constructs an explanation, stored in exp, such that:
154 : : * - All formulas in exp are of the form ((_ is C) ns), where ns
155 : : * is a chain of selectors applied to n, and
156 : : * - exp => ( n = vn )
157 : : */
158 : : void getExplanationForEquality(Node n, Node vn, std::vector<Node>& exp);
159 : : /** returns the conjunction of exp computed in the above function */
160 : : Node getExplanationForEquality(Node n, Node vn);
161 : :
162 : : /** get explanation for equality
163 : : *
164 : : * This is identical to the above function except that we
165 : : * take an additional argument cexc, which says which
166 : : * children of vn should be excluded from the explanation.
167 : : *
168 : : * For example, if vn = plus( plus( x, x ), y ) and cexc is { 0 -> true },
169 : : * then the following is appended to exp :
170 : : * { ((_ is plus) n), ((_ is y) n.1) }
171 : : * where notice that the 0^th argument of vn is excluded.
172 : : */
173 : : void getExplanationForEquality(Node n,
174 : : Node vn,
175 : : std::vector<Node>& exp,
176 : : std::map<unsigned, bool>& cexc);
177 : : /** returns the conjunction of exp computed in the above function */
178 : : Node getExplanationForEquality(Node n,
179 : : Node vn,
180 : : std::map<unsigned, bool>& cexc);
181 : :
182 : : /** get explanation for
183 : : *
184 : : * This function constructs an explanation, stored in exp, such that:
185 : : * - All formulas in exp are of the form ((_ is C) ns), where ns
186 : : * is a chain of selectors applied to n, and
187 : : * - The test et holds for [[exp]]_n, and
188 : : * - (if applicable) exp => ( n != vnr ).
189 : : *
190 : : * This function updates sz to be the term size of [[exp]]_n.
191 : : *
192 : : * If strict is false, then we also test whether the invariance test holds
193 : : * independently of the entire value of vn.
194 : : *
195 : : * The argument var_count is used for tracking the variables that we introduce
196 : : * to generalize the shape of vn. This map is passed to
197 : : * TermDbSygus::getFreeVarInc. This argument should be used if we are
198 : : * calling this function multiple times and the generalization should not
199 : : * introduce variables that shadow the variables introduced on previous calls.
200 : : */
201 : : void getExplanationFor(Node n,
202 : : Node vn,
203 : : std::vector<Node>& exp,
204 : : SygusInvarianceTest& et,
205 : : Node vnr,
206 : : unsigned& sz);
207 : : void getExplanationFor(Node n,
208 : : Node vn,
209 : : std::vector<Node>& exp,
210 : : SygusInvarianceTest& et,
211 : : Node vnr,
212 : : std::map<TypeNode, size_t>& var_count,
213 : : unsigned& sz);
214 : : void getExplanationFor(Node n,
215 : : Node vn,
216 : : std::vector<Node>& exp,
217 : : SygusInvarianceTest& et,
218 : : bool strict = true);
219 : : void getExplanationFor(Node n,
220 : : Node vn,
221 : : std::vector<Node>& exp,
222 : : SygusInvarianceTest& et,
223 : : std::map<TypeNode, size_t>& var_count,
224 : : bool strict = true);
225 : :
226 : : private:
227 : : /** sygus term database associated with this utility */
228 : : TermDbSygus* d_tdb;
229 : : /** Helper function for getExplanationFor
230 : : * var_count is the number of free variables we have introduced,
231 : : * per type, for the purposes of generalizing subterms of n.
232 : : * vnr_exp stores the explanation, if one exists, for
233 : : * n != vnr. It is only non-null if vnr is non-null.
234 : : */
235 : : void getExplanationFor(TermRecBuild& trb,
236 : : Node n,
237 : : Node vn,
238 : : std::vector<Node>& exp,
239 : : std::map<TypeNode, size_t>& var_count,
240 : : SygusInvarianceTest& et,
241 : : Node vnr,
242 : : Node& vnr_exp,
243 : : int& sz);
244 : : };
245 : :
246 : : } // namespace quantifiers
247 : : } // namespace theory
248 : : } // namespace cvc5::internal
249 : :
250 : : #endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H */
|
