Refactor the theory specific parts of definition expansion into the theory solvers.

In the process of doing this I may have fixed some bugs or some potential bugs so there
may be some user visible results of this refactoring.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>

13 files changed, 366 insertions, 262 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 03092979a..d75535e15 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -116,6 +116,7 @@ libcvc4_la_SOURCES = \
 	smt/boolean_terms.h \
 	smt/boolean_terms.cpp \
 	smt/logic_exception.h \
+	smt/logic_request.h \
 	smt/simplification_mode.h \
 	smt/simplification_mode.cpp \
 	smt/options_handlers.h \
diff --git a/src/smt/logic_request.h b/src/smt/logic_request.h
new file mode 100644
index 000000000..4985b0e65
--- /dev/null
+++ b/src/smt/logic_request.h
@@ -0,0 +1,53 @@
+/*********************                                                        */
+/*! \file logic_request.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief An object to request logic widening in the running SmtEngine
+ **
+ ** An object to request logic widening in the running SmtEngine.  This
+ ** class exists as a proxy between theory code and the SmtEngine, allowing
+ ** a theory to enable another theory in the SmtEngine after initialization
+ ** (thus the usual, public setLogic() cannot be used).  This is mainly to
+ ** support features like uninterpreted divide-by-zero (to support the
+ ** partial function DIVISION), where during theory expansion, the theory
+ ** of uninterpreted functions needs to be added to the logic to support
+ ** partial functions.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__LOGIC_REQUEST_H
+#define __CVC4__LOGIC_REQUEST_H
+
+#include "expr/kind.h"
+#include "smt/smt_engine.h"
+
+namespace CVC4 {
+
+class LogicRequest {
+  /** The SmtEngine at play. */
+  SmtEngine& d_smt;
+
+public:
+  LogicRequest(SmtEngine& smt) : d_smt(smt) { }
+
+  /** Widen the logic to include the given theory. */
+  void widenLogic(theory::TheoryId id) {
+    d_smt.d_logic.getUnlockedCopy();
+    d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+    d_smt.d_logic.enableTheory(id);
+    d_smt.d_logic.lock();
+  }
+
+};/* class LogicRequest */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__LOGIC_REQUEST_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 911a16eed..328a20c28 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -43,6 +43,7 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/model_postprocessor.h"
+#include "smt/logic_request.h"
 #include "theory/theory_engine.h"
 #include "theory/bv/theory_bv_rewriter.h"
 #include "proof/proof_manager.h"
@@ -308,44 +309,6 @@ class SmtEnginePrivate : public NodeManagerListener {
    */
   hash_map<Node, Node, NodeHashFunction> d_abstractValues;
 
-  /**
-   * Function symbol used to implement uninterpreted undefined string
-   * semantics.  Needed to deal with partial charat/substr function.
-   */
-  Node d_ufSubstr;
-
-  /**
-   * Function symbol used to implement uninterpreted undefined string
-   * semantics.  Needed to deal with partial str2int function.
-   */
-  Node d_ufS2I;
-
-  /**
-   * Function symbol used to implement uninterpreted division-by-zero
-   * semantics.  Needed to deal with partial division function ("/").
-   */
-  Node d_divByZero;
-
-  /**
-   * Maps from bit-vector width to divison-by-zero uninterpreted
-   * function symbols.
-   */
-  hash_map<unsigned, Node> d_BVDivByZero;
-  hash_map<unsigned, Node> d_BVRemByZero;
-
-  /**
-   * Function symbol used to implement uninterpreted
-   * int-division-by-zero semantics.  Needed to deal with partial
-   * function "div".
-   */
-  Node d_intDivByZero;
-
-  /**
-   * Function symbol used to implement uninterpreted mod-zero
-   * semantics.  Needed to deal with partial function "mod".
-   */
-  Node d_modZero;
-
   /** Number of calls of simplify assertions active.
    */
   unsigned d_simplifyAssertionsDepth;
@@ -448,9 +411,6 @@ public:
     d_fakeContext(),
     d_abstractValueMap(&d_fakeContext),
     d_abstractValues(),
-    d_divByZero(),
-    d_intDivByZero(),
-    d_modZero(),
     d_simplifyAssertionsDepth(0),
     d_iteSkolemMap(),
     d_iteRemover(smt.d_userContext),
@@ -554,25 +514,6 @@ public:
     throw(TypeCheckingException, LogicException);
 
   /**
-   * Return the uinterpreted function symbol corresponding to division-by-zero
-   * for this particular bit-width
-   * @param k should be UREM or UDIV
-   * @param width
-   *
-   * @return
-   */
-  Node getBVDivByZero(Kind k, unsigned width);
-
-  /**
-   * Returns the node modeling the division-by-zero semantics of node n.
-   *
-   * @param n
-   *
-   * @return
-   */
-  Node expandBVDivByZero(TNode n);
-
-  /**
    * Expand definitions in n.
    */
   Node expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache)
@@ -1002,7 +943,7 @@ void SmtEngine::setDefaults() {
       options::fmfBoundInt.set( true );
       Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
     }
-	/*
+        /*
     if(! options::rewriteDivk.wasSetByUser()) {
       options::rewriteDivk.set( true );
       Trace("smt") << "turning on rewrite-divk, for strings-exp" << std::endl;
@@ -1518,55 +1459,6 @@ void SmtEngine::defineFunction(Expr func,
 }
 
 
-Node SmtEnginePrivate::getBVDivByZero(Kind k, unsigned width) {
-  NodeManager* nm = d_smt.d_nodeManager;
-  if (k == kind::BITVECTOR_UDIV) {
-    if (d_BVDivByZero.find(width) == d_BVDivByZero.end()) {
-      // lazily create the function symbols
-      ostringstream os;
-      os << "BVUDivByZero_" << width;
-      Node divByZero = nm->mkSkolem(os.str(),
-                                    nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
-                                    "partial bvudiv", NodeManager::SKOLEM_EXACT_NAME);
-      d_BVDivByZero[width] = divByZero;
-    }
-    return d_BVDivByZero[width];
-  }
-  else if (k == kind::BITVECTOR_UREM) {
-    if (d_BVRemByZero.find(width) == d_BVRemByZero.end()) {
-      ostringstream os;
-      os << "BVURemByZero_" << width;
-      Node divByZero = nm->mkSkolem(os.str(),
-                                    nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
-                                    "partial bvurem", NodeManager::SKOLEM_EXACT_NAME);
-      d_BVRemByZero[width] = divByZero;
-    }
-    return d_BVRemByZero[width];
-  }
-
-  Unreachable();
-}
-
-
-Node SmtEnginePrivate::expandBVDivByZero(TNode n) {
-  // we only deal wioth the unsigned division operators as the signed ones should have been
-  // expanded in terms of the unsigned operators
-  NodeManager* nm = d_smt.d_nodeManager;
-  unsigned width = n.getType().getBitVectorSize();
-  Node divByZero = getBVDivByZero(n.getKind(), width);
-  TNode num = n[0], den = n[1];
-  Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(BitVector(width, Integer(0))));
-  Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
-  Node divTotalNumDen = nm->mkNode(n.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL :
-                                   kind::BITVECTOR_UREM_TOTAL, num, den);
-  Node node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
-  if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) {
-    d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
-    d_smt.d_logic.enableTheory(THEORY_UF);
-    d_smt.d_logic.lock();
-  }
-  return node;
-}
 
 
 Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache)
@@ -1575,31 +1467,36 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
   stack< triple<Node, Node, bool> > worklist;
   stack<Node> result;
   worklist.push(make_triple(Node(n), Node(n), false));
+  // The worklist is made of triples, each is input / original node then the output / rewritten node
+  // and finally a flag tracking whether the children have been explored (i.e. if this is a downward
+  // or upward pass).
 
   do {
-    n = worklist.top().first;
-    Node node = worklist.top().second;
+    n = worklist.top().first;                      // n is the input / original
+    Node node = worklist.top().second;             // node is the output / result
     bool childrenPushed = worklist.top().third;
     worklist.pop();
 
+    // Working downwards
     if(!childrenPushed) {
       Kind k = n.getKind();
 
+      // Apart from apply, we can short circuit leaves
       if(k != kind::APPLY && n.getNumChildren() == 0) {
-	SmtEngine::DefinedFunctionMap::const_iterator i = d_smt.d_definedFunctions->find(n);
-	if(i != d_smt.d_definedFunctions->end()) {
-	  // replacement must be closed
-	  if((*i).second.getFormals().size() > 0) {
-	    result.push(d_smt.d_nodeManager->mkNode(kind::LAMBDA, d_smt.d_nodeManager->mkNode(kind::BOUND_VAR_LIST, (*i).second.getFormals()), (*i).second.getFormula()));
-	    continue;
-	  }
-	  // don't bother putting in the cache
-	  result.push((*i).second.getFormula());
-	  continue;
-	}
-	// don't bother putting in the cache
-	result.push(n);
-	continue;
+        SmtEngine::DefinedFunctionMap::const_iterator i = d_smt.d_definedFunctions->find(n);
+        if(i != d_smt.d_definedFunctions->end()) {
+          // replacement must be closed
+          if((*i).second.getFormals().size() > 0) {
+            result.push(d_smt.d_nodeManager->mkNode(kind::LAMBDA, d_smt.d_nodeManager->mkNode(kind::BOUND_VAR_LIST, (*i).second.getFormals()), (*i).second.getFormula()));
+            continue;
+          }
+          // don't bother putting in the cache
+          result.push((*i).second.getFormula());
+          continue;
+        }
+        // don't bother putting in the cache
+        result.push(n);
+        continue;
       }
 
       // maybe it's in the cache
@@ -1611,134 +1508,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
       }
 
       // otherwise expand it
-
-      NodeManager* nm = d_smt.d_nodeManager;
-      // FIXME: this theory-specific code should be factored out of the
-      // SmtEngine, somehow
-      switch(k) {
-      case kind::BITVECTOR_SDIV:
-      case kind::BITVECTOR_SREM:
-      case kind::BITVECTOR_SMOD:
-        node = bv::TheoryBVRewriter::eliminateBVSDiv(node);
-        break;
-
-      case kind::BITVECTOR_UDIV:
-      case kind::BITVECTOR_UREM:
-        node = expandBVDivByZero(node);
-        break;
-
-	  case kind::STRING_CHARAT: {
-		if(d_ufSubstr.isNull()) {
-			std::vector< TypeNode > argTypes;
-			argTypes.push_back(NodeManager::currentNM()->stringType());
-			argTypes.push_back(NodeManager::currentNM()->integerType());
-			argTypes.push_back(NodeManager::currentNM()->integerType());
-			d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS",
-								NodeManager::currentNM()->mkFunctionType(
-									argTypes, NodeManager::currentNM()->stringType()),
-								"uf substr",
-								NodeManager::SKOLEM_EXACT_NAME);
-		}
-		Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT,
-							NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ), n[1] );
-		Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
-		Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, n[1], zero);
-		Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 ));
-		Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
-		Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, n[0], n[1], one);
-		Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, n[0], n[1], one);
-		node = NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf );
-		break;
-	  }
-	  case kind::STRING_SUBSTR: {
-		if(d_ufSubstr.isNull()) {
-			std::vector< TypeNode > argTypes;
-			argTypes.push_back(NodeManager::currentNM()->stringType());
-			argTypes.push_back(NodeManager::currentNM()->integerType());
-			argTypes.push_back(NodeManager::currentNM()->integerType());
-			d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS",
-								NodeManager::currentNM()->mkFunctionType(
-									argTypes, NodeManager::currentNM()->stringType()),
-								"uf substr",
-								NodeManager::SKOLEM_EXACT_NAME);
-		}
-		Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ,
-							NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ),
-							NodeManager::currentNM()->mkNode( kind::PLUS, n[1], n[2] ) );
-		Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
-		Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[1], zero);
-		Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[2], zero);
-		Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
-		Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, n[0], n[1], n[2]);
-		Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, n[0], n[1], n[2]);
-		node = NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf );
-		break;
-	  }
-      case kind::DIVISION: {
-        // partial function: division
-        if(d_divByZero.isNull()) {
-          d_divByZero = nm->mkSkolem("divByZero", nm->mkFunctionType(nm->realType(), nm->realType()),
-                                     "partial real division", NodeManager::SKOLEM_EXACT_NAME);
-          if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) {
-            d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
-            d_smt.d_logic.enableTheory(THEORY_UF);
-            d_smt.d_logic.lock();
-          }
-        }
-        TNode num = n[0], den = n[1];
-        Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
-        Node divByZeroNum = nm->mkNode(kind::APPLY_UF, d_divByZero, num);
-        Node divTotalNumDen = nm->mkNode(kind::DIVISION_TOTAL, num, den);
-        node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
-        break;
-      }
-
-      case kind::INTS_DIVISION: {
-        // partial function: integer div
-        if(d_intDivByZero.isNull()) {
-          d_intDivByZero = nm->mkSkolem("intDivByZero", nm->mkFunctionType(nm->integerType(), nm->integerType()),
-                                        "partial integer division", NodeManager::SKOLEM_EXACT_NAME);
-          if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) {
-            d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
-            d_smt.d_logic.enableTheory(THEORY_UF);
-            d_smt.d_logic.lock();
-          }
-        }
-        TNode num = n[0], den = n[1];
-        Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
-        Node intDivByZeroNum = nm->mkNode(kind::APPLY_UF, d_intDivByZero, num);
-        Node intDivTotalNumDen = nm->mkNode(kind::INTS_DIVISION_TOTAL, num, den);
-        node = nm->mkNode(kind::ITE, den_eq_0, intDivByZeroNum, intDivTotalNumDen);
-        break;
-      }
-
-      case kind::INTS_MODULUS: {
-        // partial function: mod
-        if(d_modZero.isNull()) {
-          d_modZero = nm->mkSkolem("modZero", nm->mkFunctionType(nm->integerType(), nm->integerType()),
-                                   "partial modulus", NodeManager::SKOLEM_EXACT_NAME);
-          if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) {
-            d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
-            d_smt.d_logic.enableTheory(THEORY_UF);
-            d_smt.d_logic.lock();
-          }
-        }
-        TNode num = n[0], den = n[1];
-        Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
-        Node modZeroNum = nm->mkNode(kind::APPLY_UF, d_modZero, num);
-        Node modTotalNumDen = nm->mkNode(kind::INTS_MODULUS_TOTAL, num, den);
-        node = nm->mkNode(kind::ITE, den_eq_0, modZeroNum, modTotalNumDen);
-        break;
-      }
-
-      case kind::ABS: {
-        Node out = nm->mkNode(kind::ITE, nm->mkNode(kind::LT, node[0], nm->mkConst(Rational(0))), nm->mkNode(kind::UMINUS, node[0]), node[0]);
-        cache[n] = out;
-        result.push(out);
-        continue;
-      }
-
-      case kind::APPLY: {
+      if (k == kind::APPLY) {
         // application of a user-defined symbol
         TNode func = n.getOperator();
         SmtEngine::DefinedFunctionMap::const_iterator i =
@@ -1777,25 +1547,35 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
         cache[n] = (n == expanded ? Node::null() : expanded);
         result.push(expanded);
         continue;
-      }
 
-      default:
-        // unknown kind for expansion, just iterate over the children
-        node = n;
+      } else {
+        theory::Theory* t = d_smt.d_theoryEngine->theoryOf(node);
+
+        Assert(t != NULL);
+        LogicRequest req(d_smt);
+        node = t->expandDefinition(req, n);
       }
 
       // there should be children here, otherwise we short-circuited a result-push/continue, above
+      if (node.getNumChildren() == 0) {
+        Debug("expand") << "Unexpectedly no children..." << node << endl;
+      }
+      // This invariant holds at the moment but it is concievable that a new theory
+      // might introduce a kind which can have children before definition expansion but doesn't
+      // afterwards.  If this happens, remove this assertion.
       Assert(node.getNumChildren() > 0);
 
       // the partial functions can fall through, in which case we still
       // consider their children
-      worklist.push(make_triple(Node(n), node, true));
+      worklist.push(make_triple(Node(n), node, true));            // Original and rewritten result
 
       for(size_t i = 0; i < node.getNumChildren(); ++i) {
-        worklist.push(make_triple(node[i], node[i], false));
+        worklist.push(make_triple(node[i], node[i], false));      // Rewrite the children of the result only
       }
 
     } else {
+      // Working upwards
+      // Reconstruct the node from it's (now rewritten) children on the stack
 
       Debug("expand") << "cons : " << node << endl;
       //cout << "cons : " << node << endl;
@@ -1814,7 +1594,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
         nb << expanded;
       }
       node = nb;
-      cache[n] = n == node ? Node::null() : node;
+      cache[n] = n == node ? Node::null() : node;           // Only cache once all subterms are expanded
       result.push(node);
     }
   } while(!worklist.empty());
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 51fa09864..72a04ae29 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -30,7 +30,6 @@
 #include "util/proof.h"
 #include "smt/modal_exception.h"
 #include "smt/logic_exception.h"
-#include "util/hash.h"
 #include "options/options.h"
 #include "util/result.h"
 #include "util/sexpr.h"
@@ -59,6 +58,7 @@ class TheoryEngine;
 class ProofManager;
 
 class Model;
+class LogicRequest;
 class StatisticsRegistry;
 
 namespace context {
@@ -340,6 +340,7 @@ class CVC4_PUBLIC SmtEngine {
   friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(SmtEngine*);
   friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
   friend ProofManager* ::CVC4::smt::currentProofManager();
+  friend class ::CVC4::LogicRequest;
   // to access d_modelCommands
   friend class ::CVC4::Model;
   friend class ::CVC4::theory::TheoryModel;
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 85d9d1f9b..960a5a066 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -38,6 +38,10 @@ void TheoryArith::preRegisterTerm(TNode n){
   d_internal->preRegisterTerm(n);
 }
 
+Node TheoryArith::expandDefinition(LogicRequest &logicRequest, Node node) {
+  return d_internal->expandDefinition(logicRequest, node);
+}
+
 void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   d_internal->setMasterEqualityEngine(eq);
 }
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 428c101a6..eaa9a98c6 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -53,6 +53,8 @@ public:
    */
   void preRegisterTerm(TNode n);
 
+  Node expandDefinition(LogicRequest &logicRequest, Node node);
+
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
   void setQuantifiersEngine(QuantifiersEngine* qe);
 
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 37dba5e92..a63de446c 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -38,6 +38,7 @@
 #include "util/statistics_registry.h"
 #include "util/result.h"
 
+#include "smt/logic_request.h"
 #include "smt/logic_exception.h"
 
 #include "theory/arith/arithvar.h"
@@ -4620,6 +4621,69 @@ const BoundsInfo& TheoryArithPrivate::boundsInfo(ArithVar basic) const{
   return d_rowTracking[ridx];
 }
 
+Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node) {
+  NodeManager* nm = NodeManager::currentNM();
+
+  switch(node.getKind()) {
+  case kind::DIVISION: {
+    // partial function: division
+    if(d_divByZero.isNull()) {
+      d_divByZero = nm->mkSkolem("divByZero", nm->mkFunctionType(nm->realType(), nm->realType()),
+                                 "partial real division", NodeManager::SKOLEM_EXACT_NAME);
+      logicRequest.widenLogic(THEORY_UF);
+    }
+    TNode num = node[0], den = node[1];
+    Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
+    Node divByZeroNum = nm->mkNode(kind::APPLY_UF, d_divByZero, num);
+    Node divTotalNumDen = nm->mkNode(kind::DIVISION_TOTAL, num, den);
+    return nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
+    break;
+  }
+
+  case kind::INTS_DIVISION: {
+    // partial function: integer div
+    if(d_intDivByZero.isNull()) {
+      d_intDivByZero = nm->mkSkolem("intDivByZero", nm->mkFunctionType(nm->integerType(), nm->integerType()),
+                                    "partial integer division", NodeManager::SKOLEM_EXACT_NAME);
+      logicRequest.widenLogic(THEORY_UF);
+    }
+    TNode num = node[0], den = node[1];
+    Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
+    Node intDivByZeroNum = nm->mkNode(kind::APPLY_UF, d_intDivByZero, num);
+    Node intDivTotalNumDen = nm->mkNode(kind::INTS_DIVISION_TOTAL, num, den);
+    return nm->mkNode(kind::ITE, den_eq_0, intDivByZeroNum, intDivTotalNumDen);
+    break;
+  }
+
+  case kind::INTS_MODULUS: {
+    // partial function: mod
+    if(d_modZero.isNull()) {
+      d_modZero = nm->mkSkolem("modZero", nm->mkFunctionType(nm->integerType(), nm->integerType()),
+                               "partial modulus", NodeManager::SKOLEM_EXACT_NAME);
+      logicRequest.widenLogic(THEORY_UF);
+    }
+    TNode num = node[0], den = node[1];
+    Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
+    Node modZeroNum = nm->mkNode(kind::APPLY_UF, d_modZero, num);
+    Node modTotalNumDen = nm->mkNode(kind::INTS_MODULUS_TOTAL, num, den);
+    return nm->mkNode(kind::ITE, den_eq_0, modZeroNum, modTotalNumDen);
+    break;
+  }
+
+  case kind::ABS: {
+    return nm->mkNode(kind::ITE, nm->mkNode(kind::LT, node[0], nm->mkConst(Rational(0))), nm->mkNode(kind::UMINUS, node[0]), node[0]);
+    break;
+  }
+
+  default:
+    return node;
+    break;
+  }
+
+  Unreachable();
+}
+
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 33c588ed4..68e839ef8 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -397,6 +397,7 @@ public:
    * Does non-context dependent setup for a node connected to a theory.
    */
   void preRegisterTerm(TNode n);
+  Node expandDefinition(LogicRequest &logicRequest, Node node);
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
   void setQuantifiersEngine(QuantifiersEngine* qe);
@@ -772,6 +773,26 @@ private:
   Statistics d_statistics;
 
 
+  /**
+   * Function symbol used to implement uninterpreted division-by-zero
+   * semantics.  Needed to deal with partial division function ("/").
+   */
+  Node d_divByZero;
+
+  /**
+   * Function symbol used to implement uninterpreted
+   * int-division-by-zero semantics.  Needed to deal with partial
+   * function "div".
+   */
+  Node d_intDivByZero;
+
+  /**
+   * Function symbol used to implement uninterpreted mod-zero
+   * semantics.  Needed to deal with partial function "mod".
+   */
+  Node d_modZero;
+
+
 };/* class TheoryArithPrivate */
 
 }/* CVC4::theory::arith namespace */
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 6daf99c8b..5d5e0a97c 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -25,6 +25,7 @@
 #include "theory/bv/bv_subtheory_core.h"
 #include "theory/bv/bv_subtheory_inequality.h"
 #include "theory/bv/bv_subtheory_bitblast.h"
+#include "theory/bv/theory_bv_rewriter.h"
 #include "theory/theory_model.h"
 
 using namespace CVC4;
@@ -102,6 +103,69 @@ TheoryBV::Statistics::~Statistics() {
   StatisticsRegistry::unregisterStat(&d_weightComputationTimer);
 }
 
+Node TheoryBV::getBVDivByZero(Kind k, unsigned width) {
+  NodeManager* nm = NodeManager::currentNM();
+  if (k == kind::BITVECTOR_UDIV) {
+    if (d_BVDivByZero.find(width) == d_BVDivByZero.end()) {
+      // lazily create the function symbols
+      ostringstream os;
+      os << "BVUDivByZero_" << width;
+      Node divByZero = nm->mkSkolem(os.str(),
+                                    nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
+                                    "partial bvudiv", NodeManager::SKOLEM_EXACT_NAME);
+      d_BVDivByZero[width] = divByZero;
+    }
+    return d_BVDivByZero[width];
+  }
+  else if (k == kind::BITVECTOR_UREM) {
+    if (d_BVRemByZero.find(width) == d_BVRemByZero.end()) {
+      ostringstream os;
+      os << "BVURemByZero_" << width;
+      Node divByZero = nm->mkSkolem(os.str(),
+                                    nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
+                                    "partial bvurem", NodeManager::SKOLEM_EXACT_NAME);
+      d_BVRemByZero[width] = divByZero;
+    }
+    return d_BVRemByZero[width];
+  }
+
+  Unreachable();
+}
+
+
+Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) {
+  Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node << ")" << std::endl;
+
+  switch (node.getKind()) {
+  case kind::BITVECTOR_SDIV:
+  case kind::BITVECTOR_SREM:
+  case kind::BITVECTOR_SMOD:
+    return TheoryBVRewriter::eliminateBVSDiv(node);
+    break;
+
+  case kind::BITVECTOR_UDIV:
+  case kind::BITVECTOR_UREM: {
+    NodeManager* nm = NodeManager::currentNM();
+    unsigned width = node.getType().getBitVectorSize();
+    Node divByZero = getBVDivByZero(node.getKind(), width);
+    TNode num = node[0], den = node[1];
+    Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(BitVector(width, Integer(0))));
+    Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
+    Node divTotalNumDen = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL :
+				     kind::BITVECTOR_UREM_TOTAL, num, den);
+    node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
+    logicRequest.widenLogic(THEORY_UF);
+    return node;
+  }
+    break;
+
+  default:
+    return node;
+    break;
+  }
+
+  Unreachable();
+}
 
 
 void TheoryBV::preRegisterTerm(TNode node) {
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 3d093c861..a5e2ac9ea 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -25,6 +25,7 @@
 #include "context/cdhashset.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "util/statistics_registry.h"
+#include "util/hash.h"
 #include "theory/bv/bv_subtheory.h"
 
 namespace CVC4 {
@@ -46,6 +47,8 @@ class TheoryBV : public Theory {
   
   std::vector<SubtheorySolver*> d_subtheories;
   __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap; 
+
+
 public:
 
   TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
@@ -53,6 +56,8 @@ public:
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
 
+  Node expandDefinition(LogicRequest &logicRequest, Node node);
+
   void preRegisterTerm(TNode n);
 
   void check(Effort e);
@@ -85,6 +90,25 @@ private:
 
   Statistics d_statistics;
 
+
+  /**
+   * Return the uinterpreted function symbol corresponding to division-by-zero
+   * for this particular bit-width
+   * @param k should be UREM or UDIV
+   * @param width
+   *
+   * @return
+   */
+  Node getBVDivByZero(Kind k, unsigned width);
+
+  /**
+   * Maps from bit-vector width to divison-by-zero uninterpreted
+   * function symbols.
+   */
+  __gnu_cxx::hash_map<unsigned, Node> d_BVDivByZero;
+  __gnu_cxx::hash_map<unsigned, Node> d_BVRemByZero;
+
+
   context::CDO<bool> d_lemmasAdded;
   
   // Are we in conflict?
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index a4d3145d9..c44d2d334 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -463,6 +463,66 @@ void TheoryStrings::preRegisterTerm(TNode n) {
   }
 }
 
+Node TheoryStrings::expandDefinition(LogicRequest &logicRequest, Node node) {
+  switch (node.getKind()) {
+  case kind::STRING_CHARAT: {
+    if(d_ufSubstr.isNull()) {
+      std::vector< TypeNode > argTypes;
+      argTypes.push_back(NodeManager::currentNM()->stringType());
+      argTypes.push_back(NodeManager::currentNM()->integerType());
+      argTypes.push_back(NodeManager::currentNM()->integerType());
+      d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS",
+						      NodeManager::currentNM()->mkFunctionType(
+											       argTypes, NodeManager::currentNM()->stringType()),
+						      "uf substr",
+						      NodeManager::SKOLEM_EXACT_NAME);
+    }
+    Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT,
+						     NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, node[0] ), node[1] );
+    Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
+    Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, node[1], zero);
+    Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 ));
+    Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
+    Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], one);
+    Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, node[0], node[1], one);
+    return NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf );
+  }
+  break;
+
+  case kind::STRING_SUBSTR: {
+    if(d_ufSubstr.isNull()) {
+      std::vector< TypeNode > argTypes;
+      argTypes.push_back(NodeManager::currentNM()->stringType());
+      argTypes.push_back(NodeManager::currentNM()->integerType());
+      argTypes.push_back(NodeManager::currentNM()->integerType());
+      d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS",
+						      NodeManager::currentNM()->mkFunctionType(
+											       argTypes, NodeManager::currentNM()->stringType()),
+						      "uf substr",
+						      NodeManager::SKOLEM_EXACT_NAME);
+    }
+    Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ,
+						     NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, node[0] ),
+						     NodeManager::currentNM()->mkNode( kind::PLUS, node[1], node[2] ) );
+    Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
+    Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, node[1], zero);
+    Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, node[2], zero);
+    Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
+    Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], node[2]);
+    Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, node[0], node[1], node[2]);
+    return NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf );
+  }
+  break;
+
+  default :
+    return node;
+    break;
+  }
+
+  Unreachable();
+}
+
+
 void TheoryStrings::check(Effort e) {
   //Assert( d_pending.empty() );
 
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 902b902b6..e07c61a19 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -112,6 +112,18 @@ public:
 	};/* class TheoryStrings::NotifyClass */
 
 private:
+	/**
+	 * Function symbol used to implement uninterpreted undefined string
+	 * semantics.  Needed to deal with partial charat/substr function.
+	 */
+	Node d_ufSubstr;
+
+	/**
+	 * Function symbol used to implement uninterpreted undefined string
+	 * semantics.  Needed to deal with partial str2int function.
+	 */
+	Node d_ufS2I;
+
 	// Constants
     Node d_emptyString;
 	Node d_emptyRegexp;
@@ -241,6 +253,7 @@ private:
 
 public:
 	void preRegisterTerm(TNode n);
+	Node expandDefinition(LogicRequest &logicRequest, Node n);
 	void check(Effort e);
 
 	/** Conflict when merging two constants */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index e8d53e539..42cdea280 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -22,6 +22,7 @@
 #include "expr/node.h"
 //#include "expr/attribute.h"
 #include "expr/command.h"
+#include "smt/logic_request.h"
 #include "theory/valuation.h"
 #include "theory/output_channel.h"
 #include "theory/logic_info.h"
@@ -481,6 +482,22 @@ public:
   virtual void finishInit() { }
 
   /**
+   * Some theories have kinds that are effectively definitions and
+   * should be expanded before they are handled.  Definitions allow
+   * a much wider range of actions than the normal forms given by the
+   * rewriter; they can enable other theories and create new terms.
+   * However no assumptions can be made about subterms having been
+   * expanded or rewritten.  Where possible rewrite rules should be
+   * used, definitions should only be used when rewrites are not
+   * possible, for example in handling under-specified operations
+   * using partially defined functions.
+   */
+  virtual Node expandDefinition(LogicRequest &logicRequest, Node node) {
+    // by default, do nothing
+    return node;
+  }
+
+  /**
    * Pre-register a term.  Done one time for a Node, ever.
    */
   virtual void preRegisterTerm(TNode) { }