1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Mathias Preiner, Aina Niemetz |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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::kind; |
26 |
|
using namespace cvc5::context; |
27 |
|
|
28 |
|
namespace cvc5 { |
29 |
|
namespace theory { |
30 |
|
namespace quantifiers { |
31 |
|
|
32 |
9460 |
EqualityQuery::EqualityQuery(QuantifiersState& qs, FirstOrderModel* m) |
33 |
|
: d_qstate(qs), |
34 |
|
d_model(m), |
35 |
|
d_eqi_counter(qs.getSatContext()), |
36 |
9460 |
d_reset_count(0) |
37 |
|
{ |
38 |
9460 |
} |
39 |
|
|
40 |
9460 |
EqualityQuery::~EqualityQuery() {} |
41 |
|
|
42 |
24825 |
bool EqualityQuery::reset(Theory::Effort e) |
43 |
|
{ |
44 |
24825 |
d_int_rep.clear(); |
45 |
24825 |
d_reset_count++; |
46 |
24825 |
return true; |
47 |
|
} |
48 |
|
|
49 |
75944 |
Node EqualityQuery::getInternalRepresentative(Node a, Node q, size_t index) |
50 |
|
{ |
51 |
75944 |
Assert(q.isNull() || q.getKind() == FORALL); |
52 |
151888 |
Node r = d_qstate.getRepresentative(a); |
53 |
75944 |
if( options::finiteModelFind() ){ |
54 |
67433 |
if( r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant( r ) ){ |
55 |
|
//map back from values assigned by model, if any |
56 |
6288 |
if (d_model != nullptr) |
57 |
|
{ |
58 |
12576 |
Node tr = d_model->getRepSet()->getTermForRepresentative(r); |
59 |
6288 |
if (!tr.isNull()) |
60 |
|
{ |
61 |
6288 |
r = tr; |
62 |
6288 |
r = d_qstate.getRepresentative(r); |
63 |
|
}else{ |
64 |
|
if( r.getType().isSort() ){ |
65 |
|
Trace("internal-rep-warn") << "No representative for UF constant." << std::endl; |
66 |
|
//should never happen : UF constants should never escape model |
67 |
|
Assert(false); |
68 |
|
} |
69 |
|
} |
70 |
|
} |
71 |
|
} |
72 |
|
} |
73 |
151888 |
TypeNode v_tn = q.isNull() ? a.getType() : q[0][index].getType(); |
74 |
197817 |
if (options::quantRepMode() == options::QuantRepMode::EE) |
75 |
|
{ |
76 |
|
int32_t score = getRepScore(r, q, index, v_tn); |
77 |
|
if (score >= 0) |
78 |
|
{ |
79 |
|
return r; |
80 |
|
} |
81 |
|
// if we are not a valid representative, try to select one below |
82 |
|
} |
83 |
75944 |
std::map<Node, Node>& v_int_rep = d_int_rep[v_tn]; |
84 |
75944 |
std::map<Node, Node>::const_iterator itir = v_int_rep.find(r); |
85 |
75944 |
if (itir != v_int_rep.end()) |
86 |
|
{ |
87 |
67256 |
return itir->second; |
88 |
|
} |
89 |
|
// find best selection for representative |
90 |
17376 |
Node r_best; |
91 |
17376 |
std::vector<Node> eqc; |
92 |
8688 |
d_qstate.getEquivalenceClass(r, eqc); |
93 |
17376 |
Trace("internal-rep-select") |
94 |
8688 |
<< "Choose representative for equivalence class : " << eqc |
95 |
8688 |
<< ", type = " << v_tn << std::endl; |
96 |
8688 |
int32_t r_best_score = -1; |
97 |
59019 |
for (const Node& n : eqc) |
98 |
|
{ |
99 |
50331 |
int32_t score = getRepScore(n, q, index, v_tn); |
100 |
50331 |
if (score != -2) |
101 |
|
{ |
102 |
91858 |
if (r_best.isNull() |
103 |
45929 |
|| (score >= 0 && (r_best_score < 0 || score < r_best_score))) |
104 |
|
{ |
105 |
8900 |
r_best = n; |
106 |
8900 |
r_best_score = score; |
107 |
|
} |
108 |
|
} |
109 |
|
} |
110 |
8688 |
if (r_best.isNull()) |
111 |
|
{ |
112 |
|
Trace("internal-rep-warn") |
113 |
|
<< "No valid choice for representative in eqc class " << eqc |
114 |
|
<< std::endl; |
115 |
|
return Node::null(); |
116 |
|
} |
117 |
|
// now, make sure that no other member of the class is an instance |
118 |
17376 |
std::unordered_map<TNode, Node> cache; |
119 |
8688 |
r_best = getInstance(r_best, eqc, cache); |
120 |
|
// store that this representative was chosen at this point |
121 |
8688 |
if (d_rep_score.find(r_best) == d_rep_score.end()) |
122 |
|
{ |
123 |
1598 |
d_rep_score[r_best] = d_reset_count; |
124 |
|
} |
125 |
17376 |
Trace("internal-rep-select") |
126 |
8688 |
<< "...Choose " << r_best << " with score " << r_best_score |
127 |
8688 |
<< " and type " << r_best.getType() << std::endl; |
128 |
8688 |
Assert(r_best.getType().isSubtypeOf(v_tn)); |
129 |
8688 |
v_int_rep[r] = r_best; |
130 |
8688 |
if (Trace.isOn("internal-rep-debug")) |
131 |
|
{ |
132 |
|
if (r_best != a) |
133 |
|
{ |
134 |
|
Trace("internal-rep-debug") |
135 |
|
<< "rep( " << a << " ) = " << r << ", " << std::endl; |
136 |
|
Trace("internal-rep-debug") |
137 |
|
<< "int_rep( " << a << " ) = " << r_best << ", " << std::endl; |
138 |
|
} |
139 |
|
} |
140 |
8688 |
return r_best; |
141 |
|
} |
142 |
|
|
143 |
|
//helper functions |
144 |
|
|
145 |
13207 |
Node EqualityQuery::getInstance(Node n, |
146 |
|
const std::vector<Node>& eqc, |
147 |
|
std::unordered_map<TNode, Node>& cache) |
148 |
|
{ |
149 |
13207 |
if(cache.find(n) != cache.end()) { |
150 |
509 |
return cache[n]; |
151 |
|
} |
152 |
17203 |
for( size_t i=0; i<n.getNumChildren(); i++ ){ |
153 |
9024 |
Node nn = getInstance( n[i], eqc, cache ); |
154 |
4519 |
if( !nn.isNull() ){ |
155 |
14 |
return cache[n] = nn; |
156 |
|
} |
157 |
|
} |
158 |
12684 |
if( std::find( eqc.begin(), eqc.end(), n )!=eqc.end() ){ |
159 |
8688 |
return cache[n] = n; |
160 |
|
}else{ |
161 |
3996 |
return cache[n] = Node::null(); |
162 |
|
} |
163 |
|
} |
164 |
|
|
165 |
|
//-2 : invalid, -1 : undesired, otherwise : smaller the score, the better |
166 |
50331 |
int32_t EqualityQuery::getRepScore(Node n, Node q, size_t index, TypeNode v_tn) |
167 |
|
{ |
168 |
50331 |
if( options::cegqi() && quantifiers::TermUtil::hasInstConstAttr(n) ){ //reject |
169 |
|
return -2; |
170 |
50331 |
}else if( !n.getType().isSubtypeOf( v_tn ) ){ //reject if incorrect type |
171 |
4402 |
return -2; |
172 |
45929 |
}else if( options::instMaxLevel()!=-1 ){ |
173 |
|
//score prefer lowest instantiation level |
174 |
|
if( n.hasAttribute(InstLevelAttribute()) ){ |
175 |
|
return n.getAttribute(InstLevelAttribute()); |
176 |
|
} |
177 |
7323 |
return options::instLevelInputOnly() ? -1 : 0; |
178 |
|
} |
179 |
45929 |
else if (options::quantRepMode() == options::QuantRepMode::FIRST) |
180 |
|
{ |
181 |
|
// score prefers earliest use of this term as a representative |
182 |
45929 |
return d_rep_score.find(n) == d_rep_score.end() ? -1 : d_rep_score[n]; |
183 |
|
} |
184 |
|
Assert(options::quantRepMode() == options::QuantRepMode::DEPTH); |
185 |
|
return quantifiers::TermUtil::getTermDepth(n); |
186 |
|
} |
187 |
|
|
188 |
|
} // namespace quantifiers |
189 |
|
} // namespace theory |
190 |
157390 |
} // namespace cvc5 |