GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/nl_lemma_utils.h Lines: 18 19 94.7 %
Date: 2021-03-23 Branches: 3 8 37.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file nl_lemma_utils.h
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 Utilities for processing lemmas from the non-linear solver
13
 **/
14
15
#ifndef CVC4__THEORY__ARITH__NL__NL_LEMMA_UTILS_H
16
#define CVC4__THEORY__ARITH__NL__NL_LEMMA_UTILS_H
17
18
#include <tuple>
19
#include <vector>
20
21
#include "expr/node.h"
22
#include "theory/theory_inference.h"
23
24
namespace CVC4 {
25
namespace theory {
26
namespace arith {
27
namespace nl {
28
29
class NlModel;
30
class NonlinearExtension;
31
32
/**
33
 * The data structure for a single lemma to process by the non-linear solver,
34
 * including the lemma itself and whether it should be preprocessed (see
35
 * OutputChannel::lemma).
36
 *
37
 * This also includes data structures that encapsulate the side effect of adding
38
 * this lemma in the non-linear solver. This is used to specify how the state of
39
 * the non-linear solver should update. This includes:
40
 * - A set of secant points to record (for transcendental secant plane
41
 * inferences).
42
 */
43
class NlLemma : public SimpleTheoryLemma
44
{
45
 public:
46
230
  NlLemma(InferenceId inf,
47
          Node n,
48
          LemmaProperty p = LemmaProperty::NONE,
49
          ProofGenerator* pg = nullptr)
50
230
      : SimpleTheoryLemma(inf, n, p, pg)
51
  {
52
230
  }
53
230
  ~NlLemma() {}
54
55
  TrustNode processLemma(LemmaProperty& p) override;
56
57
  /** secant points to add
58
   *
59
   * A member (tf, d, c) in this vector indicates that point c should be added
60
   * to the list of secant points for an application of a transcendental
61
   * function tf for Taylor degree d. This is used for incremental linearization
62
   * for underapproximation (resp. overapproximations) of convex (resp.
63
   * concave) regions of transcendental functions. For details, see
64
   * Cimatti et al., CADE 2017.
65
   */
66
  std::vector<std::tuple<Node, unsigned, Node> > d_secantPoint;
67
68
  NonlinearExtension* d_nlext;
69
};
70
/**
71
 * Writes a non-linear lemma to a stream.
72
 */
73
std::ostream& operator<<(std::ostream& out, NlLemma& n);
74
75
struct SortNlModel
76
{
77
3464
  SortNlModel()
78
3464
      : d_nlm(nullptr),
79
        d_isConcrete(true),
80
        d_isAbsolute(false),
81
3464
        d_reverse_order(false)
82
  {
83
3464
  }
84
  /** pointer to the model */
85
  NlModel* d_nlm;
86
  /** are we comparing concrete model values? */
87
  bool d_isConcrete;
88
  /** are we comparing absolute values? */
89
  bool d_isAbsolute;
90
  /** are we in reverse order? */
91
  bool d_reverse_order;
92
  /** the comparison */
93
  bool operator()(Node i, Node j);
94
};
95
96
/**
97
 * Wrapper for std::sort that uses SortNlModel to sort an iterator range.
98
 */
99
template <typename It>
100
394
void sortByNlModel(It begin,
101
                   It end,
102
                   NlModel* model,
103
                   bool concrete = true,
104
                   bool absolute = false,
105
                   bool reverse = false)
106
{
107
394
  SortNlModel smv;
108
394
  smv.d_nlm = model;
109
394
  smv.d_isConcrete = concrete;
110
394
  smv.d_isAbsolute = absolute;
111
394
  smv.d_reverse_order = reverse;
112
394
  std::sort(begin, end, smv);
113
394
}
114
115
struct SortNonlinearDegree
116
{
117
520
  SortNonlinearDegree(const std::map<Node, unsigned>& m) : d_mdegree(m) {}
118
  /** pointer to the non-linear extension */
119
  const std::map<Node, unsigned>& d_mdegree;
120
  /** Get the degree of n in d_mdegree */
121
  unsigned getDegree(Node n) const;
122
  /**
123
   * Sorts by degree of the monomials, where lower degree monomials come
124
   * first.
125
   */
126
  bool operator()(Node i, Node j);
127
};
128
129
/** An argument trie, for computing congruent terms */
130
7976
class ArgTrie
131
{
132
 public:
133
  /** children of this node */
134
  std::map<Node, ArgTrie> d_children;
135
  /** the data of this node */
136
  Node d_data;
137
  /**
138
   * Set d as the data on the node whose path is [args], return either d if
139
   * that node has no data, or the data that already occurs there.
140
   */
141
  Node add(Node d, const std::vector<Node>& args);
142
};
143
144
}  // namespace nl
145
}  // namespace arith
146
}  // namespace theory
147
}  // namespace CVC4
148
149
#endif /* CVC4__THEORY__ARITH__NL_LEMMA_UTILS_H */