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