diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-27 19:21:18 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-27 19:21:18 -0500 |
commit | 1fe3247a0bf4b806f99c161dcc9c6644aabb38c1 (patch) | |
tree | 0922af2e81c62268ea4747e085dc2b57441f5edf /src/theory/quantifiers/quant_util.h | |
parent | 36bf9f8bcb2a1a3aea1f90eb4d13aed3bbf6da8f (diff) |
Document quant arith (#1271)
* Initial documentation, incomplete.
* Document arith utilities in quantifiers.
* Minor
* Clang format
* Minor
* Clang format.
* Minor
* Apply new clang format.
* Document ordering.
Diffstat (limited to 'src/theory/quantifiers/quant_util.h')
-rw-r--r-- | src/theory/quantifiers/quant_util.h | 164 |
1 files changed, 150 insertions, 14 deletions
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 27e517649..07df8bb21 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -83,23 +83,159 @@ public: virtual std::string identify() const = 0; }; - +/** 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 QuantArith { public: - static bool getMonomial( Node n, Node& c, Node& v ); - static bool getMonomial( Node n, std::map< Node, Node >& msum ); - static bool getMonomialSum( Node n, std::map< Node, Node >& msum ); - static bool getMonomialSumLit( Node lit, std::map< Node, Node >& msum ); - static Node mkNode( std::map< Node, Node >& msum ); - static Node mkCoeffTerm( Node coeff, Node t ); - //return 1 : solved on LHS, return -1 : solved on RHS, return 0: failed - static int isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k ); - static int isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k, bool doCoeff = false ); - static Node solveEqualityFor( Node lit, Node v ); - static Node negate( Node t ); - static Node offset( Node t, int i ); - static void debugPrintMonomialSum( std::map< Node, Node >& msum, const char * c ); + /** 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(std::map<Node, Node>& msum); + + /** make coefficent term + * + * Input coeff is a m-constant. + * Returns the term t if coeff.isNull() or coeff*t otherwise. + */ + static Node mkCoeffTerm(Node coeff, Node 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, 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 indiciating 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, + 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); }; |