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

4 files changed, 140 insertions, 87 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) {
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 0faf9bebf..1c492c843 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -186,26 +186,21 @@ public:
 
   bool strictModeEnabled() { return d_strictMode; }
 
-  /** Get the name of the input file. */
-/*
-  inline const std::string getFilename() {
-    return d_filename;
-  }
-*/
-
   /**
-   * Sets the logic for the current benchmark. Declares any logic symbols.
+   * Returns a variable, given a name.
    *
-   * @param name the name of the logic (e.g., QF_UF, AUFLIA)
+   * @param name the name of the variable
+   * @return the variable expression
    */
-//  void setLogic(const std::string& name);
+  Expr getVariable(const std::string& name);
 
   /**
-   * Returns a variable, given a name and a type.
+   * Returns a function, given a name.
+   *
    * @param var_name the name of the variable
    * @return the variable expression
    */
-  Expr getVariable(const std::string& var_name);
+  Expr getFunction(const std::string& name);
 
   /**
    * Returns a sort, given a name.
@@ -213,7 +208,7 @@ public:
   Type getSort(const std::string& sort_name);
 
   /**
-   * Returns a sort, given a name and args.
+   * Returns a (parameterized) sort, given a name and args.
    */
   Type getSort(const std::string& sort_name,
                const std::vector<Type>& params);
@@ -240,7 +235,8 @@ public:
   /**
    * Checks whether the given name is bound to a function.
    * @param name the name to check
-   * @throws ParserException if checks are enabled and name is not bound to a function
+   * @throws ParserException if checks are enabled and name is not
+   * bound to a function
    */
   void checkFunction(const std::string& name) throw (ParserException);
 
@@ -248,23 +244,26 @@ public:
    * Check that <code>kind</code> can accept <code>numArgs</code> arguments.
    * @param kind the built-in operator to check
    * @param numArgs the number of actual arguments
-   * @throws ParserException if checks are enabled and the operator <code>kind</code> cannot be
-   * applied to <code>numArgs</code> arguments.
+   * @throws ParserException if checks are enabled and the operator
+   * <code>kind</code> cannot be applied to <code>numArgs</code>
+   * arguments.
    */
   void checkArity(Kind kind, unsigned int numArgs) throw (ParserException);
 
-  /** Check that <code>kind</code> is a legal operator in the current logic and
-   * that it can accept <code>numArgs</code> arguments.
+  /**
+   * Check that <code>kind</code> is a legal operator in the current
+   * logic and that it can accept <code>numArgs</code> arguments.
    *
    * @param kind the built-in operator to check
    * @param numArgs the number of actual arguments
-   * @throws ParserException if the parser mode is strict and the operator <code>kind</kind>
-   * has not been enabled
+   * @throws ParserException if the parser mode is strict and the
+   * operator <code>kind</kind> has not been enabled
    */
   void checkOperator(Kind kind, unsigned int numArgs) throw (ParserException);
 
   /**
    * Returns the type for the variable with the given name.
+   *
    * @param var_name the symbol to lookup
    * @param type the (namespace) type of the symbol
    */
@@ -274,27 +273,41 @@ public:
   Expr mkVar(const std::string& name, const Type& type);
 
   /**
-   * Create a set of new CVC4 variable expressions of the given
-   * type.
+   * Create a set of new CVC4 variable expressions of the given type.
    */
   const std::vector<Expr>
   mkVars(const std::vector<std::string> names, const Type& type);
 
+  /** Create a new CVC4 function expression of the given type. */
+  Expr mkFunction(const std::string& name, const Type& type);
+
   /** Create a new variable definition (e.g., from a let binding). */
   void defineVar(const std::string& name, const Expr& val);
 
+  /** Create a new function definition (e.g., from a define-fun). */
+  void defineFunction(const std::string& name, const Expr& val);
+
   /** Create a new type definition. */
   void defineType(const std::string& name, const Type& type);
 
+  /** Create a new (parameterized) type definition. */
+  void defineType(const std::string& name,
+                  const std::vector<Type>& params, const Type& type);
+
   /** Create a new type definition (e.g., from an SMT-LIBv2 define-sort). */
   void defineParameterizedType(const std::string& name,
                                const std::vector<Type>& params,
                                const Type& type);
 
   /**
-   * Creates a new sort with the given name and arity.
+   * Creates a new sort with the given name.
+   */
+  Type mkSort(const std::string& name);
+
+  /**
+   * Creates a new sort constructor with the given name and arity.
    */
-  Type mkSort(const std::string& name, size_t arity = 0);
+  Type mkSortConstructor(const std::string& name, size_t arity);
 
   /**
    * Creates new sorts with the given names (all of arity 0).
@@ -314,6 +327,9 @@ public:
   /** Is the symbol bound to a function? */
   bool isFunction(const std::string& name);
 
+  /** Is the symbol bound to a defined function? */
+  bool isDefinedFunction(const std::string& name);
+
   /** Is the symbol bound to a predicate? */
   bool isPredicate(const std::string& name);
 
diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index da352c226..7ff738dd7 100644
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -85,8 +85,8 @@ void Smt::addTheory(Theory theory) {
   case THEORY_ARRAYS_EX: {
     Type indexType = mkSort("Index");
     Type elementType = mkSort("Element");
-    
-    defineType("Array",getExprManager()->mkArrayType(indexType,elementType));
+
+    defineType("Array", getExprManager()->mkArrayType(indexType,elementType));
 
     addOperator(kind::SELECT);
     addOperator(kind::STORE);
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 4c742adfc..9ad8c3177 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -19,8 +19,8 @@
 grammar Smt2;
 
 options {
-  language = 'C';                  // C output for antlr
-//  defaultErrorHandler = false;      // Skip the default error handling, just break with exceptions
+  language = 'C'; // C output for antlr
+  //defaultErrorHandler = false; // Skip the default error handling, just break with exceptions
   k = 2;
 }
 
@@ -162,8 +162,15 @@ command returns [CVC4::Command* cmd]
     DECLARE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL
     { Debug("parser") << "declare sort: '" << name
                       << "' arity=" << n << std::endl;
-      PARSER_STATE->mkSort(name, AntlrInput::tokenToUnsigned(n));
-      $cmd = new DeclarationCommand(name,EXPR_MANAGER->kindType()); }
+      unsigned arity = AntlrInput::tokenToUnsigned(n);
+      if(arity == 0) {
+        PARSER_STATE->mkSort(name);
+        $cmd = new DeclarationCommand(name, EXPR_MANAGER->kindType());
+      } else {
+        PARSER_STATE->mkSortConstructor(name, arity);
+        $cmd = new DeclarationCommand(name, EXPR_MANAGER->kindType());
+      }
+    }
   | /* sort definition */
     DEFINE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT]
     LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
@@ -223,8 +230,8 @@ command returns [CVC4::Command* cmd]
       // declare the name down here (while parsing term, signature
       // must not be extended with the name itself; no recursion
       // permitted)
-      PARSER_STATE->mkVar(name, t);
-      $cmd = new DefineFunctionCommand(name,sortedVars,t,expr);
+      PARSER_STATE->mkFunction(name, t);
+      $cmd = new DefineFunctionCommand(name, sortedVars, t, expr);
     }
   | /* value query */
     GET_VALUE_TOK LPAREN_TOK termList[terms,expr] RPAREN_TOK
@@ -315,22 +322,18 @@ term[CVC4::Expr& expr]
 
   | /* A non-built-in function application */
     LPAREN_TOK
-    functionSymbol[expr]
-    { args.push_back(expr); }
+    functionName[name,CHECK_DECLARED]
+    { args.push_back(Expr()); }
     termList[args,expr] RPAREN_TOK
-    // TODO: check arity
-    { expr = MK_EXPR(CVC4::kind::APPLY_UF,args); }
-
-  // | /* An ite expression */
-  //   LPAREN_TOK ITE_TOK
-  //   term[expr]
-  //   { args.push_back(expr); }
-  //   term[expr]
-  //   { args.push_back(expr); }
-  //   term[expr]
-  //   { args.push_back(expr); }
-  //   RPAREN_TOK
-  //   { expr = MK_EXPR(CVC4::kind::ITE, args); }
+    { PARSER_STATE->checkFunction(name);
+      const bool isDefinedFunction =
+        PARSER_STATE->isDefinedFunction(name);
+      expr = isDefinedFunction ?
+        PARSER_STATE->getFunction(name) :
+        PARSER_STATE->getVariable(name);
+      args[0] = expr;
+      // TODO: check arity
+      expr = MK_EXPR(isDefinedFunction ? CVC4::kind::APPLY : CVC4::kind::APPLY_UF, args); }
 
   | /* a let binding */
     LPAREN_TOK LET_TOK LPAREN_TOK
@@ -479,7 +482,7 @@ sortSymbol[CVC4::Type& t]
         }
         t = EXPR_MANAGER->mkArrayType( args[0], args[1] );
       } else {
-        PARSER_STATE->parseError("Unhandled parameterized type.");
+        t = PARSER_STATE->getSort(name, args);
       }
     }
   ;
@@ -516,9 +519,7 @@ symbol[std::string& id,
 
 // Base SMT-LIB tokens
 ASSERT_TOK : 'assert';
-//CATEGORY_TOK : ':category';
 CHECKSAT_TOK : 'check-sat';
-//DIFFICULTY_TOK : ':difficulty';
 DECLARE_FUN_TOK : 'declare-fun';
 DECLARE_SORT_TOK : 'declare-sort';
 DEFINE_FUN_TOK : 'define-fun';
@@ -526,23 +527,15 @@ DEFINE_SORT_TOK : 'define-sort';
 GET_VALUE_TOK : 'get-value';
 GET_ASSERTIONS_TOK : 'get-assertions';
 EXIT_TOK : 'exit';
-//FALSE_TOK : 'false';
 ITE_TOK : 'ite';
 LET_TOK : 'let';
 LPAREN_TOK : '(';
-//NOTES_TOK : ':notes';
 RPAREN_TOK : ')';
-//SAT_TOK : 'sat';
 SET_LOGIC_TOK : 'set-logic';
 SET_INFO_TOK : 'set-info';
+GET_INFO_TOK : 'get-info';
 SET_OPTION_TOK : 'set-option';
 GET_OPTION_TOK : 'get-option';
-//SMT_VERSION_TOK : ':smt-lib-version';
-//SOURCE_TOK : ':source';
-//STATUS_TOK : ':status';
-//TRUE_TOK : 'true';
-//UNKNOWN_TOK : 'unknown';
-//UNSAT_TOK : 'unsat';
 
 // operators (NOTE: theory symbols go here)
 AMPERSAND_TOK     : '&';
@@ -605,15 +598,18 @@ WHITESPACE
   ;
 
 /**
- * Matches an integer constant from the input (non-empty sequence of digits, with
- * no leading zeroes).
+ * Matches an integer constant from the input (non-empty sequence of
+ * digits, with no leading zeroes).
  */
 INTEGER_LITERAL
   : NUMERAL
   ;
 
-/** Match an integer constant. In non-strict mode, this is any sequence of
- * digits. In strict mode, non-zero integers can't have leading zeroes. */
+/**
+ * Match an integer constant. In non-strict mode, this is any sequence
+ * of digits. In strict mode, non-zero integers can't have leading
+ * zeroes.
+ */
 fragment NUMERAL
 @init {
   char *start = (char*) GETCHARINDEX();
@@ -631,8 +627,8 @@ fragment NUMERAL
   ;
 
 /**
-  * Matches a decimal constant from the input.
-  */
+ * Matches a decimal constant from the input.
+ */
 DECIMAL_LITERAL
   : NUMERAL '.' DIGIT+
   ;
@@ -684,7 +680,8 @@ fragment DIGIT : '0'..'9';
 
 fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
 
-/** Matches the characters that may appear in a "symbol" (i.e., an identifier)
+/**
+ * Matches the characters that may appear in a "symbol" (i.e., an identifier)
  */
 fragment SYMBOL_CHAR
   : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '_' | '~'