GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/ext/split_zero_check.cpp Lines: 4 17 23.5 %
Date: 2021-03-23 Branches: 2 48 4.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file split_zero_check.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Gereon Kremer
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 Implementation of split zero check
13
 **/
14
15
#include "theory/arith/nl/ext/split_zero_check.h"
16
17
#include "expr/node.h"
18
#include "expr/proof.h"
19
#include "theory/arith/arith_msum.h"
20
#include "theory/arith/inference_manager.h"
21
#include "theory/arith/nl/nl_model.h"
22
#include "theory/arith/nl/ext/ext_state.h"
23
#include "theory/rewriter.h"
24
25
namespace CVC4 {
26
namespace theory {
27
namespace arith {
28
namespace nl {
29
30
4391
SplitZeroCheck::SplitZeroCheck(ExtState* data)
31
4391
    : d_data(data), d_zero_split(d_data->d_ctx)
32
{
33
4391
}
34
35
void SplitZeroCheck::check()
36
{
37
  for (unsigned i = 0; i < d_data->d_ms_vars.size(); i++)
38
  {
39
    Node v = d_data->d_ms_vars[i];
40
    if (d_zero_split.insert(v))
41
    {
42
      Node eq = Rewriter::rewrite(v.eqNode(d_data->d_zero));
43
      Node lem = eq.orNode(eq.negate());
44
      CDProof* proof = nullptr;
45
      if (d_data->isProofEnabled())
46
      {
47
        proof = d_data->getProof();
48
        proof->addStep(lem, PfRule::SPLIT, {}, {eq});
49
      }
50
      d_data->d_im.addPendingPhaseRequirement(eq, true);
51
      d_data->d_im.addPendingLemma(
52
          lem, InferenceId::ARITH_NL_SPLIT_ZERO, proof);
53
    }
54
  }
55
}
56
57
}  // namespace nl
58
}  // namespace arith
59
}  // namespace theory
60
26685
}  // namespace CVC4