From: Andrew Reynolds Date: Sat, 28 Oct 2017 00:21:18 +0000 (-0500) Subject: Document quant arith (#1271) X-Git-Tag: cvc5-1.0.0~5527 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1fe3247a0bf4b806f99c161dcc9c6644aabb38c1;p=cvc5.git 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. --- diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 1e30914ef..88fdec6f3 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -149,9 +149,6 @@ Node QuantArith::mkCoeffTerm( Node coeff, Node t ) { } } -// given (msum 0), solve (veq_c * v val) or (val veq_c * v), where: -// veq_c is either null (meaning 1), or positive. -// return value 1: veq_c*v is RHS, -1: veq_c*v is LHS, 0: failed. int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k ) { std::map< Node, Node >::iterator itv = msum.find( v ); if( itv!=msum.end() ){ @@ -229,6 +226,9 @@ Node QuantArith::solveEqualityFor( Node lit, Node v ) { Node val, veqc; if( QuantArith::isolate( v, msum, veqc, val, EQUAL )!=0 ){ if( veqc.isNull() ){ + // in this case, we have an integer equality with a coefficient + // on the variable we solved for that could not be eliminated, + // hence we fail. return val; } } @@ -238,6 +238,30 @@ Node QuantArith::solveEqualityFor( Node lit, Node v ) { return Node::null(); } +bool QuantArith::decompose(Node n, Node v, Node& coeff, Node& rem) +{ + std::map msum; + if (getMonomialSum(n, msum)) + { + std::map::iterator it = msum.find(v); + if (it == msum.end()) + { + return false; + } + else + { + coeff = it->second; + msum.erase(v); + rem = mkNode(msum); + return true; + } + } + else + { + return false; + } +} + Node QuantArith::negate( Node t ) { Node tt = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) ), t ); tt = Rewriter::rewrite( tt ); 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& 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& msum); + + /** get monmoial sum literal for literal lit + * + * If this function returns true, it sets msum to a monmoial sum such that + * [msum] 0 is equivalent to lit[0] 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& 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& 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] 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 val) is equivalent to [msum] 0. + * If ret=-1, then (val [veq_c] * v) is equivalent to [msum] 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& msum, Node& veq_c, Node& val, Kind k); + + /** isolate variable v in constraint ([msum] 0) + * + * If this function returns a value ret where ret != 0, then veq + * is set to a literal that is equivalent to ([msum] 0), and: + * If ret=1, then veq is of the form ( v val) if veq_c.isNull(), + * or ([veq_c] * v val) if !veq_c.isNull(). + * If ret=-1, then veq is of the form ( val v) if veq_c.isNull(), + * or (val [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& 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& msum, const char* c); };