@parser::includes {
#include "expr/command.h"
+#include "parser/input.h"
namespace CVC4 {
class Expr;
#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
}
/**
: 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]
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); }
;
/**
| /* 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); }
;
/**
CVC4::parser::SymbolType type]
: IDENTIFIER
{ id = AntlrInput::tokenText($IDENTIFIER);
- CVC_INPUT->checkDeclaration(id, check, type); }
+ ANTLR_INPUT->checkDeclaration(id, check, type); }
;
/**
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]
;
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); }
;
/**
: impliesFormula[f]
( IFF_TOK
iffFormula[e]
- { f = CVC_INPUT->mkExpr(CVC4::kind::IFF, f, e); }
+ { f = MK_EXPR(CVC4::kind::IFF, f, e); }
)?
;
}
: orFormula[f]
( IMPLIES_TOK impliesFormula[e]
- { f = CVC_INPUT->mkExpr(CVC4::kind::IMPLIES, f, e); }
+ { f = MK_EXPR(CVC4::kind::IMPLIES, f, e); }
)?
;
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);
}
}
;
}
: andFormula[f]
( XOR_TOK andFormula[e]
- { f = CVC_INPUT->mkExpr(CVC4::kind::XOR,f, e); }
+ { f = MK_EXPR(CVC4::kind::XOR,f, e); }
)*
;
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);
}
}
;
}
: /* 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]
;
}
: 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.
{ 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]
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); }
;
/**
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); }
;
/**
| 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); }
;
/**
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); }
;
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) {
*/
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.
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);
@parser::includes {
#include "expr/command.h"
+#include "parser/input.h"
namespace CVC4 {
class Expr;
#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
}
/**
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); }
}
: /* 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);
}
}
{ 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)
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 */
;
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); }
;
/**
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); }
;
/**
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
}
: sortName[name,CHECK_UNDECLARED]
{ Debug("parser") << "sort decl: '" << name << "'" << std::endl;
- SMT_INPUT->newSort(name); }
+ ANTLR_INPUT->newSort(name); }
;
/**
std::string name;
}
: sortName[name,CHECK_NONE]
- { $t = SMT_INPUT->getSort(name); }
+ { $t = ANTLR_INPUT->getSort(name); }
;
/**
Debug("parser") << "identifier: " << id
<< " check? " << toString(check)
<< " type? " << toString(type) << std::endl;
- SMT_INPUT->checkDeclaration(id, check, type); }
+ ANTLR_INPUT->checkDeclaration(id, check, type); }
;
/**
{ 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); }
;
/**
{ 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); }
;
projects / cvc5.git / commitdiff