GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/ext/ext_state.cpp Lines: 46 46 100.0 %
Date: 2021-03-22 Branches: 82 166 49.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ext_state.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Gereon Kremer, Tim King
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 Common data shared by multiple checks
13
 **/
14
15
#include "theory/arith/nl/ext/ext_state.h"
16
17
#include <vector>
18
19
#include "expr/node.h"
20
#include "expr/proof.h"
21
#include "theory/arith/inference_manager.h"
22
#include "theory/arith/nl/ext/monomial.h"
23
#include "theory/arith/nl/nl_model.h"
24
#include "theory/arith/nl/nl_lemma_utils.h"
25
26
27
namespace CVC4 {
28
namespace theory {
29
namespace arith {
30
namespace nl {
31
32
4389
ExtState::ExtState(InferenceManager& im,
33
                   NlModel& model,
34
                   ProofNodeManager* pnm,
35
4389
                   context::UserContext* c)
36
4389
    : d_im(im), d_model(model), d_pnm(pnm), d_ctx(c)
37
{
38
4389
  d_false = NodeManager::currentNM()->mkConst(false);
39
4389
  d_true = NodeManager::currentNM()->mkConst(true);
40
4389
  d_zero = NodeManager::currentNM()->mkConst(Rational(0));
41
4389
  d_one = NodeManager::currentNM()->mkConst(Rational(1));
42
4389
  d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
43
4389
  if (d_pnm != nullptr)
44
  {
45
401
    d_proof.reset(new CDProofSet<CDProof>(d_pnm, d_ctx, "nl-ext"));
46
  }
47
4389
}
48
49
2742
void ExtState::init(const std::vector<Node>& xts)
50
{
51
2742
  d_ms_vars.clear();
52
2742
  d_ms.clear();
53
2742
  d_mterms.clear();
54
2742
  d_tplane_refine.clear();
55
56
2742
  Trace("nl-ext-mv") << "Extended terms : " << std::endl;
57
  // for computing congruence
58
5484
  std::map<Kind, ArgTrie> argTrie;
59
23167
  for (unsigned i = 0, xsize = xts.size(); i < xsize; i++)
60
  {
61
40850
    Node a = xts[i];
62
20425
    d_model.computeConcreteModelValue(a);
63
20425
    d_model.computeAbstractModelValue(a);
64
20425
    d_model.printModelValue("nl-ext-mv", a);
65
20425
    Kind ak = a.getKind();
66
20425
    if (ak == Kind::NONLINEAR_MULT)
67
    {
68
14043
      d_ms.push_back(a);
69
70
      // context-independent registration
71
14043
      d_mdb.registerMonomial(a);
72
73
14043
      const std::vector<Node>& varList = d_mdb.getVariableList(a);
74
40649
      for (const Node& v : varList)
75
      {
76
26606
        if (std::find(d_ms_vars.begin(), d_ms_vars.end(), v) == d_ms_vars.end())
77
        {
78
12845
          d_ms_vars.push_back(v);
79
        }
80
      }
81
      // mark processed if has a "one" factor (will look at reduced monomial)?
82
    }
83
  }
84
85
  // register constants
86
2742
  d_mdb.registerMonomial(d_one);
87
88
  // register variables
89
2742
  Trace("nl-ext-mv") << "Variables in monomials : " << std::endl;
90
15587
  for (unsigned i = 0; i < d_ms_vars.size(); i++)
91
  {
92
25690
    Node v = d_ms_vars[i];
93
12845
    d_mdb.registerMonomial(v);
94
12845
    d_model.computeConcreteModelValue(v);
95
12845
    d_model.computeAbstractModelValue(v);
96
12845
    d_model.printModelValue("nl-ext-mv", v);
97
  }
98
99
2742
  Trace("nl-ext") << "We have " << d_ms.size() << " monomials." << std::endl;
100
2742
}
101
102
4774
bool ExtState::isProofEnabled() const { return d_proof.get() != nullptr; }
103
104
677
CDProof* ExtState::getProof()
105
{
106
677
  Assert(isProofEnabled());
107
677
  return d_proof->allocateProof(d_ctx);
108
}
109
110
}  // namespace nl
111
}  // namespace arith
112
}  // namespace theory
113
26676
}  // namespace CVC4