* Models' SubstitutionMaps are now attached to the user context

  (rather than SAT context)
* Enable part of CVC3 system test (resolves bug 375)
* Fix infinite recursion in beta reduction code (resolves bug 417)
* Some model-building assertions have been added
* Other minor changes

(this commit was certified error- and warning-free by the test-and-commit script.)

5 files changed, 76 insertions, 2 deletions

diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 549e9f19b..a724124bd 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -61,6 +61,9 @@ enumerator REAL_TYPE \
 enumerator INTEGER_TYPE \
     "::CVC4::theory::arith::IntegerEnumerator" \
     "theory/arith/type_enumerator.h"
+enumerator SUBRANGE_TYPE \
+    "::CVC4::theory::arith::SubrangeEnumerator" \
+    "theory/arith/type_enumerator.h"
 
 operator LT 2 "less than, x < y"
 operator LEQ 2 "less than or equal, x <= y"
diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h
index 4dd139be7..8b30a4ddf 100644
--- a/src/theory/arith/type_enumerator.h
+++ b/src/theory/arith/type_enumerator.h
@@ -110,6 +110,60 @@ public:
 
 };/* class IntegerEnumerator */
 
+class SubrangeEnumerator : public TypeEnumeratorBase<SubrangeEnumerator> {
+  Integer d_int;
+  SubrangeBounds d_bounds;
+  bool d_direction;// true == +, false == -
+
+public:
+
+  SubrangeEnumerator(TypeNode type) throw(AssertionException) :
+    TypeEnumeratorBase<SubrangeEnumerator>(type),
+    d_int(0),
+    d_bounds(type.getConst<SubrangeBounds>()),
+    d_direction(d_bounds.lower.hasBound()) {
+
+    d_int = d_direction ? d_bounds.lower.getBound() : d_bounds.upper.getBound();
+
+    Assert(type.getKind() == kind::SUBRANGE_TYPE);
+
+    // if we're counting down, there's no lower bound
+    Assert(d_direction || !d_bounds.lower.hasBound());
+  }
+
+  Node operator*() throw() {
+    if(isFinished()) {
+      throw NoMoreValuesException(getType());
+    }
+    return NodeManager::currentNM()->mkConst(Rational(d_int));
+  }
+
+  SubrangeEnumerator& operator++() throw() {
+    if(d_direction) {
+      if(!d_bounds.upper.hasBound() || d_int <= d_bounds.upper.getBound()) {
+        d_int += 1;
+      }
+    } else {
+      // if we're counting down, there's no lower bound
+      d_int -= 1;
+    }
+    // sequence is 0, 1, -1, 2, -2, 3, -3, ...
+    if(d_int <= 0) {
+      d_int = -d_int + 1;
+    } else {
+      d_int = -d_int;
+    }
+    return *this;
+  }
+
+  bool isFinished() throw() {
+    // if we're counting down, there's no lower bound
+    return d_direction &&
+      (!d_bounds.upper.hasBound() || d_int <= d_bounds.upper.getBound());
+  }
+
+};/* class SubrangeEnumerator */
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index d97781ab7..82d602017 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -514,6 +514,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
     Node n;
     for (i = noRepSet.begin(); i != noRepSet.end(); ++i) {
       n = typeConstSet.nextTypeEnum(t);
+      Assert(!n.isNull(), "out of values for finite type enumeration while building model");
       constantReps[*i] = n;
       Trace("model-builder") << "  New Const: Setting constant rep of " << (*i) << " to " << n << endl;
     }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 252109a26..08073c147 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -91,7 +91,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_quantEngine = new QuantifiersEngine(context, this);
 
   // build model information if applicable
-  d_curr_model = new theory::TheoryModel( context, "DefaultModel", true );
+  d_curr_model = new theory::TheoryModel( userContext, "DefaultModel", true );
   d_curr_model_builder = new theory::TheoryEngineModelBuilder( this );
 
   StatisticsRegistry::registerStat(&d_combineTheoriesTime);
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index f70d89b30..50211f1ad 100644
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -77,7 +77,23 @@ public:
       for(TNode::iterator formal = lambda[0].begin(), arg = node.begin(); formal != lambda[0].end(); ++formal, ++arg) {
         // typechecking should ensure that the APPLY_UF is well-typed, correct arity, etc.
         Assert(formal != node.end());
-        substitutions.addSubstitution(*formal, *arg);
+        // This rewrite step is important: if we have (f (f 5)) for
+        // some lambda term f, we want to beta-reduce the inside (f 5)
+        // application first.  Otherwise, we can end up in infinite
+        // recursion, because f's formal (say "x") gives the
+        // substitution "x |-> (f 5)".  Fine, the body of the lambda
+        // gets (f 5) in place for x.  But since the same lambda ("f")
+        // now occurs in the body, it's got the same bound var "x", so
+        // substitution continues and we replace that x by (f 5).  And
+        // then again.  :-(
+        //
+        // We need a better solution for distinguishing bound
+        // variables like this, but for now, handle it by going
+        // inside-out.  (Quantifiers shouldn't ever have this problem,
+        // so long as the bound vars in different quantifiers are kept
+        // different.)
+        Node n = Rewriter::rewrite(*arg);
+        substitutions.addSubstitution(*formal, n);
       }
       return RewriteResponse(REWRITE_DONE, substitutions.apply(lambda[1]));
     }