1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Morgan Deters, 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 |
|
* Implementation of counterexample-guided quantifier instantiation strategies. |
14 |
|
*/ |
15 |
|
#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" |
16 |
|
|
17 |
|
#include "expr/node_algorithm.h" |
18 |
|
#include "expr/skolem_manager.h" |
19 |
|
#include "options/quantifiers_options.h" |
20 |
|
#include "theory/quantifiers/first_order_model.h" |
21 |
|
#include "theory/quantifiers/instantiate.h" |
22 |
|
#include "theory/quantifiers/quantifiers_attributes.h" |
23 |
|
#include "theory/quantifiers/quantifiers_rewriter.h" |
24 |
|
#include "theory/quantifiers/term_database.h" |
25 |
|
#include "theory/quantifiers/term_registry.h" |
26 |
|
#include "theory/quantifiers/term_util.h" |
27 |
|
#include "theory/rewriter.h" |
28 |
|
#include "util/rational.h" |
29 |
|
|
30 |
|
using namespace std; |
31 |
|
using namespace cvc5::kind; |
32 |
|
using namespace cvc5::context; |
33 |
|
|
34 |
|
namespace cvc5 { |
35 |
|
namespace theory { |
36 |
|
namespace quantifiers { |
37 |
|
|
38 |
4694 |
InstRewriterCegqi::InstRewriterCegqi(InstStrategyCegqi* p) |
39 |
4694 |
: InstantiationRewriter(), d_parent(p) |
40 |
|
{ |
41 |
4694 |
} |
42 |
|
|
43 |
47390 |
TrustNode InstRewriterCegqi::rewriteInstantiation(Node q, |
44 |
|
std::vector<Node>& terms, |
45 |
|
Node inst, |
46 |
|
bool doVts) |
47 |
|
{ |
48 |
47390 |
return d_parent->rewriteInstantiation(q, terms, inst, doVts); |
49 |
|
} |
50 |
|
|
51 |
4694 |
InstStrategyCegqi::InstStrategyCegqi(Env& env, |
52 |
|
QuantifiersState& qs, |
53 |
|
QuantifiersInferenceManager& qim, |
54 |
|
QuantifiersRegistry& qr, |
55 |
4694 |
TermRegistry& tr) |
56 |
|
: QuantifiersModule(env, qs, qim, qr, tr), |
57 |
4694 |
d_irew(new InstRewriterCegqi(this)), |
58 |
|
d_cbqi_set_quant_inactive(false), |
59 |
|
d_incomplete_check(false), |
60 |
4694 |
d_added_cbqi_lemma(userContext()), |
61 |
4694 |
d_vtsCache(new VtsTermCache(qim)), |
62 |
|
d_bv_invert(nullptr), |
63 |
|
d_small_const_multiplier( |
64 |
9388 |
NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000))), |
65 |
28164 |
d_small_const(d_small_const_multiplier) |
66 |
|
{ |
67 |
4694 |
d_check_vts_lemma_lc = false; |
68 |
4694 |
if (options::cegqiBv()) |
69 |
|
{ |
70 |
|
// if doing instantiation for BV, need the inverter class |
71 |
3129 |
d_bv_invert.reset(new BvInverter); |
72 |
|
} |
73 |
4694 |
if (options::cegqiNestedQE()) |
74 |
|
{ |
75 |
12 |
d_nestedQe.reset(new NestedQe(d_env)); |
76 |
|
} |
77 |
4694 |
} |
78 |
|
|
79 |
9382 |
InstStrategyCegqi::~InstStrategyCegqi() {} |
80 |
|
|
81 |
33988 |
bool InstStrategyCegqi::needsCheck(Theory::Effort e) |
82 |
|
{ |
83 |
33988 |
return e>=Theory::EFFORT_LAST_CALL; |
84 |
|
} |
85 |
|
|
86 |
8683 |
QuantifiersModule::QEffort InstStrategyCegqi::needsModel(Theory::Effort e) |
87 |
|
{ |
88 |
8683 |
size_t nquant = d_treg.getModel()->getNumAssertedQuantifiers(); |
89 |
27466 |
for (size_t i = 0; i < nquant; i++) |
90 |
|
{ |
91 |
40135 |
Node q = d_treg.getModel()->getAssertedQuantifier(i); |
92 |
21352 |
if (doCbqi(q)) |
93 |
|
{ |
94 |
2569 |
return QEFFORT_STANDARD; |
95 |
|
} |
96 |
|
} |
97 |
6114 |
return QEFFORT_NONE; |
98 |
|
} |
99 |
|
|
100 |
1167 |
bool InstStrategyCegqi::registerCbqiLemma(Node q) |
101 |
|
{ |
102 |
1167 |
if( !hasAddedCbqiLemma( q ) ){ |
103 |
1126 |
NodeManager* nm = NodeManager::currentNM(); |
104 |
1126 |
d_added_cbqi_lemma.insert( q ); |
105 |
1126 |
Trace("cegqi-debug") << "Do cbqi for " << q << std::endl; |
106 |
|
//add cbqi lemma |
107 |
|
//get the counterexample literal |
108 |
2252 |
Node ceLit = getCounterexampleLiteral(q); |
109 |
2252 |
Node ceBody = d_qreg.getInstConstantBody(q); |
110 |
1126 |
if( !ceBody.isNull() ){ |
111 |
|
//add counterexample lemma |
112 |
2252 |
Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() ); |
113 |
|
//require any decision on cel to be phase=true |
114 |
1126 |
d_qim.addPendingPhaseRequirement(ceLit, true); |
115 |
1126 |
Debug("cegqi-debug") << "Require phase " << ceLit << " = true." << std::endl; |
116 |
|
//add counterexample lemma |
117 |
1126 |
lem = Rewriter::rewrite( lem ); |
118 |
1126 |
Trace("cegqi-lemma") << "Counterexample lemma : " << lem << std::endl; |
119 |
1127 |
registerCounterexampleLemma( q, lem ); |
120 |
|
|
121 |
|
//compute dependencies between quantified formulas |
122 |
2250 |
std::vector<Node> ics; |
123 |
1125 |
TermUtil::computeInstConstContains(q, ics); |
124 |
1125 |
d_parent_quant[q].clear(); |
125 |
1125 |
d_children_quant[q].clear(); |
126 |
2250 |
std::vector<Node> dep; |
127 |
1233 |
for (const Node& ic : ics) |
128 |
|
{ |
129 |
216 |
Node qi = ic.getAttribute(InstConstantAttribute()); |
130 |
324 |
if (std::find(d_parent_quant[q].begin(), d_parent_quant[q].end(), qi) |
131 |
324 |
== d_parent_quant[q].end()) |
132 |
|
{ |
133 |
68 |
d_parent_quant[q].push_back(qi); |
134 |
68 |
d_children_quant[qi].push_back(q); |
135 |
|
// may not have added the CEX lemma, but the literal is created by |
136 |
|
// the following call regardless. One rare case where this can happen |
137 |
|
// is if both sygus-inst and CEGQI are being run in parallel, and |
138 |
|
// a parent quantified formula is not handled by CEGQI, but a child |
139 |
|
// is. |
140 |
136 |
Node qicel = getCounterexampleLiteral(qi); |
141 |
68 |
dep.push_back(qi); |
142 |
68 |
dep.push_back(qicel); |
143 |
|
} |
144 |
|
} |
145 |
1125 |
if (!dep.empty()) |
146 |
|
{ |
147 |
|
// This lemma states that if the child is active, then the parent must |
148 |
|
// be asserted, in particular G => Q where G is the CEX literal for the |
149 |
|
// child and Q is the parent. |
150 |
96 |
Node dep_lemma = nm->mkNode(IMPLIES, ceLit, nm->mkNode(AND, dep)); |
151 |
96 |
Trace("cegqi-lemma") |
152 |
48 |
<< "Counterexample dependency lemma : " << dep_lemma << std::endl; |
153 |
48 |
d_qim.lemma(dep_lemma, InferenceId::QUANTIFIERS_CEGQI_CEX_DEP); |
154 |
|
} |
155 |
|
|
156 |
|
//must register all sub-quantifiers of counterexample lemma, register their lemmas |
157 |
2250 |
std::vector< Node > quants; |
158 |
1125 |
TermUtil::computeQuantContains( lem, quants ); |
159 |
1167 |
for( unsigned i=0; i<quants.size(); i++ ){ |
160 |
42 |
if( doCbqi( quants[i] ) ){ |
161 |
41 |
registerCbqiLemma( quants[i] ); |
162 |
|
} |
163 |
|
} |
164 |
|
} |
165 |
|
// The decision strategy for this quantified formula ensures that its |
166 |
|
// counterexample literal is decided on first. It is user-context dependent. |
167 |
|
std::map<Node, std::unique_ptr<DecisionStrategy>>::iterator itds = |
168 |
1125 |
d_dstrat.find(q); |
169 |
1125 |
DecisionStrategy* dlds = nullptr; |
170 |
1125 |
if (itds == d_dstrat.end()) |
171 |
|
{ |
172 |
3375 |
d_dstrat[q].reset(new DecisionStrategySingleton( |
173 |
2250 |
d_env, "CexLiteral", ceLit, d_qstate.getValuation())); |
174 |
1125 |
dlds = d_dstrat[q].get(); |
175 |
|
} |
176 |
|
else |
177 |
|
{ |
178 |
|
dlds = itds->second.get(); |
179 |
|
} |
180 |
|
// it is appended to the list of strategies |
181 |
1125 |
d_qim.getDecisionManager()->registerStrategy( |
182 |
|
DecisionManager::STRAT_QUANT_CEGQI_FEASIBLE, dlds); |
183 |
1125 |
return true; |
184 |
|
}else{ |
185 |
41 |
return false; |
186 |
|
} |
187 |
|
} |
188 |
|
|
189 |
18959 |
void InstStrategyCegqi::reset_round(Theory::Effort effort) |
190 |
|
{ |
191 |
18959 |
d_cbqi_set_quant_inactive = false; |
192 |
18959 |
d_incomplete_check = false; |
193 |
18959 |
d_active_quant.clear(); |
194 |
|
//check if any cbqi lemma has not been added yet |
195 |
18959 |
FirstOrderModel* fm = d_treg.getModel(); |
196 |
18959 |
size_t nquant = fm->getNumAssertedQuantifiers(); |
197 |
122945 |
for (size_t i = 0; i < nquant; i++) |
198 |
|
{ |
199 |
207972 |
Node q = fm->getAssertedQuantifier(i); |
200 |
|
//it is not active if it corresponds to a rewrite rule: we will process in rewrite engine |
201 |
103986 |
if( doCbqi( q ) ){ |
202 |
5262 |
if (fm->isQuantifierActive(q)) |
203 |
|
{ |
204 |
5262 |
d_active_quant[q] = true; |
205 |
5262 |
Debug("cegqi-debug") << "Check quantified formula " << q << "..." << std::endl; |
206 |
10524 |
Node cel = getCounterexampleLiteral(q); |
207 |
|
bool value; |
208 |
5262 |
if (d_qstate.getValuation().hasSatValue(cel, value)) |
209 |
|
{ |
210 |
5253 |
Debug("cegqi-debug") << "...CE Literal has value " << value << std::endl; |
211 |
5253 |
if( !value ){ |
212 |
569 |
if (d_qstate.getValuation().isDecision(cel)) |
213 |
|
{ |
214 |
|
Trace("cegqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl; |
215 |
|
}else{ |
216 |
569 |
Trace("cegqi") << "Inactive : " << q << std::endl; |
217 |
569 |
fm->setQuantifierActive(q, false); |
218 |
569 |
d_cbqi_set_quant_inactive = true; |
219 |
569 |
d_active_quant.erase( q ); |
220 |
|
} |
221 |
|
} |
222 |
|
}else{ |
223 |
9 |
Debug("cegqi-debug") << "...CE Literal does not have value " << std::endl; |
224 |
|
} |
225 |
|
} |
226 |
|
} |
227 |
|
} |
228 |
|
|
229 |
|
//refinement: only consider innermost active quantified formulas |
230 |
18959 |
if( options::cegqiInnermost() ){ |
231 |
18959 |
if( !d_children_quant.empty() && !d_active_quant.empty() ){ |
232 |
4034 |
Trace("cegqi-debug") << "Find non-innermost quantifiers..." << std::endl; |
233 |
8068 |
std::vector< Node > ninner; |
234 |
8719 |
for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){ |
235 |
4685 |
std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( it->first ); |
236 |
4685 |
if( itc!=d_children_quant.end() ){ |
237 |
4750 |
for( unsigned j=0; j<itc->second.size(); j++ ){ |
238 |
97 |
if( d_active_quant.find( itc->second[j] )!=d_active_quant.end() ){ |
239 |
31 |
Trace("cegqi-debug") << "Do not consider " << it->first << " since it is not innermost (" << itc->second[j] << std::endl; |
240 |
31 |
ninner.push_back( it->first ); |
241 |
31 |
break; |
242 |
|
} |
243 |
|
} |
244 |
|
} |
245 |
|
} |
246 |
4034 |
Trace("cegqi-debug") << "Found " << ninner.size() << " non-innermost." << std::endl; |
247 |
4065 |
for( unsigned i=0; i<ninner.size(); i++ ){ |
248 |
31 |
Assert(d_active_quant.find(ninner[i]) != d_active_quant.end()); |
249 |
31 |
d_active_quant.erase( ninner[i] ); |
250 |
|
} |
251 |
4034 |
Assert(!d_active_quant.empty()); |
252 |
4034 |
Trace("cegqi-debug") << "...done removing." << std::endl; |
253 |
|
} |
254 |
|
} |
255 |
18959 |
d_check_vts_lemma_lc = false; |
256 |
18959 |
} |
257 |
|
|
258 |
25148 |
void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e) |
259 |
|
{ |
260 |
25148 |
if (quant_e == QEFFORT_STANDARD) |
261 |
|
{ |
262 |
8656 |
Assert(!d_qstate.isInConflict()); |
263 |
8656 |
double clSet = 0; |
264 |
8656 |
if( Trace.isOn("cegqi-engine") ){ |
265 |
|
clSet = double(clock())/double(CLOCKS_PER_SEC); |
266 |
|
Trace("cegqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl; |
267 |
|
} |
268 |
8656 |
size_t lastWaiting = d_qim.numPendingLemmas(); |
269 |
21156 |
for( int ee=0; ee<=1; ee++ ){ |
270 |
|
//for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ |
271 |
|
// Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); |
272 |
|
// if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ |
273 |
17801 |
for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){ |
274 |
5790 |
Node q = it->first; |
275 |
2895 |
Trace("cegqi") << "CBQI : Process quantifier " << q[0] << " at effort " << ee << std::endl; |
276 |
2895 |
process(q, e, ee); |
277 |
2895 |
if (d_qstate.isInConflict()) |
278 |
|
{ |
279 |
|
break; |
280 |
|
} |
281 |
|
} |
282 |
14906 |
if (d_qstate.isInConflict() || d_qim.numPendingLemmas() > lastWaiting) |
283 |
|
{ |
284 |
2406 |
break; |
285 |
|
} |
286 |
|
} |
287 |
8656 |
if( Trace.isOn("cegqi-engine") ){ |
288 |
|
if (d_qim.numPendingLemmas() > lastWaiting) |
289 |
|
{ |
290 |
|
Trace("cegqi-engine") |
291 |
|
<< "Added lemmas = " << (d_qim.numPendingLemmas() - lastWaiting) |
292 |
|
<< std::endl; |
293 |
|
} |
294 |
|
double clSet2 = double(clock())/double(CLOCKS_PER_SEC); |
295 |
|
Trace("cegqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl; |
296 |
|
} |
297 |
|
} |
298 |
25148 |
} |
299 |
|
|
300 |
2308 |
bool InstStrategyCegqi::checkComplete(IncompleteId& incId) |
301 |
|
{ |
302 |
2308 |
if( ( !options::cegqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){ |
303 |
24 |
incId = IncompleteId::QUANTIFIERS_CEGQI; |
304 |
24 |
return false; |
305 |
|
}else{ |
306 |
2284 |
return true; |
307 |
|
} |
308 |
|
} |
309 |
|
|
310 |
1183 |
bool InstStrategyCegqi::checkCompleteFor(Node q) |
311 |
|
{ |
312 |
1183 |
std::map<Node, CegHandledStatus>::iterator it = d_do_cbqi.find(q); |
313 |
1183 |
if( it!=d_do_cbqi.end() ){ |
314 |
1183 |
return it->second != CEG_UNHANDLED; |
315 |
|
}else{ |
316 |
|
return false; |
317 |
|
} |
318 |
|
} |
319 |
|
|
320 |
9022 |
void InstStrategyCegqi::checkOwnership(Node q) |
321 |
|
{ |
322 |
9022 |
if (d_qreg.getOwner(q) == nullptr && doCbqi(q)) |
323 |
|
{ |
324 |
1133 |
if (d_do_cbqi[q] == CEG_HANDLED) |
325 |
|
{ |
326 |
|
//take full ownership of the quantified formula |
327 |
1119 |
d_qreg.setOwner(q, this); |
328 |
|
} |
329 |
|
} |
330 |
9022 |
} |
331 |
|
|
332 |
9041 |
void InstStrategyCegqi::preRegisterQuantifier(Node q) |
333 |
|
{ |
334 |
9041 |
if (doCbqi(q)) |
335 |
|
{ |
336 |
1133 |
if (processNestedQe(q, true)) |
337 |
|
{ |
338 |
|
// will process using nested quantifier elimination |
339 |
7 |
return; |
340 |
|
} |
341 |
|
// register the cbqi lemma |
342 |
1127 |
if( registerCbqiLemma( q ) ){ |
343 |
1084 |
Trace("cegqi") << "Registered cbqi lemma for quantifier : " << q << std::endl; |
344 |
|
} |
345 |
|
} |
346 |
|
} |
347 |
47390 |
TrustNode InstStrategyCegqi::rewriteInstantiation(Node q, |
348 |
|
std::vector<Node>& terms, |
349 |
|
Node inst, |
350 |
|
bool doVts) |
351 |
|
{ |
352 |
94780 |
Node prevInst = inst; |
353 |
47390 |
if (doVts) |
354 |
|
{ |
355 |
|
// do virtual term substitution |
356 |
22 |
inst = Rewriter::rewrite(inst); |
357 |
22 |
Trace("quant-vts-debug") << "Rewrite vts symbols in " << inst << std::endl; |
358 |
22 |
inst = d_vtsCache->rewriteVtsSymbols(inst); |
359 |
22 |
Trace("quant-vts-debug") << "...got " << inst << std::endl; |
360 |
|
} |
361 |
47390 |
if (prevInst != inst) |
362 |
|
{ |
363 |
|
// not proof producing yet |
364 |
22 |
return TrustNode::mkTrustRewrite(prevInst, inst, nullptr); |
365 |
|
} |
366 |
47368 |
return TrustNode::null(); |
367 |
|
} |
368 |
|
|
369 |
4694 |
InstantiationRewriter* InstStrategyCegqi::getInstRewriter() const |
370 |
|
{ |
371 |
4694 |
return d_irew.get(); |
372 |
|
} |
373 |
|
|
374 |
1126 |
void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem) |
375 |
|
{ |
376 |
|
// must register with the instantiator |
377 |
|
// must explicitly remove ITEs so that we record dependencies |
378 |
2252 |
std::vector<Node> ce_vars; |
379 |
3252 |
for (size_t i = 0, nics = d_qreg.getNumInstantiationConstants(q); i < nics; |
380 |
|
i++) |
381 |
|
{ |
382 |
2126 |
ce_vars.push_back(d_qreg.getInstantiationConstant(q, i)); |
383 |
|
} |
384 |
|
// send the lemma |
385 |
1127 |
d_qim.lemma(lem, InferenceId::QUANTIFIERS_CEGQI_CEX); |
386 |
|
// get the preprocessed form of the lemma we just sent |
387 |
2250 |
std::vector<Node> skolems; |
388 |
2250 |
std::vector<Node> skAsserts; |
389 |
|
Node ppLem = |
390 |
2250 |
d_qstate.getValuation().getPreprocessedTerm(lem, skAsserts, skolems); |
391 |
2250 |
std::vector<Node> lemp{ppLem}; |
392 |
1125 |
lemp.insert(lemp.end(), skAsserts.begin(), skAsserts.end()); |
393 |
1125 |
ppLem = NodeManager::currentNM()->mkAnd(lemp); |
394 |
2250 |
Trace("cegqi-debug") << "Counterexample lemma (post-preprocess): " << ppLem |
395 |
1125 |
<< std::endl; |
396 |
2250 |
std::vector<Node> auxLems; |
397 |
1125 |
CegInstantiator* cinst = getInstantiator(q); |
398 |
1125 |
cinst->registerCounterexampleLemma(ppLem, ce_vars, auxLems); |
399 |
1222 |
for (size_t i = 0, size = auxLems.size(); i < size; i++) |
400 |
|
{ |
401 |
194 |
Trace("cegqi-debug") << "Auxiliary CE lemma " << i << " : " << auxLems[i] |
402 |
97 |
<< std::endl; |
403 |
97 |
d_qim.addPendingLemma(auxLems[i], InferenceId::QUANTIFIERS_CEGQI_CEX_AUX); |
404 |
|
} |
405 |
1125 |
} |
406 |
|
|
407 |
143443 |
bool InstStrategyCegqi::doCbqi(Node q) |
408 |
|
{ |
409 |
143443 |
std::map<Node, CegHandledStatus>::iterator it = d_do_cbqi.find(q); |
410 |
143443 |
if( it==d_do_cbqi.end() ){ |
411 |
9022 |
CegHandledStatus ret = CegInstantiator::isCbqiQuant(q); |
412 |
9022 |
Trace("cegqi-quant") << "doCbqi " << q << " returned " << ret << std::endl; |
413 |
9022 |
d_do_cbqi[q] = ret; |
414 |
9022 |
return ret != CEG_UNHANDLED; |
415 |
|
} |
416 |
134421 |
return it->second != CEG_UNHANDLED; |
417 |
|
} |
418 |
|
|
419 |
2895 |
void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) { |
420 |
|
// If we are doing nested quantifier elimination, check if q was already |
421 |
|
// processed. |
422 |
2895 |
if (processNestedQe(q, false)) |
423 |
|
{ |
424 |
|
// don't need to process this, since it has been reduced |
425 |
11 |
return; |
426 |
|
} |
427 |
2884 |
if( e==0 ){ |
428 |
2776 |
CegInstantiator * cinst = getInstantiator( q ); |
429 |
2776 |
Trace("inst-alg") << "-> Run cegqi for " << q << std::endl; |
430 |
2776 |
d_curr_quant = q; |
431 |
2776 |
if( !cinst->check() ){ |
432 |
107 |
d_incomplete_check = true; |
433 |
107 |
d_check_vts_lemma_lc = true; |
434 |
|
} |
435 |
2776 |
d_curr_quant = Node::null(); |
436 |
108 |
}else if( e==1 ){ |
437 |
|
//minimize the free delta heuristically on demand |
438 |
108 |
if( d_check_vts_lemma_lc ){ |
439 |
36 |
Trace("inst-alg") << "-> Minimize delta heuristic, for " << q << std::endl; |
440 |
36 |
d_check_vts_lemma_lc = false; |
441 |
72 |
d_small_const = NodeManager::currentNM()->mkNode( |
442 |
36 |
MULT, d_small_const, d_small_const_multiplier); |
443 |
36 |
d_small_const = Rewriter::rewrite( d_small_const ); |
444 |
|
//heuristic for now, until we know how to do nested quantification |
445 |
72 |
Node delta = d_vtsCache->getVtsDelta(true, false); |
446 |
36 |
if( !delta.isNull() ){ |
447 |
|
Trace("quant-vts-debug") << "Delta lemma for " << d_small_const << std::endl; |
448 |
|
Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_small_const ); |
449 |
|
d_qim.lemma(delta_lem_ub, InferenceId::QUANTIFIERS_CEGQI_VTS_UB_DELTA); |
450 |
|
} |
451 |
72 |
std::vector< Node > inf; |
452 |
36 |
d_vtsCache->getVtsTerms(inf, true, false, false); |
453 |
36 |
for( unsigned i=0; i<inf.size(); i++ ){ |
454 |
|
Trace("quant-vts-debug") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl; |
455 |
|
Node inf_lem_lb = NodeManager::currentNM()->mkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst<Rational>() ) ); |
456 |
|
d_qim.lemma(inf_lem_lb, InferenceId::QUANTIFIERS_CEGQI_VTS_LB_INF); |
457 |
|
} |
458 |
|
} |
459 |
|
} |
460 |
|
} |
461 |
|
|
462 |
6456 |
Node InstStrategyCegqi::getCounterexampleLiteral(Node q) |
463 |
|
{ |
464 |
6456 |
std::map<Node, Node>::iterator it = d_ce_lit.find(q); |
465 |
6456 |
if (it != d_ce_lit.end()) |
466 |
|
{ |
467 |
5325 |
return it->second; |
468 |
|
} |
469 |
1131 |
NodeManager * nm = NodeManager::currentNM(); |
470 |
1131 |
SkolemManager* sm = nm->getSkolemManager(); |
471 |
2262 |
Node g = sm->mkDummySkolem("g", nm->booleanType()); |
472 |
|
// ensure that it is a SAT literal |
473 |
2262 |
Node ceLit = d_qstate.getValuation().ensureLiteral(g); |
474 |
1131 |
d_ce_lit[q] = ceLit; |
475 |
1131 |
return ceLit; |
476 |
|
} |
477 |
|
|
478 |
5628 |
bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { |
479 |
5628 |
Assert(!d_curr_quant.isNull()); |
480 |
|
// check if we need virtual term substitution (if used delta or infinity) |
481 |
5628 |
bool usedVts = d_vtsCache->containsVtsTerm(subs, false); |
482 |
5628 |
Instantiate* inst = d_qim.getInstantiate(); |
483 |
|
//if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma |
484 |
5628 |
if (d_qreg.getQuantAttributes().isQuantElimPartial(d_curr_quant)) |
485 |
|
{ |
486 |
1 |
d_cbqi_set_quant_inactive = true; |
487 |
1 |
d_incomplete_check = true; |
488 |
1 |
inst->recordInstantiation(d_curr_quant, subs, usedVts); |
489 |
1 |
return true; |
490 |
|
} |
491 |
16881 |
else if (inst->addInstantiation(d_curr_quant, |
492 |
|
subs, |
493 |
|
InferenceId::QUANTIFIERS_INST_CEGQI, |
494 |
11254 |
Node::null(), |
495 |
|
false, |
496 |
|
usedVts)) |
497 |
|
{ |
498 |
2668 |
return true; |
499 |
|
} |
500 |
|
// this should never happen for monotonic selection strategies |
501 |
2959 |
Trace("cegqi-warn") << "WARNING: Existing instantiation" << std::endl; |
502 |
2959 |
return false; |
503 |
|
} |
504 |
|
|
505 |
3901 |
CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) { |
506 |
|
std::map<Node, std::unique_ptr<CegInstantiator>>::iterator it = |
507 |
3901 |
d_cinst.find(q); |
508 |
3901 |
if( it==d_cinst.end() ){ |
509 |
1125 |
d_cinst[q].reset(new CegInstantiator(d_env, q, d_qstate, d_treg, this)); |
510 |
1125 |
return d_cinst[q].get(); |
511 |
|
} |
512 |
2776 |
return it->second.get(); |
513 |
|
} |
514 |
|
|
515 |
886 |
VtsTermCache* InstStrategyCegqi::getVtsTermCache() const |
516 |
|
{ |
517 |
886 |
return d_vtsCache.get(); |
518 |
|
} |
519 |
|
|
520 |
947 |
BvInverter* InstStrategyCegqi::getBvInverter() const |
521 |
|
{ |
522 |
947 |
return d_bv_invert.get(); |
523 |
|
} |
524 |
|
|
525 |
4028 |
bool InstStrategyCegqi::processNestedQe(Node q, bool isPreregister) |
526 |
|
{ |
527 |
4028 |
if (d_nestedQe != nullptr) |
528 |
|
{ |
529 |
36 |
if (isPreregister) |
530 |
|
{ |
531 |
|
// If at preregister, we are done if we have nested quantification. |
532 |
|
// We will process nested quantification. |
533 |
15 |
return NestedQe::hasNestedQuantification(q); |
534 |
|
} |
535 |
|
// if not a preregister, we process, which may trigger quantifier |
536 |
|
// elimination in subsolvers. |
537 |
31 |
std::vector<Node> lems; |
538 |
21 |
if (d_nestedQe->process(q, lems)) |
539 |
|
{ |
540 |
|
// add lemmas to process |
541 |
16 |
for (const Node& lem : lems) |
542 |
|
{ |
543 |
5 |
d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_CEGQI_NESTED_QE); |
544 |
|
} |
545 |
|
// don't need to process this, since it has been reduced |
546 |
11 |
return true; |
547 |
|
} |
548 |
|
} |
549 |
4002 |
return false; |
550 |
|
} |
551 |
|
|
552 |
|
} // namespace quantifiers |
553 |
|
} // namespace theory |
554 |
22746 |
} // namespace cvc5 |