support for SMT-LIBv2 :named attributes, and attributes in general; zero-ary define-fun; several set-info, set-option, get-option, get-info improvementss

3 files changed, 86 insertions, 45 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 297a2d804..09e65526d 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -103,7 +103,9 @@ bool Parser::isFunction(const std::string& name) {
 
 /* Returns true if name is bound to a defined function. */
 bool Parser::isDefinedFunction(const std::string& name) {
-  return isFunction(name) && d_declScope.isBoundDefinedFunction(name);
+  // more permissive in type than isFunction(), because defined
+  // functions can be zero-ary and declared functions cannot.
+  return d_declScope.isBoundDefinedFunction(name);
 }
 
 /* Returns true if name is bound to a function returning boolean. */
@@ -286,50 +288,42 @@ void Parser::addOperator(Kind kind) {
   d_logicOperators.insert(kind);
 }
 
+void Parser::preemptCommand(Command* cmd) {
+  d_commandQueue.push_back(cmd);
+}
+
 Command* Parser::nextCommand() throw(ParserException) {
   Debug("parser") << "nextCommand()" << std::endl;
   Command* cmd = NULL;
-  if(!done()) {
-    try {
-      cmd = d_input->parseCommand();
-      if(cmd == NULL) {
-        setDone();
-      }
-    } catch(ParserException& e) {
+  if(!d_commandQueue.empty()) {
+    cmd = d_commandQueue.front();
+    d_commandQueue.pop_front();
+    if(cmd == NULL) {
       setDone();
-      throw;
-    } catch(Exception& e) {
-      setDone();
-      stringstream ss;
-      ss << e;
-      parseError( ss.str() );
     }
-  }
-  Debug("parser") << "nextCommand() => " << cmd << std::endl;
-  return cmd;
-}
-
-Expr Parser::nextExpression() throw(ParserException) {
-  Debug("parser") << "nextExpression()" << std::endl;
-  Expr result;
-  if(!done()) {
-    try {
-      result = d_input->parseExpr();
-      if(result.isNull()) {
+  } else {
+    if(!done()) {
+      try {
+        cmd = d_input->parseCommand();
+        d_commandQueue.push_back(cmd);
+        cmd = d_commandQueue.front();
+        d_commandQueue.pop_front();
+        if(cmd == NULL) {
+          setDone();
+        }
+      } catch(ParserException& e) {
         setDone();
+        throw;
+      } catch(Exception& e) {
+        setDone();
+        stringstream ss;
+        ss << e;
+        parseError( ss.str() );
       }
-    } catch(ParserException& e) {
-      setDone();
-      throw;
-    } catch(Exception& e) {
-      setDone();
-      stringstream ss;
-      ss << e;
-      parseError( ss.str() );
     }
   }
-  Debug("parser") << "nextExpression() => " << result << std::endl;
-  return result;
+  Debug("parser") << "nextCommand() => " << cmd << std::endl;
+  return cmd;
 }
 
 
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 1c492c843..bc0142089 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -23,6 +23,7 @@
 
 #include <string>
 #include <set>
+#include <list>
 
 #include "input.h"
 #include "parser_exception.h"
@@ -124,6 +125,13 @@ class CVC4_PUBLIC Parser {
   /** The set of operators available in the current logic. */
   std::set<Kind> d_logicOperators;
 
+  /**
+   * "Preemption commands": extra commands implied by subterms that
+   * should be issued before the currently-being-parsed command is
+   * issued.  Used to support SMT-LIBv2 ":named" attribute on terms.
+   */
+  std::list<Command*> d_commandQueue;
+
   /** Lookup a symbol in the given namespace. */
   Expr getSymbol(const std::string& var_name, SymbolType type);
 
@@ -315,12 +323,20 @@ public:
   const std::vector<Type>
   mkSorts(const std::vector<std::string>& names);
 
-  /** Add an operator to the current legal set.
+  /**
+   * Add an operator to the current legal set.
    *
    * @param kind the built-in operator to add
    */
   void addOperator(Kind kind);
 
+  /**
+   * Preempt the next returned command with other ones; used to
+   * support the :named attribute in SMT-LIBv2, which implicitly
+   * inserts a new command before the current one.
+   */
+  void preemptCommand(Command* cmd);
+
   /** Is the symbol bound to a boolean variable? */
   bool isBoolean(const std::string& name);
 
@@ -334,7 +350,6 @@ public:
   bool isPredicate(const std::string& name);
 
   Command* nextCommand() throw(ParserException);
-  Expr nextExpression() throw(ParserException);
 
   inline void parseError(const std::string& msg) throw (ParserException) {
     d_input->parseError(msg);
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 4c447f9c1..ddfd1804e 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -196,7 +196,7 @@ command returns [CVC4::Command* cmd]
     sortSymbol[t]
     { Debug("parser") << "declare fun: '" << name << "'" << std::endl;
       if( sorts.size() > 0 ) {
-        t = EXPR_MANAGER->mkFunctionType(sorts,t);
+        t = EXPR_MANAGER->mkFunctionType(sorts, t);
       }
       PARSER_STATE->mkVar(name, t);
       $cmd = new DeclarationCommand(name,t); }
@@ -215,7 +215,7 @@ command returns [CVC4::Command* cmd]
             ++i) {
           sorts.push_back((*i).second);
         }
-        t = EXPR_MANAGER->mkFunctionType(sorts,t);
+        t = EXPR_MANAGER->mkFunctionType(sorts, t);
       }
       PARSER_STATE->pushScope();
       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
@@ -320,6 +320,7 @@ term[CVC4::Expr& expr]
   Kind kind;
   std::string name;
   std::vector<Expr> args;
+  SExpr sexpr;
 }
   : /* a built-in operator application */
     LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK
@@ -361,8 +362,9 @@ term[CVC4::Expr& expr]
         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); }
+      expr = MK_EXPR(isDefinedFunction ?
+                     CVC4::kind::APPLY :
+                     CVC4::kind::APPLY_UF, args); }
 
   | /* a let binding */
     LPAREN_TOK LET_TOK LPAREN_TOK
@@ -374,9 +376,38 @@ term[CVC4::Expr& expr]
     RPAREN_TOK
     { PARSER_STATE->popScope(); }
 
-  | /* a variable */
-    symbol[name,CHECK_DECLARED,SYM_VARIABLE]
-    { expr = PARSER_STATE->getVariable(name); }
+    /* a variable */
+  | symbol[name,CHECK_DECLARED,SYM_VARIABLE]
+    { const bool isDefinedFunction =
+        PARSER_STATE->isDefinedFunction(name);
+      if(isDefinedFunction) {
+        expr = MK_EXPR(CVC4::kind::APPLY,
+                       PARSER_STATE->getFunction(name));
+      } else {
+        expr = PARSER_STATE->getVariable(name);
+      }
+    }
+
+    /* attributed expressions */
+  | LPAREN_TOK ATTRIBUTE_TOK term[expr] KEYWORD symbolicExpr[sexpr] RPAREN_TOK
+    { std::string attr = AntlrInput::tokenText($KEYWORD);
+      if(attr == ":named") {
+        name = sexpr.getValue();
+        // FIXME ensure expr is a closed subterm
+        // check that sexpr is a fresh function symbol
+        PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
+        // define it
+        Expr func = PARSER_STATE->mkFunction(name, expr.getType());
+        // bind name to expr with define-fun
+        Command* c =
+          new DefineFunctionCommand(func, std::vector<Expr>(), expr);
+        PARSER_STATE->preemptCommand(c);
+      } else {
+        std::stringstream ss;
+        ss << "Attribute `" << attr << "' not supported";
+        PARSER_STATE->parseError(ss.str());
+      }
+    }
 
     /* constants */
   | INTEGER_LITERAL
@@ -558,6 +589,7 @@ GET_ASSERTIONS_TOK : 'get-assertions';
 EXIT_TOK : 'exit';
 ITE_TOK : 'ite';
 LET_TOK : 'let';
+ATTRIBUTE_TOK : '!';
 LPAREN_TOK : '(';
 RPAREN_TOK : ')';
 SET_LOGIC_TOK : 'set-logic';