1 /******************************************************************************
2 * Top contributors (to current version):
3 * Andrew Reynolds, Aina Niemetz, Andres Noetzli
5 * This file is part of the cvc5 project.
7 * Copyright (c) 2009-2021 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 * ****************************************************************************
13 * Implementation of candidate_rewrite_database.
16 #include "theory/quantifiers/candidate_rewrite_database.h"
18 #include "options/base_options.h"
19 #include "printer/printer.h"
20 #include "smt/smt_engine.h"
21 #include "smt/smt_engine_scope.h"
22 #include "smt/smt_statistics_registry.h"
23 #include "theory/datatypes/sygus_datatype_utils.h"
24 #include "theory/quantifiers/sygus/term_database_sygus.h"
25 #include "theory/quantifiers/term_util.h"
26 #include "theory/rewriter.h"
29 using namespace cvc5::kind
;
30 using namespace cvc5::context
;
34 namespace quantifiers
{
36 CandidateRewriteDatabase::CandidateRewriteDatabase(
37 Env
& env
, bool doCheck
, bool rewAccel
, bool silent
, bool filterPairs
)
40 d_ext_rewrite(nullptr),
44 d_filterPairs(filterPairs
),
48 void CandidateRewriteDatabase::initialize(const std::vector
<Node
>& vars
,
51 Assert(ss
!= nullptr);
52 d_candidate
= Node::null();
53 d_using_sygus
= false;
55 d_ext_rewrite
= nullptr;
58 d_crewrite_filter
.initialize(ss
, nullptr, false);
60 ExprMiner::initialize(vars
, ss
);
63 void CandidateRewriteDatabase::initializeSygus(const std::vector
<Node
>& vars
,
68 Assert(ss
!= nullptr);
72 d_ext_rewrite
= nullptr;
75 d_crewrite_filter
.initialize(ss
, d_tds
, d_using_sygus
);
77 ExprMiner::initialize(vars
, ss
);
80 Node
CandidateRewriteDatabase::addTerm(Node sol
,
85 // have we added this term before?
86 std::unordered_map
<Node
, Node
>::iterator itac
= d_add_term_cache
.find(sol
);
87 if (itac
!= d_add_term_cache
.end())
94 // if recursive, we first add all subterms
95 for (const Node
& solc
: sol
)
97 // whether a candidate rewrite is printed for any subterm is irrelevant
98 bool rew_printc
= false;
99 addTerm(solc
, rec
, out
, rew_printc
);
103 bool is_unique_term
= true;
104 Node eq_sol
= d_sampler
->registerTerm(sol
);
105 // eq_sol is a candidate solution that is equivalent to sol
108 is_unique_term
= false;
109 // should we filter the pair?
110 if (!d_filterPairs
|| !d_crewrite_filter
.filterPair(sol
, eq_sol
))
112 // get the actual term
114 Node eq_solb
= eq_sol
;
117 Assert(d_tds
!= nullptr);
118 solb
= d_tds
->sygusToBuiltin(sol
);
119 eq_solb
= d_tds
->sygusToBuiltin(eq_sol
);
121 // get the rewritten form
124 if (d_ext_rewrite
!= nullptr)
126 solbr
= d_ext_rewrite
->extendedRewrite(solb
);
127 eq_solr
= d_ext_rewrite
->extendedRewrite(eq_solb
);
131 solbr
= Rewriter::rewrite(solb
);
132 eq_solr
= Rewriter::rewrite(eq_solb
);
134 bool verified
= false;
135 Trace("rr-check") << "Check candidate rewrite..." << std::endl
;
136 // verify it if applicable
139 Node crr
= solbr
.eqNode(eq_solr
).negate();
140 Trace("rr-check") << "Check candidate rewrite : " << crr
<< std::endl
;
142 // Notice we don't set produce-models. rrChecker takes the same
143 // options as the SmtEngine we belong to, where we ensure that
144 // produce-models is set.
145 std::unique_ptr
<SmtEngine
> rrChecker
;
146 initializeChecker(rrChecker
, crr
);
147 Result r
= rrChecker
->checkSat();
148 Trace("rr-check") << "...result : " << r
<< std::endl
;
149 if (r
.asSatisfiabilityResult().isSat() == Result::SAT
)
151 Trace("rr-check") << "...rewrite does not hold for: " << std::endl
;
152 is_unique_term
= true;
153 std::vector
<Node
> vars
;
154 d_sampler
->getVariables(vars
);
155 std::vector
<Node
> pt
;
156 for (const Node
& v
: vars
)
160 // if a bound variable, map to the skolem we introduce before
161 // looking up the model value
162 if (v
.getKind() == BOUND_VARIABLE
)
164 std::map
<Node
, Node
>::iterator itf
= d_fv_to_skolem
.find(v
);
165 if (itf
== d_fv_to_skolem
.end())
167 // not in conjecture, can use arbitrary value
168 val
= v
.getType().mkGroundTerm();
172 // get the model value of its skolem
178 Assert(!refv
.isNull() && refv
.getKind() != BOUND_VARIABLE
);
179 val
= rrChecker
->getValue(refv
);
181 Trace("rr-check") << " " << v
<< " -> " << val
<< std::endl
;
184 d_sampler
->addSamplePoint(pt
);
185 // add the solution again
186 // by construction of the above point, we should be unique now
187 eq_sol
= d_sampler
->registerTerm(sol
);
188 Assert(eq_sol
== sol
);
192 verified
= !r
.asSatisfiabilityResult().isUnknown();
197 // just insist that constants are not relevant pairs
198 if (solb
.isConst() && eq_solb
.isConst())
200 is_unique_term
= true;
206 // register this as a relevant pair (helps filtering)
209 d_crewrite_filter
.registerRelevantPair(sol
, eq_sol
);
211 // The analog of terms sol and eq_sol are equivalent under
212 // sample points but do not rewrite to the same term. Hence,
213 // this indicates a candidate rewrite.
216 out
<< "(" << (verified
? "" : "candidate-") << "rewrite ";
219 TermDbSygus::toStreamSygus(out
, sol
);
221 TermDbSygus::toStreamSygus(out
, eq_sol
);
225 out
<< sol
<< " " << eq_sol
;
227 out
<< ")" << std::endl
;
229 // we count this as printed, despite not literally printing it
231 // debugging information
232 if (Trace
.isOn("sygus-rr-debug"))
234 Trace("sygus-rr-debug") << "; candidate #1 ext-rewrites to: " << solbr
236 Trace("sygus-rr-debug")
237 << "; candidate #2 ext-rewrites to: " << eq_solr
<< std::endl
;
239 if (d_rewAccel
&& d_using_sygus
)
241 Assert(d_tds
!= nullptr);
242 // Add a symmetry breaking clause that excludes the larger
243 // of sol and eq_sol. This effectively states that we no longer
244 // wish to enumerate any term that contains sol (resp. eq_sol)
247 unsigned sz
= datatypes::utils::getSygusTermSize(sol
);
248 unsigned eqsz
= datatypes::utils::getSygusTermSize(eq_sol
);
254 TypeNode ptn
= d_candidate
.getType();
255 Node x
= d_tds
->getFreeVar(ptn
, 0);
256 Node lem
= d_tds
->getExplain()->getExplanationForEquality(x
, exc_sol
);
258 Trace("sygus-rr-sb") << "Symmetry breaking lemma : " << lem
260 d_tds
->registerSymBreakLemma(d_candidate
, lem
, ptn
, sz
);
264 // We count this as a rewrite if we did not explicitly rule it out.
265 // The value of is_unique_term is false iff this call resulted in a rewrite.
266 // Notice that when --sygus-rr-synth-check is enabled,
267 // statistics on number of candidate rewrite rules is
268 // an accurate count of (#enumerated_terms-#unique_terms) only if
269 // the option sygus-rr-synth-filter-order is disabled. The reason
270 // is that the sygus sampler may reason that a candidate rewrite
271 // rule is not useful since its variables are unordered, whereby
272 // it discards it as a redundant candidate rewrite rule before
273 // checking its correctness.
275 d_add_term_cache
[sol
] = eq_sol
;
279 Node
CandidateRewriteDatabase::addTerm(Node sol
, bool rec
, std::ostream
& out
)
281 bool rew_print
= false;
282 return addTerm(sol
, rec
, out
, rew_print
);
284 bool CandidateRewriteDatabase::addTerm(Node sol
, std::ostream
& out
)
286 Node rsol
= addTerm(sol
, false, out
);
290 void CandidateRewriteDatabase::setSilent(bool flag
) { d_silent
= flag
; }
292 void CandidateRewriteDatabase::setExtendedRewriter(ExtendedRewriter
* er
)
297 } // namespace quantifiers
298 } // namespace theory