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