minor fixes to printing and parsing of CVC-language defined functions and lambdas...

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 29aa1a737762ea5b13b2c2b6dd123acb13979a12..3c376f632d861b74f902955513baca3d29b36e85 100644 (file)
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -206,6 +206,7 @@ Expr Expr::getOperator() const {
 Type Expr::getType(bool check) const throw (TypeCheckingException) {
   ExprManagerScope ems(*this);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  CheckArgument(!d_node->isNull(), this, "Can't get type of null expression!");
   return d_exprManager->getType(*this, check);
 }
 

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 2d659cfe3a652b29c3882d8604a3607d988e7dd7..9f0c2cddbaeffdf8e8e9e357baf093c1ca6b6584 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -897,6 +897,7 @@ declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector<std::stri
           }
         }
       } else {
+        // f is not null-- meaning this is a definition not a declaration
         if(!topLevel) {
           // must be top-level; doesn't make sense to write something
           // like e.g. FORALL(x:INT = 4): [...]
@@ -908,8 +909,9 @@ declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector<std::stri
             i != i_end;
             ++i) {
           PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE);
+          Expr func = EXPR_MANAGER->mkVar(*i, f.getType());
           PARSER_STATE->defineFunction(*i, f);
-          Command* decl = new DefineFunctionCommand(*i, Expr(), f);
+          Command* decl = new DefineFunctionCommand(*i, func, f);
           seq->addCommand(decl);
         }
       }

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 0d47c9c6c2861e913ff87730a9ffb99ded8fc910..8d76a7332566de56e35eddb191dbed80cda99c3d 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -484,15 +484,19 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw()
   Expr func = c->getFunction();
   const vector<Expr>& formals = c->getFormals();
   Expr formula = c->getFormula();
-  out << func << " : " << func.getType() << " = LAMBDA(";
-  vector<Expr>::const_iterator i = formals.begin();
-  while(i != formals.end()) {
-    out << (*i) << ":" << (*i).getType();
-    if(++i != formals.end()) {
-      out << ", ";
+  out << func << " : " << func.getType() << " = ";
+  if(formals.size() > 0) {
+    out << "LAMBDA(";
+    vector<Expr>::const_iterator i = formals.begin();
+    while(i != formals.end()) {
+      out << (*i) << ":" << (*i).getType();
+      if(++i != formals.end()) {
+        out << ", ";
+      }
     }
+    out << "): ";
   }
-  out << "): " << formula << ";";
+  out << formula << ";";
 }
 
 static void toStream(std::ostream& out, const DeclareTypeCommand* c) throw() {