Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Sygus invariance tests.
11 : : */
12 : :
13 : : #include "cvc5_private.h"
14 : :
15 : : #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H
16 : : #define CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H
17 : :
18 : : #include <unordered_map>
19 : : #include <vector>
20 : :
21 : : #include "expr/node.h"
22 : :
23 : : namespace cvc5::internal {
24 : : namespace theory {
25 : :
26 : : class Rewriter;
27 : :
28 : : namespace quantifiers {
29 : :
30 : : class TermDbSygus;
31 : : class SynthConjecture;
32 : :
33 : : /* SygusInvarianceTest
34 : : *
35 : : * This class is the standard interface for term generalization
36 : : * in SyGuS. Its interface is a single function is_variant,
37 : : * which is a virtual condition for SyGuS terms.
38 : : *
39 : : * The common use case of invariance tests is when constructing
40 : : * minimal explanations for refinement lemmas in the
41 : : * counterexample-guided inductive synthesis (CEGIS) loop.
42 : : * See sygus_explain.h for more details.
43 : : */
44 : : class SygusInvarianceTest
45 : : {
46 : : public:
47 : 80318 : SygusInvarianceTest(Rewriter* r) : d_rewriter(r) {}
48 : 80318 : virtual ~SygusInvarianceTest() {}
49 : :
50 : : /** Is nvn invariant with respect to this test ?
51 : : *
52 : : * - nvn is the term to check whether it is invariant.
53 : : * - x is a variable such that the previous call to
54 : : * is_invariant (if any) was with term nvn_prev, and
55 : : * nvn is equal to nvn_prev with some subterm
56 : : * position replaced by x. This is typically used
57 : : * for debugging only.
58 : : */
59 : 107148 : bool is_invariant(TermDbSygus* tds, Node nvn, Node x)
60 : : {
61 [ + + ]: 107148 : if (invariant(tds, nvn, x))
62 : : {
63 : 25292 : d_update_nvn = nvn;
64 : 25292 : return true;
65 : : }
66 : 81856 : return false;
67 : : }
68 : : /** get updated term */
69 : 64144 : Node getUpdatedTerm() { return d_update_nvn; }
70 : : /** set updated term */
71 : 32072 : void setUpdatedTerm(Node n) { d_update_nvn = n; }
72 : :
73 : : protected:
74 : : /** Pointer to the rewriter */
75 : : Rewriter* d_rewriter;
76 : : /** result of the node that satisfies this invariant */
77 : : Node d_update_nvn;
78 : : /** check whether nvn[ x ] is invariant */
79 : : virtual bool invariant(TermDbSygus* tds, Node nvn, Node x) = 0;
80 : : };
81 : :
82 : : /** EquivSygusInvarianceTest
83 : : *
84 : : * This class tests whether a term evaluates via evaluation
85 : : * operators in the deep embedding (Section 4 of Reynolds
86 : : * et al. CAV 2015) to fixed term d_result.
87 : : *
88 : : * For example, consider a SyGuS evaluation function eval
89 : : * for a synthesis conjecture with arguments x and y.
90 : : * Notice that the term t = (mult x y) is such that:
91 : : * eval( t, 0, 1 ) ----> 0
92 : : * This test is invariant on the content of the second
93 : : * argument of t, noting that:
94 : : * eval( (mult x _), 0, 1 ) ----> 0
95 : : * as well, via a call to EvalSygusInvarianceTest::invariant.
96 : : *
97 : : * Another example, t = ite( gt( x, y ), x, y ) is such that:
98 : : * eval( t, 2, 3 ) ----> 3
99 : : * This test is invariant on the second child of t, noting:
100 : : * eval( ite( gt( x, y ), _, y ), 2, 3 ) ----> 3
101 : : */
102 : : class EvalSygusInvarianceTest : public SygusInvarianceTest
103 : : {
104 : : public:
105 : 77561 : EvalSygusInvarianceTest(Rewriter* r)
106 : 77561 : : SygusInvarianceTest(r),
107 : 77561 : d_kind(Kind::UNDEFINED_KIND),
108 : 77561 : d_is_conjunctive(false)
109 : : {
110 : 77561 : }
111 : :
112 : : /** initialize this invariance test
113 : : *
114 : : * This sets d_terms/d_var/d_result, where we are checking whether:
115 : : * <d_kind>(d_terms) { d_var -> n } ----> d_result.
116 : : * for terms n.
117 : : */
118 : : void init(Node conj, Node var, Node res);
119 : :
120 : : protected:
121 : : /** does d_terms{ d_var -> nvn } still rewrite to d_result? */
122 : : bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
123 : :
124 : : private:
125 : : /** the formulas we are evaluating */
126 : : std::vector<Node> d_terms;
127 : : /** the variable */
128 : : TNode d_var;
129 : : /** the result of the evaluation */
130 : : Node d_result;
131 : : /** the parent kind we are checking, undefined if size(d_terms) is 1. */
132 : : Kind d_kind;
133 : : /** whether we are conjunctive
134 : : *
135 : : * If this flag is true, then the evaluation tests:
136 : : * d_terms[1] {d_var -> n} = d_result ... d_term[k] {d_var -> n} = d_result
137 : : * should be processed conjunctively, that is,
138 : : * <d_kind>(d_terms) { d_var -> n } = d_result only if each of the above
139 : : * holds. If this flag is false, then these tests are interpreted
140 : : * disjunctively, i.e. if one child test succeeds, the overall test succeeds.
141 : : */
142 : : bool d_is_conjunctive;
143 : : };
144 : :
145 : : /** EquivSygusInvarianceTest
146 : : *
147 : : * This class tests whether a builtin version of a
148 : : * sygus term is equivalent up to rewriting to a RHS value bvr.
149 : : *
150 : : * For example,
151 : : *
152 : : * ite( t>0, 0, 0 ) + s*0 ----> 0
153 : : *
154 : : * This test is invariant on the condition t>0 and s, since:
155 : : *
156 : : * ite( _, 0, 0 ) + _*0 ----> 0
157 : : *
158 : : * for any values of _.
159 : : *
160 : : * It also manages the case where the rewriting is invariant
161 : : * wrt a finite set of examples occurring in the conjecture.
162 : : * (EX1) : For example if our input examples are:
163 : : * (x,y,z) = (3,2,4), (5,2,6), (3,2,1)
164 : : * On these examples, we have:
165 : : *
166 : : * ite( x>y, z, 0) ---> 4,6,1
167 : : *
168 : : * which is invariant on the second argument:
169 : : *
170 : : * ite( x>y, z, _) ---> 4,6,1
171 : : *
172 : : * For details, see Reynolds et al SYNT 2017.
173 : : */
174 : : class EquivSygusInvarianceTest : public SygusInvarianceTest
175 : : {
176 : : public:
177 : 2665 : EquivSygusInvarianceTest(Rewriter* r)
178 : 2665 : : SygusInvarianceTest(r), d_conj(nullptr)
179 : : {
180 : 2665 : }
181 : :
182 : : /** initialize this invariance test
183 : : * tn is the sygus type for e
184 : : * aconj/e are used for conjecture-specific symmetry breaking
185 : : * bvr is the builtin version of the right hand side of the rewrite that we
186 : : * are checking for invariance
187 : : */
188 : : void init(TermDbSygus* tds, SynthConjecture* aconj, Node e, Node bvr);
189 : :
190 : : protected:
191 : : /** checks whether the analog of nvn still rewrites to d_bvr */
192 : : bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
193 : :
194 : : private:
195 : : /** the conjecture associated with the enumerator d_enum */
196 : : SynthConjecture* d_conj;
197 : : /** the enumerator associated with the term for which this test is for */
198 : : Node d_enum;
199 : : /** the RHS of the evaluation */
200 : : Node d_bvr;
201 : : /** the result of the examples
202 : : * In (EX1), this is (4,6,1)
203 : : */
204 : : std::vector<Node> d_exo;
205 : : };
206 : :
207 : : /** NegContainsSygusInvarianceTest
208 : : *
209 : : * This class is used to construct a minimal shape of a term that cannot
210 : : * be contained in at least one output of an I/O pair.
211 : : *
212 : : * Say our PBE conjecture is:
213 : : *
214 : : * exists f.
215 : : * f( "abc" ) = "abc abc" ^
216 : : * f( "de" ) = "de de"
217 : : *
218 : : * Then, this class is used when there is a candidate solution t[x1]
219 : : * such that either:
220 : : * contains( "abc abc", t["abc"] ) ---> false or
221 : : * contains( "de de", t["de"] ) ---> false
222 : : *
223 : : * It is used to determine whether certain generalizations of t[x1]
224 : : * are still sufficient to falsify one of the above containments.
225 : : *
226 : : * For example:
227 : : *
228 : : * The test for str.++( x1, "d" ) is invariant on its first argument
229 : : * ...since contains( "abc abc", str.++( _, "d" ) ) ---> false
230 : : * The test for str.replace( "de", x1, "b" ) is invariant on its third argument
231 : : * ...since contains( "abc abc", str.replace( "de", "abc", _ ) ) ---> false
232 : : */
233 : : class NegContainsSygusInvarianceTest : public SygusInvarianceTest
234 : : {
235 : : public:
236 : 92 : NegContainsSygusInvarianceTest(Rewriter* r)
237 : 92 : : SygusInvarianceTest(r), d_isUniversal(false)
238 : : {
239 : 92 : }
240 : :
241 : : /** initialize this invariance test
242 : : * e is the enumerator which we are reasoning about (associated with a synth
243 : : * fun).
244 : : * ex is the list of inputs,
245 : : * exo is the list of outputs,
246 : : * ncind is the set of possible example indices to check invariance of
247 : : * non-containment.
248 : : * For example, in the above example, when t[x1] = "ab", then this
249 : : * has the index 1 since contains("de de", "ab") ---> false but not
250 : : * the index 0 since contains("abc abc","ab") ---> true.
251 : : */
252 : : void init(Node e,
253 : : std::vector<std::vector<Node> >& ex,
254 : : std::vector<Node>& exo,
255 : : std::vector<unsigned>& ncind);
256 : : /** set universal
257 : : *
258 : : * This updates the semantics of this check such that *all* instead of some
259 : : * examples must fail the containment test.
260 : : */
261 : 6 : void setUniversal() { d_isUniversal = true; }
262 : :
263 : : protected:
264 : : /**
265 : : * Checks if contains( out_i, nvn[in_i] ) --> false for some I/O pair i; if
266 : : * d_isUniversal is true, then we check if the rewrite holds for *all* I/O
267 : : * pairs.
268 : : */
269 : : bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
270 : :
271 : : private:
272 : : /** The enumerator whose value we are considering in this invariance test */
273 : : Node d_enum;
274 : : /** The input examples */
275 : : std::vector<std::vector<Node> > d_ex;
276 : : /** The output examples for the enumerator */
277 : : std::vector<Node> d_exo;
278 : : /** The set of I/O pair indices i such that
279 : : * contains( out_i, nvn[in_i] ) ---> false
280 : : */
281 : : std::vector<unsigned> d_neg_con_indices;
282 : : /** requires not being in all examples */
283 : : bool d_isUniversal;
284 : : };
285 : :
286 : : } // namespace quantifiers
287 : : } // namespace theory
288 : : } // namespace cvc5::internal
289 : :
290 : : #endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H */
|
