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