1 /******************************************************************************
2 * Top contributors (to current version):
3 * Andrew Reynolds, Mathias Preiner, Tim King
5 * This file is part of the cvc5 project.
7 * Copyright (c) 2009-2021 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 * ****************************************************************************
13 * Sygus invariance tests.
16 #include "cvc5_private.h"
18 #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H
19 #define CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H
21 #include <unordered_map>
24 #include "expr/node.h"
28 namespace quantifiers
{
31 class SynthConjecture
;
33 /* SygusInvarianceTest
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.
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.
44 class SygusInvarianceTest
47 virtual ~SygusInvarianceTest() {}
49 /** Is nvn invariant with respect to this test ?
51 * - nvn is the term to check whether it is invariant.
52 * - x is a variable such that the previous call to
53 * is_invariant (if any) was with term nvn_prev, and
54 * nvn is equal to nvn_prev with some subterm
55 * position replaced by x. This is typically used
58 bool is_invariant(TermDbSygus
* tds
, Node nvn
, Node x
)
60 if (invariant(tds
, nvn
, x
))
67 /** get updated term */
68 Node
getUpdatedTerm() { return d_update_nvn
; }
69 /** set updated term */
70 void setUpdatedTerm(Node n
) { d_update_nvn
= n
; }
72 /** result of the node that satisfies this invariant */
74 /** check whether nvn[ x ] is invariant */
75 virtual bool invariant(TermDbSygus
* tds
, Node nvn
, Node x
) = 0;
78 /** EquivSygusInvarianceTest
80 * This class tests whether a term evaluates via evaluation
81 * operators in the deep embedding (Section 4 of Reynolds
82 * et al. CAV 2015) to fixed term d_result.
84 * For example, consider a SyGuS evaluation function eval
85 * for a synthesis conjecture with arguments x and y.
86 * Notice that the term t = (mult x y) is such that:
87 * eval( t, 0, 1 ) ----> 0
88 * This test is invariant on the content of the second
89 * argument of t, noting that:
90 * eval( (mult x _), 0, 1 ) ----> 0
91 * as well, via a call to EvalSygusInvarianceTest::invariant.
93 * Another example, t = ite( gt( x, y ), x, y ) is such that:
94 * eval( t, 2, 3 ) ----> 3
95 * This test is invariant on the second child of t, noting:
96 * eval( ite( gt( x, y ), _, y ), 2, 3 ) ----> 3
98 class EvalSygusInvarianceTest
: public SygusInvarianceTest
101 EvalSygusInvarianceTest()
102 : d_kind(kind::UNDEFINED_KIND
), d_is_conjunctive(false)
106 /** initialize this invariance test
108 * This sets d_terms/d_var/d_result, where we are checking whether:
109 * <d_kind>(d_terms) { d_var -> n } ----> d_result.
112 void init(Node conj
, Node var
, Node res
);
115 /** does d_terms{ d_var -> nvn } still rewrite to d_result? */
116 bool invariant(TermDbSygus
* tds
, Node nvn
, Node x
) override
;
119 /** the formulas we are evaluating */
120 std::vector
<Node
> d_terms
;
123 /** the result of the evaluation */
125 /** the parent kind we are checking, undefined if size(d_terms) is 1. */
127 /** whether we are conjunctive
129 * If this flag is true, then the evaluation tests:
130 * d_terms[1] {d_var -> n} = d_result ... d_term[k] {d_var -> n} = d_result
131 * should be processed conjunctively, that is,
132 * <d_kind>(d_terms) { d_var -> n } = d_result only if each of the above
133 * holds. If this flag is false, then these tests are interpreted
134 * disjunctively, i.e. if one child test succeeds, the overall test succeeds.
136 bool d_is_conjunctive
;
139 /** EquivSygusInvarianceTest
141 * This class tests whether a builtin version of a
142 * sygus term is equivalent up to rewriting to a RHS value bvr.
146 * ite( t>0, 0, 0 ) + s*0 ----> 0
148 * This test is invariant on the condition t>0 and s, since:
150 * ite( _, 0, 0 ) + _*0 ----> 0
152 * for any values of _.
154 * It also manages the case where the rewriting is invariant
155 * wrt a finite set of examples occurring in the conjecture.
156 * (EX1) : For example if our input examples are:
157 * (x,y,z) = (3,2,4), (5,2,6), (3,2,1)
158 * On these examples, we have:
160 * ite( x>y, z, 0) ---> 4,6,1
162 * which is invariant on the second argument:
164 * ite( x>y, z, _) ---> 4,6,1
166 * For details, see Reynolds et al SYNT 2017.
168 class EquivSygusInvarianceTest
: public SygusInvarianceTest
171 EquivSygusInvarianceTest() : d_conj(nullptr) {}
173 /** initialize this invariance test
174 * tn is the sygus type for e
175 * aconj/e are used for conjecture-specific symmetry breaking
176 * bvr is the builtin version of the right hand side of the rewrite that we
177 * are checking for invariance
180 TermDbSygus
* tds
, TypeNode tn
, SynthConjecture
* aconj
, Node e
, Node bvr
);
183 /** checks whether the analog of nvn still rewrites to d_bvr */
184 bool invariant(TermDbSygus
* tds
, Node nvn
, Node x
) override
;
187 /** the conjecture associated with the enumerator d_enum */
188 SynthConjecture
* d_conj
;
189 /** the enumerator associated with the term for which this test is for */
191 /** the RHS of the evaluation */
193 /** the result of the examples
194 * In (EX1), this is (4,6,1)
196 std::vector
<Node
> d_exo
;
199 /** DivByZeroSygusInvarianceTest
201 * This class tests whether a sygus term involves
204 * For example the test for:
206 * is invariant on the contents of _ below:
209 class DivByZeroSygusInvarianceTest
: public SygusInvarianceTest
212 DivByZeroSygusInvarianceTest() {}
215 /** checks whether nvn involves division by zero. */
216 bool invariant(TermDbSygus
* tds
, Node nvn
, Node x
) override
;
219 /** NegContainsSygusInvarianceTest
221 * This class is used to construct a minimal shape of a term that cannot
222 * be contained in at least one output of an I/O pair.
224 * Say our PBE conjecture is:
227 * f( "abc" ) = "abc abc" ^
228 * f( "de" ) = "de de"
230 * Then, this class is used when there is a candidate solution t[x1]
232 * contains( "abc abc", t["abc"] ) ---> false or
233 * contains( "de de", t["de"] ) ---> false
235 * It is used to determine whether certain generalizations of t[x1]
236 * are still sufficient to falsify one of the above containments.
240 * The test for str.++( x1, "d" ) is invariant on its first argument
241 * ...since contains( "abc abc", str.++( _, "d" ) ) ---> false
242 * The test for str.replace( "de", x1, "b" ) is invariant on its third argument
243 * ...since contains( "abc abc", str.replace( "de", "abc", _ ) ) ---> false
245 class NegContainsSygusInvarianceTest
: public SygusInvarianceTest
248 NegContainsSygusInvarianceTest() : d_isUniversal(false) {}
250 /** initialize this invariance test
251 * e is the enumerator which we are reasoning about (associated with a synth
253 * ex is the list of inputs,
254 * exo is the list of outputs,
255 * ncind is the set of possible example indices to check invariance of
257 * For example, in the above example, when t[x1] = "ab", then this
258 * has the index 1 since contains("de de", "ab") ---> false but not
259 * the index 0 since contains("abc abc","ab") ---> true.
262 std::vector
<std::vector
<Node
> >& ex
,
263 std::vector
<Node
>& exo
,
264 std::vector
<unsigned>& ncind
);
267 * This updates the semantics of this check such that *all* instead of some
268 * examples must fail the containment test.
270 void setUniversal() { d_isUniversal
= true; }
274 * Checks if contains( out_i, nvn[in_i] ) --> false for some I/O pair i; if
275 * d_isUniversal is true, then we check if the rewrite holds for *all* I/O
278 bool invariant(TermDbSygus
* tds
, Node nvn
, Node x
) override
;
281 /** The enumerator whose value we are considering in this invariance test */
283 /** The input examples */
284 std::vector
<std::vector
<Node
> > d_ex
;
285 /** The output examples for the enumerator */
286 std::vector
<Node
> d_exo
;
287 /** The set of I/O pair indices i such that
288 * contains( out_i, nvn[in_i] ) ---> false
290 std::vector
<unsigned> d_neg_con_indices
;
291 /** requires not being in all examples */
295 } // namespace quantifiers
296 } // namespace theory
299 #endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H */