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