1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, MikolasJanota, 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 an enumerative instantiation strategy. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/quantifiers/inst_strategy_enumerative.h" |
17 |
|
|
18 |
|
#include "options/quantifiers_options.h" |
19 |
|
#include "theory/quantifiers/instantiate.h" |
20 |
|
#include "theory/quantifiers/relevant_domain.h" |
21 |
|
#include "theory/quantifiers/term_database.h" |
22 |
|
#include "theory/quantifiers/term_tuple_enumerator.h" |
23 |
|
#include "theory/quantifiers/term_util.h" |
24 |
|
|
25 |
|
using namespace cvc5::kind; |
26 |
|
using namespace cvc5::context; |
27 |
|
|
28 |
|
namespace cvc5 { |
29 |
|
namespace theory { |
30 |
|
namespace quantifiers { |
31 |
|
|
32 |
83 |
InstStrategyEnum::InstStrategyEnum(QuantifiersState& qs, |
33 |
|
QuantifiersInferenceManager& qim, |
34 |
|
QuantifiersRegistry& qr, |
35 |
|
TermRegistry& tr, |
36 |
83 |
RelevantDomain* rd) |
37 |
83 |
: QuantifiersModule(qs, qim, qr, tr), d_rd(rd), d_fullSaturateLimit(-1) |
38 |
|
{ |
39 |
83 |
} |
40 |
83 |
void InstStrategyEnum::presolve() |
41 |
|
{ |
42 |
169 |
d_fullSaturateLimit = options::fullSaturateLimit(); |
43 |
83 |
} |
44 |
12229 |
bool InstStrategyEnum::needsCheck(Theory::Effort e) |
45 |
|
{ |
46 |
12229 |
if (d_fullSaturateLimit == 0) |
47 |
|
{ |
48 |
|
return false; |
49 |
|
} |
50 |
31736 |
if (options::fullSaturateInterleave()) |
51 |
|
{ |
52 |
|
// if interleaved, we run at the same time as E-matching |
53 |
|
if (d_qstate.getInstWhenNeedsCheck(e)) |
54 |
|
{ |
55 |
|
return true; |
56 |
|
} |
57 |
|
} |
58 |
31884 |
if (options::fullSaturateQuant()) |
59 |
|
{ |
60 |
12229 |
if (e >= Theory::EFFORT_LAST_CALL) |
61 |
|
{ |
62 |
296 |
return true; |
63 |
|
} |
64 |
|
} |
65 |
11933 |
return false; |
66 |
|
} |
67 |
|
|
68 |
1085 |
void InstStrategyEnum::reset_round(Theory::Effort e) {} |
69 |
947 |
void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) |
70 |
|
{ |
71 |
947 |
bool doCheck = false; |
72 |
947 |
bool fullEffort = false; |
73 |
947 |
if (d_fullSaturateLimit != 0) |
74 |
|
{ |
75 |
947 |
if (options::fullSaturateInterleave()) |
76 |
|
{ |
77 |
|
// we only add when interleaved with other strategies |
78 |
|
doCheck = quant_e == QEFFORT_STANDARD && d_qim.hasPendingLemma(); |
79 |
|
} |
80 |
947 |
if (options::fullSaturateQuant() && !doCheck) |
81 |
|
{ |
82 |
947 |
if (!d_qstate.getValuation().needCheck()) |
83 |
|
{ |
84 |
703 |
doCheck = quant_e == QEFFORT_LAST_CALL; |
85 |
703 |
fullEffort = true; |
86 |
|
} |
87 |
|
} |
88 |
|
} |
89 |
947 |
if (!doCheck) |
90 |
|
{ |
91 |
829 |
return; |
92 |
|
} |
93 |
118 |
Assert(!d_qstate.isInConflict()); |
94 |
118 |
double clSet = 0; |
95 |
118 |
if (Trace.isOn("fs-engine")) |
96 |
|
{ |
97 |
|
clSet = double(clock()) / double(CLOCKS_PER_SEC); |
98 |
|
Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---" |
99 |
|
<< std::endl; |
100 |
|
} |
101 |
236 |
unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1; |
102 |
118 |
unsigned rend = fullEffort ? 1 : rstart; |
103 |
118 |
unsigned addedLemmas = 0; |
104 |
|
// First try in relevant domain of all quantified formulas, if no |
105 |
|
// instantiations exist, try arbitrary ground terms. |
106 |
|
// Notice that this stratification of effort levels makes it so that some |
107 |
|
// quantified formulas may not be instantiated (if they have no instances |
108 |
|
// at effort level r=0 but another quantified formula does). We prefer |
109 |
|
// this stratification since effort level r=1 may be highly expensive in the |
110 |
|
// case where we have a quantified formula with many entailed instances. |
111 |
118 |
FirstOrderModel* fm = d_treg.getModel(); |
112 |
118 |
unsigned nquant = fm->getNumAssertedQuantifiers(); |
113 |
236 |
std::map<Node, bool> alreadyProc; |
114 |
332 |
for (unsigned r = rstart; r <= rend; r++) |
115 |
|
{ |
116 |
225 |
if (d_rd || r > 0) |
117 |
|
{ |
118 |
225 |
if (r == 0) |
119 |
|
{ |
120 |
118 |
Trace("inst-alg") << "-> Relevant domain instantiate..." << std::endl; |
121 |
118 |
Trace("inst-alg-debug") << "Compute relevant domain..." << std::endl; |
122 |
118 |
d_rd->compute(); |
123 |
118 |
Trace("inst-alg-debug") << "...finished" << std::endl; |
124 |
|
} |
125 |
|
else |
126 |
|
{ |
127 |
107 |
Trace("inst-alg") << "-> Ground term instantiate..." << std::endl; |
128 |
|
} |
129 |
2612 |
for (unsigned i = 0; i < nquant; i++) |
130 |
|
{ |
131 |
4774 |
Node q = fm->getAssertedQuantifier(i, true); |
132 |
7161 |
bool doProcess = d_qreg.hasOwnership(q, this) |
133 |
4746 |
&& fm->isQuantifierActive(q) |
134 |
9520 |
&& alreadyProc.find(q) == alreadyProc.end(); |
135 |
2387 |
if (doProcess) |
136 |
|
{ |
137 |
1920 |
if (process(q, fullEffort, r == 0)) |
138 |
|
{ |
139 |
|
// don't need to mark this if we are not stratifying |
140 |
2448 |
if (!options::fullSaturateStratify()) |
141 |
|
{ |
142 |
608 |
alreadyProc[q] = true; |
143 |
|
} |
144 |
|
// added lemma |
145 |
1118 |
addedLemmas++; |
146 |
|
} |
147 |
1920 |
if (d_qstate.isInConflict()) |
148 |
|
{ |
149 |
|
break; |
150 |
|
} |
151 |
|
} |
152 |
|
} |
153 |
450 |
if (d_qstate.isInConflict() |
154 |
225 |
|| (addedLemmas > 0 && options::fullSaturateStratify())) |
155 |
|
{ |
156 |
|
// we break if we are in conflict, or if we added any lemma at this |
157 |
|
// effort level and we stratify effort levels. |
158 |
11 |
break; |
159 |
|
} |
160 |
|
} |
161 |
|
} |
162 |
118 |
if (Trace.isOn("fs-engine")) |
163 |
|
{ |
164 |
|
Trace("fs-engine") << "Added lemmas = " << addedLemmas << std::endl; |
165 |
|
double clSet2 = double(clock()) / double(CLOCKS_PER_SEC); |
166 |
|
Trace("fs-engine") << "Finished full saturation engine, time = " |
167 |
|
<< (clSet2 - clSet) << std::endl; |
168 |
|
} |
169 |
118 |
if (d_fullSaturateLimit > 0) |
170 |
|
{ |
171 |
|
d_fullSaturateLimit--; |
172 |
|
} |
173 |
|
} |
174 |
|
|
175 |
1920 |
bool InstStrategyEnum::process(Node quantifier, bool fullEffort, bool isRd) |
176 |
|
{ |
177 |
|
// ignore if constant true (rare case of non-standard quantifier whose body |
178 |
|
// is rewritten to true) |
179 |
1920 |
if (quantifier[1].isConst() && quantifier[1].getConst<bool>()) |
180 |
|
{ |
181 |
|
return false; |
182 |
|
} |
183 |
|
|
184 |
|
TermTupleEnumeratorEnv ttec; |
185 |
1920 |
ttec.d_fullEffort = fullEffort; |
186 |
3844 |
ttec.d_increaseSum = options::fullSaturateSum(); |
187 |
|
// make the enumerator, which is either relevant domain or term database |
188 |
|
// based on the flag isRd. |
189 |
|
std::unique_ptr<TermTupleEnumeratorInterface> enumerator( |
190 |
3426 |
isRd ? mkTermTupleEnumeratorRd(quantifier, &ttec, d_rd) |
191 |
2334 |
: mkTermTupleEnumerator( |
192 |
5760 |
quantifier, &ttec, d_qstate, d_treg.getTermDatabase())); |
193 |
3840 |
std::vector<Node> terms; |
194 |
3840 |
std::vector<bool> failMask; |
195 |
1920 |
Instantiate* ie = d_qim.getInstantiate(); |
196 |
8914 |
for (enumerator->init(); enumerator->hasNext();) |
197 |
|
{ |
198 |
8112 |
if (d_qstate.isInConflict()) |
199 |
|
{ |
200 |
|
// could be conflicting for an internal reason |
201 |
|
return false; |
202 |
|
} |
203 |
8112 |
enumerator->next(terms); |
204 |
|
// try instantiation |
205 |
8112 |
failMask.clear(); |
206 |
|
/* if (ie->addInstantiation(quantifier, terms)) */ |
207 |
8112 |
if (ie->addInstantiationExpFail( |
208 |
|
quantifier, terms, failMask, InferenceId::QUANTIFIERS_INST_ENUM)) |
209 |
|
{ |
210 |
1118 |
Trace("inst-alg-rd") << "Success!" << std::endl; |
211 |
1118 |
return true; |
212 |
|
} |
213 |
|
else |
214 |
|
{ |
215 |
6994 |
enumerator->failureReason(failMask); |
216 |
|
} |
217 |
|
} |
218 |
802 |
return false; |
219 |
|
// TODO : term enumerator instantiation? |
220 |
|
} |
221 |
|
|
222 |
|
} // namespace quantifiers |
223 |
|
} // namespace theory |
224 |
70814 |
} // namespace cvc5 |