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