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 candidate_rewrite_database.
11 : : */
12 : :
13 : : #include "theory/quantifiers/candidate_rewrite_database.h"
14 : :
15 : : #include "options/base_options.h"
16 : : #include "options/quantifiers_options.h"
17 : : #include "printer/printer.h"
18 : : #include "smt/set_defaults.h"
19 : : #include "theory/datatypes/sygus_datatype_utils.h"
20 : : #include "theory/quantifiers/sygus/term_database_sygus.h"
21 : : #include "theory/quantifiers/term_util.h"
22 : : #include "theory/rewriter.h"
23 : :
24 : : using namespace std;
25 : : using namespace cvc5::internal::kind;
26 : : using namespace cvc5::context;
27 : :
28 : : namespace cvc5::internal {
29 : : namespace theory {
30 : : namespace quantifiers {
31 : :
32 : 165 : CandidateRewriteDatabase::CandidateRewriteDatabase(
33 : 165 : Env& env, bool doCheck, bool rewAccel, bool filterPairs, bool rec)
34 : : : ExprMiner(env),
35 : 165 : d_tds(nullptr),
36 : 165 : d_useExtRewriter(false),
37 : 165 : d_doCheck(doCheck),
38 : 165 : d_rewAccel(rewAccel),
39 : 165 : d_filterPairs(filterPairs),
40 : 165 : d_using_sygus(false),
41 : 165 : d_rec(rec),
42 : 165 : d_crewrite_filter(env)
43 : : {
44 : : // determine the options to use for the verification subsolvers we spawn
45 : : // we start with the provided options
46 : 165 : d_subOptions.copyValues(options());
47 : : // disable checking
48 : 165 : smt::SetDefaults::disableChecking(d_subOptions);
49 : 165 : }
50 : 165 : void CandidateRewriteDatabase::initialize(const std::vector<Node>& vars,
51 : : SygusSampler* ss)
52 : : {
53 [ - + ][ - + ]: 165 : Assert(ss != nullptr);
[ - - ]
54 : 165 : d_candidate = Node::null();
55 : 165 : d_using_sygus = false;
56 : 165 : d_tds = nullptr;
57 : 165 : d_useExtRewriter = false;
58 [ + + ]: 165 : if (d_filterPairs)
59 : : {
60 : 39 : d_crewrite_filter.initialize(ss, nullptr, false);
61 : : }
62 : 165 : ExprMiner::initialize(vars, ss);
63 : 165 : }
64 : :
65 : 0 : void CandidateRewriteDatabase::initializeSygus(const std::vector<Node>& vars,
66 : : TermDbSygus* tds,
67 : : Node f,
68 : : SygusSampler* ss)
69 : : {
70 : 0 : Assert(ss != nullptr);
71 : 0 : d_candidate = f;
72 : 0 : d_using_sygus = true;
73 : 0 : d_tds = tds;
74 : 0 : d_useExtRewriter = false;
75 [ - - ]: 0 : if (d_filterPairs)
76 : : {
77 : 0 : d_crewrite_filter.initialize(ss, d_tds, d_using_sygus);
78 : : }
79 : 0 : ExprMiner::initialize(vars, ss);
80 : 0 : }
81 : :
82 : 0 : bool CandidateRewriteDatabase::wasVerified(const Node& rewrite) const
83 : : {
84 : 0 : return d_verified.find(rewrite) != d_verified.end();
85 : : }
86 : :
87 : 2669 : Node CandidateRewriteDatabase::addOrGetTerm(Node sol,
88 : : std::vector<Node>& rewrites)
89 : : {
90 : : // have we added this term before?
91 : 2669 : std::unordered_map<Node, Node>::iterator itac = d_add_term_cache.find(sol);
92 [ + + ]: 2669 : if (itac != d_add_term_cache.end())
93 : : {
94 : 308 : return itac->second;
95 : : }
96 : :
97 [ - + ]: 2361 : if (d_rec)
98 : : {
99 : : // if recursive, we first add all subterms
100 [ - - ]: 0 : for (const Node& solc : sol)
101 : : {
102 : : // whether a candidate rewrite is printed for any subterm is irrelevant
103 : 0 : addTerm(solc, rewrites);
104 : 0 : }
105 : : }
106 : : // register the term
107 : 2361 : bool is_unique_term = true;
108 : 2361 : Node eq_sol = d_sampler->registerTerm(sol);
109 [ + - ]: 2361 : Trace("rr-check-r") << sol << " returns " << eq_sol << std::endl;
110 : : // eq_sol is a candidate solution that is equivalent to sol
111 [ + + ]: 2361 : if (eq_sol != sol)
112 : : {
113 : 277 : is_unique_term = false;
114 : : // should we filter the pair?
115 : 277 : if (!d_filterPairs || !d_crewrite_filter.filterPair(sol, eq_sol))
116 : : {
117 : : // get the actual term
118 : 277 : Node solb = sol;
119 : 277 : Node eq_solb = eq_sol;
120 [ - + ]: 277 : if (d_using_sygus)
121 : : {
122 : 0 : Assert(d_tds != nullptr);
123 : 0 : solb = d_tds->sygusToBuiltin(sol);
124 : 0 : eq_solb = d_tds->sygusToBuiltin(eq_sol);
125 : : }
126 : : // get the rewritten form
127 : 277 : Node solbr;
128 : 277 : Node eq_solr;
129 [ - + ]: 277 : if (d_useExtRewriter)
130 : : {
131 : 0 : solbr = extendedRewrite(solb);
132 : 0 : eq_solr = extendedRewrite(eq_solb);
133 : : }
134 : : else
135 : : {
136 : 277 : solbr = rewrite(solb);
137 : 277 : eq_solr = rewrite(eq_solb);
138 : : }
139 : 277 : bool verified = false;
140 [ + - ]: 277 : Trace("rr-check") << "Check candidate rewrite..." << std::endl;
141 : : // verify it if applicable
142 [ + - ]: 277 : if (d_doCheck)
143 : : {
144 : 277 : Node crr = solbr.eqNode(eq_solr).negate();
145 [ + - ]: 277 : Trace("rr-check") << "Check candidate rewrite : " << crr << std::endl;
146 : :
147 : : // Notice we don't set produce-models. rrChecker takes the same
148 : : // options as the SolverEngine we belong to, where we ensure that
149 : : // produce-models is set.
150 : 277 : SubsolverSetupInfo ssi(d_env, d_subOptions);
151 : 277 : std::unique_ptr<SolverEngine> rrChecker;
152 : 277 : initializeChecker(rrChecker, crr, ssi);
153 : 277 : Result r = rrChecker->checkSat();
154 [ + - ]: 277 : Trace("rr-check") << "...result : " << r << std::endl;
155 [ + + ]: 277 : if (r.getStatus() == Result::SAT)
156 : : {
157 [ + - ]: 236 : Trace("rr-check") << "...rewrite does not hold for: " << std::endl;
158 : 236 : is_unique_term = true;
159 : 236 : std::vector<Node> vars;
160 : 236 : d_sampler->getVariables(vars);
161 : 236 : std::vector<Node> pt;
162 [ + + ]: 760 : for (const Node& v : vars)
163 : : {
164 : 524 : Node val;
165 : 524 : Node refv = v;
166 : : // if a bound variable, map to the skolem we introduce before
167 : : // looking up the model value
168 [ + - ]: 524 : if (v.getKind() == Kind::BOUND_VARIABLE)
169 : : {
170 : 524 : std::map<Node, Node>::iterator itf = d_fv_to_skolem.find(v);
171 [ - + ]: 524 : if (itf == d_fv_to_skolem.end())
172 : : {
173 : : // not in conjecture, can use arbitrary value
174 : 0 : val = NodeManager::mkGroundTerm(v.getType());
175 : : }
176 : : else
177 : : {
178 : : // get the model value of its skolem
179 : 524 : refv = itf->second;
180 : : }
181 : : }
182 [ + - ]: 524 : if (val.isNull())
183 : : {
184 [ + - ][ + - ]: 524 : Assert(!refv.isNull() && refv.getKind() != Kind::BOUND_VARIABLE);
[ - + ][ - + ]
[ - - ]
185 : 524 : val = rrChecker->getValue(refv);
186 : : }
187 [ + - ]: 524 : Trace("rr-check") << " " << v << " -> " << val << std::endl;
188 : 524 : pt.push_back(val);
189 : 524 : }
190 : 236 : d_sampler->addSamplePoint(pt);
191 : : // add the solution again
192 : : // by construction of the above point, we should be unique now
193 : 236 : eq_sol = d_sampler->registerTerm(sol);
194 : 236 : Assert(eq_sol == sol) << "Model failed to distinguish terms "
195 [ - + ][ - + ]: 236 : << eq_sol << " and " << sol;
[ - - ]
196 : 236 : }
197 : : else
198 : : {
199 : 41 : verified = !r.isUnknown();
200 : : }
201 : 277 : }
202 : : else
203 : : {
204 : : // just insist that constants are not relevant pairs
205 : 0 : if (solb.isConst() && eq_solb.isConst())
206 : : {
207 : 0 : is_unique_term = true;
208 : 0 : eq_sol = sol;
209 : : }
210 : : }
211 [ + + ]: 277 : if (!is_unique_term)
212 : : {
213 : : // register this as a relevant pair (helps filtering)
214 [ + + ]: 41 : if (d_filterPairs)
215 : : {
216 : 3 : d_crewrite_filter.registerRelevantPair(sol, eq_sol);
217 : : }
218 : : // The analog of terms sol and eq_sol are equivalent under
219 : : // sample points but do not rewrite to the same term. Hence,
220 : : // this indicates a candidate rewrite.
221 : 41 : Node eq = solb.eqNode(eq_sol);
222 : 41 : rewrites.push_back(eq);
223 [ + - ]: 41 : if (verified)
224 : : {
225 : 41 : d_verified.insert(eq);
226 : : }
227 : : // debugging information
228 [ - + ]: 41 : if (TraceIsOn("sygus-rr-debug"))
229 : : {
230 [ - - ]: 0 : Trace("sygus-rr-debug")
231 : 0 : << "; candidate #1 ext-rewrites to: " << solbr << std::endl;
232 [ - - ]: 0 : Trace("sygus-rr-debug")
233 : 0 : << "; candidate #2 ext-rewrites to: " << eq_solr << std::endl;
234 : : }
235 [ - + ][ - - ]: 41 : if (d_rewAccel && d_using_sygus)
236 : : {
237 : 0 : Assert(d_tds != nullptr);
238 : : // Add a symmetry breaking clause that excludes the larger
239 : : // of sol and eq_sol. This effectively states that we no longer
240 : : // wish to enumerate any term that contains sol (resp. eq_sol)
241 : : // as a subterm.
242 : 0 : Node exc_sol = sol;
243 : 0 : unsigned sz = datatypes::utils::getSygusTermSize(sol);
244 : 0 : unsigned eqsz = datatypes::utils::getSygusTermSize(eq_sol);
245 [ - - ]: 0 : if (eqsz > sz)
246 : : {
247 : 0 : sz = eqsz;
248 : 0 : exc_sol = eq_sol;
249 : : }
250 : 0 : TypeNode ptn = d_candidate.getType();
251 : 0 : Node x = d_tds->getFreeVar(ptn, 0);
252 : 0 : Node lem = d_tds->getExplain()->getExplanationForEquality(x, exc_sol);
253 : 0 : lem = lem.negate();
254 [ - - ]: 0 : Trace("sygus-rr-sb")
255 : 0 : << "Symmetry breaking lemma : " << lem << std::endl;
256 : 0 : d_tds->registerSymBreakLemma(d_candidate, lem, ptn, sz);
257 : 0 : }
258 : 41 : }
259 : : // If we failed to verify, then we return the original term. This is done
260 : : // so that the user of this method is not told of a rewrite rule that
261 : : // may not hold. Furthermore, note that the term is not added to the lazy
262 : : // trie in the sygus sampler. This means that the set of rewrites is not
263 : : // complete, as we are discarding the current solution. Ideally, we would
264 : : // store a list of terms (that are pairwise unknown to be equal) at each
265 : : // leaf of the lazy trie.
266 [ + + ]: 277 : if (!verified)
267 : : {
268 : 236 : eq_sol = sol;
269 : : }
270 : 277 : }
271 : : // We count this as a rewrite if we did not explicitly rule it out.
272 : : // The value of is_unique_term is false iff this call resulted in a rewrite.
273 : : // Notice that when --sygus-rr-synth-check is enabled,
274 : : // statistics on number of candidate rewrite rules is
275 : : // an accurate count of (#enumerated_terms-#unique_terms) only if
276 : : // the option sygus-rr-synth-filter-order is disabled. The reason
277 : : // is that the sygus sampler may reason that a candidate rewrite
278 : : // rule is not useful since its variables are unordered, whereby
279 : : // it discards it as a redundant candidate rewrite rule before
280 : : // checking its correctness.
281 : : }
282 : 2361 : d_add_term_cache[sol] = eq_sol;
283 : 2361 : return eq_sol;
284 : 2361 : }
285 : :
286 : 395 : bool CandidateRewriteDatabase::addTerm(Node sol, std::vector<Node>& rewrites)
287 : : {
288 : 395 : Node rsol = addOrGetTerm(sol, rewrites);
289 : 790 : return sol == rsol;
290 : 395 : }
291 : :
292 : 0 : void CandidateRewriteDatabase::enableExtendedRewriter()
293 : : {
294 : 0 : d_useExtRewriter = true;
295 : 0 : }
296 : :
297 : : } // namespace quantifiers
298 : : } // namespace theory
299 : : } // namespace cvc5::internal
|
