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 : : * Utility for processing programming by examples synthesis conjectures.
11 : : */
12 : : #include "theory/quantifiers/sygus/sygus_pbe.h"
13 : :
14 : : #include "options/quantifiers_options.h"
15 : : #include "theory/datatypes/sygus_datatype_utils.h"
16 : : #include "theory/quantifiers/sygus/example_infer.h"
17 : : #include "theory/quantifiers/sygus/sygus_unif_io.h"
18 : : #include "theory/quantifiers/sygus/synth_conjecture.h"
19 : : #include "theory/quantifiers/sygus/term_database_sygus.h"
20 : : #include "theory/quantifiers/term_util.h"
21 : : #include "util/random.h"
22 : :
23 : : using namespace cvc5::internal;
24 : : using namespace cvc5::internal::kind;
25 : :
26 : : namespace cvc5::internal {
27 : : namespace theory {
28 : : namespace quantifiers {
29 : :
30 : 3755 : SygusPbe::SygusPbe(Env& env,
31 : : QuantifiersState& qs,
32 : : QuantifiersInferenceManager& qim,
33 : : TermDbSygus* tds,
34 : 3755 : SynthConjecture* p)
35 : 3755 : : SygusModule(env, qs, qim, tds, p)
36 : : {
37 : 3755 : d_true = nodeManager()->mkConst(true);
38 : 3755 : d_false = nodeManager()->mkConst(false);
39 : 3755 : d_is_pbe = false;
40 : 3755 : }
41 : :
42 : 7496 : SygusPbe::~SygusPbe() {}
43 : :
44 : 485 : bool SygusPbe::initialize(CVC5_UNUSED Node conj,
45 : : Node n,
46 : : const std::vector<Node>& candidates)
47 : : {
48 [ + - ]: 485 : Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl;
49 : 485 : NodeManager* nm = nodeManager();
50 : :
51 [ + + ]: 485 : if (!options().quantifiers.sygusUnifPbe)
52 : : {
53 : : // we are not doing unification
54 : 129 : return false;
55 : : }
56 : :
57 : : // PBE does not repair symbolic any-constant constructors in candidate
58 : : // solutions. Let CEGIS handle these grammars so SygusRepairConst can repair
59 : : // the concrete values for any-constant holes.
60 [ + + ]: 782 : for (const Node& c : candidates)
61 : : {
62 : 454 : TypeNode tn = c.getType();
63 : 454 : d_tds->registerSygusType(tn);
64 [ + + ]: 454 : if (d_tds->getTypeInfo(tn).hasSubtermSymbolicCons())
65 : : {
66 : 28 : return false;
67 : : }
68 [ + + ]: 454 : }
69 : :
70 : : // check if all candidates are valid examples
71 : 328 : ExampleInfer* ei = d_parent->getExampleInfer();
72 : 328 : d_is_pbe = true;
73 [ + + ]: 415 : for (const Node& c : candidates)
74 : : {
75 : : // if it has no examples or the output of the examples is invalid
76 : 334 : if (ei->getNumExamples(c) == 0 || !ei->hasExamplesOut(c))
77 : : {
78 : 247 : d_is_pbe = false;
79 : 247 : return false;
80 : : }
81 : : }
82 [ + + ]: 164 : for (const Node& c : candidates)
83 : : {
84 [ - + ][ - + ]: 83 : Assert(ei->hasExamples(c));
[ - - ]
85 : 83 : d_sygus_unif[c].reset(new SygusUnifIo(d_env, d_parent));
86 [ + - ]: 166 : Trace("sygus-pbe") << "Initialize unif utility for " << c << "..."
87 : 83 : << std::endl;
88 : 83 : std::map<Node, std::vector<Node>> strategy_lemmas;
89 : 166 : d_sygus_unif[c]->initializeCandidate(
90 : 83 : d_tds, c, d_candidate_to_enum[c], strategy_lemmas);
91 [ - + ][ - + ]: 83 : Assert(!d_candidate_to_enum[c].empty());
[ - - ]
92 [ + - ]: 166 : Trace("sygus-pbe") << "Initialize " << d_candidate_to_enum[c].size()
93 : 83 : << " enumerators for " << c << "..." << std::endl;
94 : : // collect list per type of strategy points with strategy lemmas
95 : 83 : std::map<TypeNode, std::vector<Node>> tn_to_strategy_pt;
96 [ + + ]: 179 : for (const std::pair<const Node, std::vector<Node>>& p : strategy_lemmas)
97 : : {
98 : 96 : TypeNode tnsp = p.first.getType();
99 : 96 : tn_to_strategy_pt[tnsp].push_back(p.first);
100 : 96 : }
101 : : // initialize the enumerators
102 [ + + ]: 202 : for (const Node& e : d_candidate_to_enum[c])
103 : : {
104 : 119 : TypeNode etn = e.getType();
105 : 119 : d_tds->registerEnumerator(e, c, d_parent, ROLE_ENUM_POOL);
106 : 119 : d_enum_to_candidate[e] = c;
107 : 119 : TNode te = e;
108 : : // initialize static symmetry breaking lemmas for it
109 : : // we register only one "master" enumerator per type
110 : : // thus, the strategy lemmas (which are for individual strategy points)
111 : : // are applicable (disjunctively) to the master enumerator
112 : : std::map<TypeNode, std::vector<Node>>::iterator itt =
113 : 119 : tn_to_strategy_pt.find(etn);
114 [ + + ]: 119 : if (itt != tn_to_strategy_pt.end())
115 : : {
116 : 64 : std::vector<Node> disj;
117 [ + + ]: 156 : for (const Node& sp : itt->second)
118 : : {
119 : : std::map<Node, std::vector<Node>>::iterator itsl =
120 : 92 : strategy_lemmas.find(sp);
121 [ - + ][ - + ]: 92 : Assert(itsl != strategy_lemmas.end());
[ - - ]
122 [ + - ]: 92 : if (!itsl->second.empty())
123 : : {
124 : 92 : TNode tsp = sp;
125 : 92 : Node lem = itsl->second.size() == 1
126 : 78 : ? itsl->second[0]
127 [ + + ]: 170 : : nm->mkNode(Kind::AND, itsl->second);
128 [ + + ]: 92 : if (tsp != te)
129 : : {
130 : 28 : lem = lem.substitute(tsp, te);
131 : : }
132 [ + + ]: 92 : if (std::find(disj.begin(), disj.end(), lem) == disj.end())
133 : : {
134 : 68 : disj.push_back(lem);
135 : : }
136 : 92 : }
137 : : }
138 : : // add its active guard
139 : 64 : Node ag = d_tds->getActiveGuardForEnumerator(e);
140 [ - + ][ - + ]: 64 : Assert(!ag.isNull());
[ - - ]
141 : 64 : disj.push_back(ag.negate());
142 [ - + ]: 64 : Node lem = disj.size() == 1 ? disj[0] : nm->mkNode(Kind::OR, disj);
143 : : // Apply extended rewriting on the lemma. This helps utilities like
144 : : // SygusEnumerator more easily recognize the shape of this lemma, e.g.
145 : : // ( ~is-ite(x) or ( ~is-ite(x) ^ P ) ) --> ~is-ite(x).
146 : 64 : lem = extendedRewrite(lem);
147 [ + - ]: 128 : Trace("sygus-pbe") << " static redundant op lemma : " << lem
148 : 64 : << std::endl;
149 : : // Register as a symmetry breaking lemma with the term database.
150 : : // This will either be processed via a lemma on the output channel
151 : : // of the sygus extension of the datatypes solver, or internally
152 : : // encoded as a constraint to an active enumerator.
153 : 64 : d_tds->registerSymBreakLemma(e, lem, etn, 0, false);
154 : 64 : }
155 : 119 : }
156 : 83 : }
157 : 81 : return true;
158 : : }
159 : :
160 : : // ------------------------------------------- solution construction from
161 : : // enumeration
162 : :
163 : 9992 : void SygusPbe::getTermList(const std::vector<Node>& candidates,
164 : : std::vector<Node>& terms)
165 : : {
166 [ + + ]: 20066 : for (unsigned i = 0; i < candidates.size(); i++)
167 : : {
168 : 10074 : Node v = candidates[i];
169 : : std::map<Node, std::vector<Node>>::iterator it =
170 : 10074 : d_candidate_to_enum.find(v);
171 [ + - ]: 10074 : if (it != d_candidate_to_enum.end())
172 : : {
173 : 10074 : terms.insert(terms.end(), it->second.begin(), it->second.end());
174 : : }
175 : 10074 : }
176 : 9992 : }
177 : :
178 : 9992 : bool SygusPbe::allowPartialModel()
179 : : {
180 : 9992 : return !options().quantifiers.sygusPbeMultiFair;
181 : : }
182 : :
183 : 761 : bool SygusPbe::constructCandidates(const std::vector<Node>& enums,
184 : : const std::vector<Node>& enum_values,
185 : : const std::vector<Node>& candidates,
186 : : std::vector<Node>& candidate_values)
187 : : {
188 [ - + ][ - + ]: 761 : Assert(enums.size() == enum_values.size());
[ - - ]
189 [ + - ]: 761 : if (!enums.empty())
190 : : {
191 : 761 : unsigned min_term_size = 0;
192 [ + - ]: 761 : Trace("sygus-pbe-enum") << "Register new enumerated values : " << std::endl;
193 : 761 : std::vector<unsigned> szs;
194 [ + + ]: 1924 : for (unsigned i = 0, esize = enums.size(); i < esize; i++)
195 : : {
196 [ + - ]: 1163 : Trace("sygus-pbe-enum") << " " << enums[i] << " -> ";
197 : 1163 : TermDbSygus::toStreamSygus("sygus-pbe-enum", enum_values[i]);
198 [ + - ]: 1163 : Trace("sygus-pbe-enum") << std::endl;
199 [ + + ]: 1163 : if (!enum_values[i].isNull())
200 : : {
201 : 851 : unsigned sz = datatypes::utils::getSygusTermSize(enum_values[i]);
202 : 851 : szs.push_back(sz);
203 [ + + ][ - + ]: 851 : if (i == 0 || sz < min_term_size)
204 : : {
205 : 681 : min_term_size = sz;
206 : : }
207 : : }
208 : : else
209 : : {
210 : 312 : szs.push_back(0);
211 : : }
212 : : }
213 : : // Assume two enumerators of types T1 and T2.
214 : : // If the sygusPbeMultiFair option is true,
215 : : // we ensure that all values of type T1 and size n are enumerated before
216 : : // any term of type T2 of size n+d, and vice versa, where d is
217 : : // set by the sygusPbeMultiFairDiff option. If d is zero, then our
218 : : // enumeration is such that all terms of T1 or T2 of size n are considered
219 : : // before any term of size n+1.
220 : 761 : int diffAllow = options().quantifiers.sygusPbeMultiFairDiff;
221 : 761 : std::vector<unsigned> enum_consider;
222 [ + + ]: 1924 : for (unsigned i = 0, esize = enums.size(); i < esize; i++)
223 : : {
224 [ + + ]: 1163 : if (!enum_values[i].isNull())
225 : : {
226 [ - + ][ - + ]: 851 : Assert(szs[i] >= min_term_size);
[ - - ]
227 : 851 : int diff = szs[i] - min_term_size;
228 [ - + ][ - - ]: 851 : if (!options().quantifiers.sygusPbeMultiFair || diff <= diffAllow)
[ + - ]
229 : : {
230 : 851 : enum_consider.push_back(i);
231 : : }
232 : : }
233 : : }
234 : :
235 : : // only consider the enumerators that are at minimum size (for fairness)
236 [ + - ]: 1522 : Trace("sygus-pbe-enum") << "...register " << enum_consider.size() << " / "
237 : 761 : << enums.size() << std::endl;
238 : 761 : NodeManager* nm = nodeManager();
239 [ + + ]: 1612 : for (unsigned i = 0, ecsize = enum_consider.size(); i < ecsize; i++)
240 : : {
241 : 851 : unsigned j = enum_consider[i];
242 : 851 : Node e = enums[j];
243 : 851 : Node v = enum_values[j];
244 [ - + ][ - + ]: 851 : Assert(d_enum_to_candidate.find(e) != d_enum_to_candidate.end());
[ - - ]
245 : 851 : Node c = d_enum_to_candidate[e];
246 : 851 : std::vector<Node> enum_lems;
247 : 851 : d_sygus_unif[c]->notifyEnumeration(e, v, enum_lems);
248 [ - + ]: 851 : if (!enum_lems.empty())
249 : : {
250 : : // the lemmas must be guarded by the active guard of the enumerator
251 : 0 : Node g = d_tds->getActiveGuardForEnumerator(e);
252 : 0 : Assert(!g.isNull());
253 [ - - ]: 0 : for (unsigned k = 0, size = enum_lems.size(); k < size; k++)
254 : : {
255 : 0 : Node lem = nm->mkNode(Kind::OR, g.negate(), enum_lems[k]);
256 : 0 : d_qim.addPendingLemma(lem,
257 : : InferenceId::QUANTIFIERS_SYGUS_PBE_EXCLUDE);
258 : 0 : }
259 : 0 : }
260 : 851 : }
261 : 761 : }
262 [ + + ]: 844 : for (unsigned i = 0; i < candidates.size(); i++)
263 : : {
264 : 763 : Node c = candidates[i];
265 : : // build decision tree for candidate
266 : 763 : std::vector<Node> sol;
267 : 763 : std::vector<Node> lems;
268 : 763 : bool solSuccess = d_sygus_unif[c]->constructSolution(sol, lems);
269 [ - + ]: 763 : for (const Node& lem : lems)
270 : : {
271 : 0 : d_qim.addPendingLemma(lem,
272 : : InferenceId::QUANTIFIERS_SYGUS_PBE_CONSTRUCT_SOL);
273 : : }
274 [ + + ]: 763 : if (solSuccess)
275 : : {
276 [ - + ][ - + ]: 83 : Assert(sol.size() == 1);
[ - - ]
277 : 83 : candidate_values.push_back(sol[0]);
278 : : }
279 : : else
280 : : {
281 : 680 : return false;
282 : : }
283 [ + + ][ + + ]: 2123 : }
[ + + ]
284 : 81 : return true;
285 : : }
286 : :
287 : : } // namespace quantifiers
288 : : } // namespace theory
289 : : } // namespace cvc5::internal
|
