GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/ext/ext_state.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ext_state.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Gereon Kremer, Andrew Reynolds, 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
#ifndef CVC4__THEORY__ARITH__NL__EXT__SHARED_CHECK_DATA_H
16
#define CVC4__THEORY__ARITH__NL__EXT__SHARED_CHECK_DATA_H
17
18
#include <vector>
19
20
#include "expr/node.h"
21
#include "expr/proof_set.h"
22
#include "theory/arith/nl/ext/monomial.h"
23
24
namespace CVC4 {
25
26
class CDProof;
27
28
namespace theory {
29
namespace arith {
30
31
class InferenceManager;
32
33
namespace nl {
34
35
class NlModel;
36
37
4386
struct ExtState
38
{
39
  ExtState(InferenceManager& im,
40
           NlModel& model,
41
           ProofNodeManager* pnm,
42
           context::UserContext* c);
43
44
  void init(const std::vector<Node>& xts);
45
46
  /**
47
   * Checks whether proofs are enabled.
48
   */
49
  bool isProofEnabled() const;
50
  /**
51
   * Creates and returns a new LazyCDProof that can be used to prove some lemma.
52
   */
53
  CDProof* getProof();
54
55
  Node d_false;
56
  Node d_true;
57
  Node d_zero;
58
  Node d_one;
59
  Node d_neg_one;
60
61
  /** The inference manager that we push conflicts and lemmas to. */
62
  InferenceManager& d_im;
63
  /** Reference to the non-linear model object */
64
  NlModel& d_model;
65
  /**
66
   * Pointer to the current proof node manager. nullptr, if proofs are
67
   * disabled.
68
   */
69
  ProofNodeManager* d_pnm;
70
  /** The user context. */
71
  context::UserContext* d_ctx;
72
  /**
73
   * A CDProofSet that hands out CDProof objects for lemmas.
74
   */
75
  std::unique_ptr<CDProofSet<CDProof>> d_proof;
76
77
  // information about monomials
78
  std::vector<Node> d_ms;
79
  std::vector<Node> d_ms_vars;
80
  std::vector<Node> d_mterms;
81
82
  /** Context-independent database of monomial information */
83
  MonomialDb d_mdb;
84
85
  // ( x*y, x*z, y ) for each pair of monomials ( x*y, x*z ) with common factors
86
  std::map<Node, std::map<Node, Node> > d_mono_diff;
87
  /** the set of monomials we should apply tangent planes to */
88
  std::unordered_set<Node, NodeHashFunction> d_tplane_refine;
89
};
90
91
}  // namespace nl
92
}  // namespace arith
93
}  // namespace theory
94
}  // namespace CVC4
95
96
#endif