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