GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/theory_arith_private.cpp Lines: 1833 3213 57.0 %
Date: 2021-03-23 Branches: 3838 14108 27.2 %

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