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