GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/theory_arith.cpp Lines: 132 133 99.2 %
Date: 2021-03-22 Branches: 176 376 46.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_arith.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, Alex Ozdemir
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.h"
19
20
#include "expr/proof_rule.h"
21
#include "options/smt_options.h"
22
#include "smt/smt_statistics_registry.h"
23
#include "theory/arith/arith_rewriter.h"
24
#include "theory/arith/infer_bounds.h"
25
#include "theory/arith/nl/nonlinear_extension.h"
26
#include "theory/arith/theory_arith_private.h"
27
#include "theory/ext_theory.h"
28
#include "theory/rewriter.h"
29
#include "theory/theory_model.h"
30
31
using namespace std;
32
using namespace CVC4::kind;
33
34
namespace CVC4 {
35
namespace theory {
36
namespace arith {
37
38
8995
TheoryArith::TheoryArith(context::Context* c,
39
                         context::UserContext* u,
40
                         OutputChannel& out,
41
                         Valuation valuation,
42
                         const LogicInfo& logicInfo,
43
8995
                         ProofNodeManager* pnm)
44
    : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, pnm),
45
      d_internal(
46
8995
          new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo, pnm)),
47
      d_ppRewriteTimer("theory::arith::ppRewriteTimer"),
48
      d_ppPfGen(pnm, c, "Arith::ppRewrite"),
49
8995
      d_astate(*d_internal, c, u, valuation),
50
      d_im(*this, d_astate, pnm),
51
      d_nonlinearExtension(nullptr),
52
26985
      d_arithPreproc(d_astate, d_im, pnm, logicInfo)
53
{
54
8995
  smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer);
55
56
  // indicate we are using the theory state object and inference manager
57
8995
  d_theoryState = &d_astate;
58
8995
  d_inferManager = &d_im;
59
8995
}
60
61
26976
TheoryArith::~TheoryArith(){
62
8992
  smtStatisticsRegistry()->unregisterStat(&d_ppRewriteTimer);
63
8992
  delete d_internal;
64
17984
}
65
66
8995
TheoryRewriter* TheoryArith::getTheoryRewriter() { return &d_rewriter; }
67
68
8995
bool TheoryArith::needsEqualityEngine(EeSetupInfo& esi)
69
{
70
8995
  return d_internal->needsEqualityEngine(esi);
71
}
72
8995
void TheoryArith::finishInit()
73
{
74
17990
  if (getLogicInfo().isTheoryEnabled(THEORY_ARITH)
75
8995
      && getLogicInfo().areTranscendentalsUsed())
76
  {
77
    // witness is used to eliminate square root
78
3457
    d_valuation.setUnevaluatedKind(kind::WITNESS);
79
    // we only need to add the operators that are not syntax sugar
80
3457
    d_valuation.setUnevaluatedKind(kind::EXPONENTIAL);
81
3457
    d_valuation.setUnevaluatedKind(kind::SINE);
82
3457
    d_valuation.setUnevaluatedKind(kind::PI);
83
  }
84
  // only need to create nonlinear extension if non-linear logic
85
8995
  const LogicInfo& logicInfo = getLogicInfo();
86
8995
  if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear())
87
  {
88
8778
    d_nonlinearExtension.reset(
89
4389
        new nl::NonlinearExtension(*this, d_astate, d_equalityEngine, d_pnm));
90
  }
91
  // finish initialize internally
92
8995
  d_internal->finishInit();
93
8995
}
94
95
682801
void TheoryArith::preRegisterTerm(TNode n)
96
{
97
682801
  if (d_nonlinearExtension != nullptr)
98
  {
99
315950
    d_nonlinearExtension->preRegisterTerm(n);
100
  }
101
682802
  d_internal->preRegisterTerm(n);
102
682800
}
103
104
2050
TrustNode TheoryArith::expandDefinition(Node node)
105
{
106
  // call eliminate operators, to eliminate partial operators only
107
4100
  std::vector<SkolemLemma> lems;
108
2050
  TrustNode ret = d_arithPreproc.eliminate(node, lems, true);
109
2050
  Assert(lems.empty());
110
4100
  return ret;
111
}
112
113
893833
void TheoryArith::notifySharedTerm(TNode n) { d_internal->notifySharedTerm(n); }
114
115
723373
TrustNode TheoryArith::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
116
{
117
1446746
  CodeTimer timer(d_ppRewriteTimer, /* allow_reentrant = */ true);
118
723373
  Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
119
120
723373
  if (atom.getKind() == kind::EQUAL)
121
  {
122
27947
    return ppRewriteEq(atom);
123
  }
124
695426
  Assert(Theory::theoryOf(atom) == THEORY_ARITH);
125
  // Eliminate operators. Notice we must do this here since other
126
  // theories may generate lemmas that involve non-standard operators. For
127
  // example, quantifier instantiation may use TO_INTEGER terms; SyGuS may
128
  // introduce non-standard arithmetic terms appearing in grammars.
129
  // call eliminate operators. In contrast to expandDefinitions, we eliminate
130
  // *all* extended arithmetic operators here, including total ones.
131
695432
  return d_arithPreproc.eliminate(atom, lems, false);
132
}
133
134
28681
TrustNode TheoryArith::ppRewriteEq(TNode atom)
135
{
136
28681
  Assert(atom.getKind() == kind::EQUAL);
137
28681
  if (!options::arithRewriteEq())
138
  {
139
11675
    return TrustNode::null();
140
  }
141
17006
  Assert(atom[0].getType().isReal());
142
34012
  Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1];
143
34012
  Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1];
144
34012
  Node rewritten = Rewriter::rewrite(leq.andNode(geq));
145
34012
  Debug("arith::preprocess")
146
17006
      << "arith::preprocess() : returning " << rewritten << endl;
147
  // don't need to rewrite terms since rewritten is not a non-standard op
148
17006
  if (proofsEnabled())
149
  {
150
    return d_ppPfGen.mkTrustedRewrite(
151
        atom,
152
        rewritten,
153
2645
        d_pnm->mkNode(PfRule::INT_TRUST, {}, {atom.eqNode(rewritten)}));
154
  }
155
14361
  return TrustNode::mkTrustRewrite(atom, rewritten, nullptr);
156
}
157
158
12309
Theory::PPAssertStatus TheoryArith::ppAssert(
159
    TrustNode tin, TrustSubstitutionMap& outSubstitutions)
160
{
161
12309
  return d_internal->ppAssert(tin, outSubstitutions);
162
}
163
164
91998
void TheoryArith::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
165
91998
  d_internal->ppStaticLearn(n, learned);
166
91998
}
167
168
1846007
bool TheoryArith::preCheck(Effort level)
169
{
170
1846007
  Trace("arith-check") << "TheoryArith::preCheck " << level << std::endl;
171
1846007
  return d_internal->preCheck(level);
172
}
173
174
1846007
void TheoryArith::postCheck(Effort level)
175
{
176
1846007
  Trace("arith-check") << "TheoryArith::postCheck " << level << std::endl;
177
  // check with the non-linear solver at last call
178
1846007
  if (level == Theory::EFFORT_LAST_CALL)
179
  {
180
2926
    if (d_nonlinearExtension != nullptr)
181
    {
182
2926
      d_nonlinearExtension->check(level);
183
    }
184
2926
    return;
185
  }
186
  // otherwise, check with the linear solver
187
1843081
  if (d_internal->postCheck(level))
188
  {
189
    // linear solver emitted a conflict or lemma, return
190
66348
    return;
191
  }
192
193
1776733
  if (Theory::fullEffort(level))
194
  {
195
56046
    if (d_nonlinearExtension != nullptr)
196
    {
197
25957
      d_nonlinearExtension->check(level);
198
    }
199
30089
    else if (d_internal->foundNonlinear())
200
    {
201
      // set incomplete
202
      d_im.setIncomplete();
203
    }
204
  }
205
}
206
207
5975000
bool TheoryArith::preNotifyFact(
208
    TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
209
{
210
11950000
  Trace("arith-check") << "TheoryArith::preNotifyFact: " << fact
211
5975000
                       << ", isPrereg=" << isPrereg
212
5975000
                       << ", isInternal=" << isInternal << std::endl;
213
5975000
  d_internal->preNotifyFact(atom, pol, fact);
214
  // We do not assert to the equality engine of arithmetic in the standard way,
215
  // hence we return "true" to indicate we are finished with this fact.
216
5975000
  return true;
217
}
218
219
20331
bool TheoryArith::needsCheckLastEffort() {
220
20331
  if (d_nonlinearExtension != nullptr)
221
  {
222
9918
    return d_nonlinearExtension->needsCheckLastEffort();
223
  }
224
10413
  return false;
225
}
226
227
33970
TrustNode TheoryArith::explain(TNode n) { return d_internal->explain(n); }
228
229
3023470
void TheoryArith::propagate(Effort e) {
230
3023470
  d_internal->propagate(e);
231
3023470
}
232
233
17182
bool TheoryArith::collectModelInfo(TheoryModel* m,
234
                                   const std::set<Node>& termSet)
235
{
236
  // this overrides behavior to not assert equality engine
237
17182
  return collectModelValues(m, termSet);
238
}
239
240
17182
bool TheoryArith::collectModelValues(TheoryModel* m,
241
                                     const std::set<Node>& termSet)
242
{
243
  // get the model from the linear solver
244
34364
  std::map<Node, Node> arithModel;
245
17182
  d_internal->collectModelValues(termSet, arithModel);
246
  // if non-linear is enabled, intercept the model, which may repair its values
247
17182
  if (d_nonlinearExtension != nullptr)
248
  {
249
    // Non-linear may repair values to satisfy non-linear constraints (see
250
    // documentation for NonlinearExtension::interceptModel).
251
8958
    d_nonlinearExtension->interceptModel(arithModel, termSet);
252
  }
253
  // We are now ready to assert the model.
254
322230
  for (const std::pair<const Node, Node>& p : arithModel)
255
  {
256
    // maps to constant of comparable type
257
305050
    Assert(p.first.getType().isComparableTo(p.second.getType()));
258
305050
    if (m->assertEquality(p.first, p.second, true))
259
    {
260
305048
      continue;
261
    }
262
    // If we failed to assert an equality, it is likely due to theory
263
    // combination, namely the repaired model for non-linear changed
264
    // an equality status that was agreed upon by both (linear) arithmetic
265
    // and another theory. In this case, we must add a lemma, or otherwise
266
    // we would terminate with an invalid model. Thus, we add a splitting
267
    // lemma of the form ( x = v V x != v ) where v is the model value
268
    // assigned by the non-linear solver to x.
269
2
    if (d_nonlinearExtension != nullptr)
270
    {
271
4
      Node eq = p.first.eqNode(p.second);
272
4
      Node lem = NodeManager::currentNM()->mkNode(kind::OR, eq, eq.negate());
273
2
      d_im.lemma(lem, InferenceId::ARITH_SPLIT_FOR_NL_MODEL);
274
    }
275
2
    return false;
276
  }
277
17180
  return true;
278
}
279
280
1497
void TheoryArith::notifyRestart(){
281
1497
  d_internal->notifyRestart();
282
1497
}
283
284
12416
void TheoryArith::presolve(){
285
12416
  d_internal->presolve();
286
12416
  if (d_nonlinearExtension != nullptr)
287
  {
288
4741
    d_nonlinearExtension->presolve();
289
  }
290
12416
}
291
292
1186850
EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
293
1186850
  return d_internal->getEqualityStatus(a,b);
294
}
295
296
5373
Node TheoryArith::getModelValue(TNode var) {
297
5373
  return d_internal->getModelValue( var );
298
}
299
300
5250
std::pair<bool, Node> TheoryArith::entailmentCheck(TNode lit)
301
{
302
10500
  ArithEntailmentCheckParameters def;
303
5250
  def.addLookupRowSumAlgorithms();
304
10500
  ArithEntailmentCheckSideEffects ase;
305
5250
  std::pair<bool, Node> res = d_internal->entailmentCheck(lit, def, ase);
306
10500
  return res;
307
}
308
8995
eq::ProofEqEngine* TheoryArith::getProofEqEngine()
309
{
310
8995
  return d_im.getProofEqEngine();
311
}
312
313
}/* CVC4::theory::arith namespace */
314
}/* CVC4::theory namespace */
315
26676
}/* CVC4 namespace */