Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Mathias Preiner, Aina Niemetz
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 : : * Implementation of techniques for sygus invariance tests.
14 : : */
15 : :
16 : : #include "theory/quantifiers/sygus/sygus_invariance.h"
17 : :
18 : : #include "theory/quantifiers/sygus/sygus_pbe.h"
19 : : #include "theory/quantifiers/sygus/synth_conjecture.h"
20 : : #include "theory/quantifiers/sygus/term_database_sygus.h"
21 : : #include "theory/rewriter.h"
22 : :
23 : : using namespace cvc5::internal::kind;
24 : : using namespace std;
25 : :
26 : : namespace cvc5::internal {
27 : : namespace theory {
28 : : namespace quantifiers {
29 : :
30 : 76472 : void EvalSygusInvarianceTest::init(Node conj, Node var, Node res)
31 : : {
32 : 76472 : d_terms.clear();
33 : : // simple miniscope
34 [ + + ]: 152944 : if ((conj.getKind() == Kind::AND || conj.getKind() == Kind::OR)
35 [ + - ][ + - ]: 152944 : && res.isConst())
[ + + ]
36 : : {
37 [ + + ]: 33270 : for (const Node& c : conj)
38 : : {
39 : 22180 : d_terms.push_back(c);
40 : : }
41 : 11090 : d_kind = conj.getKind();
42 : 11090 : d_is_conjunctive = res.getConst<bool>() == (d_kind == Kind::AND);
43 : : }
44 : : else
45 : : {
46 : 65382 : d_terms.push_back(conj);
47 : 65382 : d_is_conjunctive = true;
48 : : }
49 : 76472 : d_var = var;
50 : 76472 : d_result = res;
51 : 76472 : }
52 : :
53 : 135766 : bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
54 : : {
55 : 271532 : TNode tnvn = nvn;
56 : 271532 : std::unordered_map<TNode, TNode> cache;
57 : 271532 : std::vector<Node> keep;
58 [ + + ]: 197994 : for (const Node& c : d_terms)
59 : : {
60 : 293632 : Node conj_subs = c.substitute(d_var, tnvn, cache);
61 : : // Ensure ref counted for now since we are reusing the cache for substitute
62 : : // in this loop
63 : 146816 : keep.push_back(conj_subs);
64 : 146816 : Node conj_subs_unfold = tds->rewriteNode(conj_subs);
65 [ + - ]: 293632 : Trace("sygus-cref-eval2-debug")
66 : 146816 : << " ...check unfolding : " << conj_subs_unfold << std::endl;
67 [ + - ]: 293632 : Trace("sygus-cref-eval2-debug")
68 : 146816 : << " ......from : " << conj_subs << std::endl;
69 [ + + ]: 146816 : if (conj_subs_unfold != d_result)
70 : : {
71 [ + - ]: 84588 : if (d_is_conjunctive)
72 : : {
73 : : // ti /--> true implies and( t1, ..., tn ) /--> true, where "/-->" is
74 : : // "does not evaluate to".
75 : 84588 : return false;
76 : : }
77 : : }
78 [ - + ]: 62228 : else if (!d_is_conjunctive)
79 : : {
80 : : // ti --> true implies or( t1, ..., tn ) --> true
81 : 0 : return true;
82 : : }
83 [ + - ]: 124456 : Trace("sygus-cref-eval2") << "Evaluation min explain : " << conj_subs
84 : 0 : << " still evaluates to " << d_result
85 : 62228 : << " regardless of ";
86 [ + - ]: 62228 : Trace("sygus-cref-eval2") << x << std::endl;
87 : : }
88 : 51178 : return d_is_conjunctive;
89 : : }
90 : :
91 : 2374 : void EquivSygusInvarianceTest::init(
92 : : TermDbSygus* tds, TypeNode tn, SynthConjecture* aconj, Node e, Node bvr)
93 : : {
94 : : // compute the current examples
95 : 2374 : d_bvr = bvr;
96 [ - + ][ - + ]: 2374 : Assert(tds != nullptr);
[ - - ]
97 [ + - ]: 2374 : if (aconj != nullptr)
98 : : {
99 : 2374 : ExampleEvalCache* eec = aconj->getExampleEvalCache(e);
100 [ + + ]: 2374 : if (eec != nullptr)
101 : : {
102 : : // get the result of evaluating bvr on the examples of enumerator e.
103 : 526 : eec->evaluateVec(bvr, d_exo, false);
104 : 526 : d_conj = aconj;
105 : 526 : d_enum = e;
106 : : }
107 : : }
108 : 2374 : }
109 : :
110 : 9576 : bool EquivSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
111 : : {
112 : 19152 : TypeNode tn = nvn.getType();
113 : 28728 : Node nbv = tds->sygusToBuiltin(nvn, tn);
114 : 9576 : Node nbvr = d_rewriter->extendedRewrite(nbv);
115 [ + - ]: 19152 : Trace("sygus-sb-mexp-debug") << " min-exp check : " << nbv << " -> " << nbvr
116 : 9576 : << std::endl;
117 : 9576 : bool exc_arg = false;
118 : : // equivalent / singular up to normalization
119 [ + + ]: 9576 : if (nbvr == d_bvr)
120 : : {
121 : : // gives the same result : then the explanation for the child is irrelevant
122 : 74 : exc_arg = true;
123 : 148 : Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn)
124 : 74 : << " is rewritten to " << nbvr;
125 [ + - ]: 148 : Trace("sygus-sb-mexp") << " regardless of the content of "
126 : 74 : << tds->sygusToBuiltin(x) << std::endl;
127 : : }
128 : : else
129 : : {
130 [ + + ]: 9502 : if (nbvr.isVar())
131 : : {
132 : 444 : TypeNode xtn = x.getType();
133 [ + + ]: 222 : if (xtn == tn)
134 : : {
135 : 636 : Node bx = tds->sygusToBuiltin(x, xtn);
136 [ - + ][ - + ]: 212 : Assert(bx.getType() == nbvr.getType());
[ - - ]
137 [ + - ]: 212 : if (nbvr == bx)
138 : : {
139 : 424 : Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn)
140 : 0 : << " always rewrites to argument " << nbvr
141 : 212 : << std::endl;
142 : : // rewrites to the variable : then the explanation of this is
143 : : // irrelevant as well
144 : 212 : exc_arg = true;
145 : 212 : d_bvr = nbvr;
146 : : }
147 : : }
148 : : }
149 : : }
150 : : // equivalent under examples
151 [ + + ]: 9576 : if (!exc_arg)
152 : : {
153 [ + + ]: 9290 : if (!d_enum.isNull())
154 : : {
155 : 1884 : bool ex_equiv = true;
156 : 1884 : ExampleEvalCache* eec = d_conj->getExampleEvalCache(d_enum);
157 [ - + ][ - + ]: 1884 : Assert(eec != nullptr);
[ - - ]
158 [ + + ]: 2040 : for (unsigned j = 0, esize = d_exo.size(); j < esize; j++)
159 : : {
160 : 2024 : Node nbvr_ex = eec->evaluate(nbvr, j);
161 [ + + ]: 2024 : if (nbvr_ex != d_exo[j])
162 : : {
163 : 1868 : ex_equiv = false;
164 : 1868 : break;
165 : : }
166 : : }
167 [ + + ]: 1884 : if (ex_equiv)
168 : : {
169 : 16 : Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn);
170 [ + - ]: 32 : Trace("sygus-sb-mexp")
171 : 0 : << " is the same w.r.t. examples regardless of the content of "
172 : 16 : << tds->sygusToBuiltin(x) << std::endl;
173 : 16 : exc_arg = true;
174 : : }
175 : : }
176 : : }
177 : 19152 : return exc_arg;
178 : : }
179 : :
180 : 92 : void NegContainsSygusInvarianceTest::init(Node e,
181 : : std::vector<std::vector<Node> >& ex,
182 : : std::vector<Node>& exo,
183 : : std::vector<unsigned>& ncind)
184 : : {
185 [ - + ][ - + ]: 92 : Assert(ex.size() == exo.size());
[ - - ]
186 : 92 : d_enum = e;
187 : 92 : d_ex.insert(d_ex.end(), ex.begin(), ex.end());
188 : 92 : d_exo.insert(d_exo.end(), exo.begin(), exo.end());
189 : 92 : d_neg_con_indices.insert(d_neg_con_indices.end(), ncind.begin(), ncind.end());
190 : 92 : }
191 : :
192 : 130 : bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds,
193 : : Node nvn,
194 : : Node x)
195 : : {
196 [ + - ]: 130 : if (!d_enum.isNull())
197 : : {
198 : 130 : TypeNode tn = nvn.getType();
199 : 260 : Node nbv = tds->sygusToBuiltin(nvn, tn);
200 : 130 : Node nbvr = d_rewriter->extendedRewrite(nbv);
201 : : // if for any of the examples, it is not contained, then we can exclude
202 [ + + ]: 11934 : for (unsigned i = 0; i < d_neg_con_indices.size(); i++)
203 : : {
204 : 11810 : unsigned ii = d_neg_con_indices[i];
205 [ - + ][ - + ]: 11810 : Assert(ii < d_exo.size());
[ - - ]
206 : 23620 : Node nbvre = tds->evaluateBuiltin(tn, nbvr, d_ex[ii]);
207 : 11810 : Node out = d_exo[ii];
208 : 23620 : Node cont = NodeManager::mkNode(Kind::STRING_CONTAINS, out, nbvre);
209 [ + - ]: 11810 : Trace("sygus-pbe-cterm-debug") << "Check: " << cont << std::endl;
210 : 11810 : Node contr = d_rewriter->extendedRewrite(cont);
211 [ + - ]: 11810 : if (!contr.isConst())
212 : : {
213 [ + + ]: 11810 : if (d_isUniversal)
214 : : {
215 : 6 : return false;
216 : : }
217 : : }
218 [ - - ]: 0 : else if (contr.getConst<bool>() == d_isUniversal)
219 : : {
220 [ - - ]: 0 : if (TraceIsOn("sygus-pbe-cterm"))
221 : : {
222 [ - - ]: 0 : Trace("sygus-pbe-cterm")
223 : 0 : << "PBE-cterm : enumerator : do not consider ";
224 [ - - ]: 0 : Trace("sygus-pbe-cterm")
225 : 0 : << nbv << " for any " << tds->sygusToBuiltin(x) << " since "
226 : 0 : << std::endl;
227 [ - - ]: 0 : Trace("sygus-pbe-cterm") << " PBE-cterm : for input example : ";
228 [ - - ]: 0 : for (unsigned j = 0, size = d_ex[ii].size(); j < size; j++)
229 : : {
230 [ - - ]: 0 : Trace("sygus-pbe-cterm") << d_ex[ii][j] << " ";
231 : : }
232 [ - - ]: 0 : Trace("sygus-pbe-cterm") << std::endl;
233 [ - - ]: 0 : Trace("sygus-pbe-cterm")
234 : 0 : << " PBE-cterm : this rewrites to : " << nbvre << std::endl;
235 [ - - ]: 0 : Trace("sygus-pbe-cterm")
236 : 0 : << " PBE-cterm : and is not in output : " << out << std::endl;
237 : : }
238 : 0 : return !d_isUniversal;
239 : : }
240 [ + - ]: 23608 : Trace("sygus-pbe-cterm-debug2")
241 : 11804 : << "...check failed, rewrites to : " << contr << std::endl;
242 : : }
243 : : }
244 : 124 : return d_isUniversal;
245 : : }
246 : :
247 : : } // namespace quantifiers
248 : : } // namespace theory
249 : : } // namespace cvc5::internal
|
