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