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 |
9942 |
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 |
9942 |
d_reset_count(0) |
38 |
|
{ |
39 |
9942 |
} |
40 |
|
|
41 |
9939 |
EqualityQuery::~EqualityQuery() {} |
42 |
|
|
43 |
28078 |
bool EqualityQuery::reset(Theory::Effort e) |
44 |
|
{ |
45 |
28078 |
d_int_rep.clear(); |
46 |
28078 |
d_reset_count++; |
47 |
28078 |
return true; |
48 |
|
} |
49 |
|
|
50 |
76405 |
Node EqualityQuery::getInternalRepresentative(Node a, Node q, size_t index) |
51 |
|
{ |
52 |
76405 |
Assert(q.isNull() || q.getKind() == FORALL); |
53 |
152810 |
Node r = d_qstate.getRepresentative(a); |
54 |
76405 |
if( options::finiteModelFind() ){ |
55 |
65957 |
if( r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant( r ) ){ |
56 |
|
//map back from values assigned by model, if any |
57 |
5362 |
if (d_model != nullptr) |
58 |
|
{ |
59 |
10724 |
Node tr = d_model->getRepSet()->getTermForRepresentative(r); |
60 |
5362 |
if (!tr.isNull()) |
61 |
|
{ |
62 |
5362 |
r = tr; |
63 |
5362 |
r = d_qstate.getRepresentative(r); |
64 |
|
}else{ |
65 |
|
if( r.getType().isSort() ){ |
66 |
|
Trace("internal-rep-warn") << "No representative for UF constant." << std::endl; |
67 |
|
//should never happen : UF constants should never escape model |
68 |
|
Assert(false); |
69 |
|
} |
70 |
|
} |
71 |
|
} |
72 |
|
} |
73 |
|
} |
74 |
152810 |
TypeNode v_tn = q.isNull() ? a.getType() : q[0][index].getType(); |
75 |
76405 |
if (options::quantRepMode() == options::QuantRepMode::EE) |
76 |
|
{ |
77 |
|
int32_t score = getRepScore(r, q, index, v_tn); |
78 |
|
if (score >= 0) |
79 |
|
{ |
80 |
|
return r; |
81 |
|
} |
82 |
|
// if we are not a valid representative, try to select one below |
83 |
|
} |
84 |
76405 |
std::map<Node, Node>& v_int_rep = d_int_rep[v_tn]; |
85 |
76405 |
std::map<Node, Node>::const_iterator itir = v_int_rep.find(r); |
86 |
76405 |
if (itir != v_int_rep.end()) |
87 |
|
{ |
88 |
68126 |
return itir->second; |
89 |
|
} |
90 |
|
// find best selection for representative |
91 |
16558 |
Node r_best; |
92 |
16558 |
std::vector<Node> eqc; |
93 |
8279 |
d_qstate.getEquivalenceClass(r, eqc); |
94 |
16558 |
Trace("internal-rep-select") |
95 |
8279 |
<< "Choose representative for equivalence class : " << eqc |
96 |
8279 |
<< ", type = " << v_tn << std::endl; |
97 |
8279 |
int32_t r_best_score = -1; |
98 |
64707 |
for (const Node& n : eqc) |
99 |
|
{ |
100 |
56428 |
int32_t score = getRepScore(n, q, index, v_tn); |
101 |
56428 |
if (score != -2) |
102 |
|
{ |
103 |
104364 |
if (r_best.isNull() |
104 |
52182 |
|| (score >= 0 && (r_best_score < 0 || score < r_best_score))) |
105 |
|
{ |
106 |
8503 |
r_best = n; |
107 |
8503 |
r_best_score = score; |
108 |
|
} |
109 |
|
} |
110 |
|
} |
111 |
8279 |
if (r_best.isNull()) |
112 |
|
{ |
113 |
|
Trace("internal-rep-warn") |
114 |
|
<< "No valid choice for representative in eqc class " << eqc |
115 |
|
<< std::endl; |
116 |
|
return Node::null(); |
117 |
|
} |
118 |
|
// now, make sure that no other member of the class is an instance |
119 |
16558 |
std::unordered_map<TNode, Node> cache; |
120 |
8279 |
r_best = getInstance(r_best, eqc, cache); |
121 |
|
// store that this representative was chosen at this point |
122 |
8279 |
if (d_rep_score.find(r_best) == d_rep_score.end()) |
123 |
|
{ |
124 |
1742 |
d_rep_score[r_best] = d_reset_count; |
125 |
|
} |
126 |
16558 |
Trace("internal-rep-select") |
127 |
8279 |
<< "...Choose " << r_best << " with score " << r_best_score |
128 |
8279 |
<< " and type " << r_best.getType() << std::endl; |
129 |
8279 |
Assert(r_best.getType().isSubtypeOf(v_tn)); |
130 |
8279 |
v_int_rep[r] = r_best; |
131 |
8279 |
if (Trace.isOn("internal-rep-debug")) |
132 |
|
{ |
133 |
|
if (r_best != a) |
134 |
|
{ |
135 |
|
Trace("internal-rep-debug") |
136 |
|
<< "rep( " << a << " ) = " << r << ", " << std::endl; |
137 |
|
Trace("internal-rep-debug") |
138 |
|
<< "int_rep( " << a << " ) = " << r_best << ", " << std::endl; |
139 |
|
} |
140 |
|
} |
141 |
8279 |
return r_best; |
142 |
|
} |
143 |
|
|
144 |
|
//helper functions |
145 |
|
|
146 |
12608 |
Node EqualityQuery::getInstance(Node n, |
147 |
|
const std::vector<Node>& eqc, |
148 |
|
std::unordered_map<TNode, Node>& cache) |
149 |
|
{ |
150 |
12608 |
if(cache.find(n) != cache.end()) { |
151 |
495 |
return cache[n]; |
152 |
|
} |
153 |
16430 |
for( size_t i=0; i<n.getNumChildren(); i++ ){ |
154 |
8646 |
Node nn = getInstance( n[i], eqc, cache ); |
155 |
4329 |
if( !nn.isNull() ){ |
156 |
12 |
return cache[n] = nn; |
157 |
|
} |
158 |
|
} |
159 |
12101 |
if( std::find( eqc.begin(), eqc.end(), n )!=eqc.end() ){ |
160 |
8279 |
return cache[n] = n; |
161 |
|
}else{ |
162 |
3822 |
return cache[n] = Node::null(); |
163 |
|
} |
164 |
|
} |
165 |
|
|
166 |
|
//-2 : invalid, -1 : undesired, otherwise : smaller the score, the better |
167 |
56428 |
int32_t EqualityQuery::getRepScore(Node n, Node q, size_t index, TypeNode v_tn) |
168 |
|
{ |
169 |
56428 |
if( options::cegqi() && quantifiers::TermUtil::hasInstConstAttr(n) ){ //reject |
170 |
|
return -2; |
171 |
56428 |
}else if( !n.getType().isSubtypeOf( v_tn ) ){ //reject if incorrect type |
172 |
4246 |
return -2; |
173 |
52182 |
}else if( options::instMaxLevel()!=-1 ){ |
174 |
|
//score prefer lowest instantiation level |
175 |
|
if( n.hasAttribute(InstLevelAttribute()) ){ |
176 |
|
return n.getAttribute(InstLevelAttribute()); |
177 |
|
} |
178 |
|
return options::instLevelInputOnly() ? -1 : 0; |
179 |
|
} |
180 |
52182 |
else if (options::quantRepMode() == options::QuantRepMode::FIRST) |
181 |
|
{ |
182 |
|
// score prefers earliest use of this term as a representative |
183 |
52182 |
return d_rep_score.find(n) == d_rep_score.end() ? -1 : d_rep_score[n]; |
184 |
|
} |
185 |
|
Assert(options::quantRepMode() == options::QuantRepMode::DEPTH); |
186 |
|
return quantifiers::TermUtil::getTermDepth(n); |
187 |
|
} |
188 |
|
|
189 |
|
} // namespace quantifiers |
190 |
|
} // namespace theory |
191 |
29577 |
} // namespace cvc5 |