SMT-LIBv2 (define-fun...) command now functional; does eager expansion at preprocessing time

10 files changed, 215 insertions, 52 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index a1486fcab..8c90f337e 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -23,6 +23,7 @@
 
 #include "expr/command.h"
 #include "smt/smt_engine.h"
+#include "smt/bad_option_exception.h"
 #include "util/output.h"
 
 using namespace std;
@@ -217,26 +218,26 @@ void DeclarationCommand::toStream(std::ostream& out) const {
 
 /* class DefineFunctionCommand */
 
-DefineFunctionCommand::DefineFunctionCommand(const std::string& name,
-                                                    const std::vector<std::pair<std::string, Type> >& args,
-                                                    Type type,
-                                                    Expr formula) :
-  d_name(name),
-  d_args(args),
-  d_type(type),
+DefineFunctionCommand::DefineFunctionCommand(Expr func,
+                                             const std::vector<Expr>& formals,
+                                             Expr formula) :
+  d_func(func),
+  d_formals(formals),
   d_formula(formula) {
 }
 
 void DefineFunctionCommand::invoke(SmtEngine* smtEngine) {
-  smtEngine->defineFunction(d_name, d_args, d_type, d_formula);
+  smtEngine->defineFunction(d_func, d_formals, d_formula);
 }
 
 void DefineFunctionCommand::toStream(std::ostream& out) const {
-  out << "DefineFunction( \"" << d_name << "\", [";
-  copy( d_args.begin(), d_args.end() - 1,
-        ostream_iterator<std::pair<std::string, Type> >(out, ", ") );
-  out << d_args.back();
-  out << "], << " << d_type << " >>, << " << d_formula << " >> )";
+  out << "DefineFunction( \"" << d_func << "\", [";
+  if(d_formals.size() > 0) {
+    copy( d_formals.begin(), d_formals.end() - 1,
+          ostream_iterator<Expr>(out, ", ") );
+    out << d_formals.back();
+  }
+  out << "], << " << d_formula << " >> )";
 }
 
 /* class GetValueCommand */
@@ -324,7 +325,7 @@ void SetInfoCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->setInfo(d_flag, d_sexpr);
     //d_result = "success";
-  } catch(BadOption& bo) {
+  } catch(BadOptionException& bo) {
     d_result = "unsupported";
   }
 }
@@ -352,7 +353,7 @@ GetInfoCommand::GetInfoCommand(std::string flag) :
 void GetInfoCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_result = smtEngine->getInfo(d_flag).getValue();
-  } catch(BadOption& bo) {
+  } catch(BadOptionException& bo) {
     d_result = "unsupported";
   }
 }
@@ -382,7 +383,7 @@ void SetOptionCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->setOption(d_flag, d_sexpr);
     //d_result = "success";
-  } catch(BadOption& bo) {
+  } catch(BadOptionException& bo) {
     d_result = "unsupported";
   }
 }
@@ -410,7 +411,7 @@ GetOptionCommand::GetOptionCommand(std::string flag) :
 void GetOptionCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_result = smtEngine->getOption(d_flag).getValue();
-  } catch(BadOption& bo) {
+  } catch(BadOptionException& bo) {
     d_result = "unsupported";
   }
 }
diff --git a/src/expr/command.h b/src/expr/command.h
index 0c78dd1c6..4c74cfd6c 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -111,14 +111,13 @@ public:
 
 class CVC4_PUBLIC DefineFunctionCommand : public Command {
 protected:
-  std::string d_name;
-  std::vector<std::pair<std::string, Type> > d_args;
-  Type d_type;
+  Expr d_func;
+  std::vector<Expr> d_formals;
   Expr d_formula;
 public:
-  DefineFunctionCommand(const std::string& name,
-                        const std::vector<std::pair<std::string, Type> >& args,
-                        Type type, Expr formula);
+  DefineFunctionCommand(Expr func,
+                        const std::vector<Expr>& formals,
+                        Expr formula);
   void invoke(SmtEngine* smtEngine);
   void toStream(std::ostream& out) const;
 };/* class DefineFunctionCommand */
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 803808b0f..5fb931a65 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -223,7 +223,11 @@ void Expr::toStream(std::ostream& out, int depth, bool types) const {
   d_node->toStream(out, depth, types);
 }
 
-Node Expr::getNode() const {
+Node Expr::getNode() const throw() {
+  return *d_node;
+}
+
+TNode Expr::getTNode() const throw() {
   return *d_node;
 }
 
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 8fab13b37..bb227f92f 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -43,8 +43,13 @@ class NodeTemplate;
 
 class Expr;
 class ExprManager;
+class SmtEngine;
 class Type;
 
+namespace smt {
+  class SmtEnginePrivate;
+}/* CVC4::smt namespace */
+
 namespace expr {
   class CVC4_PUBLIC ExprSetDepth;
   class CVC4_PUBLIC ExprPrintTypes;
@@ -383,10 +388,17 @@ protected:
    * Returns the actual internal node.
    * @return the internal node
    */
-  NodeTemplate<true> getNode() const;
+  NodeTemplate<true> getNode() const throw();
+
+  /**
+   * Returns the actual internal node as a TNode.
+   * @return the internal node
+   */
+  NodeTemplate<false> getTNode() const throw();
 
   // Friend to access the actual internal expr information and private methods
   friend class SmtEngine;
+  friend class smt::SmtEnginePrivate;
   friend class ExprManager;
 };
 
diff --git a/src/expr/node.h b/src/expr/node.h
index 67d46a977..bd6b53522 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -380,6 +380,20 @@ public:
     throw (CVC4::TypeCheckingExceptionPrivate, CVC4::AssertionException);
 
   /**
+   * Substitution of Nodes.
+   */
+  Node substitute(TNode node, TNode replacement) const;
+
+  /**
+   * Simultaneous substitution of Nodes.
+   */
+  template <class Iterator1, class Iterator2>
+  Node substitute(Iterator1 nodesBegin,
+                  Iterator1 nodesEnd,
+                  Iterator2 replacementsBegin,
+                  Iterator2 replacementsEnd) const;
+
+  /**
    * Returns the kind of this node.
    * @return the kind
    */
@@ -1035,6 +1049,59 @@ TypeNode NodeTemplate<ref_count>::getType(bool check) const
   return NodeManager::currentNM()->getType(*this, check);
 }
 
+template <bool ref_count>
+Node NodeTemplate<ref_count>::substitute(TNode node,
+                                         TNode replacement) const {
+  NodeBuilder<> nb(getKind());
+  if(getMetaKind() == kind::metakind::PARAMETERIZED) {
+    // push the operator
+    nb << getOperator();
+  }
+  for(TNode::const_iterator i = begin(),
+        iend = end();
+      i != iend;
+      ++i) {
+    if(*i == node) {
+      nb << replacement;
+    } else {
+      (*i).substitute(node, replacement);
+    }
+  }
+  Node n = nb;
+  return n;
+}
+
+template <bool ref_count>
+template <class Iterator1, class Iterator2>
+Node NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
+                                         Iterator1 nodesEnd,
+                                         Iterator2 replacementsBegin,
+                                         Iterator2 replacementsEnd) const {
+  Assert( nodesEnd - nodesBegin == replacementsEnd - replacementsBegin,
+          "Substitution iterator ranges must be equal size" );
+  Iterator1 j = find(nodesBegin, nodesEnd, *this);
+  if(j != nodesEnd) {
+    return *(replacementsBegin + (j - nodesBegin));
+  } else if(getNumChildren() == 0) {
+    return *this;
+  } else {
+    NodeBuilder<> nb(getKind());
+    if(getMetaKind() == kind::metakind::PARAMETERIZED) {
+      // push the operator
+      nb << getOperator();
+    }
+    for(TNode::const_iterator i = begin(),
+          iend = end();
+        i != iend;
+        ++i) {
+      nb << (*i).substitute(nodesBegin, nodesEnd,
+                            replacementsBegin, replacementsEnd);
+    }
+    Node n = nb;
+    return n;
+  }
+}
+
 #ifdef CVC4_DEBUG
 /**
  * Pretty printer for use within gdb.  This is not intended to be used
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index e4fc479b7..658cb1e2d 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -171,8 +171,48 @@ private:
       return iterator(d_i++);
     }
 
-    typedef std::input_iterator_tag iterator_category;
-  };
+    iterator& operator--() {
+      --d_i;
+      return *this;
+    }
+
+    iterator operator--(int) {
+      return iterator(d_i--);
+    }
+
+    iterator& operator+=(difference_type p) {
+      d_i += p;
+      return *this;
+    }
+
+    iterator& operator-=(difference_type p) {
+      d_i -= p;
+      return *this;
+    }
+
+    iterator operator+(difference_type p) {
+      return iterator(d_i + p);
+    }
+
+    iterator operator-(difference_type p) {
+      return iterator(d_i - p);
+    }
+
+    difference_type operator-(iterator i) {
+      return d_i - i.d_i;
+    }
+
+    typedef std::random_access_iterator_tag iterator_category;
+  };/* class NodeValue::iterator<T> */
+
+  // operator+ (as a function) cannot be a template, so we have to
+  // define two versions
+  friend NodeValue::iterator<NodeTemplate<true> >
+  operator+(NodeValue::iterator<NodeTemplate<true> >::difference_type p,
+            NodeValue::iterator<NodeTemplate<true> > i);
+  friend NodeValue::iterator<NodeTemplate<false> >
+  operator+(NodeValue::iterator<NodeTemplate<false> >::difference_type p,
+            NodeValue::iterator<NodeTemplate<false> > i);
 
   /** Decrement ref counts of children */
   inline void decrRefCounts();
@@ -259,6 +299,26 @@ private:
 };/* class NodeValue */
 
 /**
+ * Provides a symmetric addition operator to that already defined in
+ * the iterator class.
+ */
+inline NodeValue::iterator<NodeTemplate<true> >
+operator+(NodeValue::iterator<NodeTemplate<true> >::difference_type p,
+          NodeValue::iterator<NodeTemplate<true> > i) {
+  return i + p;
+}
+
+/**
+ * Provides a symmetric addition operator to that already defined in
+ * the iterator class.
+ */
+inline NodeValue::iterator<NodeTemplate<false> >
+operator+(NodeValue::iterator<NodeTemplate<false> >::difference_type p,
+          NodeValue::iterator<NodeTemplate<false> > i) {
+  return i + p;
+}
+
+/**
  * For hash_maps, hash_sets, etc.. but this is for expr package
  * internal use only at present!  This is likely to be POORLY
  * PERFORMING for other uses!  NodeValue::poolHash() will lead to
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 05b69f6f4..8cf555eb0 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -111,7 +111,10 @@ Type Type::substitute(const vector<Type>& types,
     replacementsNodes.push_back(*(*i).d_typeNode);
   }
 
-  return makeType(d_typeNode->substitute(typesNodes, replacementsNodes));
+  return makeType(d_typeNode->substitute(typesNodes.begin(),
+                                         typesNodes.end(),
+                                         replacementsNodes.begin(),
+                                         replacementsNodes.end()));
 }
 
 void Type::toStream(ostream& out) const {
diff --git a/src/expr/type.h b/src/expr/type.h
index 57ec3bf5c..19c3d27f3 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -60,6 +60,8 @@ struct CVC4_PUBLIC TypeHashStrategy {
  */
 class CVC4_PUBLIC Type {
 
+  friend class SmtEngine;
+  friend class SmtEnginePrivate;
   friend class ExprManager;
   friend class TypeNode;
   friend class TypeHashStrategy;
@@ -87,7 +89,7 @@ protected:
   Type(NodeManager* em, TypeNode* typeNode);
 
   /** Accessor for derived classes */
-  static TypeNode* getTypeNode(const Type& t) { return t.d_typeNode; }
+  static TypeNode* getTypeNode(const Type& t) throw() { return t.d_typeNode; }
 
 public:
 
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index a55c05c5a..badc3b72f 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -33,7 +33,10 @@ TypeNode TypeNode::substitute(const TypeNode& type,
     // push the operator
     nb << TypeNode(d_nv->d_children[0]);
   }
-  for(TypeNode::iterator i = begin(), iend = end(); i != iend; ++i) {
+  for(TypeNode::const_iterator i = begin(),
+        iend = end();
+      i != iend;
+      ++i) {
     if(*i == type) {
       nb << replacement;
     } else {
@@ -43,26 +46,6 @@ TypeNode TypeNode::substitute(const TypeNode& type,
   return nb.constructTypeNode();
 }
 
-TypeNode TypeNode::substitute(const vector<TypeNode>& types,
-                              const vector<TypeNode>& replacements) const {
-  vector<TypeNode>::const_iterator j = find(types.begin(), types.end(), *this);
-  if(j != types.end()) {
-    return replacements[j - types.begin()];
-  } else if(getNumChildren() == 0) {
-    return *this;
-  } else {
-    NodeBuilder<> nb(getKind());
-    if(getMetaKind() == kind::metakind::PARAMETERIZED) {
-      // push the operator
-      nb << TypeNode(d_nv->d_children[0]);
-    }
-    for(TypeNode::iterator i = begin(), iend = end(); i != iend; ++i) {
-      nb << (*i).substitute(types, replacements);
-    }
-    return nb.constructTypeNode();
-  }
-}
-
 bool TypeNode::isBoolean() const {
   return getKind() == kind::TYPE_CONSTANT &&
     getConst<TypeConstant>() == BOOLEAN_TYPE;
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 6780b08f7..0e763128f 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -118,8 +118,11 @@ public:
   /**
    * Simultaneous substitution of TypeNodes.
    */
-  TypeNode substitute(const std::vector<TypeNode>& types,
-                      const std::vector<TypeNode>& replacements) const;
+  template <class Iterator1, class Iterator2>
+  TypeNode substitute(Iterator1 typesBegin,
+                      Iterator1 typesEnd,
+                      Iterator2 replacementsBegin,
+                      Iterator2 replacementsEnd) const;
 
   /**
    * Structural comparison operator for expressions.
@@ -436,6 +439,35 @@ struct TypeNodeHashStrategy {
 
 namespace CVC4 {
 
+template <class Iterator1, class Iterator2>
+TypeNode TypeNode::substitute(Iterator1 typesBegin,
+                              Iterator1 typesEnd,
+                              Iterator2 replacementsBegin,
+                              Iterator2 replacementsEnd) const {
+  Assert( typesEnd - typesBegin == replacementsEnd - replacementsBegin,
+          "Substitution iterator ranges must be equal size" );
+  Iterator1 j = find(typesBegin, typesEnd, *this);
+  if(j != typesEnd) {
+    return *(replacementsBegin + (j - typesBegin));
+  } else if(getNumChildren() == 0) {
+    return *this;
+  } else {
+    NodeBuilder<> nb(getKind());
+    if(getMetaKind() == kind::metakind::PARAMETERIZED) {
+      // push the operator
+      nb << TypeNode(d_nv->d_children[0]);
+    }
+    for(TypeNode::const_iterator i = begin(),
+          iend = end();
+        i != iend;
+        ++i) {
+      nb << (*i).substitute(typesBegin, typesEnd,
+                            replacementsBegin, replacementsEnd);
+    }
+    return nb.constructTypeNode();
+  }
+}
+
 inline size_t TypeNode::getNumChildren() const {
   return d_nv->getNumChildren();
 }