Merging the arithmetic theory draft (lra-init) back into the main trunk. This should not affect other parts of the system. This code is untested, and is volatile. It is going to be improved in the future so don't pick on it too much. I am merging this code in its current state back into the main trunk because it was getting unruly to keep merging the updated trunk back into the branch.

1 files changed, 455 insertions, 0 deletions

diff --git a/src/theory/arith/normal_form_notes.txt b/src/theory/arith/normal_form_notes.txt
new file mode 100644
index 000000000..30786e980
--- /dev/null
+++ b/src/theory/arith/normal_form_notes.txt
@@ -0,0 +1,455 @@
+
+/** DRAFT 1
+ * Normal form for predicates:
+ *    TRUE
+ *    FALSE
+ *    var_i |><| b
+ *    \sum_i product_i  |><| b
+ *  where
+ *   1) b is of type CONST_RATIONAL
+ *   2) |><| is of type <=, >, =, < or >=
+ *   3) product_i is in product normal form,
+ *   4) product_i is not 0,
+ *   5) product_i's are in strictly ascending productOrder,
+ *   6) product_i has at least 2 members,
+ *   7) product_1 has a positive coefficient, and
+ *   8) var_i has metakind variable.
+ *
+ * Normal form for terms:
+ *    c
+ *    c + \sum_i product_i
+ *  where
+ *   1) c is of type CONST_RATIONAL,
+ *   2) product_i is in product normal form,
+ *   3) product_i is not a constant,
+ *   4) and product_i's are in strictly ascending productOrder.
+ *
+ * Normal form for products:
+ *    d
+ *    var_i
+ *    e * \prod var_i
+ *  where
+ *   1) d,e is of type CONST_RATIONAL,
+ *   2) e != 0,
+ *   3) e != 1 or there are at least 2 variables,
+ *   2) var_i is of metakind VARIABLE,
+ *   3) and var_i are in increasing (not strict) nodeOrder.
+ *
+ * productOrder is well defined over normal form products as follows:
+ *   cmp(d,d') = rational order.
+ *   cmp(d,var_i)= -1
+ *   cmp(var_i,var_j) is the node order
+ *   cmp(var_i,d * \prod var_i) = -1
+ *   cmp(p = d * \prod var_i, p' = d' * \prod var_i')=
+ *      if(len(p) == len(p'))
+ *      then tupleCompare(var_i, var_i')
+ *      else len(p) - len(p')
+ */
+
+
+
+/** DRAFT 2
+ * Normal form for predicates:
+ *    TRUE
+ *    FALSE
+ *    var |><| b
+ *    (\sum_{i=1 to N} p_i)  |><| b
+ *  where
+ *   1) b is of type CONST_RATIONAL
+ *   2) |><| is of kind <, <=, =, >= or >
+ *   3) p_i is in PNF,
+ *   5) p_i's are in strictly ascending <p,
+ *   6) N >= 2,
+ *   7) the kind of (\sum_{i=1 to N} p_i) is an N arity PLUS,
+ *   8) p_1 has coefficient 1, and
+ *   9) var has metakind variable.
+ *
+ * PNF:
+ *    v
+ *    d * v
+ *    (\prod_{i=1 to M} v_i)
+ *    d * (\prod_{i=1 to M} v_i)
+ *  where
+ *   1) d is of type CONST_RATIONAL,
+ *   2) d != 0,
+ *   3) d != 1,
+ *   4) M>=2,
+ *   5) v, v_i are of metakind VARIABLE,
+ *   6) v_i are in increasing (not strict) nodeOrder, and
+ *   7) the kind of (\prod_{i=1 to M} v_i) is an M arity MULT.
+ *
+ * <p is defined over PNF as follows (skipping some symmetry):
+ *   cmp(  v,   v') is the node order over v and v'
+ *   cmp(  v,d'*v') is the node order over v and v'
+ *   cmp(d*v,d'*v') is the node order over v and v'
+ *   cmp(  v,   (\prod v'_i)) = -1
+ *   cmp(d*v,   (\prod  v_i)) = -1
+ *   cmp(  v, d*(\prod v'_i)) = -1
+ *   cmp(d*v, d*(\prod  v_i)) = -1
+ *   cmp((\prod_{i=1 to M} v_i),(\prod_{i=1 to M'} v'_i))=
+ *      if(M == M')
+ *      then tupleCompare(v_i, v'_i)
+ *      else M - M'
+ *   cmp((\prod_{i=1 to M} v_i), d*(\prod_{i=1 to M'} v'_i))=
+ *      if(M == M')
+ *      then tupleCompare(v_i, v'_i)
+ *      else M - M'
+ *   cmp(d * (\prod_{i=1 to M} v_i), d' * (\prod_{i=1 to M'} v'_i))=
+ *      if(M == M')
+ *      then tupleCompare(v_i, v'_i)
+ *      else M - M'
+ *
+ * Rewrite Normal Form for Terms:
+ *    b
+ *    p
+ *    c + p
+ *    (\sum_{i=1 to N} p_i)
+ *    c + (\sum_{i=1 to N} p_i)
+ *  where
+ *   1) b,c is of type CONST_RATIONAL,
+ *   2) c != 0,
+ *   3) p, p_i is in PNF,
+ *   4) N >= 2
+ *   5) the kind of (\sum_{i=1 to N} p_i) is an N arity PLUS,
+ *   6) and p_i's are in strictly <p.
+ *
+ */
+
+
+bool isVarMultList(TNode v){
+  for(v = 1 to l.getLength()){
+    if(!isVar(v[i])){
+      return false;
+    }
+  }
+
+  for(v = 2 to l.getLength()){
+    if(!(v[i-1] <= v[i])){
+      return false;
+    }
+  }
+  return true;
+}
+
+bool isPNF(TNode p){
+   if(p.getKind() == MULT){
+     if(p[0].getKind() == CONST_RATIONAL){
+       if(p[0].getConst<CONST_RATIONAL>() != 0 &&
+          p[0].getConst<CONST_RATIONAL> != 1){
+         if(p[1].getKind() != MULT){
+           if(p[1].getMetaKind() == VARIABLE){
+             return true; // d * v
+           }else{
+             return false;
+           }
+         }else{
+           if(isVarMultList(p[1])){
+             return true; // d * (\prod_{i=1 to M} v_i)
+           }else{
+             return false;
+           }
+         }
+       }else{
+         return false;
+       }
+     }else{
+       if(isVarMultList(p)){
+         return true; //(\prod_{i=1 to M} v_i)
+       }else{
+         return false;
+       }
+     }
+   }else{
+     if(p.getMetaKind() == VARIABLE){
+       return true; // v
+     }else{
+       return false;
+     }
+   }
+}
+
+
+bool <p(TNode p0, TNode p1){
+  PNFType t0 = same as the comments in isPNF(p0);
+  PNFType t1 = same as the comments in isPNF(p1);
+
+  bool t0IsVar = (t0 == "v") ||(t0 == "d*v");
+  bool t1IsVar = (t1 == "v") ||(t1 == "d*v");
+
+  if(t0IsVar && t1IsVar){
+    TNode v0 = (t0 == "d*v") ? p0[1] : p0;
+    TNode v1 = (t1 == "d*v") ? p1[1] : p1;
+    return v0 < v1;
+  }else if(!t0IsVar && t1IsVar){
+    return false;
+  }else if(t0IsVar && !t1IsVar){
+    return true;
+  }else{
+    TNode prod0 = (t0 == "d * (\prod_{i=1 to M} v_i)") ? p0[1] : p0;
+    TNode prod1 = (t1 == "d * (\prod_{i=1 to M} v_i)") ? p1[1] : p1;
+
+    int M0 = prod0.getNumChildren();
+    int M1 = prod1.getNumChildren();
+
+    if(M0 == M1){
+      for(i in 1 to M0){
+        if(prod0[i] < prod[i]){
+          return true;
+        }
+      }
+      return false;
+    }else{
+      return M0 < M1;
+    }
+  }
+}
+
+bool isPNFSum(TNode p){
+
+  for(i = 1 to p.getNumChildren()){
+    if(!isPNF(p[i])){
+      return false;
+    }
+  }
+  for(i = 2 to p.getNumChildren()){
+    if(!(p[i-1] <p p[i])){
+      return false;
+    }
+  }
+  return true;
+}
+
+string isNormalFormTerm(TNode t){
+  Kind k = t.getKind();
+  if(k != PLUS){
+    if(k == CONST_RATIONAL){
+      return true; // b
+    }else if(isPNF(p)){
+      return true; // p
+    }else{
+      return false;
+    }
+  }else{
+    if(t[0].getKind() == CONST_RATIONAL){
+      if(t[0].getConst<CONST_RATIONAL>() != 0){
+        if(t[1].getKind() == PLUS){
+          if(isPNFSum(t[1])){
+            return true; // c + (\sum_{i=1 to N} p_i)
+          }else{
+            return false;
+          }
+        }else{
+          if(isPNF(t[1])){
+            return true; // c + p
+          }else{
+            return false;
+          }
+        }
+      }else{
+        return false;
+      }
+    }else{
+      if(isPNFSum(t)){
+        return true; // (\sum_{i=1 to N} p_i)
+      }else{
+        return false;
+      }
+    }
+  }
+}
+
+/***********************************************/
+/***********************************************/
+/******************* DRAFT 3 *******************/
+/***********************************************/
+/***********************************************/
+
+/** DRAFT 3
+ * Normal form for predicates:
+ *    TRUE
+ *    FALSE
+ *    v |><| b
+ *    p |><| b
+ *    (+ p_1 .. p_N)  |><| b
+ *  where
+ *   1) b is of type CONST_RATIONAL
+ *   2) |><| is of kind <, <=, =, >= or >
+ *   3) p, p_i is in PNF,
+ *   5) p_i's are in strictly ascending <p,
+ *   6) N >= 2,
+ *   7) the kind of (+ p_1 .. p_N) is an N arity PLUS,
+ *   8) p.d, p_1.d are 1, and
+ *   9) v has metakind variable.
+ *
+ * PNF(t):
+ *    (* d v_1 v_2 ... v_M)
+ *  where
+ *   1) d is of type CONST_RATIONAL,
+ *   2) d != 0,
+ *   4) M>=1,
+ *   5) v_i are of metakind VARIABLE,
+ *   6) v_i are in increasing (not strict) nodeOrder, and
+ *   7) the kind of t is an M+1 arity MULT.
+ *
+ * <p is defined over PNF as follows (skipping some symmetry):
+ *   cmp( (* d v_1 v_2 ... v_M), (* d' v'_1 v'_2 ... v'_M'):
+ *      if(M == M'):
+ *      then tupleCompare(v_i, v'_i)
+ *      else M -M'
+ *
+ * Rewrite Normal Form for Terms:
+ *    b
+ *    v
+ *    (+ c p_1 p_2 ... p_N)  |  not(N=1 and c=0 and p_1.d=1)
+ *  where
+ *   1) b,c is of type CONST_RATIONAL,
+ *   2) c != 0,
+ *   3) p_i is in PNF,
+ *   4) N >= 1
+ *   5) the kind of (+ c p_1 p_2 ... p_N) is an N+1 arity PLUS,
+ *   6) and p_i's are in strictly <p.
+ *
+ */
+
+
+/* Assuming that the terms have been normalized, how much work is the case splitting.
+ * The following should provide a good insight into how difficult it is to use
+ * these normal forms when writing code.
+ */
+
+enum PredicateNFKind{TRUE, FALSE, v |><| b, p |><| b, (+ p_1 .. p_N)  |><| b};
+
+PredicateNFKind kindOfNormalFormPredicate(TNode n){
+  if(n.getKind() == CONST_BOOLEAN){
+    if(n.getConst<bool>()){
+      return TRUE;
+    }else{
+      return FALSE;
+    }
+  }else{
+    TNode left = n[0];
+    if(left.getMetaKind() == metakind::VARIABLE){
+      return v |><| b;
+    }else if(left.getKind() == MULT){
+      return p |><| b;
+    }else{
+      return (+ p_1 .. p_N)  |><| b;
+    }
+  }
+}
+
+enum TermNFKind{c, v, (+ c p_1 p_2 ... p_N)};
+
+TermNFKind kindOfTermNFKind(TNode n){
+  if(n.getMetaKind() == metakind::CONSTANT){
+     return c;
+  }else if(n.getMetaKind() == metakind::VARIABLE){
+     return v;
+  }else{
+     return (+ c p_1 p_2 ... p_N) 
+  }
+}
+
+
+/* Verify that the term meets all of the criteria for a normal form.
+ * This should provide good insight into how difficult it is to write/debug
+ * the rewriters themselves, and other parts of the code that are
+ * "highly knowledgable" about the normal form (such as helper functions).
+ */
+
+
+bool rangeIsSorted(bool strict, TNode::iterator start, TNode::iterator stop, NodeComparitor cmp){
+  if(start == stop) return true;
+  TNode prev = *start;
+  ++start;
+  while(start != stop){
+    TNode curr = *start;
+    int tmp = cmp(prev, curr);
+    if(strict && tmp >= 0
+      !strict && tmp > 0
+    ){
+      return false;
+    }
+    prev = curr;
+    ++start;
+  }
+  return true;
+}
+
+bool rangeAll(TNode::iterator start, TNode::iterator stop, NodePredicate rho){
+  for(;start != stop; ++start){
+    if(! rho(*start))  return false;
+  }
+  return true;
+}
+bool isPNF(TNode p){
+   return
+      p.getKind() == MULT &&
+      p[0].getKind() == CONST_RATIONAL&&
+      p[0].getConst<CONST_RATIONAL>() != 0 &&
+      rangeIsSorted(false, p.begin()+1, p.end(), nodeOrder) &&
+      rangeAll(p.begin()+1, p.end(), \t -> t.getMetaKind() == metakind::VARIABLE);
+}
+
+
+bool cmpPNF(TNode p0, TNode p1){
+  int M0 = p0.getNumChildren();
+  int M1 = p1.getNumChildren();
+
+  if(M0 == M1){
+    for(int i=1; i< M0; ++i){
+      int cmp = nodeOrder(p0[i],p1[i]);
+      if(cmp != 0){
+        return cmp;
+      }
+    }
+    return 0;
+  }else{
+    return M0 - M1;
+  }
+}
+
+bool isNormalFormTerm(TNode t){
+  if(t.getKind() == CONST_RATIONAL){
+    return true;
+  }else if(t.getMetaKind() == VARIABLE){
+    return true;
+  }else if(t.getKind() == PLUS){ //may be (+ c p_1 p_2 ... p_N)
+    int N = t.getNumChildren()-1;
+    TNode c = t[0];
+    return c.getKind() == CONST_RATIONAL &&
+           c.getConst<Rational>() !- 0 &&
+           N >= 1 &&  //This check is redundent because of an invariant in NodeBuilder<>
+           rangeAll(p.begin()+1, p.end(), isPNF) &&
+           rangeIsSorted(true, p.begin()+1, p.end(), cmpPNF);
+  }else{
+    return false;
+  }
+}
+
+bool isNormalFormAtom(TNode n){
+  if(n.getKind() == CONST_BOOLEAN){
+    return true;
+  }else if(n.getKind() \in {<, <=, ==, >=, >}){
+    TNode left = n[0];
+    TNode right = n[1];
+    if(right.getKind() == CONST_RATIONAL){
+      if(left.getMetaKind() == VARIABLE){
+        return true;
+      }else if(left.getKind() == MULT){
+        return isPNF(left) && left[0] == 1;
+      }else if(left.getKind() == PLUS){
+        return left.getNumChildren() >= 2 &&
+               rangeAll(left.begin(), left.end(), isPNF) &&
+               left[0][0] == 1 &&
+               rangeIsSorted(true, left.begin(), left.end(), cmpPNF);
+      }else{
+        return false;
+      }
+    }else{
+      return false;
+    }
+  }else{
+    return false;
+  }
+}