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  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& 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& 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] 0 is equivalent to lit[0] 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& 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& 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] 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 val) is equivalent to [msum] 0. 123  * If ret=-1, then (val [veq_c] * v) is equivalent to [msum] 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& msum, Node& veq_c, Node& val, Kind k); 132 133  /** isolate variable v in constraint ([msum] 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] 0), and: 137  * If ret=1, then veq is of the form ( v val) if veq_c.isNull(), 138  * or ([veq_c] * v val) if !veq_c.isNull(). 139  * If ret=-1, then veq is of the form ( val v) if veq_c.isNull(), 140  * or (val [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& 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& msum, const char* c); 183 }; 184 185 } /* CVC4::theory namespace */ 186 } /* CVC4 namespace */ 187 188 #endif /* CVC4__THEORY__ARITH__MSUM_H */

 Generated by: GCOVR (Version 3.2)