Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Andres Noetzli, 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 : : * Term registry class.
14 : : */
15 : :
16 : : #include "theory/quantifiers/term_registry.h"
17 : :
18 : : #include "options/base_options.h"
19 : : #include "options/quantifiers_options.h"
20 : : #include "options/smt_options.h"
21 : : #include "theory/quantifiers/entailment_check.h"
22 : : #include "theory/quantifiers/first_order_model.h"
23 : : #include "theory/quantifiers/fmf/first_order_model_fmc.h"
24 : : #include "theory/quantifiers/ho_term_database.h"
25 : : #include "theory/quantifiers/oracle_checker.h"
26 : : #include "theory/quantifiers/quantifiers_attributes.h"
27 : : #include "theory/quantifiers/quantifiers_state.h"
28 : : #include "theory/quantifiers/term_util.h"
29 : :
30 : : namespace cvc5::internal {
31 : : namespace theory {
32 : : namespace quantifiers {
33 : :
34 : 49953 : TermRegistry::TermRegistry(Env& env,
35 : : QuantifiersState& qs,
36 : 49953 : QuantifiersRegistry& qr)
37 : : : EnvObj(env),
38 : 49953 : d_termEnum(new TermEnumeration),
39 : 49953 : d_termPools(new TermPools(env, qs)),
40 [ + + ]: 98705 : d_termDb(logicInfo().isHigherOrder() ? new HoTermDb(env, qs, qr)
41 : 48752 : : new TermDb(env, qs, qr)),
42 : 49953 : d_echeck(new EntailmentCheck(env, qs, *d_termDb.get())),
43 : 49953 : d_sygusTdb(nullptr),
44 : 49953 : d_vtsCache(new VtsTermCache(env)),
45 : 49953 : d_ievalMan(new ieval::InstEvaluatorManager(env, qs, *d_termDb.get())),
46 : 149859 : d_qmodel(nullptr)
47 : : {
48 [ + + ]: 49953 : if (options().quantifiers.oracles)
49 : : {
50 : 535 : d_ochecker.reset(new OracleChecker(env));
51 : : }
52 [ + + ]: 49953 : if (options().quantifiers.cegqiBv)
53 : : {
54 : : // if doing instantiation for BV, need the inverter class
55 : 36994 : d_bvInvert.reset(new BvInverter(env.getRewriter()));
56 : : }
57 [ + + ][ + + ]: 49953 : if (options().quantifiers.sygus || options().quantifiers.sygusInst)
[ + + ]
58 : : {
59 : : // must be constructed here since it is required for datatypes finistInit
60 : 6385 : d_sygusTdb.reset(new TermDbSygus(env, qs));
61 : : }
62 [ + - ]: 49953 : Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
63 : 49953 : }
64 : :
65 : 49953 : void TermRegistry::finishInit(FirstOrderModel* fm,
66 : : QuantifiersInferenceManager* qim)
67 : : {
68 : 49953 : d_qmodel = fm;
69 : 49953 : d_termDb->finishInit(qim);
70 [ + + ]: 49953 : if (d_sygusTdb.get())
71 : : {
72 : 6385 : d_sygusTdb->finishInit(qim);
73 : : }
74 : 49953 : }
75 : :
76 : 97905 : void TermRegistry::addQuantifierBody(TNode n) { addTermInternal(n, true); }
77 : :
78 : 1868697 : void TermRegistry::eqNotifyNewClass(TNode t) { addTermInternal(t, false); }
79 : :
80 : 10344229 : void TermRegistry::eqNotifyMerge(TNode t1, TNode t2)
81 : : {
82 : : // notify the term database
83 : 10344229 : d_termDb->eqNotifyMerge(t1, t2);
84 : 10344229 : }
85 : :
86 : 1966602 : void TermRegistry::addTermInternal(TNode n, bool withinQuant)
87 : : {
88 : : // don't add terms in quantifier bodies
89 [ + + ][ + - ]: 1966602 : if (withinQuant && !options().quantifiers.registerQuantBodyTerms)
[ + + ]
90 : : {
91 : 97905 : return;
92 : : }
93 : 1868697 : d_termDb->addTerm(n);
94 : 1868697 : if (d_sygusTdb.get()
95 [ + + ][ + - ]: 1868697 : && options().quantifiers.sygusEvalUnfoldMode
[ + + ]
96 : : != options::SygusEvalUnfoldMode::NONE)
97 : : {
98 : 448342 : d_sygusTdb->getEvalUnfold()->registerEvalTerm(n);
99 : : }
100 : : }
101 : :
102 : 5856 : Node TermRegistry::getTermForType(TypeNode tn)
103 : : {
104 [ + + ]: 5856 : if (tn.isClosedEnumerable())
105 : : {
106 : 398 : return d_termEnum->getEnumerateTerm(tn, 0);
107 : : }
108 : 5458 : return d_termDb->getOrMakeTypeGroundTerm(tn);
109 : : }
110 : :
111 : 119 : void TermRegistry::getTermsForPool(Node p, std::vector<Node>& terms)
112 : : {
113 [ - + ]: 119 : if (p.getKind() == Kind::SET_UNIVERSE)
114 : : {
115 : : // get all ground terms of the given type
116 : 0 : TypeNode ptn = p.getType().getSetElementType();
117 : 0 : size_t nterms = d_termDb->getNumTypeGroundTerms(ptn);
118 [ - - ]: 0 : for (size_t i = 0; i < nterms; i++)
119 : : {
120 : 0 : terms.push_back(d_termDb->getTypeGroundTerm(ptn, i));
121 : : }
122 : 0 : }
123 : : else
124 : : {
125 : 119 : d_termPools->getTermsForPool(p, terms);
126 : : }
127 : 119 : }
128 : :
129 : 263 : void TermRegistry::declarePool(Node p, const std::vector<Node>& initValue)
130 : : {
131 : 263 : d_termPools->registerPool(p, initValue);
132 : 263 : }
133 : :
134 : 181806 : void TermRegistry::processInstantiation(Node q, const std::vector<Node>& terms)
135 : : {
136 : 181806 : d_termPools->processInstantiation(q, terms);
137 : 181806 : }
138 : 5908 : void TermRegistry::processSkolemization(Node q,
139 : : const std::vector<Node>& skolems)
140 : : {
141 : 5908 : d_termPools->processSkolemization(q, skolems);
142 : 5908 : }
143 : :
144 : 31890526 : TermDb* TermRegistry::getTermDatabase() const { return d_termDb.get(); }
145 : :
146 : 21422 : TermDbSygus* TermRegistry::getTermDatabaseSygus() const
147 : : {
148 : 21422 : return d_sygusTdb.get();
149 : : }
150 : :
151 : 0 : OracleChecker* TermRegistry::getOracleChecker() const
152 : : {
153 : 0 : return d_ochecker.get();
154 : : }
155 : :
156 : 125196391 : EntailmentCheck* TermRegistry::getEntailmentCheck() const
157 : : {
158 : 125196391 : return d_echeck.get();
159 : : }
160 : :
161 : 3158 : TermEnumeration* TermRegistry::getTermEnumeration() const
162 : : {
163 : 3158 : return d_termEnum.get();
164 : : }
165 : :
166 : 49958 : TermPools* TermRegistry::getTermPools() const { return d_termPools.get(); }
167 : :
168 : 19271 : VtsTermCache* TermRegistry::getVtsTermCache() const { return d_vtsCache.get(); }
169 : :
170 : 1096 : BvInverter* TermRegistry::getBvInverter() const { return d_bvInvert.get(); }
171 : :
172 : 49953 : ieval::InstEvaluatorManager* TermRegistry::getInstEvaluatorManager() const
173 : : {
174 : 49953 : return d_ievalMan.get();
175 : : }
176 : :
177 : 298887 : ieval::InstEvaluator* TermRegistry::getEvaluator(Node q,
178 : : ieval::TermEvaluatorMode tev)
179 : : {
180 : 298887 : return d_ievalMan->getEvaluator(q, tev);
181 : : }
182 : :
183 : 694283 : FirstOrderModel* TermRegistry::getModel() const { return d_qmodel; }
184 : :
185 : : } // namespace quantifiers
186 : : } // namespace theory
187 : : } // namespace cvc5::internal
|
