More parser cleanup. Should fix problems with last commit.

4 files changed, 69 insertions, 130 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 84713fc59..f32da2eac 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -48,6 +48,7 @@ options {
 
 @parser::includes {
 #include "expr/command.h"
+#include "parser/input.h"
 
 namespace CVC4 {
   class Expr;
@@ -58,15 +59,21 @@ namespace CVC4 {
 #include "expr/expr.h"
 #include "expr/kind.h"
 #include "expr/type.h"
-#include "parser/cvc/cvc_input.h"
+#include "parser/antlr_input.h"
 #include "util/output.h"
 #include <vector>
 
 using namespace CVC4;
 using namespace CVC4::parser;
 
-#undef CVC_INPUT
-#define CVC_INPUT ((CvcInput*)(PARSER->super))
+/* These need to be macros so they can refer to the PARSER macro, which will be defined
+ * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
+#undef ANTLR_INPUT 
+#define ANTLR_INPUT ((Input*)PARSER->super)
+#undef EXPR_MANAGER
+#define EXPR_MANAGER ANTLR_INPUT->getExprManager()
+#undef MK_EXPR
+#define MK_EXPR EXPR_MANAGER->mkExpr
 }
 
 /**
@@ -98,7 +105,7 @@ command returns [CVC4::Command* cmd = 0]
   : ASSERT_TOK formula[f] SEMICOLON { cmd = new AssertCommand(f);   }
   | QUERY_TOK formula[f] SEMICOLON { cmd = new QueryCommand(f);    }
   | CHECKSAT_TOK formula[f] SEMICOLON { cmd = new CheckSatCommand(f); }
-  | CHECKSAT_TOK SEMICOLON { cmd = new CheckSatCommand(CVC_INPUT->getTrueExpr()); }
+  | CHECKSAT_TOK SEMICOLON { cmd = new CheckSatCommand(MK_EXPR(CVC4::kind::TRUE)); }
   | PUSH_TOK SEMICOLON { cmd = new PushCommand(); }
   | POP_TOK SEMICOLON { cmd = new PopCommand(); }
   | declaration[cmd]
@@ -126,9 +133,9 @@ declType[CVC4::Type*& t, std::vector<std::string>& idList]
   Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
   : /* A sort declaration (e.g., "T : TYPE") */
-    TYPE_TOK { CVC_INPUT->newSorts(idList); t = CVC_INPUT->kindType(); }
+    TYPE_TOK { ANTLR_INPUT->newSorts(idList); t = ANTLR_INPUT->kindType(); }
   | /* A variable declaration */
-    type[t] { CVC_INPUT->mkVars(idList,t); }
+    type[t] { ANTLR_INPUT->mkVars(idList,t); }
   ;
 
 /**
@@ -145,13 +152,13 @@ type[CVC4::Type*& t]
   | /* Single-parameter function type */
     baseType[t] { typeList.push_back(t); }
     ARROW_TOK baseType[t] 
-    { t = CVC_INPUT->functionType(typeList,t); }
+    { t = ANTLR_INPUT->functionType(typeList,t); }
   | /* Multi-parameter function type */
     LPAREN baseType[t]
     { typeList.push_back(t); }
     (COMMA baseType[t] { typeList.push_back(t); } )+
     RPAREN ARROW_TOK baseType[t]
-    { t = CVC_INPUT->functionType(typeList,t); }
+    { t = ANTLR_INPUT->functionType(typeList,t); }
   ;
 
 /**
@@ -179,7 +186,7 @@ identifier[std::string& id,
            CVC4::parser::SymbolType type]
   : IDENTIFIER
     { id = AntlrInput::tokenText($IDENTIFIER);
-      CVC_INPUT->checkDeclaration(id, check, type); }
+      ANTLR_INPUT->checkDeclaration(id, check, type); }
   ;
 
 /**
@@ -191,7 +198,7 @@ baseType[CVC4::Type*& t]
   std::string id;
   Debug("parser-extra") << "base type: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
-  : BOOLEAN_TOK { t = CVC_INPUT->booleanType(); }
+  : BOOLEAN_TOK { t = ANTLR_INPUT->booleanType(); }
   | typeSymbol[t]
   ;
 
@@ -204,7 +211,7 @@ typeSymbol[CVC4::Type*& t]
   Debug("parser-extra") << "type symbol: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
   : identifier[id,CHECK_DECLARED,SYM_SORT]
-    { t = CVC_INPUT->getSort(id); }
+    { t = ANTLR_INPUT->getSort(id); }
   ;
 
 /**
@@ -242,7 +249,7 @@ iffFormula[CVC4::Expr& f]
   : impliesFormula[f]
     ( IFF_TOK 
     	iffFormula[e]
-        { f = CVC_INPUT->mkExpr(CVC4::kind::IFF, f, e); }
+        { f = MK_EXPR(CVC4::kind::IFF, f, e); }
     )?
   ;
 
@@ -256,7 +263,7 @@ impliesFormula[CVC4::Expr& f]
 }
   : orFormula[f]
     ( IMPLIES_TOK impliesFormula[e]
-        { f = CVC_INPUT->mkExpr(CVC4::kind::IMPLIES, f, e); }
+        { f = MK_EXPR(CVC4::kind::IMPLIES, f, e); }
     )?
   ;
 
@@ -273,7 +280,7 @@ orFormula[CVC4::Expr& f]
         xorFormula[f] { exprs.push_back(f); } )*
     {
       if( exprs.size() > 0 ) {
-        f = CVC_INPUT->mkExpr(CVC4::kind::OR, exprs);
+        f = MK_EXPR(CVC4::kind::OR, exprs);
       }
     }
   ;
@@ -288,7 +295,7 @@ xorFormula[CVC4::Expr& f]
 }
   : andFormula[f]
     ( XOR_TOK andFormula[e]
-      { f = CVC_INPUT->mkExpr(CVC4::kind::XOR,f, e); }
+      { f = MK_EXPR(CVC4::kind::XOR,f, e); }
     )*
   ;
 
@@ -305,7 +312,7 @@ andFormula[CVC4::Expr& f]
       notFormula[f] { exprs.push_back(f); } )*
     {
       if( exprs.size() > 0 ) {
-        f = CVC_INPUT->mkExpr(CVC4::kind::AND, exprs);
+        f = MK_EXPR(CVC4::kind::AND, exprs);
       }
     }
   ;
@@ -320,7 +327,7 @@ notFormula[CVC4::Expr& f]
 }
   : /* negation */
     NOT_TOK notFormula[f]
-    { f = CVC_INPUT->mkExpr(CVC4::kind::NOT, f); }
+    { f = MK_EXPR(CVC4::kind::NOT, f); }
   | /* a boolean atom */
     predFormula[f]
   ;
@@ -332,7 +339,7 @@ predFormula[CVC4::Expr& f]
 }
   : term[f]
     (EQUAL_TOK term[e]
-      { f = CVC_INPUT->mkExpr(CVC4::kind::EQUAL, f, e); }
+      { f = MK_EXPR(CVC4::kind::EQUAL, f, e); }
     )?
   ; // TODO: lt, gt, etc.
 
@@ -351,7 +358,7 @@ term[CVC4::Expr& f]
     { args.push_back( f ); }
     LPAREN formulaList[args] RPAREN
     // TODO: check arity
-    { f = CVC_INPUT->mkExpr(CVC4::kind::APPLY_UF, args); }
+    { f = MK_EXPR(CVC4::kind::APPLY_UF, args); }
 
   | /* if-then-else */
     iteTerm[f]
@@ -360,12 +367,12 @@ term[CVC4::Expr& f]
     LPAREN formula[f] RPAREN
 
     /* constants */
-  | TRUE_TOK  { f = CVC_INPUT->getTrueExpr(); }
-  | FALSE_TOK { f = CVC_INPUT->getFalseExpr(); }
+  | TRUE_TOK  { f = MK_EXPR(CVC4::kind::TRUE); }
+  | FALSE_TOK { f = MK_EXPR(CVC4::kind::FALSE); }
 
   | /* variable */
     identifier[name,CHECK_DECLARED,SYM_VARIABLE]
-    { f = CVC_INPUT->getVariable(name); }
+    { f = ANTLR_INPUT->getVariable(name); }
   ;
 
 /**
@@ -380,7 +387,7 @@ iteTerm[CVC4::Expr& f]
     THEN_TOK formula[f] { args.push_back(f); }
     iteElseTerm[f] { args.push_back(f); }
     ENDIF_TOK
-    { f = CVC_INPUT->mkExpr(CVC4::kind::ITE, args); }
+    { f = MK_EXPR(CVC4::kind::ITE, args); }
   ;
 
 /**
@@ -395,7 +402,7 @@ iteElseTerm[CVC4::Expr& f]
   | ELSEIF_TOK iteCondition = formula[f] { args.push_back(f); }
     THEN_TOK iteThen = formula[f] { args.push_back(f); }
     iteElse = iteElseTerm[f] { args.push_back(f); }
-    { f = CVC_INPUT->mkExpr(CVC4::kind::ITE, args); }
+    { f = MK_EXPR(CVC4::kind::ITE, args); }
   ;
 
 /**
@@ -409,8 +416,8 @@ functionSymbol[CVC4::Expr& f]
   std::string name;
 }
   : identifier[name,CHECK_DECLARED,SYM_FUNCTION]
-    { CVC_INPUT->checkFunction(name);
-      f = CVC_INPUT->getFunction(name); }
+    { ANTLR_INPUT->checkFunction(name);
+      f = ANTLR_INPUT->getFunction(name); }
   ;
 
 
diff --git a/src/parser/input.cpp b/src/parser/input.cpp
index 24ad93d05..06faf5106 100644
--- a/src/parser/input.cpp
+++ b/src/parser/input.cpp
@@ -209,39 +209,6 @@ bool Input::isPredicate(const std::string& name) {
   return isDeclared(name, SYM_FUNCTION) && getType(name)->isPredicate();
 }
 
-Expr Input::getTrueExpr() const {
-  return d_exprManager->mkExpr(TRUE);
-}
-
-Expr Input::getFalseExpr() const {
-  return d_exprManager->mkExpr(FALSE);
-}
-
-Expr Input::mkExpr(Kind kind, const Expr& child) {
-  Expr result = d_exprManager->mkExpr(kind, child);
-  Debug("parser") << "mkExpr() => " << result << std::endl;
-  return result;
-}
-
-Expr Input::mkExpr(Kind kind, const Expr& child_1, const Expr& child_2) {
-  Expr result = d_exprManager->mkExpr(kind, child_1, child_2);
-  Debug("parser") << "mkExpr() => " << result << std::endl;
-  return result;
-}
-
-Expr Input::mkExpr(Kind kind, const Expr& child_1, const Expr& child_2,
-                         const Expr& child_3) {
-  Expr result = d_exprManager->mkExpr(kind, child_1, child_2, child_3);
-  Debug("parser") << "mkExpr() => " << result << std::endl;
-  return result;
-}
-
-Expr Input::mkExpr(Kind kind, const std::vector<Expr>& children) {
-  Expr result = d_exprManager->mkExpr(kind, children);
-  Debug("parser") << "mkExpr() => " << result << std::endl;
-  return result;
-}
-
 Type*
 Input::functionType(Type* domainType,
                           Type* rangeType) {
diff --git a/src/parser/input.h b/src/parser/input.h
index af580d78e..42a94ab41 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -153,6 +153,11 @@ public:
    */
   static Input* newStringParser(ExprManager* exprManager, InputLanguage lang, const std::string& input, const std::string& name);
 
+  /** Get the <code>ExprManager</code> associated with this input. */
+  inline ExprManager* getExprManager() const {
+    return d_exprManager;
+  }
+
   /**
    * Parse the next command of the input. If EOF is encountered a EmptyCommand
    * is returned and done flag is set.
@@ -258,53 +263,6 @@ public:
     Type* getType(const std::string& var_name,
                         SymbolType type = SYM_VARIABLE);
 
-    /**
-     * Returns the true expression.
-     * @return the true expression
-     */
-    Expr getTrueExpr() const;
-
-    /**
-     * Returns the false expression.
-     * @return the false expression
-     */
-    Expr getFalseExpr() const;
-
-    /**
-     * Creates a new unary CVC4 expression using the expression manager.
-     * @param kind the kind of the expression
-     * @param child the child
-     * @return the new unary expression
-     */
-    Expr mkExpr(Kind kind, const Expr& child);
-
-    /**
-     * Creates a new binary CVC4 expression using the expression manager.
-     * @param kind the kind of the expression
-     * @param child1 the first child
-     * @param child2 the second child
-     * @return the new binary expression
-     */
-    Expr mkExpr(Kind kind, const Expr& child_1, const Expr& child_2);
-
-    /**
-     * Creates a new ternary CVC4 expression using the expression manager.
-     * @param kind the kind of the expression
-     * @param child_1 the first child
-     * @param child_2 the second child
-     * @param child_3
-     * @return the new ternary expression
-     */
-    Expr mkExpr(Kind kind, const Expr& child_1, const Expr& child_2,
-                const Expr& child_3);
-
-    /**
-     * Creates a new CVC4 expression using the expression manager.
-     * @param kind the kind of the expression
-     * @param children the children of the expression
-     */
-    Expr mkExpr(Kind kind, const std::vector<Expr>& children);
-
     /** Create a new CVC4 variable expression of the given type. */
     Expr mkVar(const std::string& name, Type* type);
 
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index e97ced324..56bedce81 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -48,6 +48,7 @@ options {
 
 @parser::includes {
 #include "expr/command.h"
+#include "parser/input.h"
 
 namespace CVC4 {
   class Expr;
@@ -58,15 +59,21 @@ namespace CVC4 {
 #include "expr/expr.h"
 #include "expr/kind.h"
 #include "expr/type.h"
-#include "parser/smt/smt_input.h"
+#include "parser/antlr_input.h"
 #include "util/output.h"
 #include <vector>
 
 using namespace CVC4;
 using namespace CVC4::parser;
 
-#undef SMT_INPUT
-#define SMT_INPUT ((SmtInput*)(PARSER->super))
+/* These need to be macros so they can refer to the PARSER macro, which will be defined
+ * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
+#undef ANTLR_INPUT 
+#define ANTLR_INPUT ((Input*)PARSER->super)
+#undef EXPR_MANAGER
+#define EXPR_MANAGER ANTLR_INPUT->getExprManager()
+#undef MK_EXPR
+#define MK_EXPR EXPR_MANAGER->mkExpr
 }
 
 /**
@@ -120,7 +127,7 @@ benchAttribute returns [CVC4::Command* smt_command]
   Expr expr;
 }
   : LOGIC_TOK identifier[name,CHECK_NONE,SYM_VARIABLE]
-    { SMT_INPUT->setLogic(name);
+    { ANTLR_INPUT->setLogic(name);
       smt_command = new SetBenchmarkLogicCommand(name);   }
   | ASSUMPTION_TOK annotatedFormula[expr]
     { smt_command = new AssertCommand(expr);   }
@@ -148,13 +155,13 @@ annotatedFormula[CVC4::Expr& expr]
 } 
   : /* a built-in operator application */
     LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr] RPAREN_TOK 
-    { SMT_INPUT->checkArity(kind, args.size());
+    { ANTLR_INPUT->checkArity(kind, args.size());
       if((kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) {
         /* Unary AND/OR can be replaced with the argument.
 	       It just so happens expr should already by the only argument. */
         Assert( expr == args[0] );
       } else {
-        expr = SMT_INPUT->mkExpr(kind, args);
+        expr = MK_EXPR(kind, args);
       }
     }
 
@@ -169,7 +176,7 @@ annotatedFormula[CVC4::Expr& expr]
     { args.push_back(expr); }
     annotatedFormulas[args,expr] RPAREN_TOK
     // TODO: check arity
-    { expr = SMT_INPUT->mkExpr(CVC4::kind::APPLY_UF,args); }
+    { expr = MK_EXPR(CVC4::kind::APPLY_UF,args); }
 
   | /* An ite expression */
     LPAREN_TOK (ITE_TOK | IF_THEN_ELSE_TOK) 
@@ -180,27 +187,27 @@ annotatedFormula[CVC4::Expr& expr]
     annotatedFormula[expr]
     { args.push_back(expr); } 
     RPAREN_TOK
-    { expr = SMT_INPUT->mkExpr(CVC4::kind::ITE, args); }
+    { expr = MK_EXPR(CVC4::kind::ITE, args); }
 
   | /* a let/flet binding */
     LPAREN_TOK 
     (LET_TOK LPAREN_TOK var_identifier[name,CHECK_UNDECLARED]
       | FLET_TOK LPAREN_TOK fun_identifier[name,CHECK_UNDECLARED] )
     annotatedFormula[expr] RPAREN_TOK
-    { SMT_INPUT->defineVar(name,expr); }
+    { ANTLR_INPUT->defineVar(name,expr); }
     annotatedFormula[expr]
     RPAREN_TOK
-    { SMT_INPUT->undefineVar(name); }
+    { ANTLR_INPUT->undefineVar(name); }
 
   | /* a variable */
     ( identifier[name,CHECK_DECLARED,SYM_VARIABLE]
       | var_identifier[name,CHECK_DECLARED] 
       | fun_identifier[name,CHECK_DECLARED] )
-    { expr = SMT_INPUT->getVariable(name); }
+    { expr = ANTLR_INPUT->getVariable(name); }
 
     /* constants */
-  | TRUE_TOK          { expr = SMT_INPUT->getTrueExpr(); }
-  | FALSE_TOK         { expr = SMT_INPUT->getFalseExpr(); }
+  | TRUE_TOK          { expr = MK_EXPR(CVC4::kind::TRUE); }
+  | FALSE_TOK         { expr = MK_EXPR(CVC4::kind::FALSE); }
     /* TODO: let, flet, quantifiers, arithmetic constants */
   ;
 
@@ -259,8 +266,8 @@ functionSymbol[CVC4::Expr& fun]
 	std::string name;
 }
   : functionName[name,CHECK_DECLARED]
-    { SMT_INPUT->checkFunction(name);
-      fun = SMT_INPUT->getFunction(name); }
+    { ANTLR_INPUT->checkFunction(name);
+      fun = ANTLR_INPUT->getFunction(name); }
   ;
   
 /**
@@ -281,8 +288,8 @@ functionDeclaration
       t = sortSymbol // require at least one sort
     { sorts.push_back(t); }
       sortList[sorts] RPAREN_TOK
-    { t = SMT_INPUT->functionType(sorts);
-      SMT_INPUT->mkVar(name, t); } 
+    { t = ANTLR_INPUT->functionType(sorts);
+      ANTLR_INPUT->mkVar(name, t); } 
   ;
               
 /**
@@ -294,8 +301,8 @@ predicateDeclaration
   std::vector<Type*> p_sorts;
 }
   : LPAREN_TOK predicateName[name,CHECK_UNDECLARED] sortList[p_sorts] RPAREN_TOK
-    { Type *t = SMT_INPUT->predicateType(p_sorts);
-      SMT_INPUT->mkVar(name, t); } 
+    { Type *t = ANTLR_INPUT->predicateType(p_sorts);
+      ANTLR_INPUT->mkVar(name, t); } 
   ;
 
 sortDeclaration 
@@ -304,7 +311,7 @@ sortDeclaration
 }
   : sortName[name,CHECK_UNDECLARED]
     { Debug("parser") << "sort decl: '" << name << "'" << std::endl;
-      SMT_INPUT->newSort(name); }
+      ANTLR_INPUT->newSort(name); }
   ;
   
 /**
@@ -327,7 +334,7 @@ sortSymbol returns [CVC4::Type* t]
   std::string name;
 }
   : sortName[name,CHECK_NONE] 
-  	{ $t = SMT_INPUT->getSort(name); }
+  	{ $t = ANTLR_INPUT->getSort(name); }
   ;
 
 /**
@@ -360,7 +367,7 @@ identifier[std::string& id,
       Debug("parser") << "identifier: " << id
                       << " check? " << toString(check)
                       << " type? " << toString(type) << std::endl;
-      SMT_INPUT->checkDeclaration(id, check, type); }
+      ANTLR_INPUT->checkDeclaration(id, check, type); }
   ;
 
 /**
@@ -374,7 +381,7 @@ var_identifier[std::string& id,
     { id = AntlrInput::tokenText($VAR_IDENTIFIER);
       Debug("parser") << "var_identifier: " << id
                       << " check? " << toString(check) << std::endl;
-      SMT_INPUT->checkDeclaration(id, check, SYM_VARIABLE); }
+      ANTLR_INPUT->checkDeclaration(id, check, SYM_VARIABLE); }
   ;
 
 /**
@@ -388,7 +395,7 @@ fun_identifier[std::string& id,
     { id = AntlrInput::tokenText($FUN_IDENTIFIER);
       Debug("parser") << "fun_identifier: " << id
                       << " check? " << toString(check) << std::endl;
-      SMT_INPUT->checkDeclaration(id, check, SYM_FUNCTION); }
+      ANTLR_INPUT->checkDeclaration(id, check, SYM_FUNCTION); }
   ;