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