1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Tim King, Alex Ozdemir |
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 |
|
* Arithmetic theory. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/arith/theory_arith.h" |
17 |
|
|
18 |
|
#include "options/smt_options.h" |
19 |
|
#include "proof/proof_checker.h" |
20 |
|
#include "proof/proof_rule.h" |
21 |
|
#include "smt/smt_statistics_registry.h" |
22 |
|
#include "theory/arith/arith_rewriter.h" |
23 |
|
#include "theory/arith/equality_solver.h" |
24 |
|
#include "theory/arith/infer_bounds.h" |
25 |
|
#include "theory/arith/nl/nonlinear_extension.h" |
26 |
|
#include "theory/arith/theory_arith_private.h" |
27 |
|
#include "theory/ext_theory.h" |
28 |
|
#include "theory/rewriter.h" |
29 |
|
#include "theory/theory_model.h" |
30 |
|
|
31 |
|
using namespace std; |
32 |
|
using namespace cvc5::kind; |
33 |
|
|
34 |
|
namespace cvc5 { |
35 |
|
namespace theory { |
36 |
|
namespace arith { |
37 |
|
|
38 |
9856 |
TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation) |
39 |
|
: Theory(THEORY_ARITH, env, out, valuation), |
40 |
9856 |
d_ppRewriteTimer(smtStatisticsRegistry().registerTimer( |
41 |
19712 |
"theory::arith::ppRewriteTimer")), |
42 |
|
d_astate(env, valuation), |
43 |
|
d_im(*this, d_astate, d_pnm), |
44 |
|
d_ppre(getSatContext(), d_pnm), |
45 |
|
d_bab(d_astate, d_im, d_ppre, d_pnm), |
46 |
|
d_eqSolver(nullptr), |
47 |
9856 |
d_internal(new TheoryArithPrivate(*this, env, d_bab)), |
48 |
|
d_nonlinearExtension(nullptr), |
49 |
|
d_opElim(d_pnm, getLogicInfo()), |
50 |
|
d_arithPreproc(d_astate, d_im, d_pnm, d_opElim), |
51 |
39424 |
d_rewriter(d_opElim) |
52 |
|
{ |
53 |
|
// currently a cyclic dependency to TheoryArithPrivate |
54 |
9856 |
d_astate.setParent(d_internal); |
55 |
|
// indicate we are using the theory state object and inference manager |
56 |
9856 |
d_theoryState = &d_astate; |
57 |
9856 |
d_inferManager = &d_im; |
58 |
|
|
59 |
9856 |
if (options().arith.arithEqSolver) |
60 |
|
{ |
61 |
39 |
d_eqSolver.reset(new EqualitySolver(d_astate, d_im)); |
62 |
|
} |
63 |
9856 |
} |
64 |
|
|
65 |
29568 |
TheoryArith::~TheoryArith(){ |
66 |
9856 |
delete d_internal; |
67 |
19712 |
} |
68 |
|
|
69 |
9856 |
TheoryRewriter* TheoryArith::getTheoryRewriter() { return &d_rewriter; } |
70 |
|
|
71 |
3771 |
ProofRuleChecker* TheoryArith::getProofChecker() |
72 |
|
{ |
73 |
3771 |
return d_internal->getProofChecker(); |
74 |
|
} |
75 |
|
|
76 |
9856 |
bool TheoryArith::needsEqualityEngine(EeSetupInfo& esi) |
77 |
|
{ |
78 |
|
// if the equality solver is enabled, then it is responsible for setting |
79 |
|
// up the equality engine |
80 |
9856 |
if (d_eqSolver != nullptr) |
81 |
|
{ |
82 |
39 |
return d_eqSolver->needsEqualityEngine(esi); |
83 |
|
} |
84 |
|
// otherwise, the linear arithmetic solver is responsible for setting up |
85 |
|
// the equality engine |
86 |
9817 |
return d_internal->needsEqualityEngine(esi); |
87 |
|
} |
88 |
9856 |
void TheoryArith::finishInit() |
89 |
|
{ |
90 |
19712 |
if (getLogicInfo().isTheoryEnabled(THEORY_ARITH) |
91 |
9856 |
&& getLogicInfo().areTranscendentalsUsed()) |
92 |
|
{ |
93 |
|
// witness is used to eliminate square root |
94 |
4195 |
d_valuation.setUnevaluatedKind(kind::WITNESS); |
95 |
|
// we only need to add the operators that are not syntax sugar |
96 |
4195 |
d_valuation.setUnevaluatedKind(kind::EXPONENTIAL); |
97 |
4195 |
d_valuation.setUnevaluatedKind(kind::SINE); |
98 |
4195 |
d_valuation.setUnevaluatedKind(kind::PI); |
99 |
|
} |
100 |
|
// only need to create nonlinear extension if non-linear logic |
101 |
9856 |
const LogicInfo& logicInfo = getLogicInfo(); |
102 |
9856 |
if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear()) |
103 |
|
{ |
104 |
5150 |
d_nonlinearExtension.reset(new nl::NonlinearExtension(*this, d_astate)); |
105 |
|
} |
106 |
9856 |
if (d_eqSolver != nullptr) |
107 |
|
{ |
108 |
39 |
d_eqSolver->finishInit(); |
109 |
|
} |
110 |
|
// finish initialize in the old linear solver |
111 |
9856 |
d_internal->finishInit(); |
112 |
9856 |
} |
113 |
|
|
114 |
779648 |
void TheoryArith::preRegisterTerm(TNode n) |
115 |
|
{ |
116 |
779648 |
if (d_nonlinearExtension != nullptr) |
117 |
|
{ |
118 |
378907 |
d_nonlinearExtension->preRegisterTerm(n); |
119 |
|
} |
120 |
779649 |
d_internal->preRegisterTerm(n); |
121 |
779647 |
} |
122 |
|
|
123 |
679120 |
void TheoryArith::notifySharedTerm(TNode n) { d_internal->notifySharedTerm(n); } |
124 |
|
|
125 |
777739 |
TrustNode TheoryArith::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems) |
126 |
|
{ |
127 |
1555478 |
CodeTimer timer(d_ppRewriteTimer, /* allow_reentrant = */ true); |
128 |
777739 |
Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl; |
129 |
|
|
130 |
777739 |
if (atom.getKind() == kind::EQUAL) |
131 |
|
{ |
132 |
30392 |
return d_ppre.ppRewriteEq(atom); |
133 |
|
} |
134 |
747347 |
Assert(Theory::theoryOf(atom) == THEORY_ARITH); |
135 |
|
// Eliminate operators. Notice we must do this here since other |
136 |
|
// theories may generate lemmas that involve non-standard operators. For |
137 |
|
// example, quantifier instantiation may use TO_INTEGER terms; SyGuS may |
138 |
|
// introduce non-standard arithmetic terms appearing in grammars. |
139 |
|
// call eliminate operators. In contrast to expandDefinitions, we eliminate |
140 |
|
// *all* extended arithmetic operators here, including total ones. |
141 |
747353 |
return d_arithPreproc.eliminate(atom, lems, false); |
142 |
|
} |
143 |
|
|
144 |
11661 |
Theory::PPAssertStatus TheoryArith::ppAssert( |
145 |
|
TrustNode tin, TrustSubstitutionMap& outSubstitutions) |
146 |
|
{ |
147 |
11661 |
return d_internal->ppAssert(tin, outSubstitutions); |
148 |
|
} |
149 |
|
|
150 |
105243 |
void TheoryArith::ppStaticLearn(TNode n, NodeBuilder& learned) |
151 |
|
{ |
152 |
105243 |
d_internal->ppStaticLearn(n, learned); |
153 |
105243 |
} |
154 |
|
|
155 |
1706696 |
bool TheoryArith::preCheck(Effort level) |
156 |
|
{ |
157 |
1706696 |
Trace("arith-check") << "TheoryArith::preCheck " << level << std::endl; |
158 |
1706696 |
return d_internal->preCheck(level); |
159 |
|
} |
160 |
|
|
161 |
1706696 |
void TheoryArith::postCheck(Effort level) |
162 |
|
{ |
163 |
1706696 |
Trace("arith-check") << "TheoryArith::postCheck " << level << std::endl; |
164 |
|
// check with the non-linear solver at last call |
165 |
1706696 |
if (level == Theory::EFFORT_LAST_CALL) |
166 |
|
{ |
167 |
2985 |
if (d_nonlinearExtension != nullptr) |
168 |
|
{ |
169 |
2985 |
d_nonlinearExtension->check(level); |
170 |
|
} |
171 |
2985 |
return; |
172 |
|
} |
173 |
|
// otherwise, check with the linear solver |
174 |
1703711 |
if (d_internal->postCheck(level)) |
175 |
|
{ |
176 |
|
// linear solver emitted a conflict or lemma, return |
177 |
57106 |
return; |
178 |
|
} |
179 |
|
|
180 |
1646605 |
if (Theory::fullEffort(level)) |
181 |
|
{ |
182 |
62473 |
if (d_nonlinearExtension != nullptr) |
183 |
|
{ |
184 |
33938 |
d_nonlinearExtension->check(level); |
185 |
|
} |
186 |
28535 |
else if (d_internal->foundNonlinear()) |
187 |
|
{ |
188 |
|
// set incomplete |
189 |
|
d_im.setIncomplete(IncompleteId::ARITH_NL_DISABLED); |
190 |
|
} |
191 |
|
} |
192 |
|
} |
193 |
|
|
194 |
5970676 |
bool TheoryArith::preNotifyFact( |
195 |
|
TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal) |
196 |
|
{ |
197 |
11941352 |
Trace("arith-check") << "TheoryArith::preNotifyFact: " << fact |
198 |
5970676 |
<< ", isPrereg=" << isPrereg |
199 |
5970676 |
<< ", isInternal=" << isInternal << std::endl; |
200 |
|
// We do not assert to the equality engine of arithmetic in the standard way, |
201 |
|
// hence we return "true" to indicate we are finished with this fact. |
202 |
5970676 |
bool ret = true; |
203 |
5970676 |
if (d_eqSolver != nullptr) |
204 |
|
{ |
205 |
|
// the equality solver may indicate ret = false, after which the assertion |
206 |
|
// will be asserted to the equality engine in the default way. |
207 |
2527 |
ret = d_eqSolver->preNotifyFact(atom, pol, fact, isPrereg, isInternal); |
208 |
|
} |
209 |
|
// we also always also notify the internal solver |
210 |
5970676 |
d_internal->preNotifyFact(atom, pol, fact); |
211 |
5970676 |
return ret; |
212 |
|
} |
213 |
|
|
214 |
18771 |
bool TheoryArith::needsCheckLastEffort() { |
215 |
18771 |
if (d_nonlinearExtension != nullptr) |
216 |
|
{ |
217 |
10051 |
return d_nonlinearExtension->needsCheckLastEffort(); |
218 |
|
} |
219 |
8720 |
return false; |
220 |
|
} |
221 |
|
|
222 |
28418 |
TrustNode TheoryArith::explain(TNode n) |
223 |
|
{ |
224 |
28418 |
if (d_eqSolver != nullptr) |
225 |
|
{ |
226 |
|
// if the equality solver has an explanation for it, use it |
227 |
54 |
TrustNode texp = d_eqSolver->explain(n); |
228 |
27 |
if (!texp.isNull()) |
229 |
|
{ |
230 |
|
return texp; |
231 |
|
} |
232 |
|
} |
233 |
28418 |
return d_internal->explain(n); |
234 |
|
} |
235 |
|
|
236 |
2713787 |
void TheoryArith::propagate(Effort e) { |
237 |
2713787 |
d_internal->propagate(e); |
238 |
2713787 |
} |
239 |
|
|
240 |
14537 |
bool TheoryArith::collectModelInfo(TheoryModel* m, |
241 |
|
const std::set<Node>& termSet) |
242 |
|
{ |
243 |
|
// this overrides behavior to not assert equality engine |
244 |
14537 |
return collectModelValues(m, termSet); |
245 |
|
} |
246 |
|
|
247 |
14537 |
bool TheoryArith::collectModelValues(TheoryModel* m, |
248 |
|
const std::set<Node>& termSet) |
249 |
|
{ |
250 |
|
// get the model from the linear solver |
251 |
29074 |
std::map<Node, Node> arithModel; |
252 |
14537 |
d_internal->collectModelValues(termSet, arithModel); |
253 |
|
// Double check that the model from the linear solver respects integer types, |
254 |
|
// if it does not, add a branch and bound lemma. This typically should never |
255 |
|
// be necessary, but is needed in rare cases. |
256 |
14537 |
bool addedLemma = false; |
257 |
14537 |
bool badAssignment = false; |
258 |
255247 |
for (const std::pair<const Node, Node>& p : arithModel) |
259 |
|
{ |
260 |
240710 |
if (p.first.getType().isInteger() && !p.second.getType().isInteger()) |
261 |
|
{ |
262 |
|
Assert(false) << "TheoryArithPrivate generated a bad model value for " |
263 |
|
"integer variable " |
264 |
|
<< p.first << " : " << p.second; |
265 |
|
// must branch and bound |
266 |
|
TrustNode lem = |
267 |
|
d_bab.branchIntegerVariable(p.first, p.second.getConst<Rational>()); |
268 |
|
if (d_im.trustedLemma(lem, InferenceId::ARITH_BB_LEMMA)) |
269 |
|
{ |
270 |
|
addedLemma = true; |
271 |
|
} |
272 |
|
badAssignment = true; |
273 |
|
} |
274 |
|
} |
275 |
14537 |
if (addedLemma) |
276 |
|
{ |
277 |
|
// we had to add a branch and bound lemma since the linear solver assigned |
278 |
|
// a non-integer value to an integer variable. |
279 |
|
return false; |
280 |
|
} |
281 |
|
// this would imply that linear arithmetic's model failed to satisfy a branch |
282 |
|
// and bound lemma |
283 |
14537 |
AlwaysAssert(!badAssignment) |
284 |
|
<< "Bad assignment from TheoryArithPrivate::collectModelValues, and no " |
285 |
|
"branching lemma was sent"; |
286 |
|
|
287 |
|
// if non-linear is enabled, intercept the model, which may repair its values |
288 |
14537 |
if (d_nonlinearExtension != nullptr) |
289 |
|
{ |
290 |
|
// Non-linear may repair values to satisfy non-linear constraints (see |
291 |
|
// documentation for NonlinearExtension::interceptModel). |
292 |
8911 |
d_nonlinearExtension->interceptModel(arithModel, termSet); |
293 |
|
} |
294 |
|
// We are now ready to assert the model. |
295 |
253794 |
for (const std::pair<const Node, Node>& p : arithModel) |
296 |
|
{ |
297 |
|
// maps to constant of comparable type |
298 |
239259 |
Assert(p.first.getType().isComparableTo(p.second.getType())); |
299 |
239259 |
if (m->assertEquality(p.first, p.second, true)) |
300 |
|
{ |
301 |
239257 |
continue; |
302 |
|
} |
303 |
|
// If we failed to assert an equality, it is likely due to theory |
304 |
|
// combination, namely the repaired model for non-linear changed |
305 |
|
// an equality status that was agreed upon by both (linear) arithmetic |
306 |
|
// and another theory. In this case, we must add a lemma, or otherwise |
307 |
|
// we would terminate with an invalid model. Thus, we add a splitting |
308 |
|
// lemma of the form ( x = v V x != v ) where v is the model value |
309 |
|
// assigned by the non-linear solver to x. |
310 |
2 |
if (d_nonlinearExtension != nullptr) |
311 |
|
{ |
312 |
4 |
Node eq = p.first.eqNode(p.second); |
313 |
4 |
Node lem = NodeManager::currentNM()->mkNode(kind::OR, eq, eq.negate()); |
314 |
2 |
bool added = d_im.lemma(lem, InferenceId::ARITH_SPLIT_FOR_NL_MODEL); |
315 |
2 |
AlwaysAssert(added) << "The lemma was already in cache. Probably there is something wrong with theory combination..."; |
316 |
|
} |
317 |
2 |
return false; |
318 |
|
} |
319 |
14535 |
return true; |
320 |
|
} |
321 |
|
|
322 |
1722 |
void TheoryArith::notifyRestart(){ |
323 |
1722 |
d_internal->notifyRestart(); |
324 |
1722 |
} |
325 |
|
|
326 |
15207 |
void TheoryArith::presolve(){ |
327 |
15207 |
d_internal->presolve(); |
328 |
15207 |
if (d_nonlinearExtension != nullptr) |
329 |
|
{ |
330 |
6408 |
d_nonlinearExtension->presolve(); |
331 |
|
} |
332 |
15207 |
} |
333 |
|
|
334 |
942837 |
EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) { |
335 |
942837 |
return d_internal->getEqualityStatus(a,b); |
336 |
|
} |
337 |
|
|
338 |
2678 |
Node TheoryArith::getModelValue(TNode var) { |
339 |
2678 |
return d_internal->getModelValue( var ); |
340 |
|
} |
341 |
|
|
342 |
6591 |
std::pair<bool, Node> TheoryArith::entailmentCheck(TNode lit) |
343 |
|
{ |
344 |
13182 |
ArithEntailmentCheckParameters def; |
345 |
6591 |
def.addLookupRowSumAlgorithms(); |
346 |
13182 |
ArithEntailmentCheckSideEffects ase; |
347 |
6591 |
std::pair<bool, Node> res = d_internal->entailmentCheck(lit, def, ase); |
348 |
13182 |
return res; |
349 |
|
} |
350 |
|
eq::ProofEqEngine* TheoryArith::getProofEqEngine() |
351 |
|
{ |
352 |
|
return d_im.getProofEqEngine(); |
353 |
|
} |
354 |
|
|
355 |
|
} // namespace arith |
356 |
|
} // namespace theory |
357 |
29358 |
} // namespace cvc5 |