diff options
Diffstat (limited to 'src/theory/arith/arith_msum.h')
| -rw-r--r-- | src/theory/arith/arith_msum.h | 188 |
1 files changed, 188 insertions, 0 deletions
diff --git a/src/theory/arith/arith_msum.h b/src/theory/arith/arith_msum.h new file mode 100644 index 000000000..652a395cc --- /dev/null +++ b/src/theory/arith/arith_msum.h @@ -0,0 +1,188 @@ +/********************* */ +/*! \file arith_msum.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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 */ |