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