declare-sort, define-sort working but not thoroughly tested; define-fun half working (just need to decide where to expand)

1 files changed, 61 insertions, 21 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 39f61c16d..297a2d804 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -66,11 +66,15 @@ Expr Parser::getVariable(const std::string& name) {
   return getSymbol(name, SYM_VARIABLE);
 }
 
+Expr Parser::getFunction(const std::string& name) {
+  return getSymbol(name, SYM_VARIABLE);
+}
+
 Type
 Parser::getType(const std::string& var_name,
                      SymbolType type) {
   Assert( isDeclared(var_name, type) );
-  Type t = getSymbol(var_name,type).getType();
+  Type t = getSymbol(var_name, type).getType();
   return t;
 }
 
@@ -83,8 +87,7 @@ Type Parser::getSort(const std::string& name) {
 Type Parser::getSort(const std::string& name,
                      const std::vector<Type>& params) {
   Assert( isDeclared(name, SYM_SORT) );
-  Type t = d_declScope.lookupType(name);
-  Warning() << "FIXME use params to realize parameterized sort\n";
+  Type t = d_declScope.lookupType(name, params);
   return t;
 }
 
@@ -98,6 +101,11 @@ bool Parser::isFunction(const std::string& name) {
   return isDeclared(name, SYM_VARIABLE) && getType(name).isFunction();
 }
 
+/* Returns true if name is bound to a defined function. */
+bool Parser::isDefinedFunction(const std::string& name) {
+  return isFunction(name) && d_declScope.isBoundDefinedFunction(name);
+}
+
 /* Returns true if name is bound to a function returning boolean. */
 bool Parser::isPredicate(const std::string& name) {
   return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate();
@@ -105,32 +113,54 @@ bool Parser::isPredicate(const std::string& name) {
 
 Expr
 Parser::mkVar(const std::string& name, const Type& type) {
-  Debug("parser") << "mkVar(" << name << "," << type << ")" << std::endl;
+  Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
   Expr expr = d_exprManager->mkVar(name, type);
-  defineVar(name,expr);
+  defineVar(name, expr);
+  return expr;
+}
+
+Expr
+Parser::mkFunction(const std::string& name, const Type& type) {
+  Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
+  Expr expr = d_exprManager->mkVar(name, type);
+  defineFunction(name, expr);
   return expr;
 }
 
 const std::vector<Expr>
 Parser::mkVars(const std::vector<std::string> names,
-                    const Type& type) {
+               const Type& type) {
   std::vector<Expr> vars;
   for(unsigned i = 0; i < names.size(); ++i) {
-    vars.push_back(mkVar(names[i],type));
+    vars.push_back(mkVar(names[i], type));
   }
   return vars;
 }
 
 void
 Parser::defineVar(const std::string& name, const Expr& val) {
-  d_declScope.bind(name,val);
-  Assert(isDeclared(name));
+  d_declScope.bind(name, val);
+  Assert( isDeclared(name) );
+}
+
+void
+Parser::defineFunction(const std::string& name, const Expr& val) {
+  d_declScope.bindDefinedFunction(name, val);
+  Assert( isDeclared(name) );
 }
 
 void
 Parser::defineType(const std::string& name, const Type& type) {
-  d_declScope.bindType(name,type);
-  Assert( isDeclared(name, SYM_SORT) ) ;
+  d_declScope.bindType(name, type);
+  Assert( isDeclared(name, SYM_SORT) );
+}
+
+void
+Parser::defineType(const std::string& name,
+                   const std::vector<Type>& params,
+                   const Type& type) {
+  d_declScope.bindType(name, params, type);
+  Assert( isDeclared(name, SYM_SORT) );
 }
 
 void
@@ -139,20 +169,30 @@ Parser::defineParameterizedType(const std::string& name,
                                 const Type& type) {
   if(Debug.isOn("parser")) {
     Debug("parser") << "defineParameterizedType(" << name << ", " << params.size() << ", [";
-    copy(params.begin(), params.end() - 1,
-         ostream_iterator<Type>(Debug("parser"), ", ") );
-    Debug("parser") << params.back();
+    if(params.size() > 0) {
+      copy(params.begin(), params.end() - 1,
+           ostream_iterator<Type>(Debug("parser"), ", ") );
+      Debug("parser") << params.back();
+    }
     Debug("parser") << "], " << type << ")" << std::endl;
   }
-  Warning("defineSort unimplemented\n");
-  defineType(name,type);
+  defineType(name, params, type);
+}
+
+Type
+Parser::mkSort(const std::string& name) {
+  Debug("parser") << "newSort(" << name << ")" << std::endl;
+  Type type = d_exprManager->mkSort(name);
+  defineType(name, type);
+  return type;
 }
 
 Type
-Parser::mkSort(const std::string& name, size_t arity) {
-  Debug("parser") << "newSort(" << name << ", " << arity << ")" << std::endl;
-  Type type = d_exprManager->mkSort(name, arity);
-  defineType(name,type);
+Parser::mkSortConstructor(const std::string& name, size_t arity) {
+  Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")"
+                  << std::endl;
+  Type type = d_exprManager->mkSortConstructor(name, arity);
+  defineType(name, vector<Type>(arity), type);
   return type;
 }
 
@@ -239,7 +279,7 @@ void Parser::checkOperator(Kind kind, unsigned int numArgs) throw (ParserExcepti
   if( d_strictMode && d_logicOperators.find(kind) == d_logicOperators.end() ) {
     parseError( "Operator is not defined in the current logic: " + kindToString(kind) );
   }
-  checkArity(kind,numArgs);
+  checkArity(kind, numArgs);
 }
 
 void Parser::addOperator(Kind kind) {