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
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
|
/********************* */
/*! \file arith_msum.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2019 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.\endverbatim
**
** \brief arith_msum
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__ARITH__MSUM_H
#define __CVC4__THEORY__ARITH__MSUM_H
#include <map>
#include "expr/node.h"
namespace CVC4 {
namespace theory {
/** Arithmetic utilities regarding monomial sums.
*
* Note the following terminology:
*
* We say Node c is a {monomial constant} (or m-constant) if either:
* (a) c is a constant Rational, or
* (b) c is null.
*
* We say Node v is a {monomial variable} (or m-variable) if either:
* (a) v.getType().isReal() and v is not a constant, or
* (b) v is null.
*
* For m-constant or m-variable t, we write [t] to denote 1 if t.isNull() and
* t otherwise.
*
* A monomial m is a pair ( mvariable, mconstant ) of the form ( v, c ), which
* is interpreted as [c]*[v].
*
* A {monmoial sum} msum is represented by a std::map< Node, Node > having
* key-value pairs of the form ( mvariable, mconstant ).
* It is interpreted as:
* [msum] = sum_{( v, c ) \in msum } [c]*[v]
* It is critical that this map is ordered so that operations like adding
* two monomial sums can be done efficiently. The ordering itself is not
* important, and currently corresponds to the default ordering on Nodes.
*
* The following has utilities involving monmoial sums.
*
*/
class ArithMSum
{
public:
/** get monomial
*
* If n = n[0]*n[1] where n[0] is constant and n[1] is not,
* this function returns true, sets c to n[0] and v to n[1].
*/
static bool getMonomial(Node n, Node& c, Node& v);
/** get monomial
*
* If this function returns true, it adds the ( m-constant, m-variable )
* pair corresponding to the monomial representation of n to the
* monomial sum msum.
*
* This function returns false if the m-variable of n is already
* present in n.
*/
static bool getMonomial(Node n, std::map<Node, Node>& msum);
/** get monomial sum for real-valued term n
*
* If this function returns true, it sets msum to a monmoial sum such that
* [msum] is equivalent to n
*
* This function may return false if n is not a sum of monomials
* whose variables are pairwise unique.
* If term n is in rewritten form, this function should always return true.
*/
static bool getMonomialSum(Node n, std::map<Node, Node>& msum);
/** get monmoial sum literal for literal lit
*
* If this function returns true, it sets msum to a monmoial sum such that
* [msum] <k> 0 is equivalent to lit[0] <k> lit[1]
* where k is the Kind of lit, one of { EQUAL, GEQ }.
*
* This function may return false if either side of lit is not a sum
* of monomials whose variables are pairwise unique on that side.
* If literal lit is in rewritten form, this function should always return
* true.
*/
static bool getMonomialSumLit(Node lit, std::map<Node, Node>& msum);
/** make node for monomial sum
*
* Make the Node corresponding to the interpretation of msum, [msum], where:
* [msum] = sum_{( v, c ) \in msum } [c]*[v]
*/
static Node mkNode(const std::map<Node, Node>& msum);
/** make coefficent term
*
* Input c is a m-constant.
* Returns the term t if c.isNull() or c*t otherwise.
*/
static inline Node mkCoeffTerm(Node c, Node t)
{
return c.isNull() ? t : NodeManager::currentNM()->mkNode(kind::MULT, c, t);
}
/** isolate variable v in constraint ([msum] <k> 0)
*
* If this function returns a value ret where ret != 0, then
* veq_c is set to m-constant, and val is set to a term such that:
* If ret=1, then ([veq_c] * v <k> val) is equivalent to [msum] <k> 0.
* If ret=-1, then (val <k> [veq_c] * v) is equivalent to [msum] <k> 0.
* If veq_c is non-null, then it is a positive constant Rational.
* The returned value of veq_c is only non-null if v has integer type.
*
* This function returns 0, indicating a failure, if msum does not contain
* a (non-zero) monomial having mvariable v.
*/
static int isolate(
Node v, const std::map<Node, Node>& msum, Node& veq_c, Node& val, Kind k);
/** isolate variable v in constraint ([msum] <k> 0)
*
* If this function returns a value ret where ret != 0, then veq
* is set to a literal that is equivalent to ([msum] <k> 0), and:
* If ret=1, then veq is of the form ( v <k> val) if veq_c.isNull(),
* or ([veq_c] * v <k> val) if !veq_c.isNull().
* If ret=-1, then veq is of the form ( val <k> v) if veq_c.isNull(),
* or (val <k> [veq_c] * v) if !veq_c.isNull().
* If doCoeff = false or v does not have Integer type, then veq_c is null.
*
* This function returns 0 indicating a failure if msum does not contain
* a (non-zero) monomial having variable v, or if veq_c must be non-null
* for an integer constraint and doCoeff is false.
*/
static int isolate(Node v,
const std::map<Node, Node>& msum,
Node& veq,
Kind k,
bool doCoeff = false);
/** solve equality lit for variable
*
* If return value ret is non-null, then:
* v = ret is equivalent to lit.
*
* This function may return false if lit does not contain v,
* or if lit is an integer equality with a coefficent on v,
* e.g. 3*v = 7.
*/
static Node solveEqualityFor(Node lit, Node v);
/** decompose real-valued term n
*
* If this function returns true, then
* ([coeff]*v + rem) is equivalent to n
* where coeff is non-zero m-constant.
*
* This function will return false if n is not a monomial sum containing
* a monomial with factor v.
*/
static bool decompose(Node n, Node v, Node& coeff, Node& rem);
/** return the rewritten form of (UMINUS t) */
static Node negate(Node t);
/** return the rewritten form of (PLUS t (CONST_RATIONAL i)) */
static Node offset(Node t, int i);
/** debug print for a monmoial sum, prints to Trace(c) */
static void debugPrintMonomialSum(std::map<Node, Node>& msum, const char* c);
};
} /* CVC4::theory namespace */
} /* CVC4 namespace */
#endif /* __CVC4__THEORY__ARITH__MSUM_H */
|
