projects / cvc5.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
Expand arith's farkas lemma rule as a macro (#6577)
[cvc5.git] / src / theory / arith / theory_arith_private.cpp
1 /******************************************************************************
2 * Top contributors (to current version):
3 * Tim King, Alex Ozdemir, Andrew Reynolds
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 * [[ Add one-line brief description here ]]
14 *
15 * [[ Add lengthier description here ]]
16 * \todo document this file
17 */
18
19 #include "theory/arith/theory_arith_private.h"
20
21 #include <map>
22 #include <queue>
23 #include <vector>
24
25 #include "base/output.h"
26 #include "context/cdhashset.h"
27 #include "context/cdinsert_hashmap.h"
28 #include "context/cdlist.h"
29 #include "context/cdqueue.h"
30 #include "context/context.h"
31 #include "expr/kind.h"
32 #include "expr/metakind.h"
33 #include "expr/node.h"
34 #include "expr/node_algorithm.h"
35 #include "expr/node_builder.h"
36 #include "expr/proof_generator.h"
37 #include "expr/proof_node_manager.h"
38 #include "expr/proof_rule.h"
39 #include "expr/skolem_manager.h"
40 #include "options/arith_options.h"
41 #include "options/smt_options.h" // for incrementalSolving()
42 #include "preprocessing/util/ite_utilities.h"
43 #include "smt/logic_exception.h"
44 #include "smt/smt_statistics_registry.h"
45 #include "smt_util/boolean_simplification.h"
46 #include "theory/arith/approx_simplex.h"
47 #include "theory/arith/arith_ite_utils.h"
48 #include "theory/arith/arith_rewriter.h"
49 #include "theory/arith/arith_static_learner.h"
50 #include "theory/arith/arith_utilities.h"
51 #include "theory/arith/arithvar.h"
52 #include "theory/arith/congruence_manager.h"
53 #include "theory/arith/constraint.h"
54 #include "theory/arith/cut_log.h"
55 #include "theory/arith/delta_rational.h"
56 #include "theory/arith/dio_solver.h"
57 #include "theory/arith/linear_equality.h"
58 #include "theory/arith/matrix.h"
59 #include "theory/arith/nl/nonlinear_extension.h"
60 #include "theory/arith/normal_form.h"
61 #include "theory/arith/partial_model.h"
62 #include "theory/arith/simplex.h"
63 #include "theory/arith/theory_arith.h"
64 #include "theory/ext_theory.h"
65 #include "theory/quantifiers/fmf/bounded_integers.h"
66 #include "theory/rewriter.h"
67 #include "theory/theory_model.h"
68 #include "theory/trust_substitutions.h"
69 #include "theory/valuation.h"
70 #include "util/dense_map.h"
71 #include "util/integer.h"
72 #include "util/random.h"
73 #include "util/rational.h"
74 #include "util/result.h"
75 #include "util/statistics_stats.h"
76
77 using namespace std;
78 using namespace cvc5::kind;
79
80 namespace cvc5 {
81 namespace theory {
82 namespace arith {
83
84 static Node toSumNode(const ArithVariables& vars, const DenseMap<Rational>& sum);
85 static bool complexityBelow(const DenseMap<Rational>& row, uint32_t cap);
86
87 TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
88 context::Context* c,
89 context::UserContext* u,
90 OutputChannel& out,
91 Valuation valuation,
92 const LogicInfo& logicInfo,
93 ProofNodeManager* pnm)
94 : d_containing(containing),
95 d_foundNl(false),
96 d_rowTracking(),
97 d_pnm(pnm),
98 d_checker(),
99 d_pfGen(new EagerProofGenerator(d_pnm, u)),
100 d_constraintDatabase(c,
101 u,
102 d_partialModel,
103 d_congruenceManager,
104 RaiseConflict(*this),
105 d_pfGen.get(),
106 d_pnm),
107 d_qflraStatus(Result::SAT_UNKNOWN),
108 d_unknownsInARow(0),
109 d_hasDoneWorkSinceCut(false),
110 d_learner(u),
111 d_assertionsThatDoNotMatchTheirLiterals(c),
112 d_nextIntegerCheckVar(0),
113 d_constantIntegerVariables(c),
114 d_diseqQueue(c, false),
115 d_currentPropagationList(),
116 d_learnedBounds(c),
117 d_preregisteredNodes(u),
118 d_partialModel(c, DeltaComputeCallback(*this)),
119 d_errorSet(
120 d_partialModel, TableauSizes(&d_tableau), BoundCountingLookup(*this)),
121 d_tableau(),
122 d_linEq(d_partialModel,
123 d_tableau,
124 d_rowTracking,
125 BasicVarModelUpdateCallBack(*this)),
126 d_diosolver(c),
127 d_restartsCounter(0),
128 d_tableauSizeHasBeenModified(false),
129 d_tableauResetDensity(1.6),
130 d_tableauResetPeriod(10),
131 d_conflicts(c),
132 d_blackBoxConflict(c, Node::null()),
133 d_blackBoxConflictPf(c, std::shared_ptr<ProofNode>(nullptr)),
134 d_congruenceManager(c,
135 u,
136 d_constraintDatabase,
137 SetupLiteralCallBack(*this),
138 d_partialModel,
139 RaiseEqualityEngineConflict(*this),
140 d_pnm),
141 d_cmEnabled(c, true),
142
143 d_dualSimplex(
144 d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
145 d_fcSimplex(
146 d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
147 d_soiSimplex(
148 d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
149 d_attemptSolSimplex(
150 d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
151 d_pass1SDP(NULL),
152 d_otherSDP(NULL),
153 d_lastContextIntegerAttempted(c, -1),
154
155 d_DELTA_ZERO(0),
156 d_approxCuts(c),
157 d_fullCheckCounter(0),
158 d_cutCount(c, 0),
159 d_cutInContext(c),
160 d_likelyIntegerInfeasible(c, false),
161 d_guessedCoeffSet(c, false),
162 d_guessedCoeffs(),
163 d_treeLog(NULL),
164 d_replayVariables(),
165 d_replayConstraints(),
166 d_lhsTmp(),
167 d_approxStats(NULL),
168 d_attemptSolveIntTurnedOff(u, 0),
169 d_dioSolveResources(0),
170 d_solveIntMaybeHelp(0u),
171 d_solveIntAttempts(0u),
172 d_newFacts(false),
173 d_previousStatus(Result::SAT_UNKNOWN),
174 d_statistics("theory::arith::")
175 {
176 }
177
178 TheoryArithPrivate::~TheoryArithPrivate(){
179 if(d_treeLog != NULL){ delete d_treeLog; }
180 if(d_approxStats != NULL) { delete d_approxStats; }
181 }
182
183 bool TheoryArithPrivate::needsEqualityEngine(EeSetupInfo& esi)
184 {
185 return d_congruenceManager.needsEqualityEngine(esi);
186 }
187 void TheoryArithPrivate::finishInit()
188 {
189 eq::EqualityEngine* ee = d_containing.getEqualityEngine();
190 eq::ProofEqEngine* pfee = d_containing.getProofEqEngine();
191 Assert(ee != nullptr);
192 d_congruenceManager.finishInit(ee, pfee);
193 }
194
195 static bool contains(const ConstraintCPVec& v, ConstraintP con){
196 for(unsigned i = 0, N = v.size(); i < N; ++i){
197 if(v[i] == con){
198 return true;
199 }
200 }
201 return false;
202 }
203 static void drop( ConstraintCPVec& v, ConstraintP con){
204 size_t readPos, writePos, N;
205 for(readPos = 0, writePos = 0, N = v.size(); readPos < N; ++readPos){
206 ConstraintCP curr = v[readPos];
207 if(curr != con){
208 v[writePos] = curr;
209 writePos++;
210 }
211 }
212 v.resize(writePos);
213 }
214
215
216 static void resolve(ConstraintCPVec& buf, ConstraintP c, const ConstraintCPVec& pos, const ConstraintCPVec& neg){
217 unsigned posPos CVC5_UNUSED = pos.size();
218 for(unsigned i = 0, N = pos.size(); i < N; ++i){
219 if(pos[i] == c){
220 posPos = i;
221 }else{
222 buf.push_back(pos[i]);
223 }
224 }
225 Assert(posPos < pos.size());
226 ConstraintP negc = c->getNegation();
227 unsigned negPos CVC5_UNUSED = neg.size();
228 for(unsigned i = 0, N = neg.size(); i < N; ++i){
229 if(neg[i] == negc){
230 negPos = i;
231 }else{
232 buf.push_back(neg[i]);
233 }
234 }
235 Assert(negPos < neg.size());
236
237 // Assert(dnconf.getKind() == kind::AND);
238 // Assert(upconf.getKind() == kind::AND);
239 // Assert(dnpos < dnconf.getNumChildren());
240 // Assert(uppos < upconf.getNumChildren());
241 // Assert(equalUpToNegation(dnconf[dnpos], upconf[uppos]));
242
243 // NodeBuilder nb(kind::AND);
244 // dropPosition(nb, dnconf, dnpos);
245 // dropPosition(nb, upconf, uppos);
246 // return safeConstructNary(nb);
247 }
248
249 TheoryArithPrivate::ModelException::ModelException(TNode n, const char* msg)
250 {
251 stringstream ss;
252 ss << "Cannot construct a model for " << n << " as " << endl << msg;
253 setMessage(ss.str());
254 }
255 TheoryArithPrivate::ModelException::~ModelException() {}
256
257 TheoryArithPrivate::Statistics::Statistics(const std::string& name)
258 : d_statAssertUpperConflicts(
259 smtStatisticsRegistry().registerInt(name + "AssertUpperConflicts")),
260 d_statAssertLowerConflicts(
261 smtStatisticsRegistry().registerInt(name + "AssertLowerConflicts")),
262 d_statUserVariables(
263 smtStatisticsRegistry().registerInt(name + "UserVariables")),
264 d_statAuxiliaryVariables(
265 smtStatisticsRegistry().registerInt(name + "AuxiliaryVariables")),
266 d_statDisequalitySplits(
267 smtStatisticsRegistry().registerInt(name + "DisequalitySplits")),
268 d_statDisequalityConflicts(
269 smtStatisticsRegistry().registerInt(name + "DisequalityConflicts")),
270 d_simplifyTimer(
271 smtStatisticsRegistry().registerTimer(name + "simplifyTimer")),
272 d_staticLearningTimer(
273 smtStatisticsRegistry().registerTimer(name + "staticLearningTimer")),
274 d_presolveTime(
275 smtStatisticsRegistry().registerTimer(name + "presolveTime")),
276 d_newPropTime(
277 smtStatisticsRegistry().registerTimer(name + "newPropTimer")),
278 d_externalBranchAndBounds(smtStatisticsRegistry().registerInt(
279 name + "externalBranchAndBounds")),
280 d_initialTableauSize(
281 smtStatisticsRegistry().registerInt(name + "initialTableauSize")),
282 d_currSetToSmaller(
283 smtStatisticsRegistry().registerInt(name + "currSetToSmaller")),
284 d_smallerSetToCurr(
285 smtStatisticsRegistry().registerInt(name + "smallerSetToCurr")),
286 d_restartTimer(
287 smtStatisticsRegistry().registerTimer(name + "restartTimer")),
288 d_boundComputationTime(
289 smtStatisticsRegistry().registerTimer(name + "bound::time")),
290 d_boundComputations(smtStatisticsRegistry().registerInt(
291 name + "bound::boundComputations")),
292 d_boundPropagations(smtStatisticsRegistry().registerInt(
293 name + "bound::boundPropagations")),
294 d_unknownChecks(
295 smtStatisticsRegistry().registerInt(name + "status::unknowns")),
296 d_maxUnknownsInARow(smtStatisticsRegistry().registerInt(
297 name + "status::maxUnknownsInARow")),
298 d_avgUnknownsInARow(smtStatisticsRegistry().registerAverage(
299 name + "status::avgUnknownsInARow")),
300 d_revertsOnConflicts(smtStatisticsRegistry().registerInt(
301 name + "status::revertsOnConflicts")),
302 d_commitsOnConflicts(smtStatisticsRegistry().registerInt(
303 name + "status::commitsOnConflicts")),
304 d_nontrivialSatChecks(smtStatisticsRegistry().registerInt(
305 name + "status::nontrivialSatChecks")),
306 d_replayLogRecCount(
307 smtStatisticsRegistry().registerInt(name + "z::approx::replay::rec")),
308 d_replayLogRecConflictEscalation(smtStatisticsRegistry().registerInt(
309 name + "z::approx::replay::rec::escalation")),
310 d_replayLogRecEarlyExit(smtStatisticsRegistry().registerInt(
311 name + "z::approx::replay::rec::earlyexit")),
312 d_replayBranchCloseFailures(smtStatisticsRegistry().registerInt(
313 name + "z::approx::replay::rec::branch::closefailures")),
314 d_replayLeafCloseFailures(smtStatisticsRegistry().registerInt(
315 name + "z::approx::replay::rec::leaf::closefailures")),
316 d_replayBranchSkips(smtStatisticsRegistry().registerInt(
317 name + "z::approx::replay::rec::branch::skips")),
318 d_mirCutsAttempted(smtStatisticsRegistry().registerInt(
319 name + "z::approx::cuts::mir::attempted")),
320 d_gmiCutsAttempted(smtStatisticsRegistry().registerInt(
321 name + "z::approx::cuts::gmi::attempted")),
322 d_branchCutsAttempted(smtStatisticsRegistry().registerInt(
323 name + "z::approx::cuts::branch::attempted")),
324 d_cutsReconstructed(smtStatisticsRegistry().registerInt(
325 name + "z::approx::cuts::reconstructed")),
326 d_cutsReconstructionFailed(smtStatisticsRegistry().registerInt(
327 name + "z::approx::cuts::reconstructed::failed")),
328 d_cutsProven(smtStatisticsRegistry().registerInt(
329 name + "z::approx::cuts::proofs")),
330 d_cutsProofFailed(smtStatisticsRegistry().registerInt(
331 name + "z::approx::cuts::proofs::failed")),
332 d_mipReplayLemmaCalls(smtStatisticsRegistry().registerInt(
333 name + "z::approx::external::calls")),
334 d_mipExternalCuts(smtStatisticsRegistry().registerInt(
335 name + "z::approx::external::cuts")),
336 d_mipExternalBranch(smtStatisticsRegistry().registerInt(
337 name + "z::approx::external::branches")),
338 d_inSolveInteger(smtStatisticsRegistry().registerInt(
339 name + "z::approx::inSolverInteger")),
340 d_branchesExhausted(smtStatisticsRegistry().registerInt(
341 name + "z::approx::exhausted::branches")),
342 d_execExhausted(smtStatisticsRegistry().registerInt(
343 name + "z::approx::exhausted::exec")),
344 d_pivotsExhausted(smtStatisticsRegistry().registerInt(
345 name + "z::approx::exhausted::pivots")),
346 d_panicBranches(
347 smtStatisticsRegistry().registerInt(name + "z::arith::paniclemmas")),
348 d_relaxCalls(
349 smtStatisticsRegistry().registerInt(name + "z::arith::relax::calls")),
350 d_relaxLinFeas(smtStatisticsRegistry().registerInt(
351 name + "z::arith::relax::feasible::res")),
352 d_relaxLinFeasFailures(smtStatisticsRegistry().registerInt(
353 name + "z::arith::relax::feasible::failures")),
354 d_relaxLinInfeas(smtStatisticsRegistry().registerInt(
355 name + "z::arith::relax::infeasible")),
356 d_relaxLinInfeasFailures(smtStatisticsRegistry().registerInt(
357 name + "z::arith::relax::infeasible::failures")),
358 d_relaxLinExhausted(smtStatisticsRegistry().registerInt(
359 name + "z::arith::relax::exhausted")),
360 d_relaxOthers(
361 smtStatisticsRegistry().registerInt(name + "z::arith::relax::other")),
362 d_applyRowsDeleted(smtStatisticsRegistry().registerInt(
363 name + "z::arith::cuts::applyRowsDeleted")),
364 d_replaySimplexTimer(smtStatisticsRegistry().registerTimer(
365 name + "z::approx::replay::simplex::timer")),
366 d_replayLogTimer(smtStatisticsRegistry().registerTimer(
367 name + "z::approx::replay::log::timer")),
368 d_solveIntTimer(
369 smtStatisticsRegistry().registerTimer(name + "z::solveInt::timer")),
370 d_solveRealRelaxTimer(smtStatisticsRegistry().registerTimer(
371 name + "z::solveRealRelax::timer")),
372 d_solveIntCalls(
373 smtStatisticsRegistry().registerInt(name + "z::solveInt::calls")),
374 d_solveStandardEffort(smtStatisticsRegistry().registerInt(
375 name + "z::solveInt::calls::standardEffort")),
376 d_approxDisabled(
377 smtStatisticsRegistry().registerInt(name + "z::approxDisabled")),
378 d_replayAttemptFailed(
379 smtStatisticsRegistry().registerInt(name + "z::replayAttemptFailed")),
380 d_cutsRejectedDuringReplay(smtStatisticsRegistry().registerInt(
381 name + "z::approx::replay::cuts::rejected")),
382 d_cutsRejectedDuringLemmas(smtStatisticsRegistry().registerInt(
383 name + "z::approx::external::cuts::rejected")),
384 d_satPivots(smtStatisticsRegistry().registerHistogram<uint32_t>(
385 name + "pivots::sat")),
386 d_unsatPivots(smtStatisticsRegistry().registerHistogram<uint32_t>(
387 name + "pivots::unsat")),
388 d_unknownPivots(smtStatisticsRegistry().registerHistogram<uint32_t>(
389 name + "pivots::unknown")),
390 d_solveIntModelsAttempts(smtStatisticsRegistry().registerInt(
391 name + "z::solveInt::models::attempts")),
392 d_solveIntModelsSuccessful(smtStatisticsRegistry().registerInt(
393 name + "zzz::solveInt::models::successful")),
394 d_mipTimer(smtStatisticsRegistry().registerTimer(
395 name + "z::approx::mip::timer")),
396 d_lpTimer(
397 smtStatisticsRegistry().registerTimer(name + "z::approx::lp::timer")),
398 d_mipProofsAttempted(smtStatisticsRegistry().registerInt(
399 name + "z::mip::proofs::attempted")),
400 d_mipProofsSuccessful(smtStatisticsRegistry().registerInt(
401 name + "z::mip::proofs::successful")),
402 d_numBranchesFailed(smtStatisticsRegistry().registerInt(
403 name + "z::mip::branch::proof::failed"))
404 {
405 }
406
407 bool complexityBelow(const DenseMap<Rational>& row, uint32_t cap){
408 DenseMap<Rational>::const_iterator riter, rend;
409 for(riter=row.begin(), rend=row.end(); riter != rend; ++riter){
410 ArithVar v = *riter;
411 const Rational& q = row[v];
412 if(q.complexity() > cap){
413 return false;
414 }
415 }
416 return true;
417 }
418
419 bool TheoryArithPrivate::isProofEnabled() const
420 {
421 return d_pnm != nullptr;
422 }
423
424 void TheoryArithPrivate::raiseConflict(ConstraintCP a, InferenceId id){
425 Assert(a->inConflict());
426 d_conflicts.push_back(std::make_pair(a, id));
427 }
428
429 void TheoryArithPrivate::raiseBlackBoxConflict(Node bb,
430 std::shared_ptr<ProofNode> pf)
431 {
432 Debug("arith::bb") << "raiseBlackBoxConflict: " << bb << std::endl;
433 if (d_blackBoxConflict.get().isNull())
434 {
435 if (isProofEnabled())
436 {
437 Debug("arith::bb") << " with proof " << pf << std::endl;
438 d_blackBoxConflictPf.set(pf);
439 }
440 d_blackBoxConflict = bb;
441 }
442 }
443
444 bool TheoryArithPrivate::anyConflict() const
445 {
446 return !conflictQueueEmpty() || !d_blackBoxConflict.get().isNull();
447 }
448
449 void TheoryArithPrivate::revertOutOfConflict(){
450 d_partialModel.revertAssignmentChanges();
451 clearUpdates();
452 d_currentPropagationList.clear();
453 }
454
455 void TheoryArithPrivate::clearUpdates(){
456 d_updatedBounds.purge();
457 }
458
459 // void TheoryArithPrivate::raiseConflict(ConstraintCP a, ConstraintCP b){
460 // ConstraintCPVec v;
461 // v.push_back(a);
462 // v.push_back(b);
463 // d_conflicts.push_back(v);
464 // }
465
466 // void TheoryArithPrivate::raiseConflict(ConstraintCP a, ConstraintCP b, ConstraintCP c){
467 // ConstraintCPVec v;
468 // v.push_back(a);
469 // v.push_back(b);
470 // v.push_back(c);
471 // d_conflicts.push_back(v);
472 // }
473
474 void TheoryArithPrivate::zeroDifferenceDetected(ArithVar x){
475 if(d_cmEnabled){
476 Assert(d_congruenceManager.isWatchedVariable(x));
477 Assert(d_partialModel.upperBoundIsZero(x));
478 Assert(d_partialModel.lowerBoundIsZero(x));
479
480 ConstraintP lb = d_partialModel.getLowerBoundConstraint(x);
481 ConstraintP ub = d_partialModel.getUpperBoundConstraint(x);
482
483 if(lb->isEquality()){
484 d_congruenceManager.watchedVariableIsZero(lb);
485 }else if(ub->isEquality()){
486 d_congruenceManager.watchedVariableIsZero(ub);
487 }else{
488 d_congruenceManager.watchedVariableIsZero(lb, ub);
489 }
490 }
491 }
492
493 bool TheoryArithPrivate::getSolveIntegerResource(){
494 if(d_attemptSolveIntTurnedOff > 0){
495 d_attemptSolveIntTurnedOff = d_attemptSolveIntTurnedOff - 1;
496 return false;
497 }else{
498 return true;
499 }
500 }
501
502 bool TheoryArithPrivate::getDioCuttingResource(){
503 if(d_dioSolveResources > 0){
504 d_dioSolveResources--;
505 if(d_dioSolveResources == 0){
506 d_dioSolveResources = -options::rrTurns();
507 }
508 return true;
509 }else{
510 d_dioSolveResources++;
511 if(d_dioSolveResources >= 0){
512 d_dioSolveResources = options::dioSolverTurns();
513 }
514 return false;
515 }
516 }
517
518 /* procedure AssertLower( x_i >= c_i ) */
519 bool TheoryArithPrivate::AssertLower(ConstraintP constraint){
520 Assert(constraint != NullConstraint);
521 Assert(constraint->isLowerBound());
522 Assert(constraint->isTrue());
523 Assert(!constraint->negationHasProof());
524
525 ArithVar x_i = constraint->getVariable();
526 const DeltaRational& c_i = constraint->getValue();
527
528 Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl;
529
530 Assert(!isInteger(x_i) || c_i.isIntegral());
531
532 //TODO Relax to less than?
533 if(d_partialModel.lessThanLowerBound(x_i, c_i)){
534 return false; //sat
535 }
536
537 int cmpToUB = d_partialModel.cmpToUpperBound(x_i, c_i);
538 if(cmpToUB > 0){ // c_i < \lowerbound(x_i)
539 ConstraintP ubc = d_partialModel.getUpperBoundConstraint(x_i);
540 ConstraintP negation = constraint->getNegation();
541 negation->impliedByUnate(ubc, true);
542
543 raiseConflict(constraint, InferenceId::ARITH_CONF_LOWER);
544
545 ++(d_statistics.d_statAssertLowerConflicts);
546 return true;
547 }else if(cmpToUB == 0){
548 if(isInteger(x_i)){
549 d_constantIntegerVariables.push_back(x_i);
550 Debug("dio::push") << "dio::push " << x_i << endl;
551 }
552 ConstraintP ub = d_partialModel.getUpperBoundConstraint(x_i);
553
554 if(d_cmEnabled){
555 if(!d_congruenceManager.isWatchedVariable(x_i) || c_i.sgn() != 0){
556 // if it is not a watched variable report it
557 // if it is is a watched variable and c_i == 0,
558 // let zeroDifferenceDetected(x_i) catch this
559 d_congruenceManager.equalsConstant(constraint, ub);
560 }
561 }
562
563 const ValueCollection& vc = constraint->getValueCollection();
564 if(vc.hasEquality()){
565 Assert(vc.hasDisequality());
566 ConstraintP eq = vc.getEquality();
567 ConstraintP diseq = vc.getDisequality();
568 // x <= b, x >= b |= x = b
569 // (x > b or x < b or x = b)
570 Debug("arith::eq") << "lb == ub, propagate eq" << eq << endl;
571 bool triConflict = diseq->isTrue();
572
573 if(!eq->isTrue()){
574 eq->impliedByTrichotomy(constraint, ub, triConflict);
575 eq->tryToPropagate();
576 }
577 if(triConflict){
578 ++(d_statistics.d_statDisequalityConflicts);
579 raiseConflict(eq, InferenceId::ARITH_CONF_TRICHOTOMY);
580 return true;
581 }
582 }
583 }else{
584 // l <= x <= u and l < u
585 Assert(cmpToUB < 0);
586 const ValueCollection& vc = constraint->getValueCollection();
587
588 if(vc.hasDisequality()){
589 const ConstraintP diseq = vc.getDisequality();
590 if(diseq->isTrue()){
591 const ConstraintP ub = d_constraintDatabase.ensureConstraint(const_cast<ValueCollection&>(vc), UpperBound);
592 ConstraintP negUb = ub->getNegation();
593
594 // l <= x, l != x |= l < x
595 // |= not (l >= x)
596 bool ubInConflict = ub->hasProof();
597 bool learnNegUb = !(negUb->hasProof());
598 if(learnNegUb){
599 negUb->impliedByTrichotomy(constraint, diseq, ubInConflict);
600 negUb->tryToPropagate();
601 }
602 if(ubInConflict){
603 raiseConflict(ub, InferenceId::ARITH_CONF_TRICHOTOMY);
604 return true;
605 }else if(learnNegUb){
606 d_learnedBounds.push_back(negUb);
607 }
608 }
609 }
610 }
611
612 d_currentPropagationList.push_back(constraint);
613 d_currentPropagationList.push_back(d_partialModel.getLowerBoundConstraint(x_i));
614
615 d_partialModel.setLowerBoundConstraint(constraint);
616
617 if(d_cmEnabled){
618 if(d_congruenceManager.isWatchedVariable(x_i)){
619 int sgn = c_i.sgn();
620 if(sgn > 0){
621 d_congruenceManager.watchedVariableCannotBeZero(constraint);
622 }else if(sgn == 0 && d_partialModel.upperBoundIsZero(x_i)){
623 zeroDifferenceDetected(x_i);
624 }
625 }
626 }
627
628 d_updatedBounds.softAdd(x_i);
629
630 if(Debug.isOn("model")) {
631 Debug("model") << "before" << endl;
632 d_partialModel.printModel(x_i);
633 d_tableau.debugPrintIsBasic(x_i);
634 }
635
636 if(!d_tableau.isBasic(x_i)){
637 if(d_partialModel.getAssignment(x_i) < c_i){
638 d_linEq.update(x_i, c_i);
639 }
640 }else{
641 d_errorSet.signalVariable(x_i);
642 }
643
644 if(Debug.isOn("model")) {
645 Debug("model") << "after" << endl;
646 d_partialModel.printModel(x_i);
647 d_tableau.debugPrintIsBasic(x_i);
648 }
649
650 return false; //sat
651 }
652
653 /* procedure AssertUpper( x_i <= c_i) */
654 bool TheoryArithPrivate::AssertUpper(ConstraintP constraint){
655 Assert(constraint != NullConstraint);
656 Assert(constraint->isUpperBound());
657 Assert(constraint->isTrue());
658 Assert(!constraint->negationHasProof());
659
660 ArithVar x_i = constraint->getVariable();
661 const DeltaRational& c_i = constraint->getValue();
662
663 Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
664
665
666 //Too strong because of rounding with integers
667 //Assert(!constraint->hasLiteral() || original == constraint->getLiteral());
668 Assert(!isInteger(x_i) || c_i.isIntegral());
669
670 Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
671
672 if(d_partialModel.greaterThanUpperBound(x_i, c_i) ){ // \upperbound(x_i) <= c_i
673 return false; //sat
674 }
675
676 // cmpToLb = \lowerbound(x_i).cmp(c_i)
677 int cmpToLB = d_partialModel.cmpToLowerBound(x_i, c_i);
678 if( cmpToLB < 0 ){ // \upperbound(x_i) < \lowerbound(x_i)
679 // l_i <= x_i and c_i < l_i |= c_i < x_i
680 // or ... |= not (x_i <= c_i)
681 ConstraintP lbc = d_partialModel.getLowerBoundConstraint(x_i);
682 ConstraintP negConstraint = constraint->getNegation();
683 negConstraint->impliedByUnate(lbc, true);
684 raiseConflict(constraint, InferenceId::ARITH_CONF_UPPER);
685 ++(d_statistics.d_statAssertUpperConflicts);
686 return true;
687 }else if(cmpToLB == 0){ // \lowerBound(x_i) == \upperbound(x_i)
688 if(isInteger(x_i)){
689 d_constantIntegerVariables.push_back(x_i);
690 Debug("dio::push") << "dio::push " << x_i << endl;
691 }
692
693 const ValueCollection& vc = constraint->getValueCollection();
694 ConstraintP lb = d_partialModel.getLowerBoundConstraint(x_i);
695 if(d_cmEnabled){
696 if(!d_congruenceManager.isWatchedVariable(x_i) || c_i.sgn() != 0){
697 // if it is not a watched variable report it
698 // if it is is a watched variable and c_i == 0,
699 // let zeroDifferenceDetected(x_i) catch this
700 d_congruenceManager.equalsConstant(lb, constraint);
701 }
702 }
703
704 if(vc.hasDisequality()){
705 Assert(vc.hasDisequality());
706 ConstraintP eq = vc.getEquality();
707 ConstraintP diseq = vc.getDisequality();
708 // x <= b, x >= b |= x = b
709 // (x > b or x < b or x = b)
710 Debug("arith::eq") << "lb == ub, propagate eq" << eq << endl;
711 bool triConflict = diseq->isTrue();
712 if(!eq->isTrue()){
713 eq->impliedByTrichotomy(constraint, lb, triConflict);
714 eq->tryToPropagate();
715 }
716 if(triConflict){
717 ++(d_statistics.d_statDisequalityConflicts);
718 raiseConflict(eq, InferenceId::ARITH_CONF_TRICHOTOMY);
719 return true;
720 }
721 }
722 }else if(cmpToLB > 0){
723 // l <= x <= u and l < u
724 Assert(cmpToLB > 0);
725 const ValueCollection& vc = constraint->getValueCollection();
726
727 if(vc.hasDisequality()){
728 const ConstraintP diseq = vc.getDisequality();
729 if(diseq->isTrue()){
730 const ConstraintP lb = d_constraintDatabase.ensureConstraint(const_cast<ValueCollection&>(vc), LowerBound);
731 ConstraintP negLb = lb->getNegation();
732
733 // x <= u, u != x |= u < x
734 // |= not (u >= x)
735 bool lbInConflict = lb->hasProof();
736 bool learnNegLb = !(negLb->hasProof());
737 if(learnNegLb){
738 negLb->impliedByTrichotomy(constraint, diseq, lbInConflict);
739 negLb->tryToPropagate();
740 }
741 if(lbInConflict){
742 raiseConflict(lb, InferenceId::ARITH_CONF_TRICHOTOMY);
743 return true;
744 }else if(learnNegLb){
745 d_learnedBounds.push_back(negLb);
746 }
747 }
748 }
749 }
750
751 d_currentPropagationList.push_back(constraint);
752 d_currentPropagationList.push_back(d_partialModel.getUpperBoundConstraint(x_i));
753 //It is fine if this is NullConstraint
754
755 d_partialModel.setUpperBoundConstraint(constraint);
756
757 if(d_cmEnabled){
758 if(d_congruenceManager.isWatchedVariable(x_i)){
759 int sgn = c_i.sgn();
760 if(sgn < 0){
761 d_congruenceManager.watchedVariableCannotBeZero(constraint);
762 }else if(sgn == 0 && d_partialModel.lowerBoundIsZero(x_i)){
763 zeroDifferenceDetected(x_i);
764 }
765 }
766 }
767
768 d_updatedBounds.softAdd(x_i);
769
770 if(Debug.isOn("model")) {
771 Debug("model") << "before" << endl;
772 d_partialModel.printModel(x_i);
773 d_tableau.debugPrintIsBasic(x_i);
774 }
775
776 if(!d_tableau.isBasic(x_i)){
777 if(d_partialModel.getAssignment(x_i) > c_i){
778 d_linEq.update(x_i, c_i);
779 }
780 }else{
781 d_errorSet.signalVariable(x_i);
782 }
783
784 if(Debug.isOn("model")) {
785 Debug("model") << "after" << endl;
786 d_partialModel.printModel(x_i);
787 d_tableau.debugPrintIsBasic(x_i);
788 }
789
790 return false; //sat
791 }
792
793
794 /* procedure AssertEquality( x_i == c_i ) */
795 bool TheoryArithPrivate::AssertEquality(ConstraintP constraint){
796 Assert(constraint != NullConstraint);
797 Assert(constraint->isEquality());
798 Assert(constraint->isTrue());
799 Assert(!constraint->negationHasProof());
800
801 ArithVar x_i = constraint->getVariable();
802 const DeltaRational& c_i = constraint->getValue();
803
804 Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl;
805
806 //Should be fine in integers
807 Assert(!isInteger(x_i) || c_i.isIntegral());
808
809 int cmpToLB = d_partialModel.cmpToLowerBound(x_i, c_i);
810 int cmpToUB = d_partialModel.cmpToUpperBound(x_i, c_i);
811
812 // u_i <= c_i <= l_i
813 // This can happen if both c_i <= x_i and x_i <= c_i are in the system.
814 if(cmpToUB >= 0 && cmpToLB <= 0){
815 return false; //sat
816 }
817
818 if(cmpToUB > 0 || cmpToLB < 0){
819 ConstraintP cb = (cmpToUB > 0) ? d_partialModel.getUpperBoundConstraint(x_i) :
820 d_partialModel.getLowerBoundConstraint(x_i);
821 ConstraintP diseq = constraint->getNegation();
822 Assert(!diseq->isTrue());
823 diseq->impliedByUnate(cb, true);
824 raiseConflict(constraint, InferenceId::ARITH_CONF_EQ);
825 return true;
826 }
827
828 Assert(cmpToUB <= 0);
829 Assert(cmpToLB >= 0);
830 Assert(cmpToUB < 0 || cmpToLB > 0);
831
832 if(isInteger(x_i)){
833 d_constantIntegerVariables.push_back(x_i);
834 Debug("dio::push") << "dio::push " << x_i << endl;
835 }
836
837 // Don't bother to check whether x_i != c_i is in d_diseq
838 // The a and (not a) should never be on the fact queue
839 d_currentPropagationList.push_back(constraint);
840 d_currentPropagationList.push_back(d_partialModel.getLowerBoundConstraint(x_i));
841 d_currentPropagationList.push_back(d_partialModel.getUpperBoundConstraint(x_i));
842
843 d_partialModel.setUpperBoundConstraint(constraint);
844 d_partialModel.setLowerBoundConstraint(constraint);
845
846 if(d_cmEnabled){
847 if(d_congruenceManager.isWatchedVariable(x_i)){
848 int sgn = c_i.sgn();
849 if(sgn == 0){
850 zeroDifferenceDetected(x_i);
851 }else{
852 d_congruenceManager.watchedVariableCannotBeZero(constraint);
853 d_congruenceManager.equalsConstant(constraint);
854 }
855 }else{
856 d_congruenceManager.equalsConstant(constraint);
857 }
858 }
859
860 d_updatedBounds.softAdd(x_i);
861
862 if(Debug.isOn("model")) {
863 Debug("model") << "before" << endl;
864 d_partialModel.printModel(x_i);
865 d_tableau.debugPrintIsBasic(x_i);
866 }
867
868 if(!d_tableau.isBasic(x_i)){
869 if(!(d_partialModel.getAssignment(x_i) == c_i)){
870 d_linEq.update(x_i, c_i);
871 }
872 }else{
873 d_errorSet.signalVariable(x_i);
874 }
875
876 if(Debug.isOn("model")) {
877 Debug("model") << "after" << endl;
878 d_partialModel.printModel(x_i);
879 d_tableau.debugPrintIsBasic(x_i);
880 }
881
882 return false;
883 }
884
885
886 /* procedure AssertDisequality( x_i != c_i ) */
887 bool TheoryArithPrivate::AssertDisequality(ConstraintP constraint){
888 Assert(constraint != NullConstraint);
889 Assert(constraint->isDisequality());
890 Assert(constraint->isTrue());
891 Assert(!constraint->negationHasProof());
892
893 ArithVar x_i = constraint->getVariable();
894 const DeltaRational& c_i = constraint->getValue();
895 Debug("arith") << "AssertDisequality(" << x_i << " " << c_i << ")"<< std::endl;
896
897 //Should be fine in integers
898 Assert(!isInteger(x_i) || c_i.isIntegral());
899
900 if(d_cmEnabled){
901 if(d_congruenceManager.isWatchedVariable(x_i)){
902 int sgn = c_i.sgn();
903 if(sgn == 0){
904 d_congruenceManager.watchedVariableCannotBeZero(constraint);
905 }
906 }
907 }
908
909 const ValueCollection& vc = constraint->getValueCollection();
910 if(vc.hasLowerBound() && vc.hasUpperBound()){
911 const ConstraintP lb = vc.getLowerBound();
912 const ConstraintP ub = vc.getUpperBound();
913 if(lb->isTrue() && ub->isTrue()){
914 ConstraintP eq = constraint->getNegation();
915 eq->impliedByTrichotomy(lb, ub, true);
916 raiseConflict(constraint, InferenceId::ARITH_CONF_TRICHOTOMY);
917 //in conflict
918 ++(d_statistics.d_statDisequalityConflicts);
919 return true;
920 }
921 }
922 if(vc.hasLowerBound() ){
923 const ConstraintP lb = vc.getLowerBound();
924 if(lb->isTrue()){
925 const ConstraintP ub = d_constraintDatabase.ensureConstraint(const_cast<ValueCollection&>(vc), UpperBound);
926 Assert(!ub->isTrue());
927 Debug("arith::eq") << "propagate UpperBound " << constraint << lb << ub << endl;
928 const ConstraintP negUb = ub->getNegation();
929 if(!negUb->isTrue()){
930 negUb->impliedByTrichotomy(constraint, lb, false);
931 negUb->tryToPropagate();
932 d_learnedBounds.push_back(negUb);
933 }
934 }
935 }
936 if(vc.hasUpperBound()){
937 const ConstraintP ub = vc.getUpperBound();
938 if(ub->isTrue()){
939 const ConstraintP lb = d_constraintDatabase.ensureConstraint(const_cast<ValueCollection&>(vc), LowerBound);
940 Assert(!lb->isTrue());
941
942 Debug("arith::eq") << "propagate LowerBound " << constraint << lb << ub << endl;
943 const ConstraintP negLb = lb->getNegation();
944 if(!negLb->isTrue()){
945 negLb->impliedByTrichotomy(constraint, ub, false);
946 negLb->tryToPropagate();
947 d_learnedBounds.push_back(negLb);
948 }
949 }
950 }
951
952 bool split = constraint->isSplit();
953
954 if(!split && c_i == d_partialModel.getAssignment(x_i)){
955 Debug("arith::eq") << "lemma now! " << constraint << endl;
956 outputTrustedLemma(constraint->split(), InferenceId::ARITH_SPLIT_DEQ);
957 return false;
958 }else if(d_partialModel.strictlyLessThanLowerBound(x_i, c_i)){
959 Debug("arith::eq") << "can drop as less than lb" << constraint << endl;
960 }else if(d_partialModel.strictlyGreaterThanUpperBound(x_i, c_i)){
961 Debug("arith::eq") << "can drop as less than ub" << constraint << endl;
962 }else if(!split){
963 Debug("arith::eq") << "push back" << constraint << endl;
964 d_diseqQueue.push(constraint);
965 d_partialModel.invalidateDelta();
966 }else{
967 Debug("arith::eq") << "skipping already split " << constraint << endl;
968 }
969 return false;
970 }
971
972 void TheoryArithPrivate::notifySharedTerm(TNode n)
973 {
974 Debug("arith::notifySharedTerm") << "notifySharedTerm: " << n << endl;
975 if(n.isConst()){
976 d_partialModel.invalidateDelta();
977 }
978 if(!n.isConst() && !isSetup(n)){
979 Polynomial poly = Polynomial::parsePolynomial(n);
980 Polynomial::iterator it = poly.begin();
981 Polynomial::iterator it_end = poly.end();
982 for (; it != it_end; ++ it) {
983 Monomial m = *it;
984 if (!m.isConstant() && !isSetup(m.getVarList().getNode())) {
985 setupVariableList(m.getVarList());
986 }
987 }
988 }
989 }
990
991 Node TheoryArithPrivate::getModelValue(TNode term) {
992 try{
993 const DeltaRational drv = getDeltaValue(term);
994 const Rational& delta = d_partialModel.getDelta();
995 const Rational qmodel = drv.substituteDelta( delta );
996 return mkRationalNode( qmodel );
997 } catch (DeltaRationalException& dr) {
998 return Node::null();
999 } catch (ModelException& me) {
1000 return Node::null();
1001 }
1002 }
1003
1004 Theory::PPAssertStatus TheoryArithPrivate::ppAssert(
1005 TrustNode tin, TrustSubstitutionMap& outSubstitutions)
1006 {
1007 TimerStat::CodeTimer codeTimer(d_statistics.d_simplifyTimer);
1008 TNode in = tin.getNode();
1009 Debug("simplify") << "TheoryArithPrivate::solve(" << in << ")" << endl;
1010
1011
1012 // Solve equalities
1013 Rational minConstant = 0;
1014 Node minMonomial;
1015 Node minVar;
1016 if (in.getKind() == kind::EQUAL &&
1017 Theory::theoryOf(in[0].getType()) == THEORY_ARITH) {
1018 Comparison cmp = Comparison::parseNormalForm(in);
1019
1020 Polynomial left = cmp.getLeft();
1021
1022 Monomial m = left.getHead();
1023 if (m.getVarList().singleton()){
1024 VarList vl = m.getVarList();
1025 Node var = vl.getNode();
1026 if (var.isVar())
1027 {
1028 // if vl.isIntegral then m.getConstant().isOne()
1029 if(!vl.isIntegral() || m.getConstant().isOne()){
1030 minVar = var;
1031 }
1032 }
1033 }
1034
1035 // Solve for variable
1036 if (!minVar.isNull()) {
1037 Polynomial right = cmp.getRight();
1038 Node elim = right.getNode();
1039 // ax + p = c -> (ax + p) -ax - c = -ax
1040 // x = (p - ax - c) * -1/a
1041 // Add the substitution if not recursive
1042 Assert(elim == Rewriter::rewrite(elim));
1043
1044 if (right.size() > options::ppAssertMaxSubSize())
1045 {
1046 Debug("simplify")
1047 << "TheoryArithPrivate::solve(): did not substitute due to the "
1048 "right hand side containing too many terms: "
1049 << minVar << ":" << elim << endl;
1050 Debug("simplify") << right.size() << endl;
1051 }
1052 else if (d_containing.isLegalElimination(minVar, elim))
1053 {
1054 // cannot eliminate integers here unless we know the resulting
1055 // substitution is integral
1056 Debug("simplify") << "TheoryArithPrivate::solve(): substitution "
1057 << minVar << " |-> " << elim << endl;
1058
1059 outSubstitutions.addSubstitutionSolved(minVar, elim, tin);
1060 return Theory::PP_ASSERT_STATUS_SOLVED;
1061 }
1062 else
1063 {
1064 Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute "
1065 << minVar << ":" << minVar.getType() << " |-> "
1066 << elim << ":" << elim.getType() << endl;
1067 }
1068 }
1069 }
1070
1071 // If a relation, remember the bound
1072 switch(in.getKind()) {
1073 case kind::LEQ:
1074 case kind::LT:
1075 case kind::GEQ:
1076 case kind::GT:
1077 if (in[0].isVar()) {
1078 d_learner.addBound(in);
1079 }
1080 break;
1081 default:
1082 // Do nothing
1083 break;
1084 }
1085
1086 return Theory::PP_ASSERT_STATUS_UNSOLVED;
1087 }
1088
1089 void TheoryArithPrivate::ppStaticLearn(TNode n, NodeBuilder& learned)
1090 {
1091 TimerStat::CodeTimer codeTimer(d_statistics.d_staticLearningTimer);
1092
1093 d_learner.staticLearning(n, learned);
1094 }
1095
1096 ArithVar TheoryArithPrivate::findShortestBasicRow(ArithVar variable){
1097 ArithVar bestBasic = ARITHVAR_SENTINEL;
1098 uint64_t bestRowLength = std::numeric_limits<uint64_t>::max();
1099
1100 Tableau::ColIterator basicIter = d_tableau.colIterator(variable);
1101 for(; !basicIter.atEnd(); ++basicIter){
1102 const Tableau::Entry& entry = *basicIter;
1103 Assert(entry.getColVar() == variable);
1104 RowIndex ridx = entry.getRowIndex();
1105 ArithVar basic = d_tableau.rowIndexToBasic(ridx);
1106 uint32_t rowLength = d_tableau.getRowLength(ridx);
1107 if((rowLength < bestRowLength) ||
1108 (rowLength == bestRowLength && basic < bestBasic)){
1109 bestBasic = basic;
1110 bestRowLength = rowLength;
1111 }
1112 }
1113 Assert(bestBasic == ARITHVAR_SENTINEL
1114 || bestRowLength < std::numeric_limits<uint32_t>::max());
1115 return bestBasic;
1116 }
1117
1118 void TheoryArithPrivate::setupVariable(const Variable& x){
1119 Node n = x.getNode();
1120
1121 Assert(!isSetup(n));
1122
1123 ++(d_statistics.d_statUserVariables);
1124 requestArithVar(n, false, false);
1125 //ArithVar varN = requestArithVar(n,false);
1126 //setupInitialValue(varN);
1127
1128 markSetup(n);
1129 }
1130
1131 void TheoryArithPrivate::setupVariableList(const VarList& vl){
1132 Assert(!vl.empty());
1133
1134 TNode vlNode = vl.getNode();
1135 Assert(!isSetup(vlNode));
1136 Assert(!d_partialModel.hasArithVar(vlNode));
1137
1138 for(VarList::iterator i = vl.begin(), end = vl.end(); i != end; ++i){
1139 Variable var = *i;
1140
1141 if(!isSetup(var.getNode())){
1142 setupVariable(var);
1143 }
1144 }
1145
1146 if(!vl.singleton()){
1147 // vl is the product of at least 2 variables
1148 // vl : (* v1 v2 ...)
1149 if(getLogicInfo().isLinear()){
1150 throw LogicException("A non-linear fact was asserted to arithmetic in a linear logic.");
1151 }
1152 d_foundNl = true;
1153
1154 ++(d_statistics.d_statUserVariables);
1155 requestArithVar(vlNode, false, false);
1156 //ArithVar av = requestArithVar(vlNode, false);
1157 //setupInitialValue(av);
1158
1159 markSetup(vlNode);
1160 }
1161 else if (vlNode.getKind() == kind::EXPONENTIAL
1162 || vlNode.getKind() == kind::SINE || vlNode.getKind() == kind::COSINE
1163 || vlNode.getKind() == kind::TANGENT)
1164 {
1165 d_foundNl = true;
1166 }
1167
1168 /* Note:
1169 * Only call markSetup if the VarList is not a singleton.
1170 * See the comment in setupPolynomail for more.
1171 */
1172 }
1173
1174 void TheoryArithPrivate::cautiousSetupPolynomial(const Polynomial& p){
1175 if(p.containsConstant()){
1176 if(!p.isConstant()){
1177 Polynomial noConstant = p.getTail();
1178 if(!isSetup(noConstant.getNode())){
1179 setupPolynomial(noConstant);
1180 }
1181 }
1182 }else if(!isSetup(p.getNode())){
1183 setupPolynomial(p);
1184 }
1185 }
1186
1187
1188 void TheoryArithPrivate::setupPolynomial(const Polynomial& poly) {
1189 Assert(!poly.containsConstant());
1190 TNode polyNode = poly.getNode();
1191 Assert(!isSetup(polyNode));
1192 Assert(!d_partialModel.hasArithVar(polyNode));
1193
1194 for(Polynomial::iterator i = poly.begin(), end = poly.end(); i != end; ++i){
1195 Monomial mono = *i;
1196 const VarList& vl = mono.getVarList();
1197 if(!isSetup(vl.getNode())){
1198 setupVariableList(vl);
1199 }
1200 }
1201
1202 if(polyNode.getKind() == PLUS){
1203 d_tableauSizeHasBeenModified = true;
1204
1205 vector<ArithVar> variables;
1206 vector<Rational> coefficients;
1207 asVectors(poly, coefficients, variables);
1208
1209 ArithVar varSlack = requestArithVar(polyNode, true, false);
1210 d_tableau.addRow(varSlack, coefficients, variables);
1211 setupBasicValue(varSlack);
1212 d_linEq.trackRowIndex(d_tableau.basicToRowIndex(varSlack));
1213
1214 //Add differences to the difference manager
1215 Polynomial::iterator i = poly.begin(), end = poly.end();
1216 if(i != end){
1217 Monomial first = *i;
1218 ++i;
1219 if(i != end){
1220 Monomial second = *i;
1221 ++i;
1222 if(i == end){
1223 if(first.getConstant().isOne() && second.getConstant().getValue() == -1){
1224 VarList vl0 = first.getVarList();
1225 VarList vl1 = second.getVarList();
1226 if(vl0.singleton() && vl1.singleton()){
1227 d_congruenceManager.addWatchedPair(varSlack, vl0.getNode(), vl1.getNode());
1228 }
1229 }
1230 }
1231 }
1232 }
1233
1234 ++(d_statistics.d_statAuxiliaryVariables);
1235 markSetup(polyNode);
1236 }
1237
1238 /* Note:
1239 * It is worth documenting that polyNode should only be marked as
1240 * being setup by this function if it has kind PLUS.
1241 * Other kinds will be marked as being setup by lower levels of setup
1242 * specifically setupVariableList.
1243 */
1244 }
1245
1246 void TheoryArithPrivate::setupAtom(TNode atom) {
1247 Assert(isRelationOperator(atom.getKind())) << atom;
1248 Assert(Comparison::isNormalAtom(atom));
1249 Assert(!isSetup(atom));
1250 Assert(!d_constraintDatabase.hasLiteral(atom));
1251
1252 Comparison cmp = Comparison::parseNormalForm(atom);
1253 Polynomial nvp = cmp.normalizedVariablePart();
1254 Assert(!nvp.isZero());
1255
1256 if(!isSetup(nvp.getNode())){
1257 setupPolynomial(nvp);
1258 }
1259
1260 d_constraintDatabase.addLiteral(atom);
1261
1262 markSetup(atom);
1263 }
1264
1265 void TheoryArithPrivate::preRegisterTerm(TNode n) {
1266 Debug("arith::preregister") <<"begin arith::preRegisterTerm("<< n <<")"<< endl;
1267
1268 d_preregisteredNodes.insert(n);
1269
1270 try {
1271 if(isRelationOperator(n.getKind())){
1272 if(!isSetup(n)){
1273 setupAtom(n);
1274 }
1275 ConstraintP c = d_constraintDatabase.lookup(n);
1276 Assert(c != NullConstraint);
1277
1278 Debug("arith::preregister") << "setup constraint" << c << endl;
1279 Assert(!c->canBePropagated());
1280 c->setPreregistered();
1281 }
1282 } catch(LogicException& le) {
1283 std::stringstream ss;
1284 ss << le.getMessage() << endl << "The fact in question: " << n << endl;
1285 throw LogicException(ss.str());
1286 }
1287
1288 Debug("arith::preregister") << "end arith::preRegisterTerm("<< n <<")" << endl;
1289 }
1290
1291 void TheoryArithPrivate::releaseArithVar(ArithVar v){
1292 //Assert(d_partialModel.hasNode(v));
1293
1294 d_constraintDatabase.removeVariable(v);
1295 d_partialModel.releaseArithVar(v);
1296 }
1297
1298 ArithVar TheoryArithPrivate::requestArithVar(TNode x, bool aux, bool internal){
1299 //TODO : The VarList trick is good enough?
1300 Assert(isLeaf(x) || VarList::isMember(x) || x.getKind() == PLUS || internal);
1301 if(getLogicInfo().isLinear() && Variable::isDivMember(x)){
1302 stringstream ss;
1303 ss << "A non-linear fact (involving div/mod/divisibility) was asserted to "
1304 "arithmetic in a linear logic: "
1305 << x << std::endl;
1306 throw LogicException(ss.str());
1307 }
1308 Assert(!d_partialModel.hasArithVar(x));
1309 Assert(x.getType().isReal()); // real or integer
1310
1311 ArithVar max = d_partialModel.getNumberOfVariables();
1312 ArithVar varX = d_partialModel.allocate(x, aux);
1313
1314 bool reclaim = max >= d_partialModel.getNumberOfVariables();;
1315
1316 if(!reclaim){
1317 d_dualSimplex.increaseMax();
1318
1319 d_tableau.increaseSize();
1320 d_tableauSizeHasBeenModified = true;
1321 }
1322 d_constraintDatabase.addVariable(varX);
1323
1324 Debug("arith::arithvar") << "@" << getSatContext()->getLevel()
1325 << " " << x << " |-> " << varX
1326 << "(relaiming " << reclaim << ")" << endl;
1327
1328 Assert(!d_partialModel.hasUpperBound(varX));
1329 Assert(!d_partialModel.hasLowerBound(varX));
1330
1331 return varX;
1332 }
1333
1334 void TheoryArithPrivate::asVectors(const Polynomial& p, std::vector<Rational>& coeffs, std::vector<ArithVar>& variables) {
1335 for(Polynomial::iterator i = p.begin(), end = p.end(); i != end; ++i){
1336 const Monomial& mono = *i;
1337 const Constant& constant = mono.getConstant();
1338 const VarList& variable = mono.getVarList();
1339
1340 Node n = variable.getNode();
1341
1342 Debug("arith::asVectors") << "should be var: " << n << endl;
1343
1344 // TODO: This VarList::isMember(n) can be stronger
1345 Assert(isLeaf(n) || VarList::isMember(n));
1346 Assert(theoryOf(n) != THEORY_ARITH || d_partialModel.hasArithVar(n));
1347
1348 Assert(d_partialModel.hasArithVar(n));
1349 ArithVar av = d_partialModel.asArithVar(n);
1350
1351 coeffs.push_back(constant.getValue());
1352 variables.push_back(av);
1353 }
1354 }
1355
1356 /* Requirements:
1357 * For basic variables the row must have been added to the tableau.
1358 */
1359 void TheoryArithPrivate::setupBasicValue(ArithVar x){
1360 Assert(d_tableau.isBasic(x));
1361 //If the variable is basic, assertions may have already happened and updates
1362 //may have occured before setting this variable up.
1363
1364 //This can go away if the tableau creation is done at preregister
1365 //time instead of register
1366 DeltaRational safeAssignment = d_linEq.computeRowValue(x, true);
1367 DeltaRational assignment = d_linEq.computeRowValue(x, false);
1368 d_partialModel.setAssignment(x,safeAssignment,assignment);
1369
1370 Debug("arith") << "setupVariable("<<x<<")"<<std::endl;
1371 }
1372
1373 ArithVar TheoryArithPrivate::determineArithVar(const Polynomial& p) const{
1374 Assert(!p.containsConstant());
1375 Assert(p.getHead().constantIsPositive());
1376 TNode n = p.getNode();
1377 Debug("determineArithVar") << "determineArithVar(" << n << ")" << endl;
1378 return d_partialModel.asArithVar(n);
1379 }
1380
1381 ArithVar TheoryArithPrivate::determineArithVar(TNode assertion) const{
1382 Debug("determineArithVar") << "determineArithVar " << assertion << endl;
1383 Comparison cmp = Comparison::parseNormalForm(assertion);
1384 Polynomial variablePart = cmp.normalizedVariablePart();
1385 return determineArithVar(variablePart);
1386 }
1387
1388
1389 bool TheoryArithPrivate::canSafelyAvoidEqualitySetup(TNode equality){
1390 Assert(equality.getKind() == EQUAL);
1391 return d_partialModel.hasArithVar(equality[0]);
1392 }
1393
1394 Comparison TheoryArithPrivate::mkIntegerEqualityFromAssignment(ArithVar v){
1395 const DeltaRational& beta = d_partialModel.getAssignment(v);
1396
1397 Assert(beta.isIntegral());
1398 Polynomial betaAsPolynomial = Polynomial::mkPolynomial( Constant::mkConstant(beta.floor()) );
1399
1400 TNode var = d_partialModel.asNode(v);
1401 Polynomial varAsPolynomial = Polynomial::parsePolynomial(var);
1402 return Comparison::mkComparison(EQUAL, varAsPolynomial, betaAsPolynomial);
1403 }
1404
1405 TrustNode TheoryArithPrivate::dioCutting()
1406 {
1407 context::Context::ScopedPush speculativePush(getSatContext());
1408 //DO NOT TOUCH THE OUTPUTSTREAM
1409
1410 for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
1411 ArithVar v = *vi;
1412 if(isInteger(v)){
1413 if(d_partialModel.cmpAssignmentUpperBound(v) == 0 ||
1414 d_partialModel.cmpAssignmentLowerBound(v) == 0){
1415 if(!d_partialModel.boundsAreEqual(v)){
1416 // If the bounds are equal this is already in the dioSolver
1417 //Add v = dr as a speculation.
1418 Comparison eq = mkIntegerEqualityFromAssignment(v);
1419 Debug("dio::push") << "dio::push " << v << " " << eq.getNode() << endl;
1420 Assert(!eq.isBoolean());
1421 d_diosolver.pushInputConstraint(eq, eq.getNode());
1422 // It does not matter what the explanation of eq is.
1423 // It cannot be used in a conflict
1424 }
1425 }
1426 }
1427 }
1428
1429 SumPair plane = d_diosolver.processEquationsForCut();
1430 if(plane.isZero()){
1431 return TrustNode::null();
1432 }else{
1433 Polynomial p = plane.getPolynomial();
1434 Polynomial c = Polynomial::mkPolynomial(plane.getConstant() * Constant::mkConstant(-1));
1435 Integer gcd = p.gcd();
1436 Assert(p.isIntegral());
1437 Assert(c.isIntegral());
1438 Assert(gcd > 1);
1439 Assert(!gcd.divides(c.asConstant().getNumerator()));
1440 Comparison leq = Comparison::mkComparison(LEQ, p, c);
1441 Comparison geq = Comparison::mkComparison(GEQ, p, c);
1442 Node lemma = NodeManager::currentNM()->mkNode(OR, leq.getNode(), geq.getNode());
1443 Node rewrittenLemma = Rewriter::rewrite(lemma);
1444 Debug("arith::dio::ex") << "dioCutting found the plane: " << plane.getNode() << endl;
1445 Debug("arith::dio::ex") << "resulting in the cut: " << lemma << endl;
1446 Debug("arith::dio::ex") << "rewritten " << rewrittenLemma << endl;
1447 Debug("arith::dio") << "dioCutting found the plane: " << plane.getNode() << endl;
1448 Debug("arith::dio") << "resulting in the cut: " << lemma << endl;
1449 Debug("arith::dio") << "rewritten " << rewrittenLemma << endl;
1450 if (proofsEnabled())
1451 {
1452 NodeManager* nm = NodeManager::currentNM();
1453 Node gt = nm->mkNode(kind::GT, p.getNode(), c.getNode());
1454 Node lt = nm->mkNode(kind::LT, p.getNode(), c.getNode());
1455
1456 Pf pfNotLeq = d_pnm->mkAssume(leq.getNode().negate());
1457 Pf pfGt =
1458 d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, {pfNotLeq}, {gt});
1459 Pf pfNotGeq = d_pnm->mkAssume(geq.getNode().negate());
1460 Pf pfLt =
1461 d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, {pfNotGeq}, {lt});
1462 Pf pfSum =
1463 d_pnm->mkNode(PfRule::MACRO_ARITH_SCALE_SUM_UB,
1464 {pfGt, pfLt},
1465 {nm->mkConst<Rational>(-1), nm->mkConst<Rational>(1)});
1466 Pf pfBot = d_pnm->mkNode(
1467 PfRule::MACRO_SR_PRED_TRANSFORM, {pfSum}, {nm->mkConst<bool>(false)});
1468 std::vector<Node> assumptions = {leq.getNode().negate(),
1469 geq.getNode().negate()};
1470 Pf pfNotAndNot = d_pnm->mkScope(pfBot, assumptions);
1471 Pf pfOr = d_pnm->mkNode(PfRule::NOT_AND, {pfNotAndNot}, {});
1472 Pf pfRewritten = d_pnm->mkNode(
1473 PfRule::MACRO_SR_PRED_TRANSFORM, {pfOr}, {rewrittenLemma});
1474 return d_pfGen->mkTrustNode(rewrittenLemma, pfRewritten);
1475 }
1476 else
1477 {
1478 return TrustNode::mkTrustLemma(rewrittenLemma, nullptr);
1479 }
1480 }
1481 }
1482
1483 Node TheoryArithPrivate::callDioSolver(){
1484 while(!d_constantIntegerVariables.empty()){
1485 ArithVar v = d_constantIntegerVariables.front();
1486 d_constantIntegerVariables.pop();
1487
1488 Debug("arith::dio") << "callDioSolver " << v << endl;
1489
1490 Assert(isInteger(v));
1491 Assert(d_partialModel.boundsAreEqual(v));
1492
1493 ConstraintP lb = d_partialModel.getLowerBoundConstraint(v);
1494 ConstraintP ub = d_partialModel.getUpperBoundConstraint(v);
1495
1496 Node orig = Node::null();
1497 if(lb->isEquality()){
1498 orig = Constraint::externalExplainByAssertions({lb});
1499 }else if(ub->isEquality()){
1500 orig = Constraint::externalExplainByAssertions({ub});
1501 }else {
1502 orig = Constraint::externalExplainByAssertions(ub, lb);
1503 }
1504
1505 Assert(d_partialModel.assignmentIsConsistent(v));
1506
1507 Comparison eq = mkIntegerEqualityFromAssignment(v);
1508
1509 if(eq.isBoolean()){
1510 //This can only be a conflict
1511 Assert(!eq.getNode().getConst<bool>());
1512
1513 //This should be handled by the normal form earlier in the case of equality
1514 Assert(orig.getKind() != EQUAL);
1515 return orig;
1516 }else{
1517 Debug("dio::push") << "dio::push " << v << " " << eq.getNode() << " with reason " << orig << endl;
1518 d_diosolver.pushInputConstraint(eq, orig);
1519 }
1520 }
1521
1522 return d_diosolver.processEquationsForConflict();
1523 }
1524
1525 ConstraintP TheoryArithPrivate::constraintFromFactQueue(TNode assertion)
1526 {
1527 Kind simpleKind = Comparison::comparisonKind(assertion);
1528 ConstraintP constraint = d_constraintDatabase.lookup(assertion);
1529 if(constraint == NullConstraint){
1530 Assert(simpleKind == EQUAL || simpleKind == DISTINCT);
1531 bool isDistinct = simpleKind == DISTINCT;
1532 Node eq = (simpleKind == DISTINCT) ? assertion[0] : assertion;
1533 Assert(!isSetup(eq));
1534 Node reEq = Rewriter::rewrite(eq);
1535 Debug("arith::distinct::const") << "Assertion: " << assertion << std::endl;
1536 Debug("arith::distinct::const") << "Eq : " << eq << std::endl;
1537 Debug("arith::distinct::const") << "reEq : " << reEq << std::endl;
1538 if(reEq.getKind() == CONST_BOOLEAN){
1539 if(reEq.getConst<bool>() == isDistinct){
1540 // if is (not true), or false
1541 Assert((reEq.getConst<bool>() && isDistinct)
1542 || (!reEq.getConst<bool>() && !isDistinct));
1543 if (proofsEnabled())
1544 {
1545 Pf assume = d_pnm->mkAssume(assertion);
1546 std::vector<Node> assumptions = {assertion};
1547 Pf pf = d_pnm->mkScope(d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM,
1548 {d_pnm->mkAssume(assertion)},
1549 {}),
1550 assumptions);
1551 raiseBlackBoxConflict(assertion, pf);
1552 }
1553 else
1554 {
1555 raiseBlackBoxConflict(assertion);
1556 }
1557 }
1558 return NullConstraint;
1559 }
1560 Assert(reEq.getKind() != CONST_BOOLEAN);
1561 if(!isSetup(reEq)){
1562 setupAtom(reEq);
1563 }
1564 Node reAssertion = isDistinct ? reEq.notNode() : reEq;
1565 constraint = d_constraintDatabase.lookup(reAssertion);
1566
1567 if(assertion != reAssertion){
1568 Debug("arith::nf") << "getting non-nf assertion " << assertion << " |-> " << reAssertion << endl;
1569 Assert(constraint != NullConstraint);
1570 d_assertionsThatDoNotMatchTheirLiterals.insert(assertion, constraint);
1571 }
1572 }
1573
1574 Assert(constraint != NullConstraint);
1575
1576 if(constraint->assertedToTheTheory()){
1577 //Do nothing
1578 return NullConstraint;
1579 }
1580 Assert(!constraint->assertedToTheTheory());
1581 bool inConflict = constraint->negationHasProof();
1582 constraint->setAssertedToTheTheory(assertion, inConflict);
1583
1584 if(!constraint->hasProof()){
1585 Debug("arith::constraint") << "marking as constraint as self explaining " << endl;
1586 constraint->setAssumption(inConflict);
1587 } else {
1588 Debug("arith::constraint")
1589 << "already has proof: "
1590 << Constraint::externalExplainByAssertions({constraint});
1591 }
1592
1593 if(Debug.isOn("arith::negatedassumption") && inConflict){
1594 ConstraintP negation = constraint->getNegation();
1595 if(Debug.isOn("arith::negatedassumption") && negation->isAssumption()){
1596 debugPrintFacts();
1597 }
1598 Debug("arith::eq") << "negation has proof" << endl;
1599 Debug("arith::eq") << constraint << endl;
1600 Debug("arith::eq") << negation << endl;
1601 }
1602
1603 if(inConflict){
1604 ConstraintP negation = constraint->getNegation();
1605 if(Debug.isOn("arith::negatedassumption") && negation->isAssumption()){
1606 debugPrintFacts();
1607 }
1608 Debug("arith::eq") << "negation has proof" << endl;
1609 Debug("arith::eq") << constraint << endl;
1610 Debug("arith::eq") << negation << endl;
1611 raiseConflict(negation, InferenceId::UNKNOWN);
1612 return NullConstraint;
1613 }else{
1614 return constraint;
1615 }
1616 }
1617
1618 bool TheoryArithPrivate::assertionCases(ConstraintP constraint){
1619 Assert(constraint->hasProof());
1620 Assert(!constraint->negationHasProof());
1621
1622 ArithVar x_i = constraint->getVariable();
1623
1624 switch(constraint->getType()){
1625 case UpperBound:
1626 if(isInteger(x_i) && constraint->isStrictUpperBound()){
1627 ConstraintP floorConstraint = constraint->getFloor();
1628 if(!floorConstraint->isTrue()){
1629 bool inConflict = floorConstraint->negationHasProof();
1630 if (Debug.isOn("arith::intbound")) {
1631 Debug("arith::intbound") << "literal, before: " << constraint->getLiteral() << std::endl;
1632 Debug("arith::intbound") << "constraint, after: " << floorConstraint << std::endl;
1633 }
1634 floorConstraint->impliedByIntTighten(constraint, inConflict);
1635 floorConstraint->tryToPropagate();
1636 if(inConflict){
1637 raiseConflict(floorConstraint, InferenceId::ARITH_TIGHTEN_FLOOR);
1638 return true;
1639 }
1640 }
1641 return AssertUpper(floorConstraint);
1642 }else{
1643 return AssertUpper(constraint);
1644 }
1645 case LowerBound:
1646 if(isInteger(x_i) && constraint->isStrictLowerBound()){
1647 ConstraintP ceilingConstraint = constraint->getCeiling();
1648 if(!ceilingConstraint->isTrue()){
1649 bool inConflict = ceilingConstraint->negationHasProof();
1650 if (Debug.isOn("arith::intbound")) {
1651 Debug("arith::intbound") << "literal, before: " << constraint->getLiteral() << std::endl;
1652 Debug("arith::intbound") << "constraint, after: " << ceilingConstraint << std::endl;
1653 }
1654 ceilingConstraint->impliedByIntTighten(constraint, inConflict);
1655 ceilingConstraint->tryToPropagate();
1656 if(inConflict){
1657 raiseConflict(ceilingConstraint, InferenceId::ARITH_TIGHTEN_CEIL);
1658 return true;
1659 }
1660 }
1661 return AssertLower(ceilingConstraint);
1662 }else{
1663 return AssertLower(constraint);
1664 }
1665 case Equality:
1666 return AssertEquality(constraint);
1667 case Disequality:
1668 return AssertDisequality(constraint);
1669 default:
1670 Unreachable();
1671 return false;
1672 }
1673 }
1674 /**
1675 * Looks for through the variables starting at d_nextIntegerCheckVar
1676 * for the first integer variable that is between its upper and lower bounds
1677 * that has a non-integer assignment.
1678 *
1679 * If assumeBounds is true, skip the check that the variable is in bounds.
1680 *
1681 * If there is no such variable, returns ARITHVAR_SENTINEL;
1682 */
1683 ArithVar TheoryArithPrivate::nextIntegerViolation(bool assumeBounds) const
1684 {
1685 ArithVar numVars = d_partialModel.getNumberOfVariables();
1686 ArithVar v = d_nextIntegerCheckVar;
1687 if (numVars > 0)
1688 {
1689 const ArithVar rrEnd = d_nextIntegerCheckVar;
1690 do
1691 {
1692 if (isIntegerInput(v))
1693 {
1694 if (!d_partialModel.integralAssignment(v))
1695 {
1696 if (assumeBounds || d_partialModel.assignmentIsConsistent(v))
1697 {
1698 return v;
1699 }
1700 }
1701 }
1702 v = (1 + v == numVars) ? 0 : (1 + v);
1703 } while (v != rrEnd);
1704 }
1705 return ARITHVAR_SENTINEL;
1706 }
1707
1708 /**
1709 * Checks the set of integer variables I to see if each variable
1710 * in I has an integer assignment.
1711 */
1712 bool TheoryArithPrivate::hasIntegerModel()
1713 {
1714 ArithVar next = nextIntegerViolation(true);
1715 if (next != ARITHVAR_SENTINEL)
1716 {
1717 d_nextIntegerCheckVar = next;
1718 if (Debug.isOn("arith::hasIntegerModel"))
1719 {
1720 Debug("arith::hasIntegerModel") << "has int model? " << next << endl;
1721 d_partialModel.printModel(next, Debug("arith::hasIntegerModel"));
1722 }
1723 return false;
1724 }
1725 else
1726 {
1727 return true;
1728 }
1729 }
1730
1731 Node flattenAndSort(Node n){
1732 Kind k = n.getKind();
1733 switch(k){
1734 case kind::OR:
1735 case kind::AND:
1736 case kind::PLUS:
1737 case kind::MULT:
1738 break;
1739 default:
1740 return n;
1741 }
1742
1743 std::vector<Node> out;
1744 std::vector<Node> process;
1745 process.push_back(n);
1746 while(!process.empty()){
1747 Node b = process.back();
1748 process.pop_back();
1749 if(b.getKind() == k){
1750 for(Node::iterator i=b.begin(), end=b.end(); i!=end; ++i){
1751 process.push_back(*i);
1752 }
1753 } else {
1754 out.push_back(b);
1755 }
1756 }
1757 Assert(out.size() >= 2);
1758 std::sort(out.begin(), out.end());
1759 return NodeManager::currentNM()->mkNode(k, out);
1760 }
1761
1762
1763
1764 /** Outputs conflicts to the output channel. */
1765 void TheoryArithPrivate::outputConflicts(){
1766 Debug("arith::conflict") << "outputting conflicts" << std::endl;
1767 Assert(anyConflict());
1768 static unsigned int conflicts = 0;
1769
1770 if(!conflictQueueEmpty()){
1771 Assert(!d_conflicts.empty());
1772 for(size_t i = 0, i_end = d_conflicts.size(); i < i_end; ++i){
1773 const std::pair<ConstraintCP, InferenceId>& conf = d_conflicts[i];
1774 const ConstraintCP& confConstraint = conf.first;
1775 bool hasProof = confConstraint->hasProof();
1776 Assert(confConstraint->inConflict());
1777 const ConstraintRule& pf = confConstraint->getConstraintRule();
1778 if (Debug.isOn("arith::conflict"))
1779 {
1780 pf.print(std::cout);
1781 std::cout << std::endl;
1782 }
1783 if (Debug.isOn("arith::pf::tree"))
1784 {
1785 Debug("arith::pf::tree") << "\n\nTree:\n";
1786 confConstraint->printProofTree(Debug("arith::pf::tree"));
1787 confConstraint->getNegation()->printProofTree(Debug("arith::pf::tree"));
1788 }
1789
1790 TrustNode trustedConflict = confConstraint->externalExplainConflict();
1791 Node conflict = trustedConflict.getNode();
1792
1793 ++conflicts;
1794 Debug("arith::conflict") << "d_conflicts[" << i << "] " << conflict
1795 << " has proof: " << hasProof << endl;
1796 if(Debug.isOn("arith::normalize::external")){
1797 conflict = flattenAndSort(conflict);
1798 Debug("arith::conflict") << "(normalized to) " << conflict << endl;
1799 }
1800
1801 if (isProofEnabled())
1802 {
1803 outputTrustedConflict(trustedConflict, conf.second);
1804 }
1805 else
1806 {
1807 outputConflict(conflict, conf.second);
1808 }
1809 }
1810 }
1811 if(!d_blackBoxConflict.get().isNull()){
1812 Node bb = d_blackBoxConflict.get();
1813 ++conflicts;
1814 Debug("arith::conflict") << "black box conflict" << bb
1815 //<< "("<<conflicts<<")"
1816 << endl;
1817 if(Debug.isOn("arith::normalize::external")){
1818 bb = flattenAndSort(bb);
1819 Debug("arith::conflict") << "(normalized to) " << bb << endl;
1820 }
1821 if (isProofEnabled() && d_blackBoxConflictPf.get())
1822 {
1823 auto confPf = d_blackBoxConflictPf.get();
1824 outputTrustedConflict(d_pfGen->mkTrustNode(bb, confPf, true), InferenceId::ARITH_BLACK_BOX);
1825 }
1826 else
1827 {
1828 outputConflict(bb, InferenceId::ARITH_BLACK_BOX);
1829 }
1830 }
1831 }
1832
1833 void TheoryArithPrivate::outputTrustedLemma(TrustNode lemma, InferenceId id)
1834 {
1835 Debug("arith::channel") << "Arith trusted lemma: " << lemma << std::endl;
1836 d_containing.d_im.trustedLemma(lemma, id);
1837 }
1838
1839 void TheoryArithPrivate::outputLemma(TNode lem, InferenceId id) {
1840 Debug("arith::channel") << "Arith lemma: " << lem << std::endl;
1841 d_containing.d_im.lemma(lem, id);
1842 }
1843
1844 void TheoryArithPrivate::outputTrustedConflict(TrustNode conf, InferenceId id)
1845 {
1846 Debug("arith::channel") << "Arith trusted conflict: " << conf << std::endl;
1847 d_containing.d_im.trustedConflict(conf, id);
1848 }
1849
1850 void TheoryArithPrivate::outputConflict(TNode lit, InferenceId id) {
1851 Debug("arith::channel") << "Arith conflict: " << lit << std::endl;
1852 d_containing.d_im.conflict(lit, id);
1853 }
1854
1855 void TheoryArithPrivate::outputPropagate(TNode lit) {
1856 Debug("arith::channel") << "Arith propagation: " << lit << std::endl;
1857 // call the propagate lit method of the
1858 d_containing.d_im.propagateLit(lit);
1859 }
1860
1861 void TheoryArithPrivate::outputRestart() {
1862 Debug("arith::channel") << "Arith restart!" << std::endl;
1863 (d_containing.d_out)->demandRestart();
1864 }
1865
1866 bool TheoryArithPrivate::attemptSolveInteger(Theory::Effort effortLevel, bool emmmittedLemmaOrSplit){
1867 int level = getSatContext()->getLevel();
1868 Debug("approx")
1869 << "attemptSolveInteger " << d_qflraStatus
1870 << " " << emmmittedLemmaOrSplit
1871 << " " << effortLevel
1872 << " " << d_lastContextIntegerAttempted
1873 << " " << level
1874 << " " << hasIntegerModel()
1875 << endl;
1876
1877 if(d_qflraStatus == Result::UNSAT){ return false; }
1878 if(emmmittedLemmaOrSplit){ return false; }
1879 if(!options::useApprox()){ return false; }
1880 if(!ApproximateSimplex::enabled()){ return false; }
1881
1882 if(Theory::fullEffort(effortLevel)){
1883 if(hasIntegerModel()){
1884 return false;
1885 }else{
1886 return getSolveIntegerResource();
1887 }
1888 }
1889
1890 if(d_lastContextIntegerAttempted <= 0){
1891 if(hasIntegerModel()){
1892 d_lastContextIntegerAttempted = getSatContext()->getLevel();
1893 return false;
1894 }else{
1895 return getSolveIntegerResource();
1896 }
1897 }
1898
1899
1900 if(!options::trySolveIntStandardEffort()){ return false; }
1901
1902 if (d_lastContextIntegerAttempted <= (level >> 2))
1903 {
1904 double d = (double)(d_solveIntMaybeHelp + 1)
1905 / (d_solveIntAttempts + 1 + level * level);
1906 if (Random::getRandom().pickWithProb(d))
1907 {
1908 return getSolveIntegerResource();
1909 }
1910 }
1911 return false;
1912 }
1913
1914 bool TheoryArithPrivate::replayLog(ApproximateSimplex* approx){
1915 TimerStat::CodeTimer codeTimer(d_statistics.d_replayLogTimer);
1916
1917 ++d_statistics.d_mipProofsAttempted;
1918
1919 Assert(d_replayVariables.empty());
1920 Assert(d_replayConstraints.empty());
1921
1922 size_t enteringPropN = d_currentPropagationList.size();
1923 Assert(conflictQueueEmpty());
1924 TreeLog& tl = getTreeLog();
1925 //tl.applySelected(); /* set row ids */
1926
1927 d_replayedLemmas = false;
1928
1929 /* use the try block for the purpose of pushing the sat context */
1930 context::Context::ScopedPush speculativePush(getSatContext());
1931 d_cmEnabled = false;
1932 std::vector<ConstraintCPVec> res =
1933 replayLogRec(approx, tl.getRootId(), NullConstraint, 1);
1934
1935 if(res.empty()){
1936 ++d_statistics.d_replayAttemptFailed;
1937 }else{
1938 unsigned successes = 0;
1939 for(size_t i =0, N = res.size(); i < N; ++i){
1940 ConstraintCPVec& vec = res[i];
1941 Assert(vec.size() >= 2);
1942 for(size_t j=0, M = vec.size(); j < M; ++j){
1943 ConstraintCP at_j = vec[j];
1944 Assert(at_j->isTrue());
1945 if(!at_j->negationHasProof()){
1946 successes++;
1947 vec[j] = vec.back();
1948 vec.pop_back();
1949 ConstraintP neg_at_j = at_j->getNegation();
1950
1951 Debug("approx::replayLog") << "Setting the proof for the replayLog conflict on:" << endl
1952 << " (" << neg_at_j->isTrue() <<") " << neg_at_j << endl
1953 << " (" << at_j->isTrue() <<") " << at_j << endl;
1954 neg_at_j->impliedByIntHole(vec, true);
1955 raiseConflict(at_j, InferenceId::UNKNOWN);
1956 break;
1957 }
1958 }
1959 }
1960 if(successes > 0){
1961 ++d_statistics.d_mipProofsSuccessful;
1962 }
1963 }
1964
1965 if(d_currentPropagationList.size() > enteringPropN){
1966 d_currentPropagationList.resize(enteringPropN);
1967 }
1968
1969 /* It is not clear what the d_qflraStatus is at this point */
1970 d_qflraStatus = Result::SAT_UNKNOWN;
1971
1972 Assert(d_replayVariables.empty());
1973 Assert(d_replayConstraints.empty());
1974
1975 return !conflictQueueEmpty();
1976 }
1977
1978 std::pair<ConstraintP, ArithVar> TheoryArithPrivate::replayGetConstraint(const DenseMap<Rational>& lhs, Kind k, const Rational& rhs, bool branch)
1979 {
1980 ArithVar added = ARITHVAR_SENTINEL;
1981 Node sum = toSumNode(d_partialModel, lhs);
1982 if(sum.isNull()){ return make_pair(NullConstraint, added); }
1983
1984 Debug("approx::constraint") << "replayGetConstraint " << sum
1985 << " " << k
1986 << " " << rhs
1987 << endl;
1988
1989 Assert(k == kind::LEQ || k == kind::GEQ);
1990
1991 Node comparison = NodeManager::currentNM()->mkNode(k, sum, mkRationalNode(rhs));
1992 Node rewritten = Rewriter::rewrite(comparison);
1993 if(!(Comparison::isNormalAtom(rewritten))){
1994 return make_pair(NullConstraint, added);
1995 }
1996
1997 Comparison cmp = Comparison::parseNormalForm(rewritten);
1998 if(cmp.isBoolean()){ return make_pair(NullConstraint, added); }
1999
2000 Polynomial nvp = cmp.normalizedVariablePart();
2001 if(nvp.isZero()){ return make_pair(NullConstraint, added); }
2002
2003 Node norm = nvp.getNode();
2004
2005 ConstraintType t = Constraint::constraintTypeOfComparison(cmp);
2006 DeltaRational dr = cmp.normalizedDeltaRational();
2007
2008 Debug("approx::constraint") << "rewriting " << rewritten << endl
2009 << " |-> " << norm << " " << t << " " << dr << endl;
2010
2011 Assert(!branch || d_partialModel.hasArithVar(norm));
2012 ArithVar v = ARITHVAR_SENTINEL;
2013 if(d_partialModel.hasArithVar(norm)){
2014
2015 v = d_partialModel.asArithVar(norm);
2016 Debug("approx::constraint") << "replayGetConstraint found "
2017 << norm << " |-> " << v << " @ " << getSatContext()->getLevel() << endl;
2018 Assert(!branch || d_partialModel.isIntegerInput(v));
2019 }else{
2020 v = requestArithVar(norm, true, true);
2021 d_replayVariables.push_back(v);
2022
2023 added = v;
2024
2025 Debug("approx::constraint") << "replayGetConstraint adding "
2026 << norm << " |-> " << v << " @ " << getSatContext()->getLevel() << endl;
2027
2028 Polynomial poly = Polynomial::parsePolynomial(norm);
2029 vector<ArithVar> variables;
2030 vector<Rational> coefficients;
2031 asVectors(poly, coefficients, variables);
2032 d_tableau.addRow(v, coefficients, variables);
2033 setupBasicValue(v);
2034 d_linEq.trackRowIndex(d_tableau.basicToRowIndex(v));
2035 }
2036 Assert(d_partialModel.hasArithVar(norm));
2037 Assert(d_partialModel.asArithVar(norm) == v);
2038 Assert(d_constraintDatabase.variableDatabaseIsSetup(v));
2039
2040 ConstraintP imp = d_constraintDatabase.getBestImpliedBound(v, t, dr);
2041 if(imp != NullConstraint){
2042 if(imp->getValue() == dr){
2043 Assert(added == ARITHVAR_SENTINEL);
2044 return make_pair(imp, added);
2045 }
2046 }
2047
2048 ConstraintP newc = d_constraintDatabase.getConstraint(v, t, dr);
2049 d_replayConstraints.push_back(newc);
2050 return make_pair(newc, added);
2051 }
2052
2053 std::pair<ConstraintP, ArithVar> TheoryArithPrivate::replayGetConstraint(
2054 ApproximateSimplex* approx, const NodeLog& nl)
2055 {
2056 Assert(nl.isBranch());
2057 Assert(d_lhsTmp.empty());
2058
2059 ArithVar v = approx->getBranchVar(nl);
2060 if(v != ARITHVAR_SENTINEL && d_partialModel.isIntegerInput(v)){
2061 if(d_partialModel.hasNode(v)){
2062 d_lhsTmp.set(v, Rational(1));
2063 double dval = nl.branchValue();
2064 Maybe<Rational> maybe_value = ApproximateSimplex::estimateWithCFE(dval);
2065 if (!maybe_value)
2066 {
2067 return make_pair(NullConstraint, ARITHVAR_SENTINEL);
2068 }
2069 Rational fl(maybe_value.value().floor());
2070 pair<ConstraintP, ArithVar> p;
2071 p = replayGetConstraint(d_lhsTmp, kind::LEQ, fl, true);
2072 d_lhsTmp.purge();
2073 return p;
2074 }
2075 }
2076 return make_pair(NullConstraint, ARITHVAR_SENTINEL);
2077 }
2078
2079 std::pair<ConstraintP, ArithVar> TheoryArithPrivate::replayGetConstraint(const CutInfo& ci) {
2080 Assert(ci.reconstructed());
2081 const DenseMap<Rational>& lhs = ci.getReconstruction().lhs;
2082 const Rational& rhs = ci.getReconstruction().rhs;
2083 Kind k = ci.getKind();
2084
2085 return replayGetConstraint(lhs, k, rhs, ci.getKlass() == BranchCutKlass);
2086 }
2087
2088 // Node denseVectorToLiteral(const ArithVariables& vars, const DenseVector& dv, Kind k){
2089 // NodeManager* nm = NodeManager::currentNM();
2090 // Node sumLhs = toSumNode(vars, dv.lhs);
2091 // Node ineq = nm->mkNode(k, sumLhs, mkRationalNode(dv.rhs) );
2092 // Node lit = Rewriter::rewrite(ineq);
2093 // return lit;
2094 // }
2095
2096 Node toSumNode(const ArithVariables& vars, const DenseMap<Rational>& sum){
2097 Debug("arith::toSumNode") << "toSumNode() begin" << endl;
2098 NodeBuilder nb(kind::PLUS);
2099 NodeManager* nm = NodeManager::currentNM();
2100 DenseMap<Rational>::const_iterator iter, end;
2101 iter = sum.begin(), end = sum.end();
2102 for(; iter != end; ++iter){
2103 ArithVar x = *iter;
2104 if(!vars.hasNode(x)){ return Node::null(); }
2105 Node xNode = vars.asNode(x);
2106 const Rational& q = sum[x];
2107 Node mult = nm->mkNode(kind::MULT, mkRationalNode(q), xNode);
2108 Debug("arith::toSumNode") << "toSumNode() " << x << " " << mult << endl;
2109 nb << mult;
2110 }
2111 Debug("arith::toSumNode") << "toSumNode() end" << endl;
2112 return safeConstructNary(nb);
2113 }
2114
2115 ConstraintCP TheoryArithPrivate::vectorToIntHoleConflict(const ConstraintCPVec& conflict){
2116 Assert(conflict.size() >= 2);
2117 ConstraintCPVec exp(conflict.begin(), conflict.end()-1);
2118 ConstraintCP back = conflict.back();
2119 Assert(back->hasProof());
2120 ConstraintP negBack = back->getNegation();
2121 // This can select negBack multiple times so we need to test if negBack has a proof.
2122 if(negBack->hasProof()){
2123 // back is in conflict already
2124 } else {
2125 negBack->impliedByIntHole(exp, true);
2126 }
2127
2128 return back;
2129 }
2130
2131 void TheoryArithPrivate::intHoleConflictToVector(ConstraintCP conflicting, ConstraintCPVec& conflict){
2132 ConstraintCP negConflicting = conflicting->getNegation();
2133 Assert(conflicting->hasProof());
2134 Assert(negConflicting->hasProof());
2135
2136 conflict.push_back(conflicting);
2137 conflict.push_back(negConflicting);
2138
2139 Constraint::assertionFringe(conflict);
2140 }
2141
2142 void TheoryArithPrivate::tryBranchCut(ApproximateSimplex* approx, int nid, BranchCutInfo& bci){
2143 Assert(conflictQueueEmpty());
2144 std::vector< ConstraintCPVec > conflicts;
2145
2146 approx->tryCut(nid, bci);
2147 Debug("approx::branch") << "tryBranchCut" << bci << endl;
2148 Assert(bci.reconstructed());
2149 Assert(!bci.proven());
2150 pair<ConstraintP, ArithVar> p = replayGetConstraint(bci);
2151 Assert(p.second == ARITHVAR_SENTINEL);
2152 ConstraintP bc = p.first;
2153 Assert(bc != NullConstraint);
2154 if(bc->hasProof()){
2155 return;
2156 }
2157
2158 ConstraintP bcneg = bc->getNegation();
2159 {
2160 context::Context::ScopedPush speculativePush(getSatContext());
2161 replayAssert(bcneg);
2162 if(conflictQueueEmpty()){
2163 TimerStat::CodeTimer codeTimer(d_statistics.d_replaySimplexTimer);
2164
2165 //test for linear feasibility
2166 d_partialModel.stopQueueingBoundCounts();
2167 UpdateTrackingCallback utcb(&d_linEq);
2168 d_partialModel.processBoundsQueue(utcb);
2169 d_linEq.startTrackingBoundCounts();
2170
2171 SimplexDecisionProcedure& simplex = selectSimplex(true);
2172 simplex.findModel(false);
2173 // Can change d_qflraStatus
2174
2175 d_linEq.stopTrackingBoundCounts();
2176 d_partialModel.startQueueingBoundCounts();
2177 }
2178 for(size_t i = 0, N = d_conflicts.size(); i < N; ++i){
2179
2180 conflicts.push_back(ConstraintCPVec());
2181 intHoleConflictToVector(d_conflicts[i].first, conflicts.back());
2182 Constraint::assertionFringe(conflicts.back());
2183
2184 // ConstraintCP conflicting = d_conflicts[i];
2185 // ConstraintCP negConflicting = conflicting->getNegation();
2186 // Assert(conflicting->hasProof());
2187 // Assert(negConflicting->hasProof());
2188
2189 // conflicts.push_back(ConstraintCPVec());
2190 // ConstraintCPVec& back = conflicts.back();
2191 // back.push_back(conflicting);
2192 // back.push_back(negConflicting);
2193
2194 // // remove the floor/ceiling contraint implied by bcneg
2195 // Constraint::assertionFringe(back);
2196 }
2197
2198 if(Debug.isOn("approx::branch")){
2199 if(d_conflicts.empty()){
2200 entireStateIsConsistent("branchfailure");
2201 }
2202 }
2203 }
2204
2205 Debug("approx::branch") << "branch constraint " << bc << endl;
2206 for(size_t i = 0, N = conflicts.size(); i < N; ++i){
2207 ConstraintCPVec& conf = conflicts[i];
2208
2209 // make sure to be working on the assertion fringe!
2210 if(!contains(conf, bcneg)){
2211 Debug("approx::branch") << "reraise " << conf << endl;
2212 ConstraintCP conflicting = vectorToIntHoleConflict(conf);
2213 raiseConflict(conflicting, InferenceId::UNKNOWN);
2214 }else if(!bci.proven()){
2215 drop(conf, bcneg);
2216 bci.setExplanation(conf);
2217 Debug("approx::branch") << "dropped " << bci << endl;
2218 }
2219 }
2220 }
2221
2222 void TheoryArithPrivate::replayAssert(ConstraintP c) {
2223 if(!c->assertedToTheTheory()){
2224 bool inConflict = c->negationHasProof();
2225 if(!c->hasProof()){
2226 c->setInternalAssumption(inConflict);
2227 Debug("approx::replayAssert") << "replayAssert " << c << " set internal" << endl;
2228 }else{
2229 Debug("approx::replayAssert") << "replayAssert " << c << " has explanation" << endl;
2230 }
2231 Debug("approx::replayAssert") << "replayAssertion " << c << endl;
2232 if(inConflict){
2233 raiseConflict(c, InferenceId::UNKNOWN);
2234 }else{
2235 assertionCases(c);
2236 }
2237 }else{
2238 Debug("approx::replayAssert")
2239 << "replayAssert " << c << " already asserted" << endl;
2240 }
2241 }
2242
2243
2244 void TheoryArithPrivate::resolveOutPropagated(std::vector<ConstraintCPVec>& confs, const std::set<ConstraintCP>& propagated) const {
2245 Debug("arith::resolveOutPropagated")
2246 << "starting resolveOutPropagated() " << confs.size() << endl;
2247 for(size_t i =0, N = confs.size(); i < N; ++i){
2248 ConstraintCPVec& conf = confs[i];
2249 size_t orig = conf.size();
2250 Constraint::assertionFringe(conf);
2251 Debug("arith::resolveOutPropagated")
2252 << " conf["<<i<<"] " << orig << " to " << conf.size() << endl;
2253 }
2254 Debug("arith::resolveOutPropagated")
2255 << "ending resolveOutPropagated() " << confs.size() << endl;
2256 }
2257
2258 struct SizeOrd {
2259 bool operator()(const ConstraintCPVec& a, const ConstraintCPVec& b) const{
2260 return a.size() < b.size();
2261 }
2262 };
2263
2264 void TheoryArithPrivate::subsumption(
2265 std::vector<ConstraintCPVec> &confs) const {
2266 int checks CVC5_UNUSED = 0;
2267 int subsumed CVC5_UNUSED = 0;
2268
2269 for (size_t i = 0, N = confs.size(); i < N; ++i) {
2270 ConstraintCPVec &conf = confs[i];
2271 std::sort(conf.begin(), conf.end());
2272 }
2273
2274 std::sort(confs.begin(), confs.end(), SizeOrd());
2275 for (size_t i = 0; i < confs.size(); i++) {
2276 // i is not subsumed
2277 for (size_t j = i + 1; j < confs.size();) {
2278 ConstraintCPVec& a = confs[i];
2279 ConstraintCPVec& b = confs[j];
2280 checks++;
2281 bool subsumes = std::includes(a.begin(), a.end(), b.begin(), b.end());
2282 if (subsumes) {
2283 ConstraintCPVec& back = confs.back();
2284 b.swap(back);
2285 confs.pop_back();
2286 subsumed++;
2287 } else {
2288 j++;
2289 }
2290 }
2291 }
2292 Debug("arith::subsumption") << "subsumed " << subsumed << "/" << checks
2293 << endl;
2294 }
2295
2296 std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex* approx, int nid, ConstraintP bc, int depth){
2297 ++(d_statistics.d_replayLogRecCount);
2298 Debug("approx::replayLogRec") << "replayLogRec()" << std::endl;
2299
2300 size_t rpvars_size = d_replayVariables.size();
2301 size_t rpcons_size = d_replayConstraints.size();
2302 std::vector<ConstraintCPVec> res;
2303
2304 { /* create a block for the purpose of pushing the sat context */
2305 context::Context::ScopedPush speculativePush(getSatContext());
2306 Assert(!anyConflict());
2307 Assert(conflictQueueEmpty());
2308 set<ConstraintCP> propagated;
2309
2310 TreeLog& tl = getTreeLog();
2311
2312 if(bc != NullConstraint){
2313 replayAssert(bc);
2314 }
2315
2316 const NodeLog& nl = tl.getNode(nid);
2317 NodeLog::const_iterator iter = nl.begin(), end = nl.end();
2318 for(; conflictQueueEmpty() && iter != end; ++iter){
2319 CutInfo* ci = *iter;
2320 bool reject = false;
2321 //cout << " trying " << *ci << endl;
2322 if(ci->getKlass() == RowsDeletedKlass){
2323 RowsDeleted* rd = dynamic_cast<RowsDeleted*>(ci);
2324
2325 tl.applyRowsDeleted(nid, *rd);
2326 // The previous line modifies nl
2327
2328 ++d_statistics.d_applyRowsDeleted;
2329 }else if(ci->getKlass() == BranchCutKlass){
2330 BranchCutInfo* bci = dynamic_cast<BranchCutInfo*>(ci);
2331 Assert(bci != NULL);
2332 tryBranchCut(approx, nid, *bci);
2333
2334 ++d_statistics.d_branchCutsAttempted;
2335 if(!(conflictQueueEmpty() || ci->reconstructed())){
2336 ++d_statistics.d_numBranchesFailed;
2337 }
2338 }else{
2339 approx->tryCut(nid, *ci);
2340 if(ci->getKlass() == GmiCutKlass){
2341 ++d_statistics.d_gmiCutsAttempted;
2342 }else if(ci->getKlass() == MirCutKlass){
2343 ++d_statistics.d_mirCutsAttempted;
2344 }
2345
2346 if(ci->reconstructed() && ci->proven()){
2347 const DenseMap<Rational>& row = ci->getReconstruction().lhs;
2348 reject = !complexityBelow(row, options::replayRejectCutSize());
2349 }
2350 }
2351 if(conflictQueueEmpty()){
2352 if(reject){
2353 ++d_statistics.d_cutsRejectedDuringReplay;
2354 }else if(ci->reconstructed()){
2355 // success
2356 ++d_statistics.d_cutsReconstructed;
2357
2358 pair<ConstraintP, ArithVar> p = replayGetConstraint(*ci);
2359 if(p.second != ARITHVAR_SENTINEL){
2360 Assert(ci->getRowId() >= 1);
2361 tl.mapRowId(nl.getNodeId(), ci->getRowId(), p.second);
2362 }
2363 ConstraintP con = p.first;
2364 if(Debug.isOn("approx::replayLogRec")){
2365 Debug("approx::replayLogRec") << "cut was remade " << con << " " << *ci << endl;
2366 }
2367
2368 if(ci->proven()){
2369 ++d_statistics.d_cutsProven;
2370
2371 const ConstraintCPVec& exp = ci->getExplanation();
2372 // success
2373 if(con->isTrue()){
2374 Debug("approx::replayLogRec") << "not asserted?" << endl;
2375 }else if(!con->negationHasProof()){
2376 con->impliedByIntHole(exp, false);
2377 replayAssert(con);
2378 Debug("approx::replayLogRec") << "cut prop" << endl;
2379 }else {
2380 con->impliedByIntHole(exp, true);
2381 Debug("approx::replayLogRec") << "cut into conflict " << con << endl;
2382 raiseConflict(con, InferenceId::UNKNOWN);
2383 }
2384 }else{
2385 ++d_statistics.d_cutsProofFailed;
2386 Debug("approx::replayLogRec") << "failed to get proof " << *ci << endl;
2387 }
2388 }else if(ci->getKlass() != RowsDeletedKlass){
2389 ++d_statistics.d_cutsReconstructionFailed;
2390 }
2391 }
2392 }
2393
2394 /* check if the system is feasible under with the cuts */
2395 if(conflictQueueEmpty()){
2396 Assert(options::replayEarlyCloseDepths() >= 1);
2397 if(!nl.isBranch() || depth % options::replayEarlyCloseDepths() == 0 ){
2398 TimerStat::CodeTimer codeTimer(d_statistics.d_replaySimplexTimer);
2399 //test for linear feasibility
2400 d_partialModel.stopQueueingBoundCounts();
2401 UpdateTrackingCallback utcb(&d_linEq);
2402 d_partialModel.processBoundsQueue(utcb);
2403 d_linEq.startTrackingBoundCounts();
2404
2405 SimplexDecisionProcedure& simplex = selectSimplex(true);
2406 simplex.findModel(false);
2407 // can change d_qflraStatus
2408
2409 d_linEq.stopTrackingBoundCounts();
2410 d_partialModel.startQueueingBoundCounts();
2411 }
2412 }else{
2413 ++d_statistics.d_replayLogRecConflictEscalation;
2414 }
2415
2416 if(!conflictQueueEmpty()){
2417 /* if a conflict has been found stop */
2418 for(size_t i = 0, N = d_conflicts.size(); i < N; ++i){
2419 res.push_back(ConstraintCPVec());
2420 intHoleConflictToVector(d_conflicts[i].first, res.back());
2421 }
2422 ++d_statistics.d_replayLogRecEarlyExit;
2423 }else if(nl.isBranch()){
2424 /* if it is a branch try the branch */
2425 pair<ConstraintP, ArithVar> p = replayGetConstraint(approx, nl);
2426 Assert(p.second == ARITHVAR_SENTINEL);
2427 ConstraintP dnc = p.first;
2428 if(dnc != NullConstraint){
2429 ConstraintP upc = dnc->getNegation();
2430
2431 int dnid = nl.getDownId();
2432 int upid = nl.getUpId();
2433
2434 NodeLog& dnlog = tl.getNode(dnid);
2435 NodeLog& uplog = tl.getNode(upid);
2436 dnlog.copyParentRowIds();
2437 uplog.copyParentRowIds();
2438
2439 std::vector<ConstraintCPVec> dnres;
2440 std::vector<ConstraintCPVec> upres;
2441 std::vector<size_t> containsdn;
2442 std::vector<size_t> containsup;
2443 if(res.empty()){
2444 dnres = replayLogRec(approx, dnid, dnc, depth+1);
2445 for(size_t i = 0, N = dnres.size(); i < N; ++i){
2446 ConstraintCPVec& conf = dnres[i];
2447 if(contains(conf, dnc)){
2448 containsdn.push_back(i);
2449 }else{
2450 res.push_back(conf);
2451 }
2452 }
2453 }else{
2454 Debug("approx::replayLogRec") << "replayLogRec() skipping" << dnlog << std::endl;
2455 ++d_statistics.d_replayBranchSkips;
2456 }
2457
2458 if(res.empty()){
2459 upres = replayLogRec(approx, upid, upc, depth+1);
2460
2461 for(size_t i = 0, N = upres.size(); i < N; ++i){
2462 ConstraintCPVec& conf = upres[i];
2463 if(contains(conf, upc)){
2464 containsup.push_back(i);
2465 }else{
2466 res.push_back(conf);
2467 }
2468 }
2469 }else{
2470 Debug("approx::replayLogRec") << "replayLogRec() skipping" << uplog << std::endl;
2471 ++d_statistics.d_replayBranchSkips;
2472 }
2473
2474 if(res.empty()){
2475 for(size_t i = 0, N = containsdn.size(); i < N; ++i){
2476 ConstraintCPVec& dnconf = dnres[containsdn[i]];
2477 for(size_t j = 0, M = containsup.size(); j < M; ++j){
2478 ConstraintCPVec& upconf = upres[containsup[j]];
2479
2480 res.push_back(ConstraintCPVec());
2481 ConstraintCPVec& back = res.back();
2482 resolve(back, dnc, dnconf, upconf);
2483 }
2484 }
2485 if(res.size() >= 2u){
2486 subsumption(res);
2487
2488 if(res.size() > 100u){
2489 res.resize(100u);
2490 }
2491 }
2492 }else{
2493 Debug("approx::replayLogRec") << "replayLogRec() skipping resolving" << nl << std::endl;
2494 }
2495 Debug("approx::replayLogRec") << "found #"<<res.size()<<" conflicts on branch " << nid << endl;
2496 if(res.empty()){
2497 ++d_statistics.d_replayBranchCloseFailures;
2498 }
2499
2500 }else{
2501 Debug("approx::replayLogRec") << "failed to make a branch " << nid << endl;
2502 }
2503 }else{
2504 ++d_statistics.d_replayLeafCloseFailures;
2505 Debug("approx::replayLogRec") << "failed on node " << nid << endl;
2506 Assert(res.empty());
2507 }
2508 resolveOutPropagated(res, propagated);
2509 Debug("approx::replayLogRec") << "replayLogRec() ending" << std::endl;
2510
2511
2512 if(options::replayFailureLemma()){
2513 // must be done inside the sat context to get things
2514 // propagated at this level
2515 if(res.empty() && nid == getTreeLog().getRootId()){
2516 Assert(!d_replayedLemmas);
2517 d_replayedLemmas = replayLemmas(approx);
2518 Assert(d_acTmp.empty());
2519 while(!d_approxCuts.empty()){
2520 TrustNode lem = d_approxCuts.front();
2521 d_approxCuts.pop();
2522 d_acTmp.push_back(lem);
2523 }
2524 }
2525 }
2526 } /* pop the sat context */
2527
2528 /* move into the current context. */
2529 while(!d_acTmp.empty()){
2530 TrustNode lem = d_acTmp.back();
2531 d_acTmp.pop_back();
2532 d_approxCuts.push_back(lem);
2533 }
2534 Assert(d_acTmp.empty());
2535
2536 /* Garbage collect the constraints from this call */
2537 while(d_replayConstraints.size() > rpcons_size){
2538 ConstraintP c = d_replayConstraints.back();
2539 d_replayConstraints.pop_back();
2540 d_constraintDatabase.deleteConstraintAndNegation(c);
2541 }
2542
2543 /* Garbage collect the ArithVars made by this call */
2544 if(d_replayVariables.size() > rpvars_size){
2545 d_partialModel.stopQueueingBoundCounts();
2546 UpdateTrackingCallback utcb(&d_linEq);
2547 d_partialModel.processBoundsQueue(utcb);
2548 d_linEq.startTrackingBoundCounts();
2549 while(d_replayVariables.size() > rpvars_size){
2550 ArithVar v = d_replayVariables.back();
2551 d_replayVariables.pop_back();
2552 Assert(d_partialModel.canBeReleased(v));
2553 if(!d_tableau.isBasic(v)){
2554 /* if it is not basic make it basic. */
2555 ArithVar b = ARITHVAR_SENTINEL;
2556 for(Tableau::ColIterator ci = d_tableau.colIterator(v); !ci.atEnd(); ++ci){
2557 const Tableau::Entry& e = *ci;
2558 b = d_tableau.rowIndexToBasic(e.getRowIndex());
2559 break;
2560 }
2561 Assert(b != ARITHVAR_SENTINEL);
2562 DeltaRational cp = d_partialModel.getAssignment(b);
2563 if(d_partialModel.cmpAssignmentLowerBound(b) < 0){
2564 cp = d_partialModel.getLowerBound(b);
2565 }else if(d_partialModel.cmpAssignmentUpperBound(b) > 0){
2566 cp = d_partialModel.getUpperBound(b);
2567 }
2568 d_linEq.pivotAndUpdate(b, v, cp);
2569 }
2570 Assert(d_tableau.isBasic(v));
2571 d_linEq.stopTrackingRowIndex(d_tableau.basicToRowIndex(v));
2572 d_tableau.removeBasicRow(v);
2573
2574 releaseArithVar(v);
2575 Debug("approx::vars") << "releasing " << v << endl;
2576 }
2577 d_linEq.stopTrackingBoundCounts();
2578 d_partialModel.startQueueingBoundCounts();
2579 d_partialModel.attemptToReclaimReleased();
2580 }
2581 return res;
2582 }
2583
2584 TreeLog& TheoryArithPrivate::getTreeLog(){
2585 if(d_treeLog == NULL){
2586 d_treeLog = new TreeLog();
2587 }
2588 return *d_treeLog;
2589 }
2590
2591 ApproximateStatistics& TheoryArithPrivate::getApproxStats(){
2592 if(d_approxStats == NULL){
2593 d_approxStats = new ApproximateStatistics();
2594 }
2595 return *d_approxStats;
2596 }
2597
2598 Node TheoryArithPrivate::branchToNode(ApproximateSimplex* approx,
2599 const NodeLog& bn) const
2600 {
2601 Assert(bn.isBranch());
2602 ArithVar v = approx->getBranchVar(bn);
2603 if(v != ARITHVAR_SENTINEL && d_partialModel.isIntegerInput(v)){
2604 if(d_partialModel.hasNode(v)){
2605 Node n = d_partialModel.asNode(v);
2606 double dval = bn.branchValue();
2607 Maybe<Rational> maybe_value = ApproximateSimplex::estimateWithCFE(dval);
2608 if (!maybe_value)
2609 {
2610 return Node::null();
2611 }
2612 Rational fl(maybe_value.value().floor());
2613 NodeManager* nm = NodeManager::currentNM();
2614 Node leq = nm->mkNode(kind::LEQ, n, mkRationalNode(fl));
2615 Node norm = Rewriter::rewrite(leq);
2616 return norm;
2617 }
2618 }
2619 return Node::null();
2620 }
2621
2622 Node TheoryArithPrivate::cutToLiteral(ApproximateSimplex* approx, const CutInfo& ci) const{
2623 Assert(ci.reconstructed());
2624
2625 const DenseMap<Rational>& lhs = ci.getReconstruction().lhs;
2626 Node sum = toSumNode(d_partialModel, lhs);
2627 if(!sum.isNull()){
2628 Kind k = ci.getKind();
2629 Assert(k == kind::LEQ || k == kind::GEQ);
2630 Node rhs = mkRationalNode(ci.getReconstruction().rhs);
2631
2632 NodeManager* nm = NodeManager::currentNM();
2633 Node ineq = nm->mkNode(k, sum, rhs);
2634 return Rewriter::rewrite(ineq);
2635 }
2636 return Node::null();
2637 }
2638
2639 bool TheoryArithPrivate::replayLemmas(ApproximateSimplex* approx){
2640 ++(d_statistics.d_mipReplayLemmaCalls);
2641 bool anythingnew = false;
2642
2643 TreeLog& tl = getTreeLog();
2644 NodeLog& root = tl.getRootNode();
2645 root.applySelected(); /* set row ids */
2646
2647 vector<const CutInfo*> cuts = approx->getValidCuts(root);
2648 for(size_t i =0, N =cuts.size(); i < N; ++i){
2649 const CutInfo* cut = cuts[i];
2650 Assert(cut->reconstructed());
2651 Assert(cut->proven());
2652
2653 const DenseMap<Rational>& row = cut->getReconstruction().lhs;
2654 if(!complexityBelow(row, options::lemmaRejectCutSize())){
2655 ++(d_statistics.d_cutsRejectedDuringLemmas);
2656 continue;
2657 }
2658
2659 Node cutConstraint = cutToLiteral(approx, *cut);
2660 if(!cutConstraint.isNull()){
2661 const ConstraintCPVec& exp = cut->getExplanation();
2662 Node asLemma = Constraint::externalExplainByAssertions(exp);
2663
2664 Node implied = Rewriter::rewrite(cutConstraint);
2665 anythingnew = anythingnew || !isSatLiteral(implied);
2666
2667 Node implication = asLemma.impNode(implied);
2668 // DO NOT CALL OUTPUT LEMMA!
2669 // TODO (project #37): justify
2670 d_approxCuts.push_back(TrustNode::mkTrustLemma(implication, nullptr));
2671 Debug("approx::lemmas") << "cut["<<i<<"] " << implication << endl;
2672 ++(d_statistics.d_mipExternalCuts);
2673 }
2674 }
2675 if(root.isBranch()){
2676 Node lit = branchToNode(approx, root);
2677 if(!lit.isNull()){
2678 anythingnew = anythingnew || !isSatLiteral(lit);
2679 Node branch = lit.orNode(lit.notNode());
2680 if (proofsEnabled())
2681 {
2682 d_pfGen->mkTrustNode(branch, PfRule::SPLIT, {}, {lit});
2683 }
2684 else
2685 {
2686 d_approxCuts.push_back(TrustNode::mkTrustLemma(branch, nullptr));
2687 }
2688 ++(d_statistics.d_mipExternalBranch);
2689 Debug("approx::lemmas") << "branching "<< root <<" as " << branch << endl;
2690 }
2691 }
2692 return anythingnew;
2693 }
2694
2695 void TheoryArithPrivate::turnOffApproxFor(int32_t rounds){
2696 d_attemptSolveIntTurnedOff = d_attemptSolveIntTurnedOff + rounds;
2697 ++(d_statistics.d_approxDisabled);
2698 }
2699
2700 bool TheoryArithPrivate::safeToCallApprox() const{
2701 unsigned numRows = 0;
2702 unsigned numCols = 0;
2703 var_iterator vi = var_begin(), vi_end = var_end();
2704 // Assign each variable to a row and column variable as it appears in the input
2705 for(; vi != vi_end && !(numRows > 0 && numCols > 0); ++vi){
2706 ArithVar v = *vi;
2707
2708 if(d_partialModel.isAuxiliary(v)){
2709 ++numRows;
2710 }else{
2711 ++numCols;
2712 }
2713 }
2714 return (numRows > 0 && numCols > 0);
2715 }
2716
2717 // solve()
2718 // res = solveRealRelaxation(effortLevel);
2719 // switch(res){
2720 // case LinFeas:
2721 // case LinInfeas:
2722 // return replay()
2723 // case Unknown:
2724 // case Error
2725 // if()
2726 void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){
2727 if(!safeToCallApprox()) { return; }
2728
2729 Assert(safeToCallApprox());
2730 TimerStat::CodeTimer codeTimer0(d_statistics.d_solveIntTimer);
2731
2732 ++(d_statistics.d_solveIntCalls);
2733 d_statistics.d_inSolveInteger = 1;
2734
2735 if(!Theory::fullEffort(effortLevel)){
2736 d_solveIntAttempts++;
2737 ++(d_statistics.d_solveStandardEffort);
2738 }
2739
2740 // if integers are attempted,
2741 Assert(options::useApprox());
2742 Assert(ApproximateSimplex::enabled());
2743
2744 int level = getSatContext()->getLevel();
2745 d_lastContextIntegerAttempted = level;
2746
2747
2748 static const int32_t mipLimit = 200000;
2749
2750 TreeLog& tl = getTreeLog();
2751 ApproximateStatistics& stats = getApproxStats();
2752 ApproximateSimplex* approx =
2753 ApproximateSimplex::mkApproximateSimplexSolver(d_partialModel, tl, stats);
2754
2755 approx->setPivotLimit(mipLimit);
2756 if(!d_guessedCoeffSet){
2757 d_guessedCoeffs = approx->heuristicOptCoeffs();
2758 d_guessedCoeffSet = true;
2759 }
2760 if(!d_guessedCoeffs.empty()){
2761 approx->setOptCoeffs(d_guessedCoeffs);
2762 }
2763 static const int32_t depthForLikelyInfeasible = 10;
2764 int maxDepthPass1 = d_likelyIntegerInfeasible ?
2765 depthForLikelyInfeasible : options::maxApproxDepth();
2766 approx->setBranchingDepth(maxDepthPass1);
2767 approx->setBranchOnVariableLimit(100);
2768 LinResult relaxRes = approx->solveRelaxation();
2769 if( relaxRes == LinFeasible ){
2770 MipResult mipRes = MipUnknown;
2771 {
2772 TimerStat::CodeTimer codeTimer1(d_statistics.d_mipTimer);
2773 mipRes = approx->solveMIP(false);
2774 }
2775
2776 Debug("arith::solveInteger") << "mipRes " << mipRes << endl;
2777 switch(mipRes) {
2778 case MipBingo:
2779 // attempt the solution
2780 {
2781 ++(d_statistics.d_solveIntModelsAttempts);
2782
2783 d_partialModel.stopQueueingBoundCounts();
2784 UpdateTrackingCallback utcb(&d_linEq);
2785 d_partialModel.processBoundsQueue(utcb);
2786 d_linEq.startTrackingBoundCounts();
2787
2788 ApproximateSimplex::Solution mipSolution;
2789 mipSolution = approx->extractMIP();
2790 importSolution(mipSolution);
2791 solveRelaxationOrPanic(effortLevel);
2792
2793 if (d_qflraStatus == Result::SAT)
2794 {
2795 if (!anyConflict())
2796 {
2797 if (ARITHVAR_SENTINEL == nextIntegerViolation(false))
2798 {
2799 ++(d_statistics.d_solveIntModelsSuccessful);
2800 }
2801 }
2802 }
2803
2804 // shutdown simplex
2805 d_linEq.stopTrackingBoundCounts();
2806 d_partialModel.startQueueingBoundCounts();
2807 }
2808 break;
2809 case MipClosed:
2810 /* All integer branches closed */
2811 approx->setPivotLimit(2*mipLimit);
2812 {
2813 TimerStat::CodeTimer codeTimer2(d_statistics.d_mipTimer);
2814 mipRes = approx->solveMIP(true);
2815 }
2816
2817 if(mipRes == MipClosed){
2818 d_likelyIntegerInfeasible = true;
2819 replayLog(approx);
2820 AlwaysAssert(anyConflict() || d_qflraStatus != Result::SAT);
2821
2822 if (!anyConflict())
2823 {
2824 solveRealRelaxation(effortLevel);
2825 }
2826 }
2827 if(!(anyConflict() || !d_approxCuts.empty())){
2828 turnOffApproxFor(options::replayNumericFailurePenalty());
2829 }
2830 break;
2831 case BranchesExhausted:
2832 case ExecExhausted:
2833 case PivotsExhauasted:
2834 if(mipRes == BranchesExhausted){
2835 ++d_statistics.d_branchesExhausted;
2836 }else if(mipRes == ExecExhausted){
2837 ++d_statistics.d_execExhausted;
2838 }else if(mipRes == PivotsExhauasted){
2839 ++d_statistics.d_pivotsExhausted;
2840 }
2841
2842 approx->setPivotLimit(2*mipLimit);
2843 approx->setBranchingDepth(2);
2844 {
2845 TimerStat::CodeTimer codeTimer3(d_statistics.d_mipTimer);
2846 mipRes = approx->solveMIP(true);
2847 }
2848 replayLemmas(approx);
2849 break;
2850 case MipUnknown:
2851 break;
2852 }
2853 }
2854 delete approx;
2855
2856 if(!Theory::fullEffort(effortLevel)){
2857 if(anyConflict() || !d_approxCuts.empty()){
2858 d_solveIntMaybeHelp++;
2859 }
2860 }
2861
2862 d_statistics.d_inSolveInteger = 0;
2863 }
2864
2865 SimplexDecisionProcedure& TheoryArithPrivate::selectSimplex(bool pass1){
2866 if(pass1){
2867 if(d_pass1SDP == NULL){
2868 if(options::useFC()){
2869 d_pass1SDP = (SimplexDecisionProcedure*)(&d_fcSimplex);
2870 }else if(options::useSOI()){
2871 d_pass1SDP = (SimplexDecisionProcedure*)(&d_soiSimplex);
2872 }else{
2873 d_pass1SDP = (SimplexDecisionProcedure*)(&d_dualSimplex);
2874 }
2875 }
2876 Assert(d_pass1SDP != NULL);
2877 return *d_pass1SDP;
2878 }else{
2879 if(d_otherSDP == NULL){
2880 if(options::useFC()){
2881 d_otherSDP = (SimplexDecisionProcedure*)(&d_fcSimplex);
2882 }else if(options::useSOI()){
2883 d_otherSDP = (SimplexDecisionProcedure*)(&d_soiSimplex);
2884 }else{
2885 d_otherSDP = (SimplexDecisionProcedure*)(&d_soiSimplex);
2886 }
2887 }
2888 Assert(d_otherSDP != NULL);
2889 return *d_otherSDP;
2890 }
2891 }
2892
2893 void TheoryArithPrivate::importSolution(const ApproximateSimplex::Solution& solution){
2894 if(Debug.isOn("arith::importSolution")){
2895 Debug("arith::importSolution") << "importSolution before " << d_qflraStatus << endl;
2896 d_partialModel.printEntireModel(Debug("arith::importSolution"));
2897 }
2898
2899 d_qflraStatus = d_attemptSolSimplex.attempt(solution);
2900
2901 if(Debug.isOn("arith::importSolution")){
2902 Debug("arith::importSolution") << "importSolution intermediate " << d_qflraStatus << endl;
2903 d_partialModel.printEntireModel(Debug("arith::importSolution"));
2904 }
2905
2906 if(d_qflraStatus != Result::UNSAT){
2907 static const int32_t pass2Limit = 20;
2908 int16_t oldCap = options::arithStandardCheckVarOrderPivots();
2909 Options::current().set(options::arithStandardCheckVarOrderPivots, pass2Limit);
2910 SimplexDecisionProcedure& simplex = selectSimplex(false);
2911 d_qflraStatus = simplex.findModel(false);
2912 Options::current().set(options::arithStandardCheckVarOrderPivots, oldCap);
2913 }
2914
2915 if(Debug.isOn("arith::importSolution")){
2916 Debug("arith::importSolution") << "importSolution after " << d_qflraStatus << endl;
2917 d_partialModel.printEntireModel(Debug("arith::importSolution"));
2918 }
2919 }
2920
2921 bool TheoryArithPrivate::solveRelaxationOrPanic(Theory::Effort effortLevel)
2922 {
2923 // if at this point the linear relaxation is still unknown,
2924 // attempt to branch an integer variable as a last ditch effort on full check
2925 if (d_qflraStatus == Result::SAT_UNKNOWN)
2926 {
2927 d_qflraStatus = selectSimplex(true).findModel(false);
2928 }
2929
2930 if (Theory::fullEffort(effortLevel) && d_qflraStatus == Result::SAT_UNKNOWN)
2931 {
2932 ArithVar canBranch = nextIntegerViolation(false);
2933 if (canBranch != ARITHVAR_SENTINEL)
2934 {
2935 ++d_statistics.d_panicBranches;
2936 TrustNode branch = branchIntegerVariable(canBranch);
2937 Assert(branch.getNode().getKind() == kind::OR);
2938 Node rwbranch = Rewriter::rewrite(branch.getNode()[0]);
2939 if (!isSatLiteral(rwbranch))
2940 {
2941 d_approxCuts.push_back(branch);
2942 return true;
2943 }
2944 }
2945 d_qflraStatus = selectSimplex(false).findModel(true);
2946 }
2947 return false;
2948 }
2949
2950 bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
2951 TimerStat::CodeTimer codeTimer0(d_statistics.d_solveRealRelaxTimer);
2952 Assert(d_qflraStatus != Result::SAT);
2953
2954 d_partialModel.stopQueueingBoundCounts();
2955 UpdateTrackingCallback utcb(&d_linEq);
2956 d_partialModel.processBoundsQueue(utcb);
2957 d_linEq.startTrackingBoundCounts();
2958
2959 bool noPivotLimit = Theory::fullEffort(effortLevel) ||
2960 !options::restrictedPivots();
2961
2962 SimplexDecisionProcedure& simplex = selectSimplex(true);
2963
2964 bool useApprox = options::useApprox() && ApproximateSimplex::enabled() && getSolveIntegerResource();
2965
2966 Debug("TheoryArithPrivate::solveRealRelaxation")
2967 << "solveRealRelaxation() approx"
2968 << " " << options::useApprox()
2969 << " " << ApproximateSimplex::enabled()
2970 << " " << useApprox
2971 << " " << safeToCallApprox()
2972 << endl;
2973
2974 bool noPivotLimitPass1 = noPivotLimit && !useApprox;
2975 d_qflraStatus = simplex.findModel(noPivotLimitPass1);
2976
2977 Debug("TheoryArithPrivate::solveRealRelaxation")
2978 << "solveRealRelaxation()" << " pass1 " << d_qflraStatus << endl;
2979
2980 if(d_qflraStatus == Result::SAT_UNKNOWN && useApprox && safeToCallApprox()){
2981 // pass2: fancy-final
2982 static const int32_t relaxationLimit = 10000;
2983 Assert(ApproximateSimplex::enabled());
2984
2985 TreeLog& tl = getTreeLog();
2986 ApproximateStatistics& stats = getApproxStats();
2987 ApproximateSimplex* approxSolver =
2988 ApproximateSimplex::mkApproximateSimplexSolver(d_partialModel, tl, stats);
2989
2990 approxSolver->setPivotLimit(relaxationLimit);
2991
2992 if(!d_guessedCoeffSet){
2993 d_guessedCoeffs = approxSolver->heuristicOptCoeffs();
2994 d_guessedCoeffSet = true;
2995 }
2996 if(!d_guessedCoeffs.empty()){
2997 approxSolver->setOptCoeffs(d_guessedCoeffs);
2998 }
2999
3000 ++d_statistics.d_relaxCalls;
3001
3002 ApproximateSimplex::Solution relaxSolution;
3003 LinResult relaxRes = LinUnknown;
3004 {
3005 TimerStat::CodeTimer codeTimer1(d_statistics.d_lpTimer);
3006 relaxRes = approxSolver->solveRelaxation();
3007 }
3008 Debug("solveRealRelaxation") << "solve relaxation? " << endl;
3009 switch(relaxRes){
3010 case LinFeasible:
3011 Debug("solveRealRelaxation") << "lin feasible? " << endl;
3012 ++d_statistics.d_relaxLinFeas;
3013 relaxSolution = approxSolver->extractRelaxation();
3014 importSolution(relaxSolution);
3015 if(d_qflraStatus != Result::SAT){
3016 ++d_statistics.d_relaxLinFeasFailures;
3017 }
3018 break;
3019 case LinInfeasible:
3020 // todo attempt to recreate approximate conflict
3021 ++d_statistics.d_relaxLinInfeas;
3022 Debug("solveRealRelaxation") << "lin infeasible " << endl;
3023 relaxSolution = approxSolver->extractRelaxation();
3024 importSolution(relaxSolution);
3025 if(d_qflraStatus != Result::UNSAT){
3026 ++d_statistics.d_relaxLinInfeasFailures;
3027 }
3028 break;
3029 case LinExhausted:
3030 ++d_statistics.d_relaxLinExhausted;
3031 Debug("solveRealRelaxation") << "exhuasted " << endl;
3032 break;
3033 case LinUnknown:
3034 default:
3035 ++d_statistics.d_relaxOthers;
3036 break;
3037 }
3038 delete approxSolver;
3039
3040 }
3041
3042 bool emmittedConflictOrSplit = solveRelaxationOrPanic(effortLevel);
3043
3044 // TODO Save zeroes with no conflicts
3045 d_linEq.stopTrackingBoundCounts();
3046 d_partialModel.startQueueingBoundCounts();
3047
3048 return emmittedConflictOrSplit;
3049 }
3050
3051 bool TheoryArithPrivate::hasFreshArithLiteral(Node n) const{
3052 switch(n.getKind()){
3053 case kind::LEQ:
3054 case kind::GEQ:
3055 case kind::GT:
3056 case kind::LT:
3057 return !isSatLiteral(n);
3058 case kind::EQUAL:
3059 if(n[0].getType().isReal()){
3060 return !isSatLiteral(n);
3061 }else if(n[0].getType().isBoolean()){
3062 return hasFreshArithLiteral(n[0]) ||
3063 hasFreshArithLiteral(n[1]);
3064 }else{
3065 return false;
3066 }
3067 case kind::IMPLIES:
3068 // try the rhs first
3069 return hasFreshArithLiteral(n[1]) ||
3070 hasFreshArithLiteral(n[0]);
3071 default:
3072 if(n.getType().isBoolean()){
3073 for(Node::iterator ni=n.begin(), nend=n.end(); ni!=nend; ++ni){
3074 Node child = *ni;
3075 if(hasFreshArithLiteral(child)){
3076 return true;
3077 }
3078 }
3079 }
3080 return false;
3081 }
3082 }
3083
3084 bool TheoryArithPrivate::preCheck(Theory::Effort level)
3085 {
3086 Assert(d_currentPropagationList.empty());
3087 if(Debug.isOn("arith::consistency")){
3088 Assert(unenqueuedVariablesAreConsistent());
3089 }
3090
3091 d_newFacts = !done();
3092 // If d_previousStatus == SAT, then reverts on conflicts are safe
3093 // Otherwise, they are not and must be committed.
3094 d_previousStatus = d_qflraStatus;
3095 if (d_newFacts)
3096 {
3097 d_qflraStatus = Result::SAT_UNKNOWN;
3098 d_hasDoneWorkSinceCut = true;
3099 }
3100 return false;
3101 }
3102
3103 void TheoryArithPrivate::preNotifyFact(TNode atom, bool pol, TNode fact)
3104 {
3105 ConstraintP curr = constraintFromFactQueue(fact);
3106 if (curr != NullConstraint)
3107 {
3108 bool res CVC5_UNUSED = assertionCases(curr);
3109 Assert(!res || anyConflict());
3110 }
3111 }
3112
3113 bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
3114 {
3115 if(!anyConflict()){
3116 while(!d_learnedBounds.empty()){
3117 // we may attempt some constraints twice. this is okay!
3118 ConstraintP curr = d_learnedBounds.front();
3119 d_learnedBounds.pop();
3120 Debug("arith::learned") << curr << endl;
3121
3122 bool res CVC5_UNUSED = assertionCases(curr);
3123 Assert(!res || anyConflict());
3124
3125 if(anyConflict()){ break; }
3126 }
3127 }
3128
3129 if(anyConflict()){
3130 d_qflraStatus = Result::UNSAT;
3131 if (options::revertArithModels() && d_previousStatus == Result::SAT)
3132 {
3133 ++d_statistics.d_revertsOnConflicts;
3134 Debug("arith::bt") << "clearing here "
3135 << " " << d_newFacts << " " << d_previousStatus << " "
3136 << d_qflraStatus << endl;
3137 revertOutOfConflict();
3138 d_errorSet.clear();
3139 }else{
3140 ++d_statistics.d_commitsOnConflicts;
3141 Debug("arith::bt") << "committing here "
3142 << " " << d_newFacts << " " << d_previousStatus << " "
3143 << d_qflraStatus << endl;
3144 d_partialModel.commitAssignmentChanges();
3145 revertOutOfConflict();
3146 }
3147 outputConflicts();
3148 //cout << "unate conflict 1 " << effortLevel << std::endl;
3149 return true;
3150 }
3151
3152
3153 if(Debug.isOn("arith::print_assertions")) {
3154 debugPrintAssertions(Debug("arith::print_assertions"));
3155 }
3156
3157 bool emmittedConflictOrSplit = false;
3158 Assert(d_conflicts.empty());
3159
3160 bool useSimplex = d_qflraStatus != Result::SAT;
3161 Debug("arith::ems") << "ems: " << emmittedConflictOrSplit
3162 << "pre realRelax" << endl;
3163
3164 if(useSimplex){
3165 emmittedConflictOrSplit = solveRealRelaxation(effortLevel);
3166 }
3167 Debug("arith::ems") << "ems: " << emmittedConflictOrSplit
3168 << "post realRelax" << endl;
3169
3170
3171 Debug("arith::ems") << "ems: " << emmittedConflictOrSplit
3172 << "pre solveInteger" << endl;
3173
3174 if(attemptSolveInteger(effortLevel, emmittedConflictOrSplit)){
3175 solveInteger(effortLevel);
3176 if(anyConflict()){
3177 ++d_statistics.d_commitsOnConflicts;
3178 Debug("arith::bt") << "committing here "
3179 << " " << d_newFacts << " " << d_previousStatus << " "
3180 << d_qflraStatus << endl;
3181 revertOutOfConflict();
3182 d_errorSet.clear();
3183 outputConflicts();
3184 return true;
3185 }
3186 }
3187
3188 Debug("arith::ems") << "ems: " << emmittedConflictOrSplit
3189 << "post solveInteger" << endl;
3190
3191 switch(d_qflraStatus){
3192 case Result::SAT:
3193 if (d_newFacts)
3194 {
3195 ++d_statistics.d_nontrivialSatChecks;
3196 }
3197
3198 Debug("arith::bt") << "committing sap inConflit"
3199 << " " << d_newFacts << " " << d_previousStatus << " "
3200 << d_qflraStatus << endl;
3201 d_partialModel.commitAssignmentChanges();
3202 d_unknownsInARow = 0;
3203 if(Debug.isOn("arith::consistency")){
3204 Assert(entireStateIsConsistent("sat comit"));
3205 }
3206 if(useSimplex && options::collectPivots()){
3207 if(options::useFC()){
3208 d_statistics.d_satPivots << d_fcSimplex.getPivots();
3209 }else{
3210 d_statistics.d_satPivots << d_dualSimplex.getPivots();
3211 }
3212 }
3213 break;
3214 case Result::SAT_UNKNOWN:
3215 ++d_unknownsInARow;
3216 ++(d_statistics.d_unknownChecks);
3217 Assert(!Theory::fullEffort(effortLevel));
3218 Debug("arith::bt") << "committing unknown"
3219 << " " << d_newFacts << " " << d_previousStatus << " "
3220 << d_qflraStatus << endl;
3221 d_partialModel.commitAssignmentChanges();
3222 d_statistics.d_maxUnknownsInARow.maxAssign(d_unknownsInARow);
3223
3224 if(useSimplex && options::collectPivots()){
3225 if(options::useFC()){
3226 d_statistics.d_unknownPivots << d_fcSimplex.getPivots();
3227 }else{
3228 d_statistics.d_unknownPivots << d_dualSimplex.getPivots();
3229 }
3230 }
3231 break;
3232 case Result::UNSAT:
3233 d_unknownsInARow = 0;
3234
3235 ++d_statistics.d_commitsOnConflicts;
3236
3237 Debug("arith::bt") << "committing on conflict"
3238 << " " << d_newFacts << " " << d_previousStatus << " "
3239 << d_qflraStatus << endl;
3240 d_partialModel.commitAssignmentChanges();
3241 revertOutOfConflict();
3242
3243 if(Debug.isOn("arith::consistency::comitonconflict")){
3244 entireStateIsConsistent("commit on conflict");
3245 }
3246 outputConflicts();
3247 emmittedConflictOrSplit = true;
3248 Debug("arith::conflict") << "simplex conflict" << endl;
3249
3250 if(useSimplex && options::collectPivots()){
3251 if(options::useFC()){
3252 d_statistics.d_unsatPivots << d_fcSimplex.getPivots();
3253 }else{
3254 d_statistics.d_unsatPivots << d_dualSimplex.getPivots();
3255 }
3256 }
3257 break;
3258 default:
3259 Unimplemented();
3260 }
3261 d_statistics.d_avgUnknownsInARow << d_unknownsInARow;
3262
3263 size_t nPivots =
3264 options::useFC() ? d_fcSimplex.getPivots() : d_dualSimplex.getPivots();
3265 for (std::size_t i = 0; i < nPivots; ++i)
3266 {
3267 d_containing.d_out->spendResource(
3268 Resource::ArithPivotStep);
3269 }
3270
3271 Debug("arith::ems") << "ems: " << emmittedConflictOrSplit
3272 << "pre approx cuts" << endl;
3273 if(!d_approxCuts.empty()){
3274 bool anyFresh = false;
3275 while(!d_approxCuts.empty()){
3276 TrustNode lem = d_approxCuts.front();
3277 d_approxCuts.pop();
3278 Debug("arith::approx::cuts") << "approximate cut:" << lem << endl;
3279 anyFresh = anyFresh || hasFreshArithLiteral(lem.getNode());
3280 Debug("arith::lemma") << "approximate cut:" << lem << endl;
3281 outputTrustedLemma(lem, InferenceId::ARITH_APPROX_CUT);
3282 }
3283 if(anyFresh){
3284 emmittedConflictOrSplit = true;
3285 }
3286 }
3287
3288 Debug("arith::ems") << "ems: " << emmittedConflictOrSplit
3289 << "post approx cuts" << endl;
3290
3291 // This should be fine if sat or unknown
3292 if (!emmittedConflictOrSplit
3293 && (options::arithPropagationMode()
3294 == options::ArithPropagationMode::UNATE_PROP
3295 || options::arithPropagationMode()
3296 == options::ArithPropagationMode::BOTH_PROP))
3297 {
3298 TimerStat::CodeTimer codeTimer0(d_statistics.d_newPropTime);
3299 Assert(d_qflraStatus != Result::UNSAT);
3300
3301 while(!d_currentPropagationList.empty() && !anyConflict()){
3302 ConstraintP curr = d_currentPropagationList.front();
3303 d_currentPropagationList.pop_front();
3304
3305 ConstraintType t = curr->getType();
3306 Assert(t != Disequality)
3307 << "Disequalities are not allowed in d_currentPropagation";
3308
3309 switch(t){
3310 case LowerBound:
3311 {
3312 ConstraintP prev = d_currentPropagationList.front();
3313 d_currentPropagationList.pop_front();
3314 d_constraintDatabase.unatePropLowerBound(curr, prev);
3315 break;
3316 }
3317 case UpperBound:
3318 {
3319 ConstraintP prev = d_currentPropagationList.front();
3320 d_currentPropagationList.pop_front();
3321 d_constraintDatabase.unatePropUpperBound(curr, prev);
3322 break;
3323 }
3324 case Equality:
3325 {
3326 ConstraintP prevLB = d_currentPropagationList.front();
3327 d_currentPropagationList.pop_front();
3328 ConstraintP prevUB = d_currentPropagationList.front();
3329 d_currentPropagationList.pop_front();
3330 d_constraintDatabase.unatePropEquality(curr, prevLB, prevUB);
3331 break;
3332 }
3333 default: Unhandled() << curr->getType();
3334 }
3335 }
3336
3337 if(anyConflict()){
3338 Debug("arith::unate") << "unate conflict" << endl;
3339 revertOutOfConflict();
3340 d_qflraStatus = Result::UNSAT;
3341 outputConflicts();
3342 emmittedConflictOrSplit = true;
3343 //cout << "unate conflict " << endl;
3344 Debug("arith::bt") << "committing on unate conflict"
3345 << " " << d_newFacts << " " << d_previousStatus << " "
3346 << d_qflraStatus << endl;
3347
3348 Debug("arith::conflict") << "unate arith conflict" << endl;
3349 }
3350 }
3351 else
3352 {
3353 TimerStat::CodeTimer codeTimer1(d_statistics.d_newPropTime);
3354 d_currentPropagationList.clear();
3355 }
3356 Assert(d_currentPropagationList.empty());
3357
3358 Debug("arith::ems") << "ems: " << emmittedConflictOrSplit
3359 << "post unate" << endl;
3360
3361 if(!emmittedConflictOrSplit && Theory::fullEffort(effortLevel)){
3362 ++d_fullCheckCounter;
3363 }
3364 if(!emmittedConflictOrSplit && Theory::fullEffort(effortLevel)){
3365 emmittedConflictOrSplit = splitDisequalities();
3366 }
3367 Debug("arith::ems") << "ems: " << emmittedConflictOrSplit
3368 << "pos splitting" << endl;
3369
3370
3371 Debug("arith") << "integer? "
3372 << " conf/split " << emmittedConflictOrSplit
3373 << " fulleffort " << Theory::fullEffort(effortLevel)
3374 << " hasintmodel " << hasIntegerModel() << endl;
3375
3376 if(!emmittedConflictOrSplit && Theory::fullEffort(effortLevel) && !hasIntegerModel()){
3377 Node possibleConflict = Node::null();
3378 if(!emmittedConflictOrSplit && options::arithDioSolver()){
3379 possibleConflict = callDioSolver();
3380 if(possibleConflict != Node::null()){
3381 revertOutOfConflict();
3382 Debug("arith::conflict") << "dio conflict " << possibleConflict << endl;
3383 // TODO (project #37): justify (proofs in the DIO solver)
3384 raiseBlackBoxConflict(possibleConflict);
3385 outputConflicts();
3386 emmittedConflictOrSplit = true;
3387 }
3388 }
3389
3390 if(!emmittedConflictOrSplit && d_hasDoneWorkSinceCut && options::arithDioSolver()){
3391 if(getDioCuttingResource()){
3392 TrustNode possibleLemma = dioCutting();
3393 if(!possibleLemma.isNull()){
3394 emmittedConflictOrSplit = true;
3395 d_hasDoneWorkSinceCut = false;
3396 d_cutCount = d_cutCount + 1;
3397 Debug("arith::lemma") << "dio cut " << possibleLemma << endl;
3398 outputTrustedLemma(possibleLemma, InferenceId::ARITH_DIO_CUT);
3399 }
3400 }
3401 }
3402
3403 if(!emmittedConflictOrSplit) {
3404 TrustNode possibleLemma = roundRobinBranch();
3405 if (!possibleLemma.getNode().isNull())
3406 {
3407 ++(d_statistics.d_externalBranchAndBounds);
3408 d_cutCount = d_cutCount + 1;
3409 emmittedConflictOrSplit = true;
3410 Debug("arith::lemma") << "rrbranch lemma"
3411 << possibleLemma << endl;
3412 outputTrustedLemma(possibleLemma, InferenceId::ARITH_BB_LEMMA);
3413 }
3414 }
3415
3416 if(options::maxCutsInContext() <= d_cutCount){
3417 if(d_diosolver.hasMoreDecompositionLemmas()){
3418 while(d_diosolver.hasMoreDecompositionLemmas()){
3419 Node decompositionLemma = d_diosolver.nextDecompositionLemma();
3420 Debug("arith::lemma") << "dio decomposition lemma "
3421 << decompositionLemma << endl;
3422 outputLemma(decompositionLemma, InferenceId::ARITH_DIO_DECOMPOSITION);
3423 }
3424 }else{
3425 Debug("arith::restart") << "arith restart!" << endl;
3426 outputRestart();
3427 }
3428 }
3429 }//if !emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel()
3430
3431 if(Theory::fullEffort(effortLevel)){
3432 if(Debug.isOn("arith::consistency::final")){
3433 entireStateIsConsistent("arith::consistency::final");
3434 }
3435 }
3436
3437 if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
3438 if(Debug.isOn("arith::print_model")) {
3439 debugPrintModel(Debug("arith::print_model"));
3440 }
3441 Debug("arith") << "TheoryArithPrivate::check end" << std::endl;
3442 return emmittedConflictOrSplit;
3443 }
3444
3445 bool TheoryArithPrivate::foundNonlinear() const { return d_foundNl; }
3446
3447 TrustNode TheoryArithPrivate::branchIntegerVariable(ArithVar x) const
3448 {
3449 const DeltaRational& d = d_partialModel.getAssignment(x);
3450 Assert(!d.isIntegral());
3451 const Rational& r = d.getNoninfinitesimalPart();
3452 const Rational& i = d.getInfinitesimalPart();
3453 Trace("integers") << "integers: assignment to [[" << d_partialModel.asNode(x) << "]] is " << r << "[" << i << "]" << endl;
3454
3455 Assert(!(r.getDenominator() == 1 && i.getNumerator() == 0));
3456 Assert(!d.isIntegral());
3457 TNode var = d_partialModel.asNode(x);
3458 Integer floor_d = d.floor();
3459
3460 TrustNode lem = TrustNode::null();
3461 NodeManager* nm = NodeManager::currentNM();
3462 if (options::brabTest())
3463 {
3464 Trace("integers") << "branch-round-and-bound enabled" << endl;
3465 Integer ceil_d = d.ceiling();
3466 Rational f = r - floor_d;
3467 // Multiply by -1 to get abs value.
3468 Rational c = (r - ceil_d) * (-1);
3469 Integer nearest = (c > f) ? floor_d : ceil_d;
3470
3471 // Prioritize trying a simple rounding of the real solution first,
3472 // it that fails, fall back on original branch and bound strategy.
3473 Node ub = Rewriter::rewrite(
3474 nm->mkNode(kind::LEQ, var, mkRationalNode(nearest - 1)));
3475 Node lb = Rewriter::rewrite(
3476 nm->mkNode(kind::GEQ, var, mkRationalNode(nearest + 1)));
3477 Node right = nm->mkNode(kind::OR, ub, lb);
3478 Node rawEq = nm->mkNode(kind::EQUAL, var, mkRationalNode(nearest));
3479 Node eq = Rewriter::rewrite(rawEq);
3480 // Also preprocess it before we send it out. This is important since
3481 // arithmetic may prefer eliminating equalities.
3482 TrustNode teq;
3483 if (Theory::theoryOf(eq) == THEORY_ARITH)
3484 {
3485 teq = d_containing.ppRewriteEq(eq);
3486 eq = teq.isNull() ? eq : teq.getNode();
3487 }
3488 Node literal = d_containing.getValuation().ensureLiteral(eq);
3489 Trace("integers") << "eq: " << eq << "\nto: " << literal << endl;
3490 d_containing.getOutputChannel().requirePhase(literal, true);
3491 Node l = nm->mkNode(kind::OR, literal, right);
3492 Trace("integers") << "l: " << l << endl;
3493 if (proofsEnabled())
3494 {
3495 Node less = nm->mkNode(kind::LT, var, mkRationalNode(nearest));
3496 Node greater = nm->mkNode(kind::GT, var, mkRationalNode(nearest));
3497 // TODO (project #37): justify. Thread proofs through *ensureLiteral*.
3498 Debug("integers::pf") << "less: " << less << endl;
3499 Debug("integers::pf") << "greater: " << greater << endl;
3500 Debug("integers::pf") << "literal: " << literal << endl;
3501 Debug("integers::pf") << "eq: " << eq << endl;
3502 Debug("integers::pf") << "rawEq: " << rawEq << endl;
3503 Pf pfNotLit = d_pnm->mkAssume(literal.negate());
3504 // rewrite notLiteral to notRawEq, using teq.
3505 Pf pfNotRawEq =
3506 literal == rawEq
3507 ? pfNotLit
3508 : d_pnm->mkNode(
3509 PfRule::MACRO_SR_PRED_TRANSFORM,
3510 {pfNotLit, teq.getGenerator()->getProofFor(teq.getProven())},
3511 {rawEq.negate()});
3512 Pf pfBot =
3513 d_pnm->mkNode(PfRule::CONTRA,
3514 {d_pnm->mkNode(PfRule::ARITH_TRICHOTOMY,
3515 {d_pnm->mkAssume(less.negate()), pfNotRawEq},
3516 {greater}),
3517 d_pnm->mkAssume(greater.negate())},
3518 {});
3519 std::vector<Node> assumptions = {
3520 literal.negate(), less.negate(), greater.negate()};
3521 // Proof of (not (and (not (= v i)) (not (< v i)) (not (> v i))))
3522 Pf pfNotAnd = d_pnm->mkScope(pfBot, assumptions);
3523 Pf pfL = d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM,
3524 {d_pnm->mkNode(PfRule::NOT_AND, {pfNotAnd}, {})},
3525 {l});
3526 lem = d_pfGen->mkTrustNode(l, pfL);
3527 }
3528 else
3529 {
3530 lem = TrustNode::mkTrustLemma(l, nullptr);
3531 }
3532 }
3533 else
3534 {
3535 Node ub =
3536 Rewriter::rewrite(nm->mkNode(kind::LEQ, var, mkRationalNode(floor_d)));
3537 Node lb = ub.notNode();
3538 if (proofsEnabled())
3539 {
3540 lem = d_pfGen->mkTrustNode(
3541 nm->mkNode(kind::OR, ub, lb), PfRule::SPLIT, {}, {ub});
3542 }
3543 else
3544 {
3545 lem = TrustNode::mkTrustLemma(nm->mkNode(kind::OR, ub, lb), nullptr);
3546 }
3547 }
3548
3549 Trace("integers") << "integers: branch & bound: " << lem << endl;
3550 if (Debug.isOn("integers"))
3551 {
3552 Node l = lem.getNode();
3553 if (isSatLiteral(l[0]))
3554 {
3555 Debug("integers") << " " << l[0] << " == " << getSatValue(l[0])
3556 << endl;
3557 }
3558 else
3559 {
3560 Debug("integers") << " " << l[0] << " is not assigned a SAT literal"
3561 << endl;
3562 }
3563 if (isSatLiteral(l[1]))
3564 {
3565 Debug("integers") << " " << l[1] << " == " << getSatValue(l[1])
3566 << endl;
3567 }
3568 else
3569 {
3570 Debug("integers") << " " << l[1] << " is not assigned a SAT literal"
3571 << endl;
3572 }
3573 }
3574 return lem;
3575 }
3576
3577 std::vector<ArithVar> TheoryArithPrivate::cutAllBounded() const{
3578 vector<ArithVar> lemmas;
3579 ArithVar max = d_partialModel.getNumberOfVariables();
3580
3581 if(options::doCutAllBounded() && max > 0){
3582 for(ArithVar iter = 0; iter != max; ++iter){
3583 //Do not include slack variables
3584 const DeltaRational& d = d_partialModel.getAssignment(iter);
3585 if(isIntegerInput(iter) &&
3586 !d_cutInContext.contains(iter) &&
3587 d_partialModel.hasUpperBound(iter) &&
3588 d_partialModel.hasLowerBound(iter) &&
3589 !d.isIntegral()){
3590 lemmas.push_back(iter);
3591 }
3592 }
3593 }
3594 return lemmas;
3595 }
3596
3597 /** Returns true if the roundRobinBranching() issues a lemma. */
3598 TrustNode TheoryArithPrivate::roundRobinBranch()
3599 {
3600 if(hasIntegerModel()){
3601 return TrustNode::null();
3602 }else{
3603 ArithVar v = d_nextIntegerCheckVar;
3604
3605 Assert(isInteger(v));
3606 Assert(!isAuxiliaryVariable(v));
3607 return branchIntegerVariable(v);
3608 }
3609 }
3610
3611 bool TheoryArithPrivate::splitDisequalities(){
3612 bool splitSomething = false;
3613
3614 vector<ConstraintP> save;
3615
3616 while(!d_diseqQueue.empty()){
3617 ConstraintP front = d_diseqQueue.front();
3618 d_diseqQueue.pop();
3619
3620 if(front->isSplit()){
3621 Debug("arith::eq") << "split already" << endl;
3622 }else{
3623 Debug("arith::eq") << "not split already" << endl;
3624
3625 ArithVar lhsVar = front->getVariable();
3626
3627 const DeltaRational& lhsValue = d_partialModel.getAssignment(lhsVar);
3628 const DeltaRational& rhsValue = front->getValue();
3629 if(lhsValue == rhsValue){
3630 Debug("arith::lemma") << "Splitting on " << front << endl;
3631 Debug("arith::lemma") << "LHS value = " << lhsValue << endl;
3632 Debug("arith::lemma") << "RHS value = " << rhsValue << endl;
3633 TrustNode lemma = front->split();
3634 ++(d_statistics.d_statDisequalitySplits);
3635
3636 Debug("arith::lemma")
3637 << "Now " << Rewriter::rewrite(lemma.getNode()) << endl;
3638 outputTrustedLemma(lemma, InferenceId::ARITH_SPLIT_DEQ);
3639 //cout << "Now " << Rewriter::rewrite(lemma) << endl;
3640 splitSomething = true;
3641 }else if(d_partialModel.strictlyLessThanLowerBound(lhsVar, rhsValue)){
3642 Debug("arith::eq") << "can drop as less than lb" << front << endl;
3643 }else if(d_partialModel.strictlyGreaterThanUpperBound(lhsVar, rhsValue)){
3644 Debug("arith::eq") << "can drop as greater than ub" << front << endl;
3645 }else{
3646 Debug("arith::eq") << "save" << front << ": " <<lhsValue << " != " << rhsValue << endl;
3647 save.push_back(front);
3648 }
3649 }
3650 }
3651 vector<ConstraintP>::const_iterator i=save.begin(), i_end = save.end();
3652 for(; i != i_end; ++i){
3653 d_diseqQueue.push(*i);
3654 }
3655 return splitSomething;
3656 }
3657
3658 /**
3659 * Should be guarded by at least Debug.isOn("arith::print_assertions").
3660 * Prints to Debug("arith::print_assertions")
3661 */
3662 void TheoryArithPrivate::debugPrintAssertions(std::ostream& out) const {
3663 out << "Assertions:" << endl;
3664 for (var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
3665 ArithVar i = *vi;
3666 if (d_partialModel.hasLowerBound(i)) {
3667 ConstraintP lConstr = d_partialModel.getLowerBoundConstraint(i);
3668 out << lConstr << endl;
3669 }
3670
3671 if (d_partialModel.hasUpperBound(i)) {
3672 ConstraintP uConstr = d_partialModel.getUpperBoundConstraint(i);
3673 out << uConstr << endl;
3674 }
3675 }
3676 context::CDQueue<ConstraintP>::const_iterator it = d_diseqQueue.begin();
3677 context::CDQueue<ConstraintP>::const_iterator it_end = d_diseqQueue.end();
3678 for(; it != it_end; ++ it) {
3679 out << *it << endl;
3680 }
3681 }
3682
3683 void TheoryArithPrivate::debugPrintModel(std::ostream& out) const{
3684 out << "Model:" << endl;
3685 for (var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
3686 ArithVar i = *vi;
3687 if(d_partialModel.hasNode(i)){
3688 out << d_partialModel.asNode(i) << " : " <<
3689 d_partialModel.getAssignment(i);
3690 if(d_tableau.isBasic(i)){
3691 out << " (basic)";
3692 }
3693 out << endl;
3694 }
3695 }
3696 }
3697
3698 TrustNode TheoryArithPrivate::explain(TNode n)
3699 {
3700 Debug("arith::explain") << "explain @" << getSatContext()->getLevel() << ": " << n << endl;
3701
3702 ConstraintP c = d_constraintDatabase.lookup(n);
3703 TrustNode exp;
3704 if(c != NullConstraint){
3705 Assert(!c->isAssumption());
3706 exp = c->externalExplainForPropagation(n);
3707 Debug("arith::explain") << "constraint explanation" << n << ":" << exp << endl;
3708 }else if(d_assertionsThatDoNotMatchTheirLiterals.find(n) != d_assertionsThatDoNotMatchTheirLiterals.end()){
3709 c = d_assertionsThatDoNotMatchTheirLiterals[n];
3710 if(!c->isAssumption()){
3711 exp = c->externalExplainForPropagation(n);
3712 Debug("arith::explain") << "assertions explanation" << n << ":" << exp << endl;
3713 }else{
3714 Debug("arith::explain") << "this is a strange mismatch" << n << endl;
3715 Assert(d_congruenceManager.canExplain(n));
3716 exp = d_congruenceManager.explain(n);
3717 }
3718 }else{
3719 Assert(d_congruenceManager.canExplain(n));
3720 Debug("arith::explain") << "dm explanation" << n << endl;
3721 exp = d_congruenceManager.explain(n);
3722 }
3723 return exp;
3724 }
3725
3726 void TheoryArithPrivate::propagate(Theory::Effort e) {
3727 // This uses model values for safety. Disable for now.
3728 if (d_qflraStatus == Result::SAT
3729 && (options::arithPropagationMode()
3730 == options::ArithPropagationMode::BOUND_INFERENCE_PROP
3731 || options::arithPropagationMode()
3732 == options::ArithPropagationMode::BOTH_PROP)
3733 && hasAnyUpdates())
3734 {
3735 if(options::newProp()){
3736 propagateCandidatesNew();
3737 }else{
3738 propagateCandidates();
3739 }
3740 }
3741 else
3742 {
3743 clearUpdates();
3744 }
3745
3746 while(d_constraintDatabase.hasMorePropagations()){
3747 ConstraintCP c = d_constraintDatabase.nextPropagation();
3748 Debug("arith::prop") << "next prop" << getSatContext()->getLevel() << ": " << c << endl;
3749
3750 if(c->negationHasProof()){
3751 Debug("arith::prop") << "negation has proof " << c->getNegation() << endl;
3752 Debug("arith::prop") << c->getNegation()->externalExplainByAssertions()
3753 << endl;
3754 }
3755 Assert(!c->negationHasProof())
3756 << "A constraint has been propagated on the constraint propagation "
3757 "queue, but the negation has been set to true. Contact Tim now!";
3758
3759 if(!c->assertedToTheTheory()){
3760 Node literal = c->getLiteral();
3761 Debug("arith::prop") << "propagating @" << getSatContext()->getLevel() << " " << literal << endl;
3762
3763 outputPropagate(literal);
3764 }else{
3765 Debug("arith::prop") << "already asserted to the theory " << c->getLiteral() << endl;
3766 }
3767 }
3768
3769 while(d_congruenceManager.hasMorePropagations()){
3770 TNode toProp = d_congruenceManager.getNextPropagation();
3771
3772 //Currently if the flag is set this came from an equality detected by the
3773 //equality engine in the the difference manager.
3774 Node normalized = Rewriter::rewrite(toProp);
3775
3776 ConstraintP constraint = d_constraintDatabase.lookup(normalized);
3777 if(constraint == NullConstraint){
3778 Debug("arith::prop") << "propagating on non-constraint? " << toProp << endl;
3779
3780 outputPropagate(toProp);
3781 }else if(constraint->negationHasProof()){
3782 // The congruence manager can prove: antecedents => toProp,
3783 // ergo. antecedents ^ ~toProp is a conflict.
3784 TrustNode exp = d_congruenceManager.explain(toProp);
3785 Node notNormalized = normalized.negate();
3786 std::vector<Node> ants(exp.getNode().begin(), exp.getNode().end());
3787 ants.push_back(notNormalized);
3788 Node lp = safeConstructNary(kind::AND, ants);
3789 Debug("arith::prop") << "propagate conflict" << lp << endl;
3790 if (proofsEnabled())
3791 {
3792 // Assume all of antecedents and ~toProp (rewritten)
3793 std::vector<Pf> pfAntList;
3794 for (size_t i = 0; i < ants.size(); ++i)
3795 {
3796 pfAntList.push_back(d_pnm->mkAssume(ants[i]));
3797 }
3798 Pf pfAnt = pfAntList.size() > 1
3799 ? d_pnm->mkNode(PfRule::AND_INTRO, pfAntList, {})
3800 : pfAntList[0];
3801 // Use modus ponens to get toProp (un rewritten)
3802 Pf pfConc = d_pnm->mkNode(
3803 PfRule::MODUS_PONENS,
3804 {pfAnt, exp.getGenerator()->getProofFor(exp.getProven())},
3805 {});
3806 // prove toProp (rewritten)
3807 Pf pfConcRewritten = d_pnm->mkNode(
3808 PfRule::MACRO_SR_PRED_TRANSFORM, {pfConc}, {normalized});
3809 Pf pfNotNormalized = d_pnm->mkAssume(notNormalized);
3810 // prove bottom from toProp and ~toProp
3811 Pf pfBot;
3812 if (normalized.getKind() == kind::NOT)
3813 {
3814 pfBot = d_pnm->mkNode(
3815 PfRule::CONTRA, {pfNotNormalized, pfConcRewritten}, {});
3816 }
3817 else
3818 {
3819 pfBot = d_pnm->mkNode(
3820 PfRule::CONTRA, {pfConcRewritten, pfNotNormalized}, {});
3821 }
3822 // close scope
3823 Pf pfNotAnd = d_pnm->mkScope(pfBot, ants);
3824 raiseBlackBoxConflict(lp, pfNotAnd);
3825 }
3826 else
3827 {
3828 raiseBlackBoxConflict(lp);
3829 }
3830 outputConflicts();
3831 return;
3832 }else{
3833 Debug("arith::prop") << "propagating still?" << toProp << endl;
3834 outputPropagate(toProp);
3835 }
3836 }
3837 }
3838
3839 DeltaRational TheoryArithPrivate::getDeltaValue(TNode term) const
3840 {
3841 AlwaysAssert(d_qflraStatus != Result::SAT_UNKNOWN);
3842 Debug("arith::value") << term << std::endl;
3843
3844 if (d_partialModel.hasArithVar(term)) {
3845 ArithVar var = d_partialModel.asArithVar(term);
3846 return d_partialModel.getAssignment(var);
3847 }
3848
3849 switch (Kind kind = term.getKind()) {
3850 case kind::CONST_RATIONAL:
3851 return term.getConst<Rational>();
3852
3853 case kind::PLUS: { // 2+ args
3854 DeltaRational value(0);
3855 for (TNode::iterator i = term.begin(), iend = term.end(); i != iend;
3856 ++i) {
3857 value = value + getDeltaValue(*i);
3858 }
3859 return value;
3860 }
3861
3862 case kind::NONLINEAR_MULT:
3863 case kind::MULT: { // 2+ args
3864 Assert(!isSetup(term));
3865 DeltaRational value(1);
3866 for (TNode::iterator i = term.begin(), iend = term.end(); i != iend;
3867 ++i) {
3868 value = value * getDeltaValue(*i);
3869 }
3870 return value;
3871 }
3872 case kind::MINUS: { // 2 args
3873 return getDeltaValue(term[0]) - getDeltaValue(term[1]);
3874 }
3875 case kind::UMINUS: { // 1 arg
3876 return (-getDeltaValue(term[0]));
3877 }
3878
3879 case kind::DIVISION: { // 2 args
3880 Assert(!isSetup(term));
3881 return getDeltaValue(term[0]) / getDeltaValue(term[1]);
3882 }
3883 case kind::DIVISION_TOTAL:
3884 case kind::INTS_DIVISION_TOTAL:
3885 case kind::INTS_MODULUS_TOTAL: { // 2 args
3886 Assert(!isSetup(term));
3887 DeltaRational denominator = getDeltaValue(term[1]);
3888 if (denominator.isZero()) {
3889 return DeltaRational(0, 0);
3890 }
3891 DeltaRational numerator = getDeltaValue(term[0]);
3892 if (kind == kind::DIVISION_TOTAL) {
3893 return numerator / denominator;
3894 } else if (kind == kind::INTS_DIVISION_TOTAL) {
3895 return Rational(numerator.euclidianDivideQuotient(denominator));
3896 } else {
3897 Assert(kind == kind::INTS_MODULUS_TOTAL);
3898 return Rational(numerator.euclidianDivideRemainder(denominator));
3899 }
3900 }
3901
3902 default:
3903 throw ModelException(term, "No model assignment.");
3904 }
3905 }
3906
3907 Rational TheoryArithPrivate::deltaValueForTotalOrder() const{
3908 Rational min(2);
3909 std::set<DeltaRational> relevantDeltaValues;
3910 context::CDQueue<ConstraintP>::const_iterator qiter = d_diseqQueue.begin();
3911 context::CDQueue<ConstraintP>::const_iterator qiter_end = d_diseqQueue.end();
3912
3913 for(; qiter != qiter_end; ++qiter){
3914 ConstraintP curr = *qiter;
3915
3916 const DeltaRational& rhsValue = curr->getValue();
3917 relevantDeltaValues.insert(rhsValue);
3918 }
3919
3920 Theory::shared_terms_iterator shared_iter = d_containing.shared_terms_begin();
3921 Theory::shared_terms_iterator shared_end = d_containing.shared_terms_end();
3922 for(; shared_iter != shared_end; ++shared_iter){
3923 Node sharedCurr = *shared_iter;
3924
3925 // ModelException is fatal as this point. Don't catch!
3926 // DeltaRationalException is fatal as this point. Don't catch!
3927 DeltaRational val = getDeltaValue(sharedCurr);
3928 relevantDeltaValues.insert(val);
3929 }
3930
3931 for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
3932 ArithVar v = *vi;
3933 const DeltaRational& value = d_partialModel.getAssignment(v);
3934 relevantDeltaValues.insert(value);
3935 if( d_partialModel.hasLowerBound(v)){
3936 const DeltaRational& lb = d_partialModel.getLowerBound(v);
3937 relevantDeltaValues.insert(lb);
3938 }
3939 if( d_partialModel.hasUpperBound(v)){
3940 const DeltaRational& ub = d_partialModel.getUpperBound(v);
3941 relevantDeltaValues.insert(ub);
3942 }
3943 }
3944
3945 if(relevantDeltaValues.size() >= 2){
3946 std::set<DeltaRational>::const_iterator iter = relevantDeltaValues.begin();
3947 std::set<DeltaRational>::const_iterator iter_end = relevantDeltaValues.end();
3948 DeltaRational prev = *iter;
3949 ++iter;
3950 for(; iter != iter_end; ++iter){
3951 const DeltaRational& curr = *iter;
3952
3953 Assert(prev < curr);
3954
3955 DeltaRational::seperatingDelta(min, prev, curr);
3956 prev = curr;
3957 }
3958 }
3959
3960 Assert(min.sgn() > 0);
3961 Rational belowMin = min/Rational(2);
3962 return belowMin;
3963 }
3964
3965 void TheoryArithPrivate::collectModelValues(const std::set<Node>& termSet,
3966 std::map<Node, Node>& arithModel)
3967 {
3968 AlwaysAssert(d_qflraStatus == Result::SAT);
3969
3970 if(Debug.isOn("arith::collectModelInfo")){
3971 debugPrintFacts();
3972 }
3973
3974 Debug("arith::collectModelInfo") << "collectModelInfo() begin " << endl;
3975
3976 // Delta lasts at least the duration of the function call
3977 const Rational& delta = d_partialModel.getDelta();
3978 std::unordered_set<TNode> shared = d_containing.currentlySharedTerms();
3979
3980 // TODO:
3981 // This is not very good for user push/pop....
3982 // Revisit when implementing push/pop
3983 for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
3984 ArithVar v = *vi;
3985
3986 if(!isAuxiliaryVariable(v)){
3987 Node term = d_partialModel.asNode(v);
3988
3989 if((theoryOf(term) == THEORY_ARITH || shared.find(term) != shared.end())
3990 && termSet.find(term) != termSet.end()){
3991
3992 const DeltaRational& mod = d_partialModel.getAssignment(v);
3993 Rational qmodel = mod.substituteDelta(delta);
3994
3995 Node qNode = mkRationalNode(qmodel);
3996 Debug("arith::collectModelInfo") << "m->assertEquality(" << term << ", " << qmodel << ", true)" << endl;
3997 // Add to the map
3998 arithModel[term] = qNode;
3999 }else{
4000 Debug("arith::collectModelInfo") << "Skipping m->assertEquality(" << term << ", true)" << endl;
4001
4002 }
4003 }
4004 }
4005
4006 // Iterate over equivalence classes in LinearEqualityModule
4007 // const eq::EqualityEngine& ee = d_congruenceManager.getEqualityEngine();
4008 // m->assertEqualityEngine(&ee);
4009
4010 Debug("arith::collectModelInfo") << "collectModelInfo() end " << endl;
4011 }
4012
4013 bool TheoryArithPrivate::safeToReset() const {
4014 Assert(!d_tableauSizeHasBeenModified);
4015 Assert(d_errorSet.noSignals());
4016
4017 ErrorSet::error_iterator error_iter = d_errorSet.errorBegin();
4018 ErrorSet::error_iterator error_end = d_errorSet.errorEnd();
4019 for(; error_iter != error_end; ++error_iter){
4020 ArithVar basic = *error_iter;
4021 if(!d_smallTableauCopy.isBasic(basic)){
4022 return false;
4023 }
4024 }
4025
4026 return true;
4027 }
4028
4029 void TheoryArithPrivate::notifyRestart(){
4030 TimerStat::CodeTimer codeTimer(d_statistics.d_restartTimer);
4031
4032 if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
4033
4034 ++d_restartsCounter;
4035 d_solveIntMaybeHelp = 0;
4036 d_solveIntAttempts = 0;
4037 }
4038
4039 bool TheoryArithPrivate::entireStateIsConsistent(const string& s){
4040 bool result = true;
4041 for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
4042 ArithVar var = *vi;
4043 //ArithVar var = d_partialModel.asArithVar(*i);
4044 if(!d_partialModel.assignmentIsConsistent(var)){
4045 d_partialModel.printModel(var);
4046 Warning() << s << ":" << "Assignment is not consistent for " << var << d_partialModel.asNode(var);
4047 if(d_tableau.isBasic(var)){
4048 Warning() << " (basic)";
4049 }
4050 Warning() << endl;
4051 result = false;
4052 }else if(d_partialModel.isInteger(var) && !d_partialModel.integralAssignment(var)){
4053 d_partialModel.printModel(var);
4054 Warning() << s << ":" << "Assignment is not integer for integer variable " << var << d_partialModel.asNode(var);
4055 if(d_tableau.isBasic(var)){
4056 Warning() << " (basic)";
4057 }
4058 Warning() << endl;
4059 result = false;
4060 }
4061 }
4062 return result;
4063 }
4064
4065 bool TheoryArithPrivate::unenqueuedVariablesAreConsistent(){
4066 bool result = true;
4067 for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
4068 ArithVar var = *vi;
4069 if(!d_partialModel.assignmentIsConsistent(var)){
4070 if(!d_errorSet.inError(var)){
4071
4072 d_partialModel.printModel(var);
4073 Warning() << "Unenqueued var is not consistent for " << var << d_partialModel.asNode(var);
4074 if(d_tableau.isBasic(var)){
4075 Warning() << " (basic)";
4076 }
4077 Warning() << endl;
4078 result = false;
4079 } else if(Debug.isOn("arith::consistency::initial")){
4080 d_partialModel.printModel(var);
4081 Warning() << "Initial var is not consistent for " << var << d_partialModel.asNode(var);
4082 if(d_tableau.isBasic(var)){
4083 Warning() << " (basic)";
4084 }
4085 Warning() << endl;
4086 }
4087 }
4088 }
4089 return result;
4090 }
4091
4092 void TheoryArithPrivate::presolve(){
4093 TimerStat::CodeTimer codeTimer(d_statistics.d_presolveTime);
4094
4095 d_statistics.d_initialTableauSize = d_tableau.size();
4096
4097 if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
4098
4099 static thread_local unsigned callCount = 0;
4100 if(Debug.isOn("arith::presolve")) {
4101 Debug("arith::presolve") << "TheoryArithPrivate::presolve #" << callCount << endl;
4102 callCount = callCount + 1;
4103 }
4104
4105 vector<TrustNode> lemmas;
4106 if(!options::incrementalSolving()) {
4107 switch(options::arithUnateLemmaMode()){
4108 case options::ArithUnateLemmaMode::NO: break;
4109 case options::ArithUnateLemmaMode::INEQUALITY:
4110 d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
4111 break;
4112 case options::ArithUnateLemmaMode::EQUALITY:
4113 d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
4114 break;
4115 case options::ArithUnateLemmaMode::ALL:
4116 d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
4117 d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
4118 break;
4119 default: Unhandled() << options::arithUnateLemmaMode();
4120 }
4121 }
4122
4123 vector<TrustNode>::const_iterator i = lemmas.begin(), i_end = lemmas.end();
4124 for(; i != i_end; ++i){
4125 TrustNode lem = *i;
4126 Debug("arith::oldprop") << " lemma lemma duck " <<lem << endl;
4127 outputTrustedLemma(lem, InferenceId::ARITH_UNATE);
4128 }
4129 }
4130
4131 EqualityStatus TheoryArithPrivate::getEqualityStatus(TNode a, TNode b) {
4132 if(d_qflraStatus == Result::SAT_UNKNOWN){
4133 return EQUALITY_UNKNOWN;
4134 }else{
4135 try {
4136 if (getDeltaValue(a) == getDeltaValue(b)) {
4137 return EQUALITY_TRUE_IN_MODEL;
4138 } else {
4139 return EQUALITY_FALSE_IN_MODEL;
4140 }
4141 } catch (DeltaRationalException& dr) {
4142 return EQUALITY_UNKNOWN;
4143 } catch (ModelException& me) {
4144 return EQUALITY_UNKNOWN;
4145 }
4146 }
4147 }
4148
4149 bool TheoryArithPrivate::propagateCandidateBound(ArithVar basic, bool upperBound){
4150 ++d_statistics.d_boundComputations;
4151
4152 RowIndex ridx = d_tableau.basicToRowIndex(basic);
4153 DeltaRational bound = d_linEq.computeRowBound(ridx, upperBound, basic);
4154
4155 if((upperBound && d_partialModel.strictlyLessThanUpperBound(basic, bound)) ||
4156 (!upperBound && d_partialModel.strictlyGreaterThanLowerBound(basic, bound))){
4157
4158 // TODO: "Policy point"
4159 //We are only going to recreate the functionality for now.
4160 //In the future this can be improved to generate a temporary constraint
4161 //if none exists.
4162 //Experiment with doing this every time or only when the new constraint
4163 //implies an unknown fact.
4164
4165 ConstraintType t = upperBound ? UpperBound : LowerBound;
4166 ConstraintP bestImplied = d_constraintDatabase.getBestImpliedBound(basic, t, bound);
4167
4168 // Node bestImplied = upperBound ?
4169 // d_apm.getBestImpliedUpperBound(basic, bound):
4170 // d_apm.getBestImpliedLowerBound(basic, bound);
4171
4172 if(bestImplied != NullConstraint){
4173 //This should be stronger
4174 Assert(!upperBound || bound <= bestImplied->getValue());
4175 Assert(
4176 !upperBound
4177 || d_partialModel.lessThanUpperBound(basic, bestImplied->getValue()));
4178
4179 Assert(upperBound || bound >= bestImplied->getValue());
4180 Assert(upperBound
4181 || d_partialModel.greaterThanLowerBound(basic,
4182 bestImplied->getValue()));
4183 //slightly changed
4184
4185 // ConstraintP c = d_constraintDatabase.lookup(bestImplied);
4186 // Assert(c != NullConstraint);
4187
4188 bool assertedToTheTheory = bestImplied->assertedToTheTheory();
4189 bool canBePropagated = bestImplied->canBePropagated();
4190 bool hasProof = bestImplied->hasProof();
4191
4192 Debug("arith::prop") << "arith::prop" << basic
4193 << " " << assertedToTheTheory
4194 << " " << canBePropagated
4195 << " " << hasProof
4196 << endl;
4197
4198 if(bestImplied->negationHasProof()){
4199 Warning() << "the negation of " << bestImplied << " : " << endl
4200 << "has proof " << bestImplied->getNegation() << endl
4201 << bestImplied->getNegation()->externalExplainByAssertions()
4202 << endl;
4203 }
4204
4205 if(!assertedToTheTheory && canBePropagated && !hasProof ){
4206 d_linEq.propagateBasicFromRow(bestImplied);
4207 // I think this can be skipped if canBePropagated is true
4208 //d_learnedBounds.push(bestImplied);
4209 if(Debug.isOn("arith::prop")){
4210 Debug("arith::prop") << "success " << bestImplied << endl;
4211 d_partialModel.printModel(basic, Debug("arith::prop"));
4212 }
4213 return true;
4214 }
4215 if(Debug.isOn("arith::prop")){
4216 Debug("arith::prop") << "failed " << basic
4217 << " " << bound
4218 << " " << assertedToTheTheory
4219 << " " << canBePropagated
4220 << " " << hasProof << endl;
4221 d_partialModel.printModel(basic, Debug("arith::prop"));
4222 }
4223 }
4224 }else if(Debug.isOn("arith::prop")){
4225 Debug("arith::prop") << "false " << bound << " ";
4226 d_partialModel.printModel(basic, Debug("arith::prop"));
4227 }
4228 return false;
4229 }
4230
4231 void TheoryArithPrivate::propagateCandidate(ArithVar basic){
4232 bool success = false;
4233 RowIndex ridx = d_tableau.basicToRowIndex(basic);
4234
4235 bool tryLowerBound =
4236 d_partialModel.strictlyAboveLowerBound(basic) &&
4237 d_linEq.rowLacksBound(ridx, false, basic) == NULL;
4238
4239 bool tryUpperBound =
4240 d_partialModel.strictlyBelowUpperBound(basic) &&
4241 d_linEq.rowLacksBound(ridx, true, basic) == NULL;
4242
4243 if(tryLowerBound){
4244 success |= propagateCandidateLowerBound(basic);
4245 }
4246 if(tryUpperBound){
4247 success |= propagateCandidateUpperBound(basic);
4248 }
4249 if(success){
4250 ++d_statistics.d_boundPropagations;
4251 }
4252 }
4253
4254 void TheoryArithPrivate::propagateCandidates(){
4255 TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime);
4256
4257 Debug("arith::prop") << "propagateCandidates begin" << endl;
4258
4259 Assert(d_candidateBasics.empty());
4260
4261 if(d_updatedBounds.empty()){ return; }
4262
4263 DenseSet::const_iterator i = d_updatedBounds.begin();
4264 DenseSet::const_iterator end = d_updatedBounds.end();
4265 for(; i != end; ++i){
4266 ArithVar var = *i;
4267 if(d_tableau.isBasic(var) &&
4268 d_tableau.basicRowLength(var) <= options::arithPropagateMaxLength()){
4269 d_candidateBasics.softAdd(var);
4270 }else{
4271 Tableau::ColIterator basicIter = d_tableau.colIterator(var);
4272 for(; !basicIter.atEnd(); ++basicIter){
4273 const Tableau::Entry& entry = *basicIter;
4274 RowIndex ridx = entry.getRowIndex();
4275 ArithVar rowVar = d_tableau.rowIndexToBasic(ridx);
4276 Assert(entry.getColVar() == var);
4277 Assert(d_tableau.isBasic(rowVar));
4278 if(d_tableau.getRowLength(ridx) <= options::arithPropagateMaxLength()){
4279 d_candidateBasics.softAdd(rowVar);
4280 }
4281 }
4282 }
4283 }
4284 d_updatedBounds.purge();
4285
4286 while(!d_candidateBasics.empty()){
4287 ArithVar candidate = d_candidateBasics.back();
4288 d_candidateBasics.pop_back();
4289 Assert(d_tableau.isBasic(candidate));
4290 propagateCandidate(candidate);
4291 }
4292 Debug("arith::prop") << "propagateCandidates end" << endl << endl << endl;
4293 }
4294
4295 void TheoryArithPrivate::propagateCandidatesNew(){
4296 /* Four criteria must be met for progagation on a variable to happen using a row:
4297 * 0: A new bound has to have been added to the row.
4298 * 1: The hasBoundsCount for the row must be "full" or be full minus one variable
4299 * (This is O(1) to check, but requires book keeping.)
4300 * 2: The current assignment must be strictly smaller/greater than the current bound.
4301 * assign(x) < upper(x)
4302 * (This is O(1) to compute.)
4303 * 3: There is a bound that is strictly smaller/greater than the current assignment.
4304 * assign(x) < c for some x <= c literal
4305 * (This is O(log n) to compute.)
4306 * 4: The implied bound on x is strictly smaller/greater than the current bound.
4307 * (This is O(n) to compute.)
4308 */
4309
4310 TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime);
4311 Debug("arith::prop") << "propagateCandidatesNew begin" << endl;
4312
4313 Assert(d_qflraStatus == Result::SAT);
4314 if(d_updatedBounds.empty()){ return; }
4315 dumpUpdatedBoundsToRows();
4316 Assert(d_updatedBounds.empty());
4317
4318 if(!d_candidateRows.empty()){
4319 UpdateTrackingCallback utcb(&d_linEq);
4320 d_partialModel.processBoundsQueue(utcb);
4321 }
4322
4323 while(!d_candidateRows.empty()){
4324 RowIndex candidate = d_candidateRows.back();
4325 d_candidateRows.pop_back();
4326 propagateCandidateRow(candidate);
4327 }
4328 Debug("arith::prop") << "propagateCandidatesNew end" << endl << endl << endl;
4329 }
4330
4331 bool TheoryArithPrivate::propagateMightSucceed(ArithVar v, bool ub) const{
4332 int cmp = ub ? d_partialModel.cmpAssignmentUpperBound(v)
4333 : d_partialModel.cmpAssignmentLowerBound(v);
4334 bool hasSlack = ub ? cmp < 0 : cmp > 0;
4335 if(hasSlack){
4336 ConstraintType t = ub ? UpperBound : LowerBound;
4337 const DeltaRational& a = d_partialModel.getAssignment(v);
4338
4339 if(isInteger(v) && !a.isIntegral()){
4340 return true;
4341 }
4342
4343 ConstraintP strongestPossible = d_constraintDatabase.getBestImpliedBound(v, t, a);
4344 if(strongestPossible == NullConstraint){
4345 return false;
4346 }else{
4347 bool assertedToTheTheory = strongestPossible->assertedToTheTheory();
4348 bool canBePropagated = strongestPossible->canBePropagated();
4349 bool hasProof = strongestPossible->hasProof();
4350
4351 return !assertedToTheTheory && canBePropagated && !hasProof;
4352 }
4353 }else{
4354 return false;
4355 }
4356 }
4357
4358 bool TheoryArithPrivate::attemptSingleton(RowIndex ridx, bool rowUp){
4359 Debug("arith::prop") << " attemptSingleton" << ridx;
4360
4361 const Tableau::Entry* ep;
4362 ep = d_linEq.rowLacksBound(ridx, rowUp, ARITHVAR_SENTINEL);
4363 Assert(ep != NULL);
4364
4365 ArithVar v = ep->getColVar();
4366 const Rational& coeff = ep->getCoefficient();
4367
4368 // 0 = c * v + \sum rest
4369 // Suppose rowUp
4370 // - c * v = \sum rest \leq D
4371 // if c > 0, v \geq -D/c so !vUp
4372 // if c < 0, v \leq -D/c so vUp
4373 // Suppose not rowUp
4374 // - c * v = \sum rest \geq D
4375 // if c > 0, v \leq -D/c so vUp
4376 // if c < 0, v \geq -D/c so !vUp
4377 bool vUp = (rowUp == ( coeff.sgn() < 0));
4378
4379 Debug("arith::prop") << " " << rowUp << " " << v << " " << coeff << " " << vUp << endl;
4380 Debug("arith::prop") << " " << propagateMightSucceed(v, vUp) << endl;
4381
4382 if(propagateMightSucceed(v, vUp)){
4383 DeltaRational dr = d_linEq.computeRowBound(ridx, rowUp, v);
4384 DeltaRational bound = dr / (- coeff);
4385 return tryToPropagate(ridx, rowUp, v, vUp, bound);
4386 }
4387 return false;
4388 }
4389
4390 bool TheoryArithPrivate::attemptFull(RowIndex ridx, bool rowUp){
4391 Debug("arith::prop") << " attemptFull" << ridx << endl;
4392
4393 vector<const Tableau::Entry*> candidates;
4394
4395 for(Tableau::RowIterator i = d_tableau.ridRowIterator(ridx); !i.atEnd(); ++i){
4396 const Tableau::Entry& e =*i;
4397 const Rational& c = e.getCoefficient();
4398 ArithVar v = e.getColVar();
4399 bool vUp = (rowUp == (c.sgn() < 0));
4400 if(propagateMightSucceed(v, vUp)){
4401 candidates.push_back(&e);
4402 }
4403 }
4404 if(candidates.empty()){ return false; }
4405
4406 const DeltaRational slack =
4407 d_linEq.computeRowBound(ridx, rowUp, ARITHVAR_SENTINEL);
4408 bool any = false;
4409 vector<const Tableau::Entry*>::const_iterator i, iend;
4410 for(i = candidates.begin(), iend = candidates.end(); i != iend; ++i){
4411 const Tableau::Entry* ep = *i;
4412 const Rational& c = ep->getCoefficient();
4413 ArithVar v = ep->getColVar();
4414
4415 // See the comment for attemptSingleton()
4416 bool activeUp = (rowUp == (c.sgn() > 0));
4417 bool vUb = (rowUp == (c.sgn() < 0));
4418
4419 const DeltaRational& activeBound = activeUp ?
4420 d_partialModel.getUpperBound(v):
4421 d_partialModel.getLowerBound(v);
4422
4423 DeltaRational contribution = activeBound * c;
4424 DeltaRational impliedBound = (slack - contribution)/(-c);
4425
4426 bool success = tryToPropagate(ridx, rowUp, v, vUb, impliedBound);
4427 any |= success;
4428 }
4429 return any;
4430 }
4431
4432 bool TheoryArithPrivate::tryToPropagate(RowIndex ridx, bool rowUp, ArithVar v, bool vUb, const DeltaRational& bound){
4433
4434 bool weaker = vUb ? d_partialModel.strictlyLessThanUpperBound(v, bound):
4435 d_partialModel.strictlyGreaterThanLowerBound(v, bound);
4436 if(weaker){
4437 ConstraintType t = vUb ? UpperBound : LowerBound;
4438
4439 ConstraintP implied = d_constraintDatabase.getBestImpliedBound(v, t, bound);
4440 if(implied != NullConstraint){
4441 return rowImplicationCanBeApplied(ridx, rowUp, implied);
4442 }
4443 }
4444 return false;
4445 }
4446
4447 Node flattenImplication(Node imp){
4448 NodeBuilder nb(kind::OR);
4449 std::unordered_set<Node> included;
4450 Node left = imp[0];
4451 Node right = imp[1];
4452
4453 if(left.getKind() == kind::AND){
4454 for(Node::iterator i = left.begin(), iend = left.end(); i != iend; ++i) {
4455 if (!included.count((*i).negate()))
4456 {
4457 nb << (*i).negate();
4458 included.insert((*i).negate());
4459 }
4460 }
4461 }else{
4462 if (!included.count(left.negate()))
4463 {
4464 nb << left.negate();
4465 included.insert(left.negate());
4466 }
4467 }
4468
4469 if(right.getKind() == kind::OR){
4470 for(Node::iterator i = right.begin(), iend = right.end(); i != iend; ++i) {
4471 if (!included.count(*i))
4472 {
4473 nb << *i;
4474 included.insert(*i);
4475 }
4476 }
4477 }else{
4478 if (!included.count(right))
4479 {
4480 nb << right;
4481 included.insert(right);
4482 }
4483 }
4484
4485 return nb;
4486 }
4487
4488 bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, ConstraintP implied){
4489 Assert(implied != NullConstraint);
4490 ArithVar v = implied->getVariable();
4491
4492 bool assertedToTheTheory = implied->assertedToTheTheory();
4493 bool canBePropagated = implied->canBePropagated();
4494 bool hasProof = implied->hasProof();
4495
4496 Debug("arith::prop") << "arith::prop" << v
4497 << " " << assertedToTheTheory
4498 << " " << canBePropagated
4499 << " " << hasProof
4500 << endl;
4501
4502
4503 if( !assertedToTheTheory && canBePropagated && !hasProof ){
4504 ConstraintCPVec explain;
4505 ARITH_PROOF(d_farkasBuffer.clear());
4506 RationalVectorP coeffs = ARITH_NULLPROOF(&d_farkasBuffer);
4507
4508 // After invoking `propegateRow`:
4509 // * coeffs[0] is for implied
4510 // * coeffs[i+1] is for explain[i]
4511 d_linEq.propagateRow(explain, ridx, rowUp, implied, coeffs);
4512 if(d_tableau.getRowLength(ridx) <= options::arithPropAsLemmaLength()){
4513 if (Debug.isOn("arith::prop::pf")) {
4514 for (const auto & constraint : explain) {
4515 Assert(constraint->hasProof());
4516 constraint->printProofTree(Debug("arith::prop::pf"));
4517 }
4518 }
4519 Node implication = implied->externalImplication(explain);
4520 Node clause = flattenImplication(implication);
4521 std::shared_ptr<ProofNode> clausePf{nullptr};
4522
4523 if (isProofEnabled())
4524 {
4525 // We can prove this lemma from Farkas...
4526 std::vector<std::shared_ptr<ProofNode>> conflictPfs;
4527 // Assume the negated getLiteral version of the implied constaint
4528 // then rewrite it into proof normal form.
4529 conflictPfs.push_back(
4530 d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM,
4531 {d_pnm->mkAssume(implied->getLiteral().negate())},
4532 {implied->getNegation()->getProofLiteral()}));
4533 // Add the explaination proofs.
4534 for (const auto constraint : explain)
4535 {
4536 NodeBuilder nb;
4537 conflictPfs.push_back(constraint->externalExplainByAssertions(nb));
4538 }
4539 // Collect the farkas coefficients, as nodes.
4540 std::vector<Node> farkasCoefficients;
4541 farkasCoefficients.reserve(coeffs->size());
4542 auto nm = NodeManager::currentNM();
4543 std::transform(
4544 coeffs->begin(),
4545 coeffs->end(),
4546 std::back_inserter(farkasCoefficients),
4547 [nm](const Rational& r) { return nm->mkConst<Rational>(r); });
4548
4549 // Prove bottom.
4550 auto sumPf = d_pnm->mkNode(
4551 PfRule::MACRO_ARITH_SCALE_SUM_UB, conflictPfs, farkasCoefficients);
4552 auto botPf = d_pnm->mkNode(
4553 PfRule::MACRO_SR_PRED_TRANSFORM, {sumPf}, {nm->mkConst(false)});
4554
4555 // Prove the conflict
4556 std::vector<Node> assumptions;
4557 assumptions.reserve(clause.getNumChildren());
4558 std::transform(clause.begin(),
4559 clause.end(),
4560 std::back_inserter(assumptions),
4561 [](TNode r) { return r.negate(); });
4562 auto notAndNotPf = d_pnm->mkScope(botPf, assumptions);
4563
4564 // Convert it to a clause
4565 auto orNotNotPf = d_pnm->mkNode(PfRule::NOT_AND, {notAndNotPf}, {});
4566 clausePf = d_pnm->mkNode(
4567 PfRule::MACRO_SR_PRED_TRANSFORM, {orNotNotPf}, {clause});
4568
4569 // Output it
4570 TrustNode trustedClause = d_pfGen->mkTrustNode(clause, clausePf);
4571 outputTrustedLemma(trustedClause, InferenceId::ARITH_ROW_IMPL);
4572 }
4573 else
4574 {
4575 outputLemma(clause, InferenceId::ARITH_ROW_IMPL);
4576 }
4577 }else{
4578 Assert(!implied->negationHasProof());
4579 implied->impliedByFarkas(explain, coeffs, false);
4580 implied->tryToPropagate();
4581 }
4582 return true;
4583 }
4584
4585 if(Debug.isOn("arith::prop")){
4586 Debug("arith::prop")
4587 << "failed " << v << " " << assertedToTheTheory << " "
4588 << canBePropagated << " " << hasProof << " " << implied << endl;
4589 d_partialModel.printModel(v, Debug("arith::prop"));
4590 }
4591 return false;
4592 }
4593
4594 bool TheoryArithPrivate::propagateCandidateRow(RowIndex ridx){
4595 BoundCounts hasCount = d_linEq.hasBoundCount(ridx);
4596 uint32_t rowLength = d_tableau.getRowLength(ridx);
4597
4598 bool success = false;
4599 static int instance = 0;
4600 ++instance;
4601
4602 Debug("arith::prop")
4603 << "propagateCandidateRow " << instance << " attempt " << rowLength << " " << hasCount << endl;
4604
4605 if (rowLength >= options::arithPropagateMaxLength()
4606 && Random::getRandom().pickWithProb(
4607 1.0 - double(options::arithPropagateMaxLength()) / rowLength))
4608 {
4609 return false;
4610 }
4611
4612 if(hasCount.lowerBoundCount() == rowLength){
4613 success |= attemptFull(ridx, false);
4614 }else if(hasCount.lowerBoundCount() + 1 == rowLength){
4615 success |= attemptSingleton(ridx, false);
4616 }
4617
4618 if(hasCount.upperBoundCount() == rowLength){
4619 success |= attemptFull(ridx, true);
4620 }else if(hasCount.upperBoundCount() + 1 == rowLength){
4621 success |= attemptSingleton(ridx, true);
4622 }
4623 return success;
4624 }
4625
4626 void TheoryArithPrivate::dumpUpdatedBoundsToRows(){
4627 Assert(d_candidateRows.empty());
4628 DenseSet::const_iterator i = d_updatedBounds.begin();
4629 DenseSet::const_iterator end = d_updatedBounds.end();
4630 for(; i != end; ++i){
4631 ArithVar var = *i;
4632 if(d_tableau.isBasic(var)){
4633 RowIndex ridx = d_tableau.basicToRowIndex(var);
4634 d_candidateRows.softAdd(ridx);
4635 }else{
4636 Tableau::ColIterator basicIter = d_tableau.colIterator(var);
4637 for(; !basicIter.atEnd(); ++basicIter){
4638 const Tableau::Entry& entry = *basicIter;
4639 RowIndex ridx = entry.getRowIndex();
4640 d_candidateRows.softAdd(ridx);
4641 }
4642 }
4643 }
4644 d_updatedBounds.purge();
4645 }
4646
4647 const BoundsInfo& TheoryArithPrivate::boundsInfo(ArithVar basic) const{
4648 RowIndex ridx = d_tableau.basicToRowIndex(basic);
4649 return d_rowTracking[ridx];
4650 }
4651
4652 std::pair<bool, Node> TheoryArithPrivate::entailmentCheck(TNode lit, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out){
4653 using namespace inferbounds;
4654
4655 // l k r
4656 // diff : (l - r) k 0
4657 Debug("arith::entailCheck") << "TheoryArithPrivate::entailmentCheck(" << lit << ")"<< endl;
4658 Kind k;
4659 int primDir;
4660 Rational lm, rm, dm;
4661 Node lp, rp, dp;
4662 DeltaRational sep;
4663 bool successful = decomposeLiteral(lit, k, primDir, lm, lp, rm, rp, dm, dp, sep);
4664 if(!successful) { return make_pair(false, Node::null()); }
4665
4666 if(dp.getKind() == CONST_RATIONAL){
4667 Node eval = Rewriter::rewrite(lit);
4668 Assert(eval.getKind() == kind::CONST_BOOLEAN);
4669 // if true, true is an acceptable explaination
4670 // if false, the node is uninterpreted and eval can be forgotten
4671 return make_pair(eval.getConst<bool>(), eval);
4672 }
4673 Assert(dm != Rational(0));
4674 Assert(primDir == 1 || primDir == -1);
4675
4676 int negPrim = -primDir;
4677
4678 int secDir = (k == EQUAL || k == DISTINCT) ? negPrim: 0;
4679 int negSecDir = (k == EQUAL || k == DISTINCT) ? primDir: 0;
4680
4681 // primDir*[lm*( lp )] k primDir*[ [rm*( rp )] + sep ]
4682 // primDir*[lm*( lp ) - rm*( rp ) ] k primDir*sep
4683 // primDir*[dm * dp] k primDir*sep
4684
4685 std::pair<Node, DeltaRational> bestPrimLeft, bestNegPrimRight, bestPrimDiff, tmp;
4686 std::pair<Node, DeltaRational> bestSecLeft, bestNegSecRight, bestSecDiff;
4687 bestPrimLeft.first = Node::null(); bestNegPrimRight.first = Node::null(); bestPrimDiff.first = Node::null();
4688 bestSecLeft.first = Node::null(); bestNegSecRight.first = Node::null(); bestSecDiff.first = Node::null();
4689
4690
4691
4692 ArithEntailmentCheckParameters::const_iterator alg, alg_end;
4693 for( alg = params.begin(), alg_end = params.end(); alg != alg_end; ++alg ){
4694 const inferbounds::InferBoundAlgorithm& ibalg = *alg;
4695
4696 Debug("arith::entailCheck") << "entailmentCheck trying " << (inferbounds::Algorithms) ibalg.getAlgorithm() << endl;
4697 switch(ibalg.getAlgorithm()){
4698 case inferbounds::None:
4699 break;
4700 case inferbounds::Lookup:
4701 case inferbounds::RowSum:
4702 {
4703 typedef void (TheoryArithPrivate::*EntailmentCheckFunc)(std::pair<Node, DeltaRational>&, int, TNode) const;
4704
4705 EntailmentCheckFunc ecfunc =
4706 (ibalg.getAlgorithm() == inferbounds::Lookup)
4707 ? (&TheoryArithPrivate::entailmentCheckBoundLookup)
4708 : (&TheoryArithPrivate::entailmentCheckRowSum);
4709
4710 (*this.*ecfunc)(tmp, primDir * lm.sgn(), lp);
4711 setToMin(primDir * lm.sgn(), bestPrimLeft, tmp);
4712
4713 (*this.*ecfunc)(tmp, negPrim * rm.sgn(), rp);
4714 setToMin(negPrim * rm.sgn(), bestNegPrimRight, tmp);
4715
4716 (*this.*ecfunc)(tmp, secDir * lm.sgn(), lp);
4717 setToMin(secDir * lm.sgn(), bestSecLeft, tmp);
4718
4719 (*this.*ecfunc)(tmp, negSecDir * rm.sgn(), rp);
4720 setToMin(negSecDir * rm.sgn(), bestNegSecRight, tmp);
4721
4722 (*this.*ecfunc)(tmp, primDir * dm.sgn(), dp);
4723 setToMin(primDir * dm.sgn(), bestPrimDiff, tmp);
4724
4725 (*this.*ecfunc)(tmp, secDir * dm.sgn(), dp);
4726 setToMin(secDir * dm.sgn(), bestSecDiff, tmp);
4727 }
4728 break;
4729 default:
4730 Unhandled();
4731 }
4732
4733 // turn bounds on prim * left and -prim * right into bounds on prim * diff
4734 if(!bestPrimLeft.first.isNull() && !bestNegPrimRight.first.isNull()){
4735 // primDir*lm* lp <= primDir*lm*L
4736 // -primDir*rm* rp <= -primDir*rm*R
4737 // primDir*lm* lp -primDir*rm* rp <= primDir*lm*L - primDir*rm*R
4738 // primDir [lm* lp -rm* rp] <= primDir[lm*L - *rm*R]
4739 // primDir [dm * dp] <= primDir[lm*L - *rm*R]
4740 // primDir [dm * dp] <= primDir * dm * ([lm*L - *rm*R]/dm)
4741 tmp.second = ((bestPrimLeft.second * lm) - (bestNegPrimRight.second * rm)) / dm;
4742 tmp.first = (bestPrimLeft.first).andNode(bestNegPrimRight.first);
4743 setToMin(primDir, bestPrimDiff, tmp);
4744 }
4745
4746 // turn bounds on sec * left and sec * right into bounds on sec * diff
4747 if(secDir != 0 && !bestSecLeft.first.isNull() && !bestNegSecRight.first.isNull()){
4748 // secDir*lm* lp <= secDir*lm*L
4749 // -secDir*rm* rp <= -secDir*rm*R
4750 // secDir*lm* lp -secDir*rm* rp <= secDir*lm*L - secDir*rm*R
4751 // secDir [lm* lp -rm* rp] <= secDir[lm*L - *rm*R]
4752 // secDir [dm * dp] <= secDir[lm*L - *rm*R]
4753 // secDir [dm * dp] <= secDir * dm * ([lm*L - *rm*R]/dm)
4754 tmp.second = ((bestSecLeft.second * lm) - (bestNegSecRight.second * rm)) / dm;
4755 tmp.first = (bestSecLeft.first).andNode(bestNegSecRight.first);
4756 setToMin(secDir, bestSecDiff, tmp);
4757 }
4758
4759 switch(k){
4760 case LEQ:
4761 if(!bestPrimDiff.first.isNull()){
4762 DeltaRational d = (bestPrimDiff.second * dm);
4763 if((primDir > 0 && d <= sep) || (primDir < 0 && d >= sep) ){
4764 Debug("arith::entailCheck") << "entailmentCheck found "
4765 << primDir << "*" << dm << "*(" << dp<<")"
4766 << " <= " << primDir << "*" << dm << "*" << bestPrimDiff.second
4767 << " <= " << primDir << "*" << sep << endl
4768 << " by " << bestPrimDiff.first << endl;
4769 Assert(bestPrimDiff.second * (Rational(primDir) * dm)
4770 <= (sep * Rational(primDir)));
4771 return make_pair(true, bestPrimDiff.first);
4772 }
4773 }
4774 break;
4775 case EQUAL:
4776 if(!bestPrimDiff.first.isNull() && !bestSecDiff.first.isNull()){
4777 // Is primDir [dm * dp] == primDir * sep entailed?
4778 // Iff [dm * dp] == sep entailed?
4779 // Iff dp == sep / dm entailed?
4780 // Iff dp <= sep / dm and dp >= sep / dm entailed?
4781
4782 // primDir [dm * dp] <= primDir * dm * U
4783 // secDir [dm * dp] <= secDir * dm * L
4784
4785 // Suppose primDir * dm > 0
4786 // then secDir * dm < 0
4787 // dp >= (secDir * L) / secDir * dm
4788 // dp >= (primDir * L) / primDir * dm
4789 //
4790 // dp <= U / dm
4791 // dp >= L / dm
4792 // dp == sep / dm entailed iff U == L == sep
4793 // Suppose primDir * dm < 0
4794 // then secDir * dm > 0
4795 // dp >= U / dm
4796 // dp <= L / dm
4797 // dp == sep / dm entailed iff U == L == sep
4798 if(bestPrimDiff.second == bestSecDiff.second){
4799 if(bestPrimDiff.second == sep){
4800 return make_pair(true, (bestPrimDiff.first).andNode(bestSecDiff.first));
4801 }
4802 }
4803 }
4804 // intentionally fall through to DISTINCT case!
4805 // entailments of negations are eager exit cases for EQUAL
4806 CVC5_FALLTHROUGH;
4807 case DISTINCT:
4808 if(!bestPrimDiff.first.isNull()){
4809 // primDir [dm * dp] <= primDir * dm * U < primDir * sep
4810 if((primDir > 0 && (bestPrimDiff.second * dm < sep)) ||
4811 (primDir < 0 && (bestPrimDiff.second * dm > sep))){
4812 // entailment of negation
4813 if(k == DISTINCT){
4814 return make_pair(true, bestPrimDiff.first);
4815 }else{
4816 Assert(k == EQUAL);
4817 return make_pair(false, Node::null());
4818 }
4819 }
4820 }
4821 if(!bestSecDiff.first.isNull()){
4822 // If primDir [dm * dp] > primDir * sep, then this is not entailed.
4823 // If primDir [dm * dp] >= primDir * dm * L > primDir * sep
4824 // -primDir * dm * L < -primDir * sep
4825 // secDir * dm * L < secDir * sep
4826 if((secDir > 0 && (bestSecDiff.second * dm < sep)) ||
4827 (secDir < 0 && (bestSecDiff.second * dm > sep))){
4828 if(k == DISTINCT){
4829 return make_pair(true, bestSecDiff.first);
4830 }else{
4831 Assert(k == EQUAL);
4832 return make_pair(false, Node::null());
4833 }
4834 }
4835 }
4836
4837 break;
4838 default:
4839 Unreachable();
4840 break;
4841 }
4842 }
4843 return make_pair(false, Node::null());
4844 }
4845
4846 bool TheoryArithPrivate::decomposeTerm(Node term, Rational& m, Node& p, Rational& c){
4847 Node t = Rewriter::rewrite(term);
4848 if(!Polynomial::isMember(t)){
4849 return false;
4850 }
4851
4852 // TODO Speed up
4853 preprocessing::util::ContainsTermITEVisitor ctv;
4854 if(ctv.containsTermITE(t)){
4855 return false;
4856 }
4857
4858 Polynomial poly = Polynomial::parsePolynomial(t);
4859 if(poly.isConstant()){
4860 c = poly.getHead().getConstant().getValue();
4861 p = mkRationalNode(Rational(0));
4862 m = Rational(1);
4863 return true;
4864 }else if(poly.containsConstant()){
4865 c = poly.getHead().getConstant().getValue();
4866 poly = poly.getTail();
4867 }else{
4868 c = Rational(0);
4869 }
4870 Assert(!poly.isConstant());
4871 Assert(!poly.containsConstant());
4872
4873 const bool intVars = poly.allIntegralVariables();
4874
4875 if(intVars){
4876 m = Rational(1);
4877 if(!poly.isIntegral()){
4878 Integer denom = poly.denominatorLCM();
4879 m /= denom;
4880 poly = poly * denom;
4881 }
4882 Integer g = poly.gcd();
4883 m *= g;
4884 poly = poly * Rational(1,g);
4885 Assert(poly.isIntegral());
4886 Assert(poly.leadingCoefficientIsPositive());
4887 }else{
4888 Assert(!intVars);
4889 m = poly.getHead().getConstant().getValue();
4890 poly = poly * m.inverse();
4891 Assert(poly.leadingCoefficientIsAbsOne());
4892 }
4893 p = poly.getNode();
4894 return true;
4895 }
4896
4897 void TheoryArithPrivate::setToMin(int sgn, std::pair<Node, DeltaRational>& min, const std::pair<Node, DeltaRational>& e){
4898 if(sgn != 0){
4899 if(min.first.isNull() && !e.first.isNull()){
4900 min = e;
4901 }else if(!min.first.isNull() && !e.first.isNull()){
4902 if(sgn > 0 && min.second > e.second){
4903 min = e;
4904 }else if(sgn < 0 && min.second < e.second){
4905 min = e;
4906 }
4907 }
4908 }
4909 }
4910
4911 // std::pair<bool, Node> TheoryArithPrivate::entailmentUpperCheck(const Rational& lm, Node lp, const Rational& rm, Node rp, const DeltaRational& sep, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out){
4912
4913 // Rational negRM = -rm;
4914 // Node diff = NodeManager::currentNM()->mkNode(MULT, mkRationalConstan(lm), lp) + (negRM * rp);
4915
4916 // Rational diffm;
4917 // Node diffp;
4918 // decompose(diff, diffm, diffNode);
4919
4920
4921 // std::pair<Node, DeltaRational> bestUbLeft, bestLbRight, bestUbDiff, tmp;
4922 // bestUbLeft = bestLbRight = bestUbDiff = make_pair(Node::Null(), DeltaRational());
4923
4924 // return make_pair(false, Node::null());
4925 // }
4926
4927 /**
4928 * Decomposes a literal into the form:
4929 * dir*[lm*( lp )] k dir*[ [rm*( rp )] + sep ]
4930 * dir*[dm* dp] k dir *sep
4931 * dir is either 1 or -1
4932 */
4933 bool TheoryArithPrivate::decomposeLiteral(Node lit, Kind& k, int& dir, Rational& lm, Node& lp, Rational& rm, Node& rp, Rational& dm, Node& dp, DeltaRational& sep){
4934 bool negated = (lit.getKind() == kind::NOT);
4935 TNode atom = negated ? lit[0] : lit;
4936
4937 TNode left = atom[0];
4938 TNode right = atom[1];
4939
4940 // left : lm*( lp ) + lc
4941 // right: rm*( rp ) + rc
4942 Rational lc, rc;
4943 bool success = decomposeTerm(left, lm, lp, lc);
4944 if(!success){ return false; }
4945 success = decomposeTerm(right, rm, rp, rc);
4946 if(!success){ return false; }
4947
4948 Node diff = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::MINUS, left, right));
4949 Rational dc;
4950 success = decomposeTerm(diff, dm, dp, dc);
4951 Assert(success);
4952
4953 // reduce the kind of the to not include literals
4954 // GT, NOT LEQ
4955 // GEQ, NOT LT
4956 // LT, NOT GEQ
4957 // LEQ, NOT LT
4958 Kind atomKind = atom.getKind();
4959 Kind normKind = negated ? negateKind(atomKind) : atomKind;
4960
4961 if(normKind == GEQ || normKind == GT){
4962 dir = -1;
4963 normKind = (normKind == GEQ) ? LEQ : LT;
4964 }else{
4965 dir = 1;
4966 }
4967
4968 Debug("arith::decomp") << "arith::decomp "
4969 << lit << "(" << normKind << "*" << dir << ")"<< endl
4970 << " left:" << lc << " + " << lm << "*(" << lp << ") : " <<left << endl
4971 << " right:" << rc << " + " << rm << "*(" << rp << ") : " << right << endl
4972 << " diff: " << dc << " + " << dm << "*("<< dp <<"): " << diff << endl
4973 << " sep: " << sep << endl;
4974
4975
4976 // k in LT, LEQ, EQUAL, DISEQUAL
4977 // [dir*lm*( lp ) + dir*lc] k [dir*rm*( rp ) + dir*rc]
4978 Rational change = rc - lc;
4979 Assert(change == (-dc));
4980 // [dir*lm*( lp )] k [dir*rm*( rp ) + dir*(rc - lc)]
4981 if(normKind == LT){
4982 sep = DeltaRational(change, Rational(-1));
4983 k = LEQ;
4984 }else{
4985 sep = DeltaRational(change);
4986 k = normKind;
4987 }
4988 // k in LEQ, EQUAL, DISEQUAL
4989 // dir*lm*( lp ) k [dir*rm*( rp )] + dir*(sep + d * delta)
4990 return true;
4991 }
4992
4993 /**
4994 * Precondition:
4995 * tp is a polynomial not containing an ite.
4996 * either tp is constant or contains no constants.
4997 * Post:
4998 * if tmp.first is not null, then
4999 * sgn * tp <= sgn * tmp.second
5000 */
5001 void TheoryArithPrivate::entailmentCheckBoundLookup(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const {
5002 tmp.first = Node::null();
5003 if(sgn == 0){ return; }
5004
5005 Assert(Polynomial::isMember(tp));
5006 if(tp.getKind() == CONST_RATIONAL){
5007 tmp.first = mkBoolNode(true);
5008 tmp.second = DeltaRational(tp.getConst<Rational>());
5009 }else if(d_partialModel.hasArithVar(tp)){
5010 Assert(tp.getKind() != CONST_RATIONAL);
5011 ArithVar v = d_partialModel.asArithVar(tp);
5012 Assert(v != ARITHVAR_SENTINEL);
5013 ConstraintP c = (sgn > 0)
5014 ? d_partialModel.getUpperBoundConstraint(v)
5015 : d_partialModel.getLowerBoundConstraint(v);
5016 if(c != NullConstraint){
5017 tmp.first = Constraint::externalExplainByAssertions({c});
5018 tmp.second = c->getValue();
5019 }
5020 }
5021 }
5022
5023 void TheoryArithPrivate::entailmentCheckRowSum(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const {
5024 tmp.first = Node::null();
5025 if(sgn == 0){ return; }
5026 if(tp.getKind() != PLUS){ return; }
5027 Assert(Polynomial::isMember(tp));
5028
5029 tmp.second = DeltaRational(0);
5030 NodeBuilder nb(kind::AND);
5031
5032 Polynomial p = Polynomial::parsePolynomial(tp);
5033 for(Polynomial::iterator i = p.begin(), iend = p.end(); i != iend; ++i) {
5034 Monomial m = *i;
5035 Node x = m.getVarList().getNode();
5036 if(d_partialModel.hasArithVar(x)){
5037 ArithVar v = d_partialModel.asArithVar(x);
5038 const Rational& coeff = m.getConstant().getValue();
5039 int dir = sgn * coeff.sgn();
5040 ConstraintP c = (dir > 0)
5041 ? d_partialModel.getUpperBoundConstraint(v)
5042 : d_partialModel.getLowerBoundConstraint(v);
5043 if(c != NullConstraint){
5044 tmp.second += c->getValue() * coeff;
5045 c->externalExplainByAssertions(nb);
5046 }else{
5047 //failed
5048 return;
5049 }
5050 }else{
5051 // failed
5052 return;
5053 }
5054 }
5055 // success
5056 tmp.first = nb;
5057 }
5058
5059 ArithProofRuleChecker* TheoryArithPrivate::getProofChecker()
5060 {
5061 return &d_checker;
5062 }
5063
5064 } // namespace arith
5065 } // namespace theory
5066 } // namespace cvc5