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.

2 files changed, 177 insertions, 17 deletions

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 <k> 0), solve (veq_c * v <k> val) or (val <k> 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<Node, Node> msum;
+  if (getMonomialSum(n, msum))
+  {
+    std::map<Node, Node>::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<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);
 };