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