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 dynamic quantifiers splitting.
11 : : */
12 : :
13 : : #include "theory/quantifiers/quant_split.h"
14 : :
15 : : #include "expr/bound_var_manager.h"
16 : : #include "expr/dtype.h"
17 : : #include "expr/dtype_cons.h"
18 : : #include "options/quantifiers_options.h"
19 : : #include "options/smt_options.h"
20 : : #include "proof/proof.h"
21 : : #include "proof/proof_generator.h"
22 : : #include "theory/datatypes/theory_datatypes_utils.h"
23 : : #include "theory/quantifiers/first_order_model.h"
24 : : #include "theory/quantifiers/term_database.h"
25 : : #include "util/rational.h"
26 : :
27 : : using namespace cvc5::internal::kind;
28 : :
29 : : namespace cvc5::internal {
30 : : namespace theory {
31 : : namespace quantifiers {
32 : :
33 : : /**
34 : : * A proof generator for quantifiers splitting inferences
35 : : */
36 : : class QuantDSplitProofGenerator : protected EnvObj, public ProofGenerator
37 : : {
38 : : public:
39 : 13596 : QuantDSplitProofGenerator(Env& env) : EnvObj(env), d_index(userContext()) {}
40 : 27151 : virtual ~QuantDSplitProofGenerator() {}
41 : : /**
42 : : * Get proof for fact. This expects facts of the form
43 : : * q = QuantDSplit::split(nm, q, n)
44 : : * We prove this by:
45 : : * ------ QUANT_VAR_REORDERING ---------------------------- QUANT_DT_SPLIT
46 : : * q = q' q' = QuantDSplit::split(nm, q', 0)
47 : : * --------------------------------------------------------------- TRANS
48 : : * q = QuantDSplit::split(nm, q, n)
49 : : *
50 : : * where the variables in q' is reordered from q such that the variable to
51 : : * split comes first.
52 : : *
53 : : * Note that this elaboration relies on the fact that the variables
54 : : * introduced for QuantDSplit::split(nm, q', 0) are the same as those for
55 : : * QuantDSplit::split(nm, q, n), since q and q' have the same body
56 : : * and these two splits refer to the same variables, which is the basis
57 : : * for the bound variables introduced (QDSplitVarAttribute).
58 : : */
59 : 40 : std::shared_ptr<ProofNode> getProofFor(Node fact) override
60 : : {
61 : 80 : CDProof cdp(d_env);
62 : : // find the index of the variable that was split for this lemma
63 : 40 : context::CDHashMap<Node, size_t>::iterator it = d_index.find(fact);
64 [ - + ]: 40 : if (it == d_index.end())
65 : : {
66 : 0 : DebugUnhandled() << "QuantDSplitProofGenerator failed to get proof";
67 : : return nullptr;
68 : : }
69 : 40 : Assert(fact.getKind() == Kind::EQUAL && fact[0].getKind() == Kind::FORALL);
70 : 40 : Node q = fact[0];
71 : 40 : std::vector<Node> transEq;
72 [ + + ]: 40 : if (it->second != 0)
73 : : {
74 : : // must reorder variables
75 : 10 : std::vector<Node> newVars;
76 : 10 : newVars.push_back(q[0][it->second]);
77 [ + + ]: 34 : for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
78 : : {
79 [ + + ]: 24 : if (i != it->second)
80 : : {
81 : 14 : newVars.emplace_back(q[0][i]);
82 : : }
83 : : }
84 : 10 : std::vector<Node> qc(q.begin(), q.end());
85 : 10 : NodeManager* nm = nodeManager();
86 : 10 : qc[0] = nm->mkNode(Kind::BOUND_VAR_LIST, newVars);
87 : 10 : Node qn = nm->mkNode(Kind::FORALL, qc);
88 : 10 : Node eqq = q.eqNode(qn);
89 : 20 : cdp.addStep(eqq, ProofRule::QUANT_VAR_REORDERING, {}, {eqq});
90 : 10 : transEq.emplace_back(eqq);
91 : 10 : q = qn;
92 : 10 : }
93 : 40 : Node eqq2 = q.eqNode(fact[1]);
94 : 40 : cdp.addTheoryRewriteStep(eqq2, ProofRewriteRule::QUANT_DT_SPLIT);
95 [ + + ]: 40 : if (!transEq.empty())
96 : : {
97 : 10 : transEq.emplace_back(eqq2);
98 : 10 : cdp.addStep(fact, ProofRule::TRANS, transEq, {});
99 : : }
100 : 40 : return cdp.getProofFor(fact);
101 : 40 : }
102 : : /** identify */
103 : 0 : std::string identify() const override { return "QuantDSplitProofGenerator"; }
104 : : /**
105 : : * Notify that the given lemma used the given variable index to split. We
106 : : * store this in d_index and use it to guide proof reconstruction above.
107 : : */
108 : 1149 : void notifyLemma(const Node& lem, size_t index) { d_index[lem] = index; }
109 : :
110 : : private:
111 : : /** Mapping from lemmas to their notified index */
112 : : context::CDHashMap<Node, size_t> d_index;
113 : : };
114 : :
115 : 41109 : QuantDSplit::QuantDSplit(Env& env,
116 : : QuantifiersState& qs,
117 : : QuantifiersInferenceManager& qim,
118 : : QuantifiersRegistry& qr,
119 : 41109 : TermRegistry& tr)
120 : : : QuantifiersModule(env, qs, qim, qr, tr),
121 : 41109 : d_quant_to_reduce(userContext()),
122 : 41109 : d_added_split(userContext()),
123 [ + + ]: 41109 : d_pfgen(options().smt.produceProofs ? new QuantDSplitProofGenerator(d_env)
124 : 41109 : : nullptr)
125 : : {
126 : 41109 : }
127 : :
128 : 31297 : void QuantDSplit::checkOwnership(Node q)
129 : : {
130 : : // If q is non-standard (marked as sygus, quantifier elimination, etc.), then
131 : : // do no split it.
132 : 31297 : QAttributes qa;
133 : 31297 : QuantAttributes::computeQuantAttributes(q, qa);
134 [ + + ]: 31297 : if (!qa.isStandard())
135 : : {
136 : 3647 : return;
137 : : }
138 : : // do not split if there is a trigger
139 [ + + ]: 27650 : if (qa.d_hasPattern)
140 : : {
141 : 2270 : return;
142 : : }
143 : 25380 : bool takeOwnership = false;
144 : 25380 : bool doSplit = false;
145 : 25380 : QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference();
146 [ + - ]: 50760 : Trace("quant-dsplit-debug")
147 : 25380 : << "Check split quantified formula : " << q << std::endl;
148 [ + + ]: 81019 : for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
149 : : {
150 : 114210 : TypeNode tn = q[0][i].getType();
151 [ + + ]: 57105 : if (tn.isDatatype())
152 : : {
153 : 7701 : bool isFinite = d_env.isFiniteType(tn);
154 : 7701 : const DType& dt = tn.getDType();
155 [ + + ]: 7701 : if (dt.isRecursiveSingleton(tn))
156 : : {
157 [ + - ][ - + ]: 644 : Trace("quant-dsplit-debug") << "Datatype " << dt.getName()
[ - - ]
158 : 322 : << " is recursive singleton." << std::endl;
159 : : }
160 : : else
161 : : {
162 : 7379 : if (options().quantifiers.quantDynamicSplit
163 [ - + ]: 7379 : == options::QuantDSplitMode::AGG)
164 : : {
165 : : // split if it is a finite datatype
166 : 0 : doSplit = isFinite;
167 : : }
168 : 7379 : else if (options().quantifiers.quantDynamicSplit
169 [ + - ]: 7379 : == options::QuantDSplitMode::DEFAULT)
170 : : {
171 [ + + ]: 7379 : if (!qbi.isFiniteBound(q, q[0][i]))
172 : : {
173 [ + + ]: 7197 : if (isFinite)
174 : : {
175 : : // split if goes from being unhandled -> handled by finite
176 : : // instantiation. An example is datatypes with uninterpreted sort
177 : : // fields which are "interpreted finite" but not "finite".
178 : 46 : doSplit = true;
179 : : // we additionally take ownership of this formula, in other words,
180 : : // we mark it reduced.
181 : 46 : takeOwnership = true;
182 : : }
183 [ + + ][ + - ]: 7151 : else if (dt.getNumConstructors() == 1 && !dt.isCodatatype())
[ + + ]
184 : : {
185 : : // split if only one constructor
186 : 1420 : doSplit = true;
187 : : }
188 : : }
189 : : }
190 [ + + ]: 7379 : if (doSplit)
191 : : {
192 : : // store the index to split
193 : 1466 : d_quant_to_reduce[q] = i;
194 [ + - ]: 2932 : Trace("quant-dsplit-debug")
195 [ - + ][ - - ]: 1466 : << "Split at index " << i << " based on datatype " << dt.getName()
196 : 1466 : << std::endl;
197 : 1466 : break;
198 : : }
199 [ + - ]: 11826 : Trace("quant-dsplit-debug")
200 [ - + ][ - - ]: 5913 : << "Do not split based on datatype " << dt.getName() << std::endl;
201 : : }
202 : : }
203 [ + + ]: 57105 : }
204 : :
205 [ + + ]: 25380 : if (takeOwnership)
206 : : {
207 [ + - ]: 46 : Trace("quant-dsplit-debug") << "Will take ownership." << std::endl;
208 : 46 : d_qreg.setOwner(q, this);
209 : : }
210 : : // Notice we may not take ownership in some cases, meaning that both the
211 : : // original quantified formula and the split one are generated. This may
212 : : // increase our ability to answer "unsat", since quantifier instantiation
213 : : // heuristics may be more effective for one or the other (see issues #993
214 : : // and 3481).
215 [ + + ]: 31297 : }
216 : :
217 : : /* whether this module needs to check this round */
218 : 113042 : bool QuantDSplit::needsCheck(Theory::Effort e)
219 : : {
220 [ + + ][ + + ]: 113042 : return e >= Theory::EFFORT_FULL && !d_quant_to_reduce.empty();
221 : : }
222 : :
223 : 786 : bool QuantDSplit::checkCompleteFor(Node q)
224 : : {
225 : : // true if we split q
226 : 786 : return d_added_split.find(q) != d_added_split.end();
227 : : }
228 : :
229 : : /* Call during quantifier engine's check */
230 : 3463 : void QuantDSplit::check(CVC5_UNUSED Theory::Effort e, QEffort quant_e)
231 : : {
232 : : // add lemmas ASAP (they are a reduction)
233 [ + + ]: 3463 : if (quant_e != QEFFORT_CONFLICT)
234 : : {
235 : 2211 : return;
236 : : }
237 [ + - ]: 1252 : Trace("quant-dsplit") << "QuantDSplit::check" << std::endl;
238 : 1252 : FirstOrderModel* m = d_treg.getModel();
239 : 1252 : for (NodeIntMap::iterator it = d_quant_to_reduce.begin();
240 [ + + ]: 23277 : it != d_quant_to_reduce.end();
241 : 22025 : ++it)
242 : : {
243 : 22025 : Node q = it->first;
244 [ + - ]: 22025 : Trace("quant-dsplit") << "- Split quantifier " << q << std::endl;
245 [ + + ]: 22025 : if (d_added_split.find(q) != d_added_split.end())
246 : : {
247 : 20420 : continue;
248 : : }
249 : 1605 : if (m->isQuantifierAsserted(q) && m->isQuantifierActive(q))
250 : : {
251 : 1425 : d_added_split.insert(q);
252 : 1425 : Node qsplit = split(nodeManager(), q, it->second);
253 : 1425 : Node lem = q.eqNode(qsplit);
254 : : // must remember the variable index if proofs are enabled
255 [ + + ]: 1425 : if (d_pfgen != nullptr)
256 : : {
257 : 1136 : d_pfgen->notifyLemma(lem, it->second);
258 : : }
259 [ + - ]: 1425 : Trace("quant-dsplit") << "QuantDSplit lemma : " << lem << std::endl;
260 [ + + ]: 1425 : d_qim.addPendingLemma(lem,
261 : : InferenceId::QUANTIFIERS_DSPLIT,
262 : : LemmaProperty::NONE,
263 : 1425 : d_pfgen.get());
264 : 1425 : }
265 [ + + ]: 22025 : }
266 [ + - ]: 1252 : Trace("quant-dsplit") << "QuantDSplit::check finished" << std::endl;
267 : : }
268 : :
269 : 1608 : Node QuantDSplit::split(NodeManager* nm, const Node& q, size_t index)
270 : : {
271 : 1608 : std::vector<Node> bvs;
272 [ + + ]: 6838 : for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
273 : : {
274 [ + + ]: 5230 : if (i != index)
275 : : {
276 : 3622 : bvs.push_back(q[0][i]);
277 : : }
278 : : }
279 : 3216 : TNode svar = q[0][index];
280 : 1608 : TypeNode tn = svar.getType();
281 [ - + ][ - + ]: 1608 : Assert(tn.isDatatype());
[ - - ]
282 : 1608 : std::vector<Node> cons;
283 : 1608 : const DType& dt = tn.getDType();
284 : 1608 : BoundVarManager* bvm = nm->getBoundVarManager();
285 : 1608 : size_t varCount = 0;
286 [ + + ]: 3634 : for (size_t j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
287 : : {
288 : 2026 : std::vector<Node> vars;
289 : 2026 : TypeNode dtjtn = dt[j].getInstantiatedConstructorType(tn);
290 [ - + ][ - + ]: 2026 : Assert(dtjtn.getNumChildren() == dt[j].getNumArgs() + 1);
[ - - ]
291 [ + + ]: 5690 : for (size_t k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
292 : : {
293 : 3664 : TypeNode tns = dtjtn[k];
294 : 7328 : Node cacheVal = bvm->getCacheValue(q[1], q[0][index], varCount);
295 : 3664 : varCount++;
296 : 7328 : Node v = bvm->mkBoundVar(BoundVarId::QUANT_DT_SPLIT, cacheVal, tns);
297 : 3664 : vars.push_back(v);
298 : 3664 : }
299 : 2026 : std::vector<Node> bvs_cmb;
300 : 2026 : bvs_cmb.insert(bvs_cmb.end(), bvs.begin(), bvs.end());
301 : 2026 : bvs_cmb.insert(bvs_cmb.end(), vars.begin(), vars.end());
302 : 2026 : Node c = datatypes::utils::mkApplyCons(tn, dt, j, vars);
303 : 2026 : TNode ct = c;
304 : 4052 : Node body = q[1].substitute(svar, ct);
305 [ + + ]: 2026 : if (!bvs_cmb.empty())
306 : : {
307 : 1981 : Node bvl = nm->mkNode(Kind::BOUND_VAR_LIST, bvs_cmb);
308 : 1981 : std::vector<Node> children;
309 : 1981 : children.push_back(bvl);
310 : 1981 : children.push_back(body);
311 [ - + ]: 1981 : if (q.getNumChildren() == 3)
312 : : {
313 : 0 : Node ipls = q[2].substitute(svar, ct);
314 : 0 : children.push_back(ipls);
315 : 0 : }
316 : 1981 : body = nm->mkNode(Kind::FORALL, children);
317 : 1981 : }
318 : 2026 : cons.push_back(body);
319 : 2026 : }
320 : 3216 : return nm->mkAnd(cons);
321 : 1608 : }
322 : :
323 : 13 : std::shared_ptr<ProofNode> QuantDSplit::getQuantDtSplitProof(Env& env,
324 : : const Node& q,
325 : : size_t index)
326 : : {
327 : 13 : Node qs = split(env.getNodeManager(), q, index);
328 [ - + ]: 13 : if (qs.isNull())
329 : : {
330 : 0 : return nullptr;
331 : : }
332 : 13 : Node eq = q.eqNode(qs);
333 : 13 : QuantDSplitProofGenerator pg(env);
334 : 13 : pg.notifyLemma(eq, index);
335 : 13 : return pg.getProofFor(eq);
336 : 13 : }
337 : :
338 : : } // namespace quantifiers
339 : : } // namespace theory
340 : : } // namespace cvc5::internal
|
