Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Mathias Preiner
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 : : * Instantiator for counterexample-guided quantifier instantiation.
14 : : */
15 : :
16 : : #include "cvc5_private.h"
17 : :
18 : : #ifndef CVC5__THEORY__QUANTIFIERS__INSTANTIATOR_H
19 : : #define CVC5__THEORY__QUANTIFIERS__INSTANTIATOR_H
20 : :
21 : : #include <vector>
22 : :
23 : : #include "expr/node.h"
24 : : #include "smt/env_obj.h"
25 : : #include "theory/quantifiers/cegqi/ceg_instantiator.h"
26 : :
27 : : namespace cvc5::internal {
28 : : namespace theory {
29 : : namespace quantifiers {
30 : :
31 : : class CegInstanatior;
32 : :
33 : : /** Instantiator class
34 : : *
35 : : * This is a virtual class that is used for methods for constructing
36 : : * substitutions for individual variables in counterexample-guided
37 : : * instantiation techniques.
38 : : *
39 : : * This class contains a set of interface functions below, which are called
40 : : * based on a fixed instantiation method implemented by CegInstantiator.
41 : : * In these calls, the Instantiator in turn makes calls to methods in
42 : : * CegInstanatior (primarily constructInstantiationInc).
43 : : */
44 : : class Instantiator : protected EnvObj
45 : : {
46 : : public:
47 : : Instantiator(Env& env, TypeNode tn);
48 : 5092 : virtual ~Instantiator() {}
49 : : /** reset
50 : : * This is called once, prior to any of the below methods are called.
51 : : * This function sets up any initial information necessary for constructing
52 : : * instantiations for pv based on the current context.
53 : : */
54 : 15565 : virtual void reset(CVC5_UNUSED CegInstantiator* ci,
55 : : CVC5_UNUSED SolvedForm& sf,
56 : : CVC5_UNUSED Node pv,
57 : : CVC5_UNUSED CegInstEffort effort)
58 : : {
59 : 15565 : }
60 : :
61 : : /** has process equal term
62 : : *
63 : : * Whether this instantiator implements processEqualTerm and
64 : : * processEqualTerms.
65 : : */
66 : 86096 : virtual bool hasProcessEqualTerm(CVC5_UNUSED CegInstantiator* ci,
67 : : CVC5_UNUSED SolvedForm& sf,
68 : : CVC5_UNUSED Node pv,
69 : : CVC5_UNUSED CegInstEffort effort)
70 : : {
71 : 86096 : return false;
72 : : }
73 : : /** process equal term
74 : : *
75 : : * This method is called when the entailment:
76 : : * E |= pv_prop.getModifiedTerm(pv) = n
77 : : * holds in the current context E, and n is eligible for instantiation.
78 : : *
79 : : * Returns true if an instantiation was successfully added via a call to
80 : : * CegInstantiator::constructInstantiationInc.
81 : : */
82 : : virtual bool processEqualTerm(CegInstantiator* ci,
83 : : SolvedForm& sf,
84 : : Node pv,
85 : : TermProperties& pv_prop,
86 : : Node n,
87 : : CegInstEffort effort);
88 : : /** process equal terms
89 : : *
90 : : * This method is called after process equal term, where eqc is the list of
91 : : * eligible terms in the equivalence class of pv.
92 : : *
93 : : * Returns true if an instantiation was successfully added via a call to
94 : : * CegInstantiator::constructInstantiationInc.
95 : : */
96 : 0 : virtual bool processEqualTerms(CVC5_UNUSED CegInstantiator* ci,
97 : : CVC5_UNUSED SolvedForm& sf,
98 : : CVC5_UNUSED Node pv,
99 : : CVC5_UNUSED std::vector<Node>& eqc,
100 : : CVC5_UNUSED CegInstEffort effort)
101 : : {
102 : 0 : return false;
103 : : }
104 : :
105 : : /** whether the instantiator implements processEquality */
106 : 20168 : virtual bool hasProcessEquality(CVC5_UNUSED CegInstantiator* ci,
107 : : CVC5_UNUSED SolvedForm& sf,
108 : : CVC5_UNUSED Node pv,
109 : : CVC5_UNUSED CegInstEffort effort)
110 : : {
111 : 20168 : return false;
112 : : }
113 : : /** process equality
114 : : * The input is such that term_props.size() = terms.size() = 2
115 : : * This method is called when the entailment:
116 : : * E ^ term_props[0].getModifiedTerm(x0) =
117 : : * terms[0] ^ term_props[1].getModifiedTerm(x1) = terms[1] |= x0 = x1
118 : : * holds in current context E for fresh variables xi, terms[i] are eligible,
119 : : * and at least one terms[i] contains pv for i = 0,1.
120 : : * Notice in the basic case, E |= terms[0] = terms[1].
121 : : *
122 : : * Returns true if an instantiation was successfully added via a call to
123 : : * CegInstantiator::constructInstantiationInc.
124 : : */
125 : 0 : virtual bool processEquality(
126 : : CVC5_UNUSED CegInstantiator* ci,
127 : : CVC5_UNUSED SolvedForm& sf,
128 : : CVC5_UNUSED Node pv,
129 : : CVC5_UNUSED std::vector<TermProperties>& term_props,
130 : : CVC5_UNUSED std::vector<Node>& terms,
131 : : CVC5_UNUSED CegInstEffort effort)
132 : : {
133 : 0 : return false;
134 : : }
135 : :
136 : : /** whether the instantiator implements processAssertion for any literal */
137 : 15388 : virtual bool hasProcessAssertion(CVC5_UNUSED CegInstantiator* ci,
138 : : CVC5_UNUSED SolvedForm& sf,
139 : : CVC5_UNUSED Node pv,
140 : : CVC5_UNUSED CegInstEffort effort)
141 : : {
142 : 15388 : return false;
143 : : }
144 : : /** has process assertion
145 : : *
146 : : * This method is called when the entailment:
147 : : * E |= lit
148 : : * holds in current context E. Typically, lit belongs to the list of current
149 : : * assertions.
150 : : *
151 : : * This method is used to determine whether the instantiator implements
152 : : * processAssertion for literal lit.
153 : : * If this method returns null, then this intantiator does not handle the
154 : : * literal lit. Otherwise, this method returns a literal lit' such that:
155 : : * (1) lit' is true in the current model,
156 : : * (2) lit' implies lit.
157 : : * where typically lit' = lit.
158 : : */
159 : 0 : virtual Node hasProcessAssertion(CVC5_UNUSED CegInstantiator* ci,
160 : : CVC5_UNUSED SolvedForm& sf,
161 : : CVC5_UNUSED Node pv,
162 : : CVC5_UNUSED Node lit,
163 : : CVC5_UNUSED CegInstEffort effort)
164 : : {
165 : 0 : return Node::null();
166 : : }
167 : : /** process assertion
168 : : * This method processes the assertion slit for variable pv.
169 : : * lit : the substituted form (under sf) of a literal returned by
170 : : * hasProcessAssertion
171 : : * alit : the asserted literal, given as input to hasProcessAssertion
172 : : *
173 : : * Returns true if an instantiation was successfully added via a call to
174 : : * CegInstantiator::constructInstantiationInc.
175 : : */
176 : 0 : virtual bool processAssertion(CVC5_UNUSED CegInstantiator* ci,
177 : : CVC5_UNUSED SolvedForm& sf,
178 : : CVC5_UNUSED Node pv,
179 : : CVC5_UNUSED Node lit,
180 : : CVC5_UNUSED Node alit,
181 : : CVC5_UNUSED CegInstEffort effort)
182 : : {
183 : 0 : return false;
184 : : }
185 : : /** process assertions
186 : : *
187 : : * Called after processAssertion is called for each literal asserted to the
188 : : * instantiator.
189 : : *
190 : : * Returns true if an instantiation was successfully added via a call to
191 : : * CegInstantiator::constructInstantiationInc.
192 : : */
193 : 0 : virtual bool processAssertions(CVC5_UNUSED CegInstantiator* ci,
194 : : CVC5_UNUSED SolvedForm& sf,
195 : : CVC5_UNUSED Node pv,
196 : : CVC5_UNUSED CegInstEffort effort)
197 : : {
198 : 0 : return false;
199 : : }
200 : :
201 : : /** do we use the model value as instantiation for pv?
202 : : * This method returns true if we use model value instantiations
203 : : * at the same effort level as those determined by this instantiator.
204 : : */
205 : 2674 : virtual bool useModelValue(CVC5_UNUSED CegInstantiator* ci,
206 : : CVC5_UNUSED SolvedForm& sf,
207 : : CVC5_UNUSED Node pv,
208 : : CegInstEffort effort)
209 : : {
210 : 2674 : return effort > CEG_INST_EFFORT_STANDARD;
211 : : }
212 : : /** do we allow the model value as instantiation for pv? */
213 : 20933 : virtual bool allowModelValue(CVC5_UNUSED CegInstantiator* ci,
214 : : CVC5_UNUSED SolvedForm& sf,
215 : : CVC5_UNUSED Node pv,
216 : : CVC5_UNUSED CegInstEffort effort)
217 : : {
218 : 20933 : return d_closed_enum_type;
219 : : }
220 : :
221 : : /** do we need to postprocess the solved form for pv? */
222 : 20668 : virtual bool needsPostProcessInstantiationForVariable(
223 : : CVC5_UNUSED CegInstantiator* ci,
224 : : CVC5_UNUSED SolvedForm& sf,
225 : : CVC5_UNUSED Node pv,
226 : : CVC5_UNUSED CegInstEffort effort)
227 : : {
228 : 20668 : return false;
229 : : }
230 : : /** postprocess the solved form for pv
231 : : *
232 : : * This method returns true if we successfully postprocessed the solved form.
233 : : * lemmas is a set of lemmas we wish to return along with the instantiation.
234 : : */
235 : 0 : virtual bool postProcessInstantiationForVariable(
236 : : CVC5_UNUSED CegInstantiator* ci,
237 : : CVC5_UNUSED SolvedForm& sf,
238 : : CVC5_UNUSED Node pv,
239 : : CVC5_UNUSED CegInstEffort effort)
240 : : {
241 : 0 : return true;
242 : : }
243 : :
244 : : /** Identify this module (for debugging) */
245 : 0 : virtual std::string identify() const { return "Default"; }
246 : : protected:
247 : : /** the type of the variable we are instantiating */
248 : : TypeNode d_type;
249 : : /** whether d_type is a closed enumerable type */
250 : : bool d_closed_enum_type;
251 : : };
252 : :
253 : : class ModelValueInstantiator : public Instantiator {
254 : : public:
255 : 315 : ModelValueInstantiator(Env& env, TypeNode tn) : Instantiator(env, tn) {}
256 : 630 : virtual ~ModelValueInstantiator() {}
257 : 15129 : bool useModelValue(CVC5_UNUSED CegInstantiator* ci,
258 : : CVC5_UNUSED SolvedForm& sf,
259 : : CVC5_UNUSED Node pv,
260 : : CVC5_UNUSED CegInstEffort effort) override
261 : : {
262 : 15129 : return true;
263 : : }
264 : 0 : std::string identify() const override { return "ModelValue"; }
265 : : };
266 : :
267 : : /** instantiator preprocess
268 : : *
269 : : * This class implements techniques for preprocessing the counterexample lemma
270 : : * generated for counterexample-guided quantifier instantiation.
271 : : */
272 : : class InstantiatorPreprocess
273 : : {
274 : : public:
275 : 1107 : InstantiatorPreprocess() {}
276 : 1107 : virtual ~InstantiatorPreprocess() {}
277 : : /** register counterexample lemma
278 : : * This implements theory-specific preprocessing and registration
279 : : * of counterexample lemmas, with the same contract as
280 : : * CegInstantiation::registerCounterexampleLemma.
281 : : */
282 : 0 : virtual void registerCounterexampleLemma(
283 : : CVC5_UNUSED Node lem,
284 : : CVC5_UNUSED std::vector<Node>& ceVars,
285 : : CVC5_UNUSED std::vector<Node>& auxLems)
286 : : {
287 : 0 : }
288 : : };
289 : :
290 : : } // namespace quantifiers
291 : : } // namespace theory
292 : : } // namespace cvc5::internal
293 : :
294 : : #endif
|
