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 |
332 |
EnumValueManager::EnumValueManager(Env& env, |
37 |
|
QuantifiersState& qs, |
38 |
|
QuantifiersInferenceManager& qim, |
39 |
|
TermRegistry& tr, |
40 |
|
SygusStatistics& s, |
41 |
|
Node e, |
42 |
332 |
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 |
332 |
d_tds(tr.getTermDatabaseSygus()), |
50 |
664 |
d_eec(hasExamples ? new ExampleEvalCache(d_tds, e) : nullptr) |
51 |
|
{ |
52 |
332 |
} |
53 |
|
|
54 |
664 |
EnumValueManager::~EnumValueManager() {} |
55 |
|
|
56 |
43888 |
Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete) |
57 |
|
{ |
58 |
87776 |
Node e = d_enum; |
59 |
43888 |
bool isEnum = d_tds->isEnumerator(e); |
60 |
|
|
61 |
43888 |
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 |
3846 |
Trace("sygus-engine-debug") |
67 |
1923 |
<< "Enumerator " << e << " does not have proper model value." |
68 |
1923 |
<< std::endl; |
69 |
1923 |
return Node::null(); |
70 |
|
} |
71 |
|
|
72 |
41965 |
if (!isEnum || d_tds->isPassiveEnumerator(e)) |
73 |
|
{ |
74 |
6993 |
return getModelValue(e); |
75 |
|
} |
76 |
|
|
77 |
|
// management of actively generated enumerators goes here |
78 |
|
|
79 |
|
// initialize the enumerated value generator for e |
80 |
34972 |
if (d_evg == nullptr) |
81 |
|
{ |
82 |
115 |
if (d_tds->isVariableAgnosticEnumerator(e)) |
83 |
|
{ |
84 |
1 |
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 |
114 |
Assert(d_tds->isBasicEnumerator(e)); |
92 |
228 |
if (options::sygusActiveGenMode() |
93 |
114 |
== options::SygusActiveGenMode::ENUM_BASIC) |
94 |
|
{ |
95 |
|
d_evg.reset(new EnumValGeneratorBasic(d_tds, e.getType())); |
96 |
|
} |
97 |
|
else |
98 |
|
{ |
99 |
114 |
Assert(options::sygusActiveGenMode() |
100 |
|
== options::SygusActiveGenMode::ENUM |
101 |
|
|| options::sygusActiveGenMode() |
102 |
|
== options::SygusActiveGenMode::AUTO); |
103 |
|
// create the enumerator callback |
104 |
114 |
if (options::sygusSymBreakDynamic()) |
105 |
|
{ |
106 |
114 |
std::ostream* out = nullptr; |
107 |
114 |
if (options::sygusRewVerify()) |
108 |
|
{ |
109 |
6 |
d_samplerRrV.reset(new SygusSampler); |
110 |
12 |
d_samplerRrV->initializeSygus( |
111 |
6 |
d_tds, e, options::sygusSamples(), false); |
112 |
|
// use the default output for the output of sygusRewVerify |
113 |
6 |
out = options().base.out; |
114 |
|
} |
115 |
228 |
d_secd.reset(new SygusEnumeratorCallbackDefault( |
116 |
114 |
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 |
228 |
d_evg.reset(new SygusEnumerator( |
121 |
114 |
d_tds, d_secd.get(), &d_stats, false, options::sygusRepairConst())); |
122 |
|
} |
123 |
|
} |
124 |
230 |
Trace("sygus-active-gen") |
125 |
115 |
<< "Active-gen: initialize for " << e << std::endl; |
126 |
115 |
d_evg->initialize(e); |
127 |
115 |
d_ev_curr_active_gen = Node::null(); |
128 |
115 |
Trace("sygus-active-gen-debug") << "...finish" << std::endl; |
129 |
|
} |
130 |
|
// if we have a waiting value, return it |
131 |
34972 |
if (!d_evActiveGenWaiting.isNull()) |
132 |
|
{ |
133 |
|
Trace("sygus-active-gen-debug") |
134 |
|
<< "Active-gen: return waiting " << d_evActiveGenWaiting << std::endl; |
135 |
|
return d_evActiveGenWaiting; |
136 |
|
} |
137 |
|
// Check if there is an (abstract) value absE we were actively generating |
138 |
|
// values based on. |
139 |
69944 |
Node absE = d_ev_curr_active_gen; |
140 |
34972 |
bool firstTime = false; |
141 |
34972 |
if (absE.isNull()) |
142 |
|
{ |
143 |
|
// None currently exist. The next abstract value is the model value for e. |
144 |
115 |
absE = getModelValue(e); |
145 |
115 |
if (Trace.isOn("sygus-active-gen")) |
146 |
|
{ |
147 |
|
Trace("sygus-active-gen") << "Active-gen: new abstract value : "; |
148 |
|
TermDbSygus::toStreamSygus("sygus-active-gen", e); |
149 |
|
Trace("sygus-active-gen") << " -> "; |
150 |
|
TermDbSygus::toStreamSygus("sygus-active-gen", absE); |
151 |
|
Trace("sygus-active-gen") << std::endl; |
152 |
|
} |
153 |
115 |
d_ev_curr_active_gen = absE; |
154 |
115 |
d_evg->addValue(absE); |
155 |
115 |
firstTime = true; |
156 |
|
} |
157 |
34972 |
bool inc = true; |
158 |
34972 |
if (!firstTime) |
159 |
|
{ |
160 |
34857 |
inc = d_evg->increment(); |
161 |
|
} |
162 |
69944 |
Node v; |
163 |
34972 |
if (inc) |
164 |
|
{ |
165 |
34967 |
v = d_evg->getCurrent(); |
166 |
|
} |
167 |
69926 |
Trace("sygus-active-gen-debug") |
168 |
34963 |
<< "...generated " << v << ", with increment success : " << inc |
169 |
34963 |
<< std::endl; |
170 |
34963 |
if (!inc) |
171 |
|
{ |
172 |
|
// No more concrete values generated from absE. |
173 |
5 |
NodeManager* nm = NodeManager::currentNM(); |
174 |
5 |
d_ev_curr_active_gen = Node::null(); |
175 |
10 |
std::vector<Node> exp; |
176 |
|
// If we are a basic enumerator, a single abstract value maps to *all* |
177 |
|
// concrete values of its type, thus we don't depend on the current |
178 |
|
// solution. |
179 |
5 |
if (!d_tds->isBasicEnumerator(e)) |
180 |
|
{ |
181 |
|
// We must block e = absE |
182 |
1 |
d_tds->getExplain()->getExplanationForEquality(e, absE, exp); |
183 |
2 |
for (unsigned i = 0, size = exp.size(); i < size; i++) |
184 |
|
{ |
185 |
1 |
exp[i] = exp[i].negate(); |
186 |
|
} |
187 |
|
} |
188 |
10 |
Node g = d_tds->getActiveGuardForEnumerator(e); |
189 |
5 |
if (!g.isNull()) |
190 |
|
{ |
191 |
5 |
if (d_evActiveGenFirstVal.isNull()) |
192 |
|
{ |
193 |
5 |
exp.push_back(g.negate()); |
194 |
5 |
d_evActiveGenFirstVal = absE; |
195 |
|
} |
196 |
|
} |
197 |
|
else |
198 |
|
{ |
199 |
|
Assert(false); |
200 |
|
} |
201 |
10 |
Node lem = exp.size() == 1 ? exp[0] : nm->mkNode(OR, exp); |
202 |
10 |
Trace("cegqi-lemma") << "Cegqi::Lemma : actively-generated enumerator " |
203 |
5 |
"exclude current solution : " |
204 |
5 |
<< lem << std::endl; |
205 |
5 |
if (Trace.isOn("sygus-active-gen-debug")) |
206 |
|
{ |
207 |
|
Trace("sygus-active-gen-debug") << "Active-gen: block "; |
208 |
|
TermDbSygus::toStreamSygus("sygus-active-gen-debug", absE); |
209 |
|
Trace("sygus-active-gen-debug") << std::endl; |
210 |
|
} |
211 |
5 |
d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_EXCLUDE_CURRENT); |
212 |
|
} |
213 |
|
else |
214 |
|
{ |
215 |
|
// We are waiting to send e -> v to the module that requested it. |
216 |
34958 |
if (v.isNull()) |
217 |
|
{ |
218 |
20844 |
activeIncomplete = true; |
219 |
|
} |
220 |
|
else |
221 |
|
{ |
222 |
14114 |
d_evActiveGenWaiting = v; |
223 |
|
} |
224 |
34958 |
if (Trace.isOn("sygus-active-gen")) |
225 |
|
{ |
226 |
|
Trace("sygus-active-gen") << "Active-gen : " << e << " : "; |
227 |
|
TermDbSygus::toStreamSygus("sygus-active-gen", absE); |
228 |
|
Trace("sygus-active-gen") << " -> "; |
229 |
|
TermDbSygus::toStreamSygus("sygus-active-gen", v); |
230 |
|
Trace("sygus-active-gen") << std::endl; |
231 |
|
} |
232 |
|
} |
233 |
|
|
234 |
34963 |
return v; |
235 |
|
} |
236 |
|
|
237 |
23676 |
void EnumValueManager::notifyCandidate(bool modelSuccess) |
238 |
|
{ |
239 |
23676 |
d_evActiveGenWaiting = Node::null(); |
240 |
|
// clear evaluation |
241 |
23676 |
if (modelSuccess && d_eec != nullptr) |
242 |
|
{ |
243 |
3394 |
d_eec->clearEvaluationAll(); |
244 |
|
} |
245 |
23676 |
} |
246 |
|
|
247 |
18233 |
ExampleEvalCache* EnumValueManager::getExampleEvalCache() |
248 |
|
{ |
249 |
18233 |
return d_eec.get(); |
250 |
|
} |
251 |
|
|
252 |
7108 |
Node EnumValueManager::getModelValue(Node n) |
253 |
|
{ |
254 |
7108 |
return d_treg.getModel()->getValue(n); |
255 |
|
} |
256 |
|
|
257 |
|
} // namespace quantifiers |
258 |
|
} // namespace theory |
259 |
29574 |
} // namespace cvc5 |