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 : : * Pool-based instantiation strategy
11 : : */
12 : :
13 : : #include "theory/quantifiers/inst_strategy_pool.h"
14 : :
15 : : #include "options/quantifiers_options.h"
16 : : #include "theory/quantifiers/first_order_model.h"
17 : : #include "theory/quantifiers/instantiate.h"
18 : : #include "theory/quantifiers/quantifiers_inference_manager.h"
19 : : #include "theory/quantifiers/term_pools.h"
20 : : #include "theory/quantifiers/term_registry.h"
21 : : #include "theory/quantifiers/term_tuple_enumerator.h"
22 : :
23 : : using namespace cvc5::internal::kind;
24 : : using namespace cvc5::context;
25 : :
26 : : namespace cvc5::internal {
27 : : namespace theory {
28 : : namespace quantifiers {
29 : :
30 : 44250 : InstStrategyPool::InstStrategyPool(Env& env,
31 : : QuantifiersState& qs,
32 : : QuantifiersInferenceManager& qim,
33 : : QuantifiersRegistry& qr,
34 : 44250 : TermRegistry& tr)
35 : 44250 : : QuantifiersModule(env, qs, qim, qr, tr)
36 : : {
37 : 44250 : }
38 : :
39 : 40070 : void InstStrategyPool::presolve() {}
40 : :
41 : 148127 : bool InstStrategyPool::needsCheck(Theory::Effort e)
42 : : {
43 : 148127 : return d_qstate.getInstWhenNeedsCheck(e);
44 : : }
45 : :
46 : 67790 : void InstStrategyPool::reset_round(CVC5_UNUSED Theory::Effort e) {}
47 : :
48 : 53670 : void InstStrategyPool::registerQuantifier(Node q)
49 : : {
50 [ - + ]: 53670 : if (options().quantifiers.userPoolQuant == options::UserPoolMode::IGNORE)
51 : : {
52 : 0 : return;
53 : : }
54 : : // take into account user pools
55 [ + + ]: 53670 : if (q.getNumChildren() == 3)
56 : : {
57 : 21966 : Node subsPat = d_qreg.substituteBoundVariablesToInstConstants(q[2], q);
58 : : // add patterns
59 [ + + ]: 22826 : for (const Node& p : subsPat)
60 : : {
61 [ + + ]: 11843 : if (p.getKind() == Kind::INST_POOL)
62 : : {
63 : 54 : if (hasTupleSemantics(q, p) || hasProductSemantics(q, p))
64 : : {
65 : 54 : d_userPools[q].push_back(p);
66 : : }
67 : : else
68 : : {
69 [ - - ]: 0 : Warning() << "Cannot find semantics of pool " << p << " in " << q
70 : 0 : << std::endl;
71 : : }
72 : : }
73 : 11843 : }
74 : 10983 : }
75 : : }
76 : :
77 : 53670 : void InstStrategyPool::checkOwnership(Node q)
78 : : {
79 : 53670 : if (options().quantifiers.userPoolQuant == options::UserPoolMode::TRUST
80 [ + - ][ + + ]: 53670 : && q.getNumChildren() == 3)
[ + + ]
81 : : {
82 : : // if only using pools for instantiation, take ownership of this quantified
83 : : // formula
84 [ + + ]: 22767 : for (const Node& p : q[2])
85 : : {
86 [ + + ]: 11838 : if (p.getKind() == Kind::INST_POOL)
87 : : {
88 : 54 : d_qreg.setOwner(q, this, 1);
89 : 54 : return;
90 : : }
91 [ + + ][ + + ]: 22821 : }
92 : : }
93 : : }
94 : :
95 : 302 : bool InstStrategyPool::hasProductSemantics(Node q, Node p)
96 : : {
97 [ + - ][ + - ]: 302 : Assert(q.getKind() == Kind::EXISTS || q.getKind() == Kind::FORALL);
[ - + ][ - + ]
[ - - ]
98 [ - + ][ - + ]: 302 : Assert(p.getKind() == Kind::INST_POOL);
[ - - ]
99 : 302 : size_t nchild = p.getNumChildren();
100 [ + + ]: 302 : if (nchild != q[0].getNumChildren())
101 : : {
102 : 9 : return false;
103 : : }
104 [ + + ]: 687 : for (size_t i = 0; i < nchild; i++)
105 : : {
106 [ - + ][ - + ]: 394 : Assert(p[i].getType().isSet());
[ - - ]
107 : 788 : TypeNode tn = p[i].getType().getSetElementType();
108 [ - + ]: 394 : if (tn != q[0][i].getType())
109 : : {
110 : : // the i^th pool in the annotation does not match the i^th variable
111 : 0 : return false;
112 : : }
113 [ + - ]: 394 : }
114 : 293 : return true;
115 : : }
116 : :
117 : 147 : bool InstStrategyPool::hasTupleSemantics(Node q, Node p)
118 : : {
119 [ + - ][ + - ]: 147 : Assert(q.getKind() == Kind::EXISTS || q.getKind() == Kind::FORALL);
[ - + ][ - + ]
[ - - ]
120 [ - + ][ - + ]: 147 : Assert(p.getKind() == Kind::INST_POOL);
[ - - ]
121 [ + + ]: 147 : if (p.getNumChildren() != 1)
122 : : {
123 : 50 : return false;
124 : : }
125 [ - + ][ - + ]: 97 : Assert(p[0].getType().isSet());
[ - - ]
126 : 194 : TypeNode ptn = p[0].getType().getSetElementType();
127 [ + + ]: 97 : if (!ptn.isTuple())
128 : : {
129 : 78 : return false;
130 : : }
131 : 19 : std::vector<TypeNode> targs = ptn.getTupleTypes();
132 : 19 : size_t nchild = targs.size();
133 [ - + ]: 19 : if (nchild != q[0].getNumChildren())
134 : : {
135 : 0 : return false;
136 : : }
137 [ + + ]: 57 : for (size_t i = 0; i < nchild; i++)
138 : : {
139 [ - + ]: 38 : if (targs[i] != q[0][i].getType())
140 : : {
141 : : // the i^th component type of the pool in the annotation does not match
142 : : // the i^th variable
143 : 0 : return false;
144 : : }
145 : : }
146 : 19 : return true;
147 : 97 : }
148 : :
149 : 131949 : void InstStrategyPool::check(CVC5_UNUSED Theory::Effort e,
150 : : CVC5_UNUSED QEffort quant_e)
151 : : {
152 [ + + ]: 131949 : if (d_userPools.empty())
153 : : {
154 : 131910 : return;
155 : : }
156 : 39 : beginCallDebug();
157 : 39 : FirstOrderModel* fm = d_treg.getModel();
158 : 39 : bool inConflict = false;
159 : 39 : uint64_t addedLemmas = 0;
160 : 39 : size_t nquant = fm->getNumAssertedQuantifiers();
161 : 39 : std::map<Node, std::vector<Node> >::iterator uit;
162 [ + + ]: 143 : for (size_t i = 0; i < nquant; i++)
163 : : {
164 : 104 : Node q = fm->getAssertedQuantifier(i, true);
165 : 104 : uit = d_userPools.find(q);
166 [ + + ]: 104 : if (uit == d_userPools.end())
167 : : {
168 : : // no user pools for this
169 : 20 : continue;
170 : : }
171 [ - + ]: 84 : if (!d_qreg.hasOwnership(q, this))
172 : : {
173 : : // quantified formula is not owned by this
174 : 0 : continue;
175 : : }
176 : : // process with each user pool
177 [ + + ]: 168 : for (const Node& p : uit->second)
178 : : {
179 : 84 : inConflict = process(q, p, addedLemmas);
180 [ - + ]: 84 : if (inConflict)
181 : : {
182 : 0 : break;
183 : : }
184 : : }
185 [ - + ]: 84 : if (inConflict)
186 : : {
187 : 0 : break;
188 : : }
189 [ + + ][ - ]: 104 : }
190 : 39 : endCallDebug();
191 : : }
192 : :
193 : 0 : std::string InstStrategyPool::identify() const { return "pool-inst"; }
194 : :
195 : 84 : bool InstStrategyPool::process(Node q, Node p, uint64_t& addedLemmas)
196 : : {
197 [ + - ][ + - ]: 84 : Assert(q.getKind() == Kind::FORALL && p.getKind() == Kind::INST_POOL);
[ - + ][ - + ]
[ - - ]
198 : : // maybe has tuple semantics?
199 [ + + ]: 84 : if (hasTupleSemantics(q, p))
200 : : {
201 : 5 : return processTuple(q, p, addedLemmas);
202 : : }
203 [ - + ][ - + ]: 79 : Assert(hasProductSemantics(q, p));
[ - - ]
204 : : // otherwise, process standard
205 : 79 : Instantiate* ie = d_qim.getInstantiate();
206 : : TermTupleEnumeratorEnv ttec;
207 : 79 : ttec.d_fullEffort = true;
208 : 79 : ttec.d_increaseSum = options().quantifiers.enumInstSum;
209 : 79 : ttec.d_tr = &d_treg;
210 : : std::shared_ptr<TermTupleEnumeratorInterface> enumerator(
211 : 158 : mkTermTupleEnumeratorPool(q, &ttec, p));
212 : 79 : std::vector<Node> terms;
213 : 79 : std::vector<bool> failMask;
214 : : // we instantiate exhaustively
215 : 79 : enumerator->init();
216 [ + + ]: 755 : while (enumerator->hasNext())
217 : : {
218 [ - + ]: 676 : if (d_qstate.isInConflict())
219 : : {
220 : : // could be conflicting for an internal reason
221 : 0 : return true;
222 : : }
223 : 676 : enumerator->next(terms);
224 : : // try instantiation
225 : 676 : failMask.clear();
226 [ + + ]: 676 : if (ie->addInstantiationExpFail(
227 : : q, terms, failMask, InferenceId::QUANTIFIERS_INST_POOL))
228 : : {
229 [ + - ]: 491 : Trace("pool-inst") << "Success with " << terms << std::endl;
230 : 491 : addedLemmas++;
231 : : }
232 : : else
233 : : {
234 [ + - ]: 185 : Trace("pool-inst") << "Fail with " << terms << std::endl;
235 : : // notify the enumerator of the failure
236 : 185 : enumerator->failureReason(failMask);
237 : : }
238 : : }
239 : 79 : return false;
240 : 79 : }
241 : :
242 : 5 : bool InstStrategyPool::processTuple(Node q, Node p, uint64_t& addedLemmas)
243 : : {
244 : 5 : Instantiate* ie = d_qim.getInstantiate();
245 : 5 : TermPools* tp = d_treg.getTermPools();
246 : : // get the terms
247 : 5 : std::vector<Node> terms;
248 : 5 : tp->getTermsForPool(p[0], terms);
249 : : // instantiation for each term in pool
250 [ + + ]: 20 : for (const Node& t : terms)
251 : : {
252 [ - + ]: 15 : if (d_qstate.isInConflict())
253 : : {
254 : 0 : return true;
255 : : }
256 [ - + ]: 15 : if (t.getKind() != Kind::APPLY_CONSTRUCTOR)
257 : : {
258 : : // a symbolic tuple is in the pool, we ignore it.
259 : 0 : continue;
260 : : }
261 : 15 : std::vector<Node> inst(t.begin(), t.end());
262 [ - + ][ - + ]: 15 : Assert(inst.size() == q[0].getNumChildren());
[ - - ]
263 [ + - ]: 15 : if (ie->addInstantiation(q, inst, InferenceId::QUANTIFIERS_INST_POOL_TUPLE))
264 : : {
265 [ + - ]: 15 : Trace("pool-inst") << "Success (tuple) with " << inst << std::endl;
266 : 15 : addedLemmas++;
267 : : }
268 : : else
269 : : {
270 [ - - ]: 0 : Trace("pool-inst") << "Fail (tuple) with " << inst << std::endl;
271 : : }
272 : 15 : }
273 : 5 : return false;
274 : 5 : }
275 : :
276 : : } // namespace quantifiers
277 : : } // namespace theory
278 : : } // namespace cvc5::internal
|
