Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/arith_msum.h	Lines:	2	2	100.0 %
Date:	2021-09-30	Branches:	11	20	55.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner
 *
 * 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.
 * ****************************************************************************
 *
 * Arithmetic utilities regarding monomial sums.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__ARITH__MSUM_H
#define CVC5__THEORY__ARITH__MSUM_H

#include <map>

#include "expr/node.h"

namespace cvc5 {
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);
};

}  // namespace theory
}  // namespace cvc5

#endif /* CVC5__THEORY__ARITH__MSUM_H */


Generated by: GCOVR (Version 3.2)

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