GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/arith_msum.h Lines: 2 2 100.0 %
Date: 2021-03-23 Branches: 11 20 55.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file arith_msum.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner
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 arith_msum
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__ARITH__MSUM_H
18
#define CVC4__THEORY__ARITH__MSUM_H
19
20
#include <map>
21
22
#include "expr/node.h"
23
24
namespace CVC4 {
25
namespace theory {
26
27
/** Arithmetic utilities regarding monomial sums.
28
 *
29
 * Note the following terminology:
30
 *
31
 *   We say Node c is a {monomial constant} (or m-constant) if either:
32
 *   (a) c is a constant Rational, or
33
 *   (b) c is null.
34
 *
35
 *   We say Node v is a {monomial variable} (or m-variable) if either:
36
 *   (a) v.getType().isReal() and v is not a constant, or
37
 *   (b) v is null.
38
 *
39
 *   For m-constant or m-variable t, we write [t] to denote 1 if t.isNull() and
40
 *   t otherwise.
41
 *
42
 *   A monomial m is a pair ( mvariable, mconstant ) of the form ( v, c ), which
43
 *   is interpreted as [c]*[v].
44
 *
45
 *   A {monmoial sum} msum is represented by a std::map< Node, Node > having
46
 *   key-value pairs of the form ( mvariable, mconstant ).
47
 *   It is interpreted as:
48
 *   [msum] = sum_{( v, c ) \in msum } [c]*[v]
49
 *   It is critical that this map is ordered so that operations like adding
50
 *   two monomial sums can be done efficiently. The ordering itself is not
51
 *   important, and currently corresponds to the default ordering on Nodes.
52
 *
53
 * The following has utilities involving monmoial sums.
54
 *
55
 */
56
class ArithMSum
57
{
58
 public:
59
  /** get monomial
60
   *
61
   * If n = n[0]*n[1] where n[0] is constant and n[1] is not,
62
   * this function returns true, sets c to n[0] and v to n[1].
63
   */
64
  static bool getMonomial(Node n, Node& c, Node& v);
65
66
  /** get monomial
67
   *
68
   * If this function returns true, it adds the ( m-constant, m-variable )
69
   * pair corresponding to the monomial representation of n to the
70
   * monomial sum msum.
71
   *
72
   * This function returns false if the m-variable of n is already
73
   * present in n.
74
   */
75
  static bool getMonomial(Node n, std::map<Node, Node>& msum);
76
77
  /** get monomial sum for real-valued term n
78
   *
79
   * If this function returns true, it sets msum to a monmoial sum such that
80
   *   [msum] is equivalent to n
81
   *
82
   * This function may return false if n is not a sum of monomials
83
   * whose variables are pairwise unique.
84
   * If term n is in rewritten form, this function should always return true.
85
   */
86
  static bool getMonomialSum(Node n, std::map<Node, Node>& msum);
87
88
  /** get monmoial sum literal for literal lit
89
   *
90
   * If this function returns true, it sets msum to a monmoial sum such that
91
   *   [msum] <k> 0  is equivalent to lit[0] <k> lit[1]
92
   * where k is the Kind of lit, one of { EQUAL, GEQ }.
93
   *
94
   * This function may return false if either side of lit is not a sum
95
   * of monomials whose variables are pairwise unique on that side.
96
   * If literal lit is in rewritten form, this function should always return
97
   * true.
98
   */
99
  static bool getMonomialSumLit(Node lit, std::map<Node, Node>& msum);
100
101
  /** make node for monomial sum
102
   *
103
   * Make the Node corresponding to the interpretation of msum, [msum], where:
104
   *   [msum] = sum_{( v, c ) \in msum } [c]*[v]
105
   */
106
  static Node mkNode(const std::map<Node, Node>& msum);
107
108
  /** make coefficent term
109
   *
110
   * Input c is a m-constant.
111
   * Returns the term t if c.isNull() or c*t otherwise.
112
   */
113
379817
  static inline Node mkCoeffTerm(Node c, Node t)
114
  {
115
379817
    return c.isNull() ? t : NodeManager::currentNM()->mkNode(kind::MULT, c, t);
116
  }
117
118
  /** isolate variable v in constraint ([msum] <k> 0)
119
   *
120
   * If this function returns a value ret where ret != 0, then
121
   * veq_c is set to m-constant, and val is set to a term such that:
122
   *    If ret=1, then ([veq_c] * v <k> val) is equivalent to [msum] <k> 0.
123
   *   If ret=-1, then (val <k> [veq_c] * v) is equivalent to [msum] <k> 0.
124
   *   If veq_c is non-null, then it is a positive constant Rational.
125
   * The returned value of veq_c is only non-null if v has integer type.
126
   *
127
   * This function returns 0, indicating a failure, if msum does not contain
128
   * a (non-zero) monomial having mvariable v.
129
   */
130
  static int isolate(
131
      Node v, const std::map<Node, Node>& msum, Node& veq_c, Node& val, Kind k);
132
133
  /** isolate variable v in constraint ([msum] <k> 0)
134
   *
135
   * If this function returns a value ret where ret != 0, then veq
136
   * is set to a literal that is equivalent to ([msum] <k> 0), and:
137
   *    If ret=1, then veq is of the form ( v <k> val) if veq_c.isNull(),
138
   *                   or ([veq_c] * v <k> val) if !veq_c.isNull().
139
   *   If ret=-1, then veq is of the form ( val <k> v) if veq_c.isNull(),
140
   *                   or (val <k> [veq_c] * v) if !veq_c.isNull().
141
   * If doCoeff = false or v does not have Integer type, then veq_c is null.
142
   *
143
   * This function returns 0 indicating a failure if msum does not contain
144
   * a (non-zero) monomial having variable v, or if veq_c must be non-null
145
   * for an integer constraint and doCoeff is false.
146
   */
147
  static int isolate(Node v,
148
                     const std::map<Node, Node>& msum,
149
                     Node& veq,
150
                     Kind k,
151
                     bool doCoeff = false);
152
153
  /** solve equality lit for variable
154
   *
155
   * If return value ret is non-null, then:
156
   *    v = ret is equivalent to lit.
157
   *
158
   * This function may return false if lit does not contain v,
159
   * or if lit is an integer equality with a coefficent on v,
160
   * e.g. 3*v = 7.
161
   */
162
  static Node solveEqualityFor(Node lit, Node v);
163
164
  /** decompose real-valued term n
165
  *
166
  * If this function returns true, then
167
  *   ([coeff]*v + rem) is equivalent to n
168
  * where coeff is non-zero m-constant.
169
  *
170
  * This function will return false if n is not a monomial sum containing
171
  * a monomial with factor v.
172
  */
173
  static bool decompose(Node n, Node v, Node& coeff, Node& rem);
174
175
  /** return the rewritten form of (UMINUS t) */
176
  static Node negate(Node t);
177
178
  /** return the rewritten form of (PLUS t (CONST_RATIONAL i)) */
179
  static Node offset(Node t, int i);
180
181
  /** debug print for a monmoial sum, prints to Trace(c) */
182
  static void debugPrintMonomialSum(std::map<Node, Node>& msum, const char* c);
183
};
184
185
} /* CVC4::theory namespace */
186
} /* CVC4 namespace */
187
188
#endif /* CVC4__THEORY__ARITH__MSUM_H */