1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Mathias Preiner, Haniel Barbosa |
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 |
|
* Management of current value for an enumerator |
14 |
|
*/ |
15 |
|
#include "theory/quantifiers/sygus/enum_value_manager.h" |
16 |
|
|
17 |
|
#include "options/base_options.h" |
18 |
|
#include "options/datatypes_options.h" |
19 |
|
#include "options/quantifiers_options.h" |
20 |
|
#include "theory/datatypes/sygus_datatype_utils.h" |
21 |
|
#include "theory/quantifiers/first_order_model.h" |
22 |
|
#include "theory/quantifiers/quantifiers_inference_manager.h" |
23 |
|
#include "theory/quantifiers/sygus/enum_stream_substitution.h" |
24 |
|
#include "theory/quantifiers/sygus/sygus_enumerator.h" |
25 |
|
#include "theory/quantifiers/sygus/sygus_enumerator_basic.h" |
26 |
|
#include "theory/quantifiers/sygus/term_database_sygus.h" |
27 |
|
#include "theory/quantifiers/term_registry.h" |
28 |
|
|
29 |
|
using namespace cvc5::kind; |
30 |
|
using namespace std; |
31 |
|
|
32 |
|
namespace cvc5 { |
33 |
|
namespace theory { |
34 |
|
namespace quantifiers { |
35 |
|
|
36 |
573 |
EnumValueManager::EnumValueManager(Env& env, |
37 |
|
QuantifiersState& qs, |
38 |
|
QuantifiersInferenceManager& qim, |
39 |
|
TermRegistry& tr, |
40 |
|
SygusStatistics& s, |
41 |
|
Node e, |
42 |
573 |
bool hasExamples) |
43 |
|
: EnvObj(env), |
44 |
|
d_enum(e), |
45 |
|
d_qstate(qs), |
46 |
|
d_qim(qim), |
47 |
|
d_treg(tr), |
48 |
|
d_stats(s), |
49 |
573 |
d_tds(tr.getTermDatabaseSygus()), |
50 |
1146 |
d_eec(hasExamples ? new ExampleEvalCache(d_tds, e) : nullptr) |
51 |
|
{ |
52 |
573 |
} |
53 |
|
|
54 |
1146 |
EnumValueManager::~EnumValueManager() {} |
55 |
|
|
56 |
66828 |
Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete) |
57 |
|
{ |
58 |
133656 |
Node e = d_enum; |
59 |
66828 |
bool isEnum = d_tds->isEnumerator(e); |
60 |
|
|
61 |
66828 |
if (isEnum && !e.getAttribute(SygusSymBreakOkAttribute())) |
62 |
|
{ |
63 |
|
// if the current model value of e was not registered by the datatypes |
64 |
|
// sygus solver, or was excluded by symmetry breaking, then it does not |
65 |
|
// have a proper model value that we should consider, thus we return null. |
66 |
9848 |
Trace("sygus-engine-debug") |
67 |
4924 |
<< "Enumerator " << e << " does not have proper model value." |
68 |
4924 |
<< std::endl; |
69 |
4924 |
return Node::null(); |
70 |
|
} |
71 |
|
|
72 |
61904 |
if (!isEnum || d_tds->isPassiveEnumerator(e)) |
73 |
|
{ |
74 |
11266 |
return getModelValue(e); |
75 |
|
} |
76 |
|
|
77 |
|
// management of actively generated enumerators goes here |
78 |
|
|
79 |
|
// initialize the enumerated value generator for e |
80 |
50638 |
if (d_evg == nullptr) |
81 |
|
{ |
82 |
206 |
if (d_tds->isVariableAgnosticEnumerator(e)) |
83 |
|
{ |
84 |
2 |
d_evg.reset(new EnumStreamConcrete(d_tds)); |
85 |
|
} |
86 |
|
else |
87 |
|
{ |
88 |
|
// Actively-generated enumerators are currently either variable agnostic |
89 |
|
// or basic. The auto mode always prefers the optimized enumerator over |
90 |
|
// the basic one. |
91 |
204 |
Assert(d_tds->isBasicEnumerator(e)); |
92 |
408 |
if (options().quantifiers.sygusActiveGenMode |
93 |
204 |
== options::SygusActiveGenMode::ENUM_BASIC) |
94 |
|
{ |
95 |
|
d_evg.reset(new EnumValGeneratorBasic(d_tds, e.getType())); |
96 |
|
} |
97 |
|
else |
98 |
|
{ |
99 |
204 |
Assert(options().quantifiers.sygusActiveGenMode |
100 |
|
== options::SygusActiveGenMode::ENUM |
101 |
|
|| options().quantifiers.sygusActiveGenMode |
102 |
|
== options::SygusActiveGenMode::AUTO); |
103 |
|
// create the enumerator callback |
104 |
204 |
if (options().datatypes.sygusSymBreakDynamic) |
105 |
|
{ |
106 |
204 |
std::ostream* out = nullptr; |
107 |
204 |
if (options().quantifiers.sygusRewVerify) |
108 |
|
{ |
109 |
6 |
d_samplerRrV.reset(new SygusSampler(d_env)); |
110 |
12 |
d_samplerRrV->initializeSygus( |
111 |
6 |
d_tds, e, options().quantifiers.sygusSamples, false); |
112 |
|
// use the default output for the output of sygusRewVerify |
113 |
6 |
out = options().base.out; |
114 |
|
} |
115 |
408 |
d_secd.reset(new SygusEnumeratorCallbackDefault( |
116 |
204 |
e, &d_stats, d_eec.get(), d_samplerRrV.get(), out)); |
117 |
|
} |
118 |
|
// if sygus repair const is enabled, we enumerate terms with free |
119 |
|
// variables as arguments to any-constant constructors |
120 |
408 |
d_evg.reset( |
121 |
|
new SygusEnumerator(d_tds, |
122 |
204 |
d_secd.get(), |
123 |
204 |
&d_stats, |
124 |
|
false, |
125 |
408 |
options().quantifiers.sygusRepairConst)); |
126 |
|
} |
127 |
|
} |
128 |
412 |
Trace("sygus-active-gen") |
129 |
206 |
<< "Active-gen: initialize for " << e << std::endl; |
130 |
206 |
d_evg->initialize(e); |
131 |
206 |
d_ev_curr_active_gen = Node::null(); |
132 |
206 |
Trace("sygus-active-gen-debug") << "...finish" << std::endl; |
133 |
|
} |
134 |
|
// if we have a waiting value, return it |
135 |
50638 |
if (!d_evActiveGenWaiting.isNull()) |
136 |
|
{ |
137 |
|
Trace("sygus-active-gen-debug") |
138 |
|
<< "Active-gen: return waiting " << d_evActiveGenWaiting << std::endl; |
139 |
|
return d_evActiveGenWaiting; |
140 |
|
} |
141 |
|
// Check if there is an (abstract) value absE we were actively generating |
142 |
|
// values based on. |
143 |
101276 |
Node absE = d_ev_curr_active_gen; |
144 |
50638 |
bool firstTime = false; |
145 |
50638 |
if (absE.isNull()) |
146 |
|
{ |
147 |
|
// None currently exist. The next abstract value is the model value for e. |
148 |
206 |
absE = getModelValue(e); |
149 |
206 |
if (Trace.isOn("sygus-active-gen")) |
150 |
|
{ |
151 |
|
Trace("sygus-active-gen") << "Active-gen: new abstract value : "; |
152 |
|
TermDbSygus::toStreamSygus("sygus-active-gen", e); |
153 |
|
Trace("sygus-active-gen") << " -> "; |
154 |
|
TermDbSygus::toStreamSygus("sygus-active-gen", absE); |
155 |
|
Trace("sygus-active-gen") << std::endl; |
156 |
|
} |
157 |
206 |
d_ev_curr_active_gen = absE; |
158 |
206 |
d_evg->addValue(absE); |
159 |
206 |
firstTime = true; |
160 |
|
} |
161 |
50638 |
bool inc = true; |
162 |
50638 |
if (!firstTime) |
163 |
|
{ |
164 |
50432 |
inc = d_evg->increment(); |
165 |
|
} |
166 |
101276 |
Node v; |
167 |
50638 |
if (inc) |
168 |
|
{ |
169 |
50627 |
v = d_evg->getCurrent(); |
170 |
|
} |
171 |
101248 |
Trace("sygus-active-gen-debug") |
172 |
50624 |
<< "...generated " << v << ", with increment success : " << inc |
173 |
50624 |
<< std::endl; |
174 |
50624 |
if (!inc) |
175 |
|
{ |
176 |
|
// No more concrete values generated from absE. |
177 |
11 |
NodeManager* nm = NodeManager::currentNM(); |
178 |
11 |
d_ev_curr_active_gen = Node::null(); |
179 |
22 |
std::vector<Node> exp; |
180 |
|
// If we are a basic enumerator, a single abstract value maps to *all* |
181 |
|
// concrete values of its type, thus we don't depend on the current |
182 |
|
// solution. |
183 |
11 |
if (!d_tds->isBasicEnumerator(e)) |
184 |
|
{ |
185 |
|
// We must block e = absE |
186 |
2 |
d_tds->getExplain()->getExplanationForEquality(e, absE, exp); |
187 |
4 |
for (unsigned i = 0, size = exp.size(); i < size; i++) |
188 |
|
{ |
189 |
2 |
exp[i] = exp[i].negate(); |
190 |
|
} |
191 |
|
} |
192 |
22 |
Node g = d_tds->getActiveGuardForEnumerator(e); |
193 |
11 |
if (!g.isNull()) |
194 |
|
{ |
195 |
11 |
if (d_evActiveGenFirstVal.isNull()) |
196 |
|
{ |
197 |
11 |
exp.push_back(g.negate()); |
198 |
11 |
d_evActiveGenFirstVal = absE; |
199 |
|
} |
200 |
|
} |
201 |
|
else |
202 |
|
{ |
203 |
|
Assert(false); |
204 |
|
} |
205 |
22 |
Node lem = exp.size() == 1 ? exp[0] : nm->mkNode(OR, exp); |
206 |
22 |
Trace("cegqi-lemma") << "Cegqi::Lemma : actively-generated enumerator " |
207 |
11 |
"exclude current solution : " |
208 |
11 |
<< lem << std::endl; |
209 |
11 |
if (Trace.isOn("sygus-active-gen-debug")) |
210 |
|
{ |
211 |
|
Trace("sygus-active-gen-debug") << "Active-gen: block "; |
212 |
|
TermDbSygus::toStreamSygus("sygus-active-gen-debug", absE); |
213 |
|
Trace("sygus-active-gen-debug") << std::endl; |
214 |
|
} |
215 |
11 |
d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_EXCLUDE_CURRENT); |
216 |
|
} |
217 |
|
else |
218 |
|
{ |
219 |
|
// We are waiting to send e -> v to the module that requested it. |
220 |
50613 |
if (v.isNull()) |
221 |
|
{ |
222 |
33413 |
activeIncomplete = true; |
223 |
|
} |
224 |
|
else |
225 |
|
{ |
226 |
17200 |
d_evActiveGenWaiting = v; |
227 |
|
} |
228 |
50613 |
if (Trace.isOn("sygus-active-gen")) |
229 |
|
{ |
230 |
|
Trace("sygus-active-gen") << "Active-gen : " << e << " : "; |
231 |
|
TermDbSygus::toStreamSygus("sygus-active-gen", absE); |
232 |
|
Trace("sygus-active-gen") << " -> "; |
233 |
|
TermDbSygus::toStreamSygus("sygus-active-gen", v); |
234 |
|
Trace("sygus-active-gen") << std::endl; |
235 |
|
} |
236 |
|
} |
237 |
|
|
238 |
50624 |
return v; |
239 |
|
} |
240 |
|
|
241 |
33869 |
void EnumValueManager::notifyCandidate(bool modelSuccess) |
242 |
|
{ |
243 |
33869 |
d_evActiveGenWaiting = Node::null(); |
244 |
|
// clear evaluation |
245 |
33869 |
if (modelSuccess && d_eec != nullptr) |
246 |
|
{ |
247 |
5696 |
d_eec->clearEvaluationAll(); |
248 |
|
} |
249 |
33869 |
} |
250 |
|
|
251 |
30002 |
ExampleEvalCache* EnumValueManager::getExampleEvalCache() |
252 |
|
{ |
253 |
30002 |
return d_eec.get(); |
254 |
|
} |
255 |
|
|
256 |
11472 |
Node EnumValueManager::getModelValue(Node n) |
257 |
|
{ |
258 |
11472 |
return d_treg.getModel()->getValue(n); |
259 |
|
} |
260 |
|
|
261 |
|
} // namespace quantifiers |
262 |
|
} // namespace theory |
263 |
31137 |
} // namespace cvc5 |