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