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 : : * Utilities used for querying about equality information.
11 : : */
12 : :
13 : : #include "theory/quantifiers/equality_query.h"
14 : :
15 : : #include "options/quantifiers_options.h"
16 : : #include "theory/quantifiers/first_order_model.h"
17 : : #include "theory/quantifiers/quantifiers_attributes.h"
18 : : #include "theory/quantifiers/quantifiers_state.h"
19 : : #include "theory/quantifiers/term_util.h"
20 : :
21 : : using namespace std;
22 : : using namespace cvc5::internal::kind;
23 : : using namespace cvc5::context;
24 : :
25 : : namespace cvc5::internal {
26 : : namespace theory {
27 : : namespace quantifiers {
28 : :
29 : 51004 : EqualityQuery::EqualityQuery(Env& env, QuantifiersState& qs, FirstOrderModel* m)
30 : : : QuantifiersUtil(env),
31 : 51004 : d_qstate(qs),
32 : 51004 : d_model(m),
33 : 51004 : d_eqi_counter(context()),
34 : 102008 : d_reset_count(0)
35 : : {
36 : 51004 : }
37 : :
38 : 50659 : EqualityQuery::~EqualityQuery() {}
39 : :
40 : 68681 : bool EqualityQuery::reset(CVC5_UNUSED Theory::Effort e)
41 : : {
42 : 68681 : d_int_rep.clear();
43 : 68681 : d_reset_count++;
44 : 68681 : return true;
45 : : }
46 : :
47 : 88046 : Node EqualityQuery::getInternalRepresentative(Node a, Node q, size_t index)
48 : : {
49 [ + + ][ + - ]: 88046 : Assert(q.isNull() || q.getKind() == Kind::FORALL);
[ - + ][ - + ]
[ - - ]
50 : 176092 : Node r = d_qstate.getRepresentative(a);
51 [ + + ]: 88046 : if (options().quantifiers.finiteModelFind)
52 : : {
53 [ + + ][ + + ]: 74136 : if (r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant(r))
[ + + ][ + + ]
[ - - ]
54 : : {
55 : : // map back from values assigned by model, if any
56 [ + - ]: 5779 : if (d_model != nullptr)
57 : : {
58 : 5779 : Node tr = d_model->getRepSet()->getTermForRepresentative(r);
59 [ + - ]: 5779 : if (!tr.isNull())
60 : : {
61 : 5779 : r = tr;
62 : 5779 : r = d_qstate.getRepresentative(r);
63 : : }
64 : : else
65 : : {
66 [ - - ]: 0 : if (r.getType().isUninterpretedSort())
67 : : {
68 [ - - ]: 0 : Trace("internal-rep-warn")
69 : 0 : << "No representative for UF constant." << std::endl;
70 : : // should never happen : UF constants should never escape model
71 : 0 : DebugUnhandled();
72 : : }
73 : : }
74 : 5779 : }
75 : : }
76 : : }
77 : 166631 : TypeNode v_tn = q.isNull() ? a.getType() : q[0][index].getType();
78 [ + + ]: 88046 : if (options().quantifiers.quantRepMode == options::QuantRepMode::EE)
79 : : {
80 : 6 : int32_t score = getRepScore(r, v_tn);
81 [ + - ]: 6 : if (score >= 0)
82 : : {
83 : 6 : return r;
84 : : }
85 : : // if we are not a valid representative, try to select one below
86 : : }
87 : 88040 : std::map<Node, Node>& v_int_rep = d_int_rep[v_tn];
88 : 88040 : std::map<Node, Node>::const_iterator itir = v_int_rep.find(r);
89 [ + + ]: 88040 : if (itir != v_int_rep.end())
90 : : {
91 : 73597 : return itir->second;
92 : : }
93 : : // find best selection for representative
94 : 14443 : Node r_best;
95 : 14443 : std::vector<Node> eqc;
96 : 14443 : d_qstate.getEquivalenceClass(r, eqc);
97 [ + - ]: 28886 : Trace("internal-rep-select")
98 : 0 : << "Choose representative for equivalence class : " << eqc
99 : 14443 : << ", type = " << v_tn << std::endl;
100 : 14443 : int32_t r_best_score = -1;
101 [ + + ]: 73215 : for (const Node& n : eqc)
102 : : {
103 : 58772 : int32_t score = getRepScore(n, v_tn);
104 [ + - ]: 58772 : if (score != -2)
105 : : {
106 : 58772 : if (r_best.isNull()
107 [ + + ][ + + ]: 58772 : || (score >= 0 && (r_best_score < 0 || score < r_best_score)))
[ + + ][ + + ]
[ + + ]
108 : : {
109 : 14770 : r_best = n;
110 : 14770 : r_best_score = score;
111 : : }
112 : : }
113 : : }
114 [ - + ]: 14443 : if (r_best.isNull())
115 : : {
116 [ - - ]: 0 : Trace("internal-rep-warn")
117 : 0 : << "No valid choice for representative in eqc class " << eqc
118 : 0 : << std::endl;
119 : 0 : return Node::null();
120 : : }
121 : : // now, make sure that no other member of the class is an instance
122 : 14443 : std::unordered_map<TNode, Node> cache;
123 : 14443 : r_best = getInstance(r_best, eqc, cache);
124 : : // store that this representative was chosen at this point
125 [ + + ]: 14443 : if (d_rep_score.find(r_best) == d_rep_score.end())
126 : : {
127 : 4111 : d_rep_score[r_best] = d_reset_count;
128 : : }
129 [ + - ]: 28886 : Trace("internal-rep-select")
130 : 0 : << "...Choose " << r_best << " with score " << r_best_score
131 [ - + ][ - - ]: 14443 : << " and type " << r_best.getType() << std::endl;
132 [ - + ][ - + ]: 14443 : Assert(r_best.getType() == v_tn);
[ - - ]
133 : 14443 : v_int_rep[r] = r_best;
134 [ - + ]: 14443 : if (TraceIsOn("internal-rep-debug"))
135 : : {
136 [ - - ]: 0 : if (r_best != a)
137 : : {
138 [ - - ]: 0 : Trace("internal-rep-debug")
139 : 0 : << "rep( " << a << " ) = " << r << ", " << std::endl;
140 [ - - ]: 0 : Trace("internal-rep-debug")
141 : 0 : << "int_rep( " << a << " ) = " << r_best << ", " << std::endl;
142 : : }
143 : : }
144 : 14443 : return r_best;
145 : 88046 : }
146 : :
147 : : // helper functions
148 : :
149 : 19073 : Node EqualityQuery::getInstance(Node n,
150 : : const std::vector<Node>& eqc,
151 : : std::unordered_map<TNode, Node>& cache)
152 : : {
153 [ + + ]: 19073 : if (cache.find(n) != cache.end())
154 : : {
155 : 436 : return cache[n];
156 : : }
157 [ + + ]: 23251 : for (size_t i = 0; i < n.getNumChildren(); i++)
158 : : {
159 : 4630 : Node nn = getInstance(n[i], eqc, cache);
160 [ + + ]: 4630 : if (!nn.isNull())
161 : : {
162 : 32 : return cache[n] = nn;
163 : : }
164 [ + + ]: 4630 : }
165 [ + + ]: 18621 : if (std::find(eqc.begin(), eqc.end(), n) != eqc.end())
166 : : {
167 : 28886 : return cache[n] = n;
168 : : }
169 : : else
170 : : {
171 : 8356 : return cache[n] = Node::null();
172 : : }
173 : : }
174 : :
175 : : //-2 : invalid, -1 : undesired, otherwise : smaller the score, the better
176 : 58778 : int32_t EqualityQuery::getRepScore(Node n, TypeNode v_tn)
177 : : {
178 [ - + ]: 58778 : if (quantifiers::TermUtil::hasInstConstAttr(n))
179 : : { // reject
180 : 0 : return -2;
181 : : }
182 [ - + ]: 58778 : else if (n.getType() != v_tn)
183 : : { // reject if incorrect type
184 : 0 : return -2;
185 : : }
186 [ - + ]: 58778 : else if (options().quantifiers.instMaxLevel != -1)
187 : : {
188 : : // score prefer lowest instantiation level
189 : : uint64_t level;
190 [ - - ]: 0 : if (QuantAttributes::getInstantiationLevel(n, level))
191 : : {
192 : 0 : return static_cast<int32_t>(level);
193 : : }
194 : 0 : return -1;
195 : : }
196 [ + + ]: 58778 : else if (options().quantifiers.quantRepMode == options::QuantRepMode::FIRST)
197 : : {
198 : : // score prefers earliest use of this term as a representative
199 [ + + ]: 58772 : return d_rep_score.find(n) == d_rep_score.end() ? -1 : d_rep_score[n];
200 : : }
201 [ - + ]: 6 : else if (options().quantifiers.quantRepMode == options::QuantRepMode::DEPTH)
202 : : {
203 : 0 : return quantifiers::TermUtil::getTermDepth(n);
204 : : }
205 : : // no preference
206 : 6 : return 0;
207 : : }
208 : :
209 : : } // namespace quantifiers
210 : : } // namespace theory
211 : : } // namespace cvc5::internal
|
