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