Partial merge from kind-backend branch, including Minisat and CNF work to

support incrementality.

Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.

Expected performance change negligible; slightly better on memory:
  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!

3 files changed, 69 insertions, 4 deletions

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index a309b9403..c0ef02ec4 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -93,6 +93,21 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
     return preRewritePlus(t);
   }else if(t.getKind() == kind::MULT){
     return preRewriteMult(t);
+  }else if(t.getKind() == kind::INTS_DIVISION){
+    Integer intOne(1);
+    if(t[1].getKind()== kind::CONST_INTEGER && t[1].getConst<Integer>() == intOne){
+      return RewriteResponse(REWRITE_AGAIN, t[0]);
+    }else{
+      return RewriteResponse(REWRITE_DONE, t);
+    }
+  }else if(t.getKind() == kind::INTS_MODULUS){
+    Integer intOne(1);
+    if(t[1].getKind()== kind::CONST_INTEGER && t[1].getConst<Integer>() == intOne){
+      Integer intZero(0);
+      return RewriteResponse(REWRITE_AGAIN, mkIntegerNode(intZero));
+    }else{
+      return RewriteResponse(REWRITE_DONE, t);
+    }
   }else{
     Unreachable();
   }
@@ -112,6 +127,10 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
     return postRewritePlus(t);
   }else if(t.getKind() == kind::MULT){
     return postRewriteMult(t);
+  }else if(t.getKind() == kind::INTS_DIVISION){
+    return RewriteResponse(REWRITE_DONE, t);
+  }else if(t.getKind() == kind::INTS_MODULUS){
+    return RewriteResponse(REWRITE_DONE, t);
   }else{
     Unreachable();
   }
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index bf5ea24c1..95d7d6ed1 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -17,7 +17,9 @@ operator PLUS 2: "arithmetic addition"
 operator MULT 2: "arithmetic multiplication"
 operator MINUS 2 "arithmetic binary subtraction operator"
 operator UMINUS 1 "arithmetic unary negation"
-operator DIVISION 2 "arithmetic division"
+operator DIVISION 2 "real division"
+operator INTS_DIVISION 2 "ints division"
+operator INTS_MODULUS 2 "ints modulus"
 operator POW 2 "arithmetic power"
 
 sort REAL_TYPE \
@@ -39,6 +41,19 @@ sort PSEUDOBOOLEAN_TYPE \
         "expr/node_manager.h" \
     "Pseudoboolean type"
 
+constant SUBRANGE_TYPE \
+    ::CVC4::SubrangeBounds \
+    ::CVC4::SubrangeBoundsHashStrategy \
+    "util/subrange_bound.h" \
+    "the type of an integer subrange"
+cardinality SUBRANGE_TYPE \
+    "::CVC4::theory::arith::SubrangeProperties::computeCardinality(%TYPE%)" \
+    "theory/arith/theory_arith_type_rules.h"
+well-founded SUBRANGE_TYPE \
+    true \
+    "::CVC4::theory::arith::SubrangeProperties::mkGroundTerm(%TYPE%)" \
+    "theory/arith/theory_arith_type_rules.h"
+
 constant CONST_RATIONAL \
     ::CVC4::Rational \
     ::CVC4::RationalHashStrategy \
@@ -75,4 +90,7 @@ typerule LEQ ::CVC4::theory::arith::ArithPredicateTypeRule
 typerule GT ::CVC4::theory::arith::ArithPredicateTypeRule
 typerule GEQ ::CVC4::theory::arith::ArithPredicateTypeRule
 
+typerule INTS_DIVISION ::CVC4::theory::arith::ArithOperatorTypeRule
+typerule INTS_MODULUS ::CVC4::theory::arith::ArithOperatorTypeRule
+
 endtheory
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 511982d48..8d0d79f0a 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -21,6 +21,8 @@
 #ifndef __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
 #define __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
 
+#include "util/subrange_bound.h"
+
 namespace CVC4 {
 namespace theory {
 namespace arith {
@@ -33,7 +35,7 @@ public:
     if (n.getKind() == kind::CONST_RATIONAL) return nodeManager->realType();
     return nodeManager->integerType();
   }
-};
+};/* class ArithConstantTypeRule */
 
 class ArithOperatorTypeRule {
 public:
@@ -60,7 +62,7 @@ public:
     }
     return (isInteger ? integerType : realType);
   }
-};
+};/* class ArithOperatorTypeRule */
 
 class ArithPredicateTypeRule {
 public:
@@ -80,7 +82,33 @@ public:
     }
     return nodeManager->booleanType();
   }
-};
+};/* class ArithPredicateTypeRule */
+
+class SubrangeProperties {
+public:
+  inline static Cardinality computeCardinality(TypeNode type) {
+    Assert(type.getKind() == kind::SUBRANGE_TYPE);
+
+    const SubrangeBounds& bounds = type.getConst<SubrangeBounds>();
+    if(!bounds.lower.hasBound() || !bounds.upper.hasBound()) {
+      return Cardinality::INTEGERS;
+    }
+    return Cardinality(bounds.upper.getBound() - bounds.lower.getBound());
+  }
+
+  inline static Node mkGroundTerm(TypeNode type) {
+    Assert(type.getKind() == kind::SUBRANGE_TYPE);
+
+    const SubrangeBounds& bounds = type.getConst<SubrangeBounds>();
+    if(bounds.lower.hasBound()) {
+      return NodeManager::currentNM()->mkConst(bounds.lower.getBound());
+    }
+    if(bounds.upper.hasBound()) {
+      return NodeManager::currentNM()->mkConst(bounds.upper.getBound());
+    }
+    return NodeManager::currentNM()->mkConst(Integer(0));
+  }
+};/* class SubrangeProperties */
 
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */