diff options
Diffstat (limited to 'src/parser/smt1')
-rw-r--r-- | src/parser/smt1/Smt1.g | 893 | ||||
-rw-r--r-- | src/parser/smt1/smt1.cpp | 336 | ||||
-rw-r--r-- | src/parser/smt1/smt1.h | 133 | ||||
-rw-r--r-- | src/parser/smt1/smt1_input.cpp | 70 | ||||
-rw-r--r-- | src/parser/smt1/smt1_input.h | 85 |
5 files changed, 0 insertions, 1517 deletions
diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g deleted file mode 100644 index ca67ec592..000000000 --- a/src/parser/smt1/Smt1.g +++ /dev/null @@ -1,893 +0,0 @@ -/* ******************* */ -/*! \file Smt1.g - ** \verbatim - ** Top contributors (to current version): - ** Christopher L. Conway, Morgan Deters, Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Parser for SMT-LIB input language. - ** - ** Parser for SMT-LIB input language. - **/ - -grammar Smt1; - -options { - // C output for antlr - language = 'C'; - - // Skip the default error handling, just break with exceptions - // defaultErrorHandler = false; - - // Only lookahead of <= k requested (disable for LL* parsing) - // Note that CVC4's BoundedTokenBuffer requires a fixed k ! - // If you change this k, change it also in smt1_input.cpp ! - k = 2; -}/* options */ - -@header { -/** - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information. - **/ -}/* @header */ - -@lexer::includes { - -/** This suppresses warnings about the redefinition of token symbols between - * different parsers. The redefinitions should be harmless as long as no - * client: (a) #include's the lexer headers for two grammars AND (b) uses the - * token symbol definitions. - */ -#pragma GCC system_header - -#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK) -/* This improves performance by ~10 percent on big inputs. - * This option is only valid if we know the input is ASCII (or some 8-bit encoding). - * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16. - * Otherwise, we have to let the lexer detect the encoding at runtime. - */ -# define ANTLR3_INLINE_INPUT_ASCII -# define ANTLR3_INLINE_INPUT_8BIT -#endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ - -#include "parser/antlr_tracing.h" -}/* @lexer::includes */ - -@parser::includes { - -#include <algorithm> -#include <memory> -#include <stdint.h> - -#include "smt/command.h" -#include "parser/parser.h" -#include "parser/antlr_tracing.h" - -namespace CVC4 { - class Expr; - - namespace parser { - namespace smt1 { - /** - * Just exists to provide the uintptr_t constructor that ANTLR - * requires. - */ - struct myExpr : public CVC4::Expr { - myExpr() : CVC4::Expr() {} - myExpr(void*) : CVC4::Expr() {} - myExpr(const Expr& e) : CVC4::Expr(e) {} - myExpr(const myExpr& e) : CVC4::Expr(e) {} - };/* struct myExpr */ - - /** - * Just exists to provide the uintptr_t constructor that ANTLR - * requires. - */ - struct myType : public CVC4::Type { - myType() : CVC4::Type() {} - myType(void*) : CVC4::Type() {} - myType(const Type& t) : CVC4::Type(t) {} - myType(const myType& t) : CVC4::Type(t) {} - };/* struct myType */ - }/* CVC4::parser::smt1 namespace */ - }/* CVC4::parser namespace */ -}/* CVC4 namespace */ - -}/* @parser::includes */ - -@parser::postinclude { - -#include <vector> - -#include "base/output.h" -#include "expr/expr.h" -#include "expr/kind.h" -#include "expr/type.h" -#include "parser/antlr_input.h" -#include "parser/parser.h" -#include "parser/smt1/smt1.h" -#include "util/integer.h" -#include "util/rational.h" - -using namespace CVC4; -using namespace CVC4::parser; - -/* 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 PARSER_STATE -#define PARSER_STATE ((Smt1*)PARSER->super) -#undef EXPR_MANAGER -#define EXPR_MANAGER PARSER_STATE->getExprManager() -#undef MK_EXPR -#define MK_EXPR EXPR_MANAGER->mkExpr -#undef MK_CONST -#define MK_CONST EXPR_MANAGER->mkConst - -}/* @parser::postinclude */ - - -/** - * Parses an expression. - * @return the parsed expression - */ -parseExpr returns [CVC4::parser::smt1::myExpr expr] - : annotatedFormula[expr] - | EOF - ; - -/** - * Parses a command (the whole benchmark) - * @return the command of the benchmark - */ -parseCommand returns [CVC4::Command* cmd_return = NULL] -@declarations { - std::unique_ptr<CVC4::Command> cmd; -} -@after { - cmd_return = cmd.release(); -} - : b = benchmark[&cmd] - | LPAREN_TOK c=IDENTIFIER - { std::string s = AntlrInput::tokenText($c); - if(s == "set" || s == "get") { - PARSER_STATE->parseError(std::string("In SMT-LIBv1 mode, expected keyword `benchmark', but it looks like you're writing SMT-LIBv2. Use --lang smt for SMT-LIBv2.")); - } else { - PARSER_STATE->parseError(std::string("expected keyword `benchmark', got `" + s + "'")); - } - } - ; - -/** - * Matches the whole SMT-LIB benchmark. - * @return the sequence command containing the whole problem - */ -benchmark [std::unique_ptr<CVC4::Command>* cmd] - : LPAREN_TOK BENCHMARK_TOK IDENTIFIER benchAttributes[cmd] RPAREN_TOK - | EOF - ; - -/** - * Matches a sequence of benchmark attributes and returns a pointer to a - * command sequence. - * @return the command sequence - */ -benchAttributes [std::unique_ptr<CVC4::Command>* cmd] -@init { - std::unique_ptr<CVC4::CommandSequence> cmd_seq(new CommandSequence()); - std::unique_ptr<CVC4::Command> attribute; -} -@after { - cmd->reset(cmd_seq.release()); -} - : (benchAttribute[&attribute] - { if (attribute) cmd_seq->addCommand(attribute.release()); } - )+ - ; - -/** - * Matches a benchmark attribute, such as ':logic', ':formula', and returns - * a corresponding command - * @return a command corresponding to the attribute - */ -benchAttribute [std::unique_ptr<CVC4::Command>* smt_command] -@declarations { - std::string name; - BenchmarkStatus b_status; - Expr expr; - std::unique_ptr<CVC4::CommandSequence> command_seq; - std::unique_ptr<CVC4::Command> declaration_command; -} - : LOGIC_TOK identifier[name,CHECK_NONE,SYM_VARIABLE] - { PARSER_STATE->preemptCommand(new SetBenchmarkLogicCommand(name)); - PARSER_STATE->setLogic(name); - smt_command->reset(new EmptyCommand()); - } - | ASSUMPTION_TOK annotatedFormula[expr] - { smt_command->reset(new AssertCommand(expr)); } - | FORMULA_TOK annotatedFormula[expr] - { smt_command->reset(new CheckSatCommand(expr)); } - | STATUS_TOK status[b_status] - { smt_command->reset(new SetBenchmarkStatusCommand(b_status)); } - | EXTRAFUNS_TOK LPAREN_TOK - { command_seq.reset(new CommandSequence()); } - ( functionDeclaration[&declaration_command] - { command_seq->addCommand(declaration_command.release()); } - )+ RPAREN_TOK - { smt_command->reset(command_seq.release()); } - | EXTRAPREDS_TOK LPAREN_TOK - { command_seq.reset(new CommandSequence()); } - ( predicateDeclaration[&declaration_command] - { command_seq->addCommand(declaration_command.release()); } - )+ RPAREN_TOK - { smt_command->reset(command_seq.release()); } - | EXTRASORTS_TOK LPAREN_TOK - { command_seq.reset(new CommandSequence()); } - ( sortDeclaration[&declaration_command] - { command_seq->addCommand(declaration_command.release()); } - )+ RPAREN_TOK - { smt_command->reset(command_seq.release()); } - | NOTES_TOK STRING_LITERAL - { smt_command->reset( - new CommentCommand(AntlrInput::tokenText($STRING_LITERAL))); } - | annotation[smt_command] - ; - -/** - * Matches an annotated formula. - * @return the expression representing the formula - */ -annotatedFormula[CVC4::Expr& expr] -@init { - Debug("parser") << "annotated formula: " << AntlrInput::tokenText(LT(1)) << std::endl; - Kind kind; - std::string name; - std::vector<Expr> args; /* = getExprVector(); */ - std::vector<Expr> args2; - Expr op; /* Operator expression FIXME: move away kill it */ -} - : /* a built-in operator application */ - LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr] - { 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 be the only argument. */ - assert( expr == args[0] ); - } else if( CVC4::kind::isAssociative(kind) && - args.size() > EXPR_MANAGER->maxArity(kind) ) { - /* Special treatment for associative operators with lots of children */ - expr = EXPR_MANAGER->mkAssociative(kind,args); - } else if(!PARSER_STATE->strictModeEnabled() && - kind == CVC4::kind::MINUS && args.size() == 1) { - /* Special fix-up for unary minus improperly used in some benchmarks */ - expr = MK_EXPR(CVC4::kind::UMINUS, args[0]); - } else { - PARSER_STATE->checkArity(kind, args.size()); - expr = MK_EXPR(kind, args); - } - } - termAnnotation[expr]* RPAREN_TOK - - | /* A quantifier */ - LPAREN_TOK - ( FORALL_TOK { kind = kind::FORALL; } | EXISTS_TOK { kind = kind::EXISTS; } ) - { PARSER_STATE->pushScope(); } - ( LPAREN_TOK let_identifier[name,CHECK_NONE] t=sortSymbol RPAREN_TOK - { args.push_back(PARSER_STATE->mkBoundVar(name, t)); } - )+ - annotatedFormula[expr] - { args2.push_back( MK_EXPR( kind::BOUND_VAR_LIST, args ) ); - args2.push_back(expr); - expr = MK_EXPR(kind, args2); - } - termAnnotation[expr]* RPAREN_TOK - { PARSER_STATE->popScope(); } - - | /* A non-built-in function application */ - - // Semantic predicate not necessary if parenthesized subexpressions - // are disallowed - // { isFunction(LT(2)->getText()) }? - LPAREN_TOK - parameterizedOperator[op] - annotatedFormulas[args,expr] - // TODO: check arity - { expr = MK_EXPR(op,args); } - termAnnotation[expr]* RPAREN_TOK - - | /* An ite expression */ - LPAREN_TOK ITE_TOK - annotatedFormula[expr] - { args.push_back(expr); } - annotatedFormula[expr] - { args.push_back(expr); } - annotatedFormula[expr] - { args.push_back(expr); - expr = MK_EXPR(CVC4::kind::ITE, args); } - termAnnotation[expr]* RPAREN_TOK - - | /* a let/flet binding */ - LPAREN_TOK - ( LET_TOK LPAREN_TOK let_identifier[name,CHECK_UNDECLARED] - | FLET_TOK LPAREN_TOK flet_identifier[name,CHECK_UNDECLARED] ) - annotatedFormula[expr] RPAREN_TOK - { PARSER_STATE->pushScope(); - PARSER_STATE->defineVar(name,expr); } - annotatedFormula[expr] - termAnnotation[expr]* RPAREN_TOK - { PARSER_STATE->popScope(); } - - /* constants */ - | TRUE_TOK { expr = MK_CONST(bool(true)); } - | FALSE_TOK { expr = MK_CONST(bool(false)); } - | NUMERAL_TOK - { expr = MK_CONST( AntlrInput::tokenToInteger($NUMERAL_TOK) ); } - | RATIONAL_TOK - { // FIXME: This doesn't work because an SMT rational is not a - // valid GMP rational string - expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL_TOK) ); } - | n = BITVECTOR_BV_CONST '[' size = NUMERAL_TOK ']' - { expr = MK_CONST( AntlrInput::tokenToBitvector($n, $size) ); } - | n = BITVECTOR1_BV_CONST - { unsigned int bit = AntlrInput::tokenText($n)[3] - '0'; - expr = MK_CONST( BitVector(1, bit) ); - } - // NOTE: Theory constants go here - /* TODO: quantifiers, arithmetic constants */ - - | /* a variable */ - ( identifier[name,CHECK_DECLARED,SYM_VARIABLE] - | let_identifier[name,CHECK_DECLARED] - | flet_identifier[name,CHECK_DECLARED] ) - { expr = PARSER_STATE->getVariable(name); } - ; - -/** - * Matches a sequence of annotated formulas and puts them into the - * formulas vector. - * @param formulas the vector to fill with formulas - * @param expr an Expr reference for the elements of the sequence - */ -/* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every - * time through this rule. */ -annotatedFormulas[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr] - : ( annotatedFormula[expr] { formulas.push_back(expr); } )+ - ; - -/** -* Matches a builtin operator symbol and sets kind to its associated Expr kind. -*/ -builtinOp[CVC4::Kind& kind] -@init { - Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl; -} - : NOT_TOK { $kind = CVC4::kind::NOT; } - | IMPLIES_TOK { $kind = CVC4::kind::IMPLIES; } - | AND_TOK { $kind = CVC4::kind::AND; } - | OR_TOK { $kind = CVC4::kind::OR; } - | XOR_TOK { $kind = CVC4::kind::XOR; } - | IFF_TOK { $kind = CVC4::kind::EQUAL; } - | EQUAL_TOK { $kind = CVC4::kind::EQUAL; } - | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; } - // Arithmetic - | GREATER_THAN_TOK - { $kind = CVC4::kind::GT; } - | GREATER_THAN_TOK EQUAL_TOK - { $kind = CVC4::kind::GEQ; } - | LESS_THAN_TOK EQUAL_TOK - { $kind = CVC4::kind::LEQ; } - | LESS_THAN_TOK - { $kind = CVC4::kind::LT; } - | PLUS_TOK { $kind = CVC4::kind::PLUS; } - | STAR_TOK { $kind = CVC4::kind::MULT; } - | TILDE_TOK { $kind = CVC4::kind::UMINUS; } - | MINUS_TOK { $kind = CVC4::kind::MINUS; } - | DIV_TOK { $kind = CVC4::kind::DIVISION; } - // Bit-vectors - | CONCAT_TOK { $kind = CVC4::kind::BITVECTOR_CONCAT; } - | BVAND_TOK { $kind = CVC4::kind::BITVECTOR_AND; } - | BVOR_TOK { $kind = CVC4::kind::BITVECTOR_OR; } - | BVXOR_TOK { $kind = CVC4::kind::BITVECTOR_XOR; } - | BVNOT_TOK { $kind = CVC4::kind::BITVECTOR_NOT; } - | BVNAND_TOK { $kind = CVC4::kind::BITVECTOR_NAND; } - | BVNOR_TOK { $kind = CVC4::kind::BITVECTOR_NOR; } - | BVXNOR_TOK { $kind = CVC4::kind::BITVECTOR_XNOR; } - | BVCOMP_TOK { $kind = CVC4::kind::BITVECTOR_COMP; } - | BVMUL_TOK { $kind = CVC4::kind::BITVECTOR_MULT; } - | BVADD_TOK { $kind = CVC4::kind::BITVECTOR_PLUS; } - | BVSUB_TOK { $kind = CVC4::kind::BITVECTOR_SUB; } - | BVNEG_TOK { $kind = CVC4::kind::BITVECTOR_NEG; } - | BVUDIV_TOK { $kind = CVC4::kind::BITVECTOR_UDIV; } - | BVUREM_TOK { $kind = CVC4::kind::BITVECTOR_UREM; } - | BVSDIV_TOK { $kind = CVC4::kind::BITVECTOR_SDIV; } - | BVSREM_TOK { $kind = CVC4::kind::BITVECTOR_SREM; } - | BVSMOD_TOK { $kind = CVC4::kind::BITVECTOR_SMOD; } - | BVSHL_TOK { $kind = CVC4::kind::BITVECTOR_SHL; } - | BVLSHR_TOK { $kind = CVC4::kind::BITVECTOR_LSHR; } - | BVASHR_TOK { $kind = CVC4::kind::BITVECTOR_ASHR; } - | BVULT_TOK { $kind = CVC4::kind::BITVECTOR_ULT; } - | BVULE_TOK { $kind = CVC4::kind::BITVECTOR_ULE; } - | BVUGT_TOK { $kind = CVC4::kind::BITVECTOR_UGT; } - | BVUGE_TOK { $kind = CVC4::kind::BITVECTOR_UGE; } - | BVSLT_TOK { $kind = CVC4::kind::BITVECTOR_SLT; } - | BVSLE_TOK { $kind = CVC4::kind::BITVECTOR_SLE; } - | BVSGT_TOK { $kind = CVC4::kind::BITVECTOR_SGT; } - | BVSGE_TOK { $kind = CVC4::kind::BITVECTOR_SGE; } - // arrays - | SELECT_TOK { $kind = CVC4::kind::SELECT; } - | STORE_TOK { $kind = CVC4::kind::STORE; } - // NOTE: Theory operators go here - ; - -/** - * Matches an operator. - */ -parameterizedOperator[CVC4::Expr& op] - : functionSymbol[op] - | bitVectorOperator[op] - ; - -/** - * Matches a bit-vector operator (the ones parametrized by numbers) - */ -bitVectorOperator[CVC4::Expr& op] - : EXTRACT_TOK '[' n1 = NUMERAL_TOK ':' n2 = NUMERAL_TOK ']' - { op = MK_CONST(BitVectorExtract(AntlrInput::tokenToUnsigned($n1), AntlrInput::tokenToUnsigned($n2))); } - | REPEAT_TOK '[' n = NUMERAL_TOK ']' - { op = MK_CONST(BitVectorRepeat(AntlrInput::tokenToUnsigned($n))); } - | ZERO_EXTEND_TOK '[' n = NUMERAL_TOK ']' - { op = MK_CONST(BitVectorZeroExtend(AntlrInput::tokenToUnsigned($n))); } - | SIGN_EXTEND_TOK '[' n = NUMERAL_TOK ']' - { op = MK_CONST(BitVectorSignExtend(AntlrInput::tokenToUnsigned($n))); } - | ROTATE_LEFT_TOK '[' n = NUMERAL_TOK ']' - { op = MK_CONST(BitVectorRotateLeft(AntlrInput::tokenToUnsigned($n))); } - | ROTATE_RIGHT_TOK '[' n = NUMERAL_TOK ']' - { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); } - ; - -/** - * Matches a (possibly undeclared) predicate identifier (returning the string). - * @param check what kind of check to do with the symbol - */ -predicateName[std::string& name, CVC4::parser::DeclarationCheck check] - : functionName[name,check] - ; - -/** - * Matches a (possibly undeclared) function identifier (returning the string) - * @param check what kind of check to do with the symbol - */ -functionName[std::string& name, CVC4::parser::DeclarationCheck check] - : identifier[name,check,SYM_VARIABLE] - ; - -/** - * Matches an previously declared function symbol (returning an Expr) - */ -functionSymbol[CVC4::Expr& fun] -@declarations { - std::string name; -} - : functionName[name,CHECK_DECLARED] - { fun = PARSER_STATE->getVariable(name); - PARSER_STATE->checkFunctionLike(fun); } - ; - -/** - * Matches an attribute name from the input (:attribute_name). - */ -attribute[std::string& s] - : ATTR_IDENTIFIER - { s = AntlrInput::tokenText($ATTR_IDENTIFIER); } - ; - -functionDeclaration[std::unique_ptr<CVC4::Command>* smt_command] -@declarations { - std::string name; - std::vector<Type> sorts; -} - : LPAREN_TOK functionName[name,CHECK_UNDECLARED] - t = sortSymbol // require at least one sort - { sorts.push_back(t); } - sortList[sorts] RPAREN_TOK - { if( sorts.size() == 1 ) { - assert( t == sorts[0] ); - } else { - t = EXPR_MANAGER->mkFunctionType(sorts); - } - Expr func = PARSER_STATE->mkVar(name, t); - smt_command->reset(new DeclareFunctionCommand(name, func, t)); - } - ; - -/** - * Matches the declaration of a predicate and declares it - */ -predicateDeclaration[std::unique_ptr<CVC4::Command>* smt_command] -@declarations { - std::string name; - std::vector<Type> p_sorts; -} - : LPAREN_TOK predicateName[name,CHECK_UNDECLARED] sortList[p_sorts] RPAREN_TOK - { Type t; - if( p_sorts.empty() ) { - t = EXPR_MANAGER->booleanType(); - } else { - t = EXPR_MANAGER->mkPredicateType(p_sorts); - } - Expr func = PARSER_STATE->mkVar(name, t); - smt_command->reset(new DeclareFunctionCommand(name, func, t)); - } - ; - -sortDeclaration[std::unique_ptr<CVC4::Command>* smt_command] -@declarations { - std::string name; -} - : sortName[name,CHECK_UNDECLARED] - { Debug("parser") << "sort decl: '" << name << "'" << std::endl; - Type type = PARSER_STATE->mkSort(name); - smt_command->reset(new DeclareTypeCommand(name, 0, type)); - } - ; - -/** - * Matches a sequence of sort symbols and fills them into the given vector. - */ -sortList[std::vector<CVC4::Type>& sorts] - : ( t = sortSymbol { sorts.push_back(t); })* - ; - -/** - * Matches the sort symbol, which can be an arbitrary identifier. - * @param check the check to perform on the name - */ -sortName[std::string& name, CVC4::parser::DeclarationCheck check] - : identifier[name,check,SYM_SORT] - ; - -sortSymbol returns [CVC4::parser::smt1::myType t] -@declarations { - std::string name; -} - : sortName[name,CHECK_NONE] - { $t = PARSER_STATE->getSort(name); } - | BITVECTOR_TOK '[' NUMERAL_TOK ']' { - $t = EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned($NUMERAL_TOK)); - } - /* attaching 'Array' to '[' allows us to parse regular 'Array' correctly in - * e.g. QF_AX, and also 'Array[m:n]' in e.g. QF_AUFBV */ - | 'Array[' n1=NUMERAL_TOK ':' n2=NUMERAL_TOK ']' { - $t = EXPR_MANAGER->mkArrayType(EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned(n1)), - EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned(n2))); - } - ; - -/** - * Matches the status of the benchmark, one of 'sat', 'unsat' or 'unknown'. - */ -status[ CVC4::BenchmarkStatus& status ] - : SAT_TOK { $status = SMT_SATISFIABLE; } - | UNSAT_TOK { $status = SMT_UNSATISFIABLE; } - | UNKNOWN_TOK { $status = SMT_UNKNOWN; } - ; - -/** - * Matches an annotation, which is an attribute name, with an optional user - * value. - */ -annotation[std::unique_ptr<CVC4::Command>* smt_command] -@init { - std::string key, value; - std::vector<Expr> pats; - Expr pat; -} - : PATTERN_ANNOTATION_BEGIN - { PARSER_STATE->warning(":pat not supported here; ignored"); } - annotatedFormulas[pats,pat] '}' - | attribute[key] - ( userValue[value] - { smt_command->reset( - new SetInfoCommand(key.c_str() + 1, SExpr(value))); } - | { smt_command->reset( - new EmptyCommand(std::string("annotation: ") + key)); } - ) - ; - -/** - * Matches an annotation, which is an attribute name, with an optional user - * value. - */ -termAnnotation[CVC4::Expr& expr] -@init { - std::string key, value; - std::vector<Expr> pats; - Expr pat; -} - : PATTERN_ANNOTATION_BEGIN annotatedFormulas[pats,pat] '}' - { if(expr.getKind() == kind::FORALL || expr.getKind() == kind::EXISTS) { - pat = MK_EXPR(kind::INST_PATTERN, pats); - if(expr.getNumChildren() == 3) { - // we have other user patterns attached to the quantifier - // already; add this one to the existing list - pats = expr[2].getChildren(); - pats.push_back(pat); - expr = MK_EXPR(expr.getKind(), expr[0], expr[1], MK_EXPR(kind::INST_PATTERN_LIST, pats)); - } else { - // this is the only user pattern for the quantifier - expr = MK_EXPR(expr.getKind(), expr[0], expr[1], MK_EXPR(kind::INST_PATTERN_LIST, pat)); - } - } else { - PARSER_STATE->warning(":pat only supported on quantifiers"); - } - } - | ':pat' - { PARSER_STATE->warning("expected an instantiation pattern after :pat"); } - | attribute[key] userValue[value]? - { PARSER_STATE->attributeNotSupported(key); } - ; - -/** - * Matches an identifier and sets the string reference parameter id. - * @param id string to hold the identifier - * @param check what kinds of check to do on the symbol - * @param type the intended namespace for the identifier - */ -identifier[std::string& id, - CVC4::parser::DeclarationCheck check, - CVC4::parser::SymbolType type] - : IDENTIFIER - { id = AntlrInput::tokenText($IDENTIFIER); - Debug("parser") << "identifier: " << id - << " check? " << check - << " type? " << type << std::endl; - PARSER_STATE->checkDeclaration(id, check, type); } - ; - -/** - * Matches a let-bound identifier and sets the string reference parameter id. - * @param id string to hold the identifier - * @param check what kinds of check to do on the symbol - */ -let_identifier[std::string& id, - CVC4::parser::DeclarationCheck check] - : LET_IDENTIFIER - { id = AntlrInput::tokenText($LET_IDENTIFIER); - Debug("parser") << "let_identifier: " << id - << " check? " << check << std::endl; - PARSER_STATE->checkDeclaration(id, check, SYM_VARIABLE); } - ; - -/** - * Matches an flet-bound identifier and sets the string reference parameter id. - * @param id string to hold the identifier - * @param check what kinds of check to do on the symbol - */ -flet_identifier[std::string& id, - CVC4::parser::DeclarationCheck check] - : FLET_IDENTIFIER - { id = AntlrInput::tokenText($FLET_IDENTIFIER); - Debug("parser") << "flet_identifier: " << id - << " check? " << check << std::endl; - PARSER_STATE->checkDeclaration(id, check); } - ; - -// Base SMT-LIB tokens -ASSUMPTION_TOK : ':assumption'; -BENCHMARK_TOK : 'benchmark'; -EXTRAFUNS_TOK : ':extrafuns'; -EXTRAPREDS_TOK : ':extrapreds'; -EXTRASORTS_TOK : ':extrasorts'; -FALSE_TOK : 'false'; -FLET_TOK : 'flet'; -FORMULA_TOK : ':formula'; -ITE_TOK : 'ite' | 'if_then_else'; -LET_TOK : 'let'; -LOGIC_TOK : ':logic'; -LPAREN_TOK : '('; -NOTES_TOK : ':notes'; -RPAREN_TOK : ')'; -SAT_TOK : 'sat'; -STATUS_TOK : ':status'; -THEORY_TOK : 'theory'; -TRUE_TOK : 'true'; -UNKNOWN_TOK : 'unknown'; -UNSAT_TOK : 'unsat'; - -// operators (NOTE: theory symbols go here) -AMPERSAND_TOK : '&'; -AND_TOK : 'and'; -AT_TOK : '@'; -DISTINCT_TOK : 'distinct'; -DIV_TOK : '/'; -EQUAL_TOK : '='; -EXISTS_TOK : 'exists'; -FORALL_TOK : 'forall'; -GREATER_THAN_TOK : '>'; -IFF_TOK : 'iff'; -IMPLIES_TOK : 'implies'; -LESS_THAN_TOK : '<'; -MINUS_TOK : '-'; -NOT_TOK : 'not'; -OR_TOK : 'or'; -PERCENT_TOK : '%'; -PIPE_TOK : '|'; -PLUS_TOK : '+'; -POUND_TOK : '#'; -SELECT_TOK : 'select'; -STAR_TOK : '*'; -STORE_TOK : 'store'; -TILDE_TOK : '~'; -XOR_TOK : 'xor'; - -// Bitvector tokens -BITVECTOR_TOK : 'BitVec'; -CONCAT_TOK : 'concat'; -EXTRACT_TOK : 'extract'; -BVAND_TOK : 'bvand'; -BVOR_TOK : 'bvor'; -BVXOR_TOK : 'bvxor'; -BVNOT_TOK : 'bvnot'; -BVNAND_TOK : 'bvnand'; -BVNOR_TOK : 'bvnor'; -BVXNOR_TOK : 'bvxnor'; -BVCOMP_TOK : 'bvcomp'; -BVMUL_TOK : 'bvmul'; -BVADD_TOK : 'bvadd'; -BVSUB_TOK : 'bvsub'; -BVNEG_TOK : 'bvneg'; -BVUDIV_TOK : 'bvudiv'; -BVUREM_TOK : 'bvurem'; -BVSDIV_TOK : 'bvsdiv'; -BVSREM_TOK : 'bvsrem'; -BVSMOD_TOK : 'bvsmod'; -BVSHL_TOK : 'bvshl'; -BVLSHR_TOK : 'bvlshr'; -BVASHR_TOK : 'bvashr'; -BVULT_TOK : 'bvult'; -BVULE_TOK : 'bvule'; -BVUGT_TOK : 'bvugt'; -BVUGE_TOK : 'bvuge'; -BVSLT_TOK : 'bvslt'; -BVSLE_TOK : 'bvsle'; -BVSGT_TOK : 'bvsgt'; -BVSGE_TOK : 'bvsge'; -REPEAT_TOK : 'repeat'; -ZERO_EXTEND_TOK : 'zero_extend'; -SIGN_EXTEND_TOK : 'sign_extend'; -ROTATE_LEFT_TOK : 'rotate_left'; -ROTATE_RIGHT_TOK : 'rotate_right'; - -/** - * Matches a bit-vector constant of the form bv123 - */ -BITVECTOR_BV_CONST - : 'bv' DIGIT+ - ; - -/** - * Matches a bit-vector constant of the form bit(0|1) - */ -BITVECTOR1_BV_CONST - : 'bit0' | 'bit1' - ; - - -/** - * Matches an identifier from the input. An identifier is a sequence of letters, - * digits and "_", "'", "." symbols, starting with a letter. - */ -IDENTIFIER - : ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')* - ; - -/** - * Matches an identifier starting with a colon. - */ -ATTR_IDENTIFIER - : ':' IDENTIFIER - ; - -/** - * Matches an identifier starting with a question mark. - */ -LET_IDENTIFIER - : '?' IDENTIFIER - ; - -/** - * Matches an identifier starting with a dollar sign. - */ -FLET_IDENTIFIER - : '$' IDENTIFIER - ; - -/** - * Matches the value of user-defined annotations or attributes. The - * only constraint imposed on a user-defined value is that it start - * with an open brace and end with closed brace. - */ -userValue[std::string& s] - : USER_VALUE - { s = AntlrInput::tokenText($USER_VALUE); - assert(*s.begin() == '{'); - assert(*s.rbegin() == '}'); - // trim whitespace - s.erase(s.begin(), s.begin() + 1); - s.erase(s.begin(), std::find_if(s.begin(), s.end(), std::not1(std::ptr_fun<int, int>(std::isspace)))); - s.erase(s.end() - 1); - s.erase(std::find_if(s.rbegin(), s.rend(), std::not1(std::ptr_fun<int, int>(std::isspace))).base(), s.end()); - } - ; - -PATTERN_ANNOTATION_BEGIN - : ':pat' (' ' | '\t' | '\f' | '\r' | '\n')* '{' - ; - -USER_VALUE - : '{' ('\\{' | '\\}' | ~('{' | '}'))* '}' - ; - -/** - * Matches and skips whitespace in the input. - */ -WHITESPACE - : (' ' | '\t' | '\f' | '\r' | '\n')+ - { SKIP(); } - ; - -/** - * Matches a numeral from the input (non-empty sequence of digits). - */ -NUMERAL_TOK - : DIGIT+ - ; - -RATIONAL_TOK - : DIGIT+ '.' DIGIT+ - ; - -/** - * Matches a double quoted string literal. Escaping is supported, and escape - * character '\' has to be escaped. - */ -STRING_LITERAL - : '"' (ESCAPE | ~('"'|'\\'))* '"' - ; - -/** - * Matches the comments and ignores them - */ -COMMENT - : ';' (~('\n' | '\r'))* - { SKIP(); } - ; - - -/** - * Matches any letter ('a'-'z' and 'A'-'Z'). - */ -fragment -ALPHA - : 'a'..'z' - | 'A'..'Z' - ; - -/** - * Matches the digits (0-9) - */ -fragment DIGIT : '0'..'9'; -// fragment NON_ZERO_DIGIT : '1'..'9'; -// fragment NUMERAL_SEQ : '0' | NON_ZERO_DIGIT DIGIT*; - -/** - * Matches an allowed escaped character. - */ -fragment ESCAPE : '\\' ('"' | '\\' | 'n' | 't' | 'r'); - diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp deleted file mode 100644 index 979880f8b..000000000 --- a/src/parser/smt1/smt1.cpp +++ /dev/null @@ -1,336 +0,0 @@ -/********************* */ -/*! \file smt1.cpp - ** \verbatim - ** Top contributors (to current version): - ** Christopher L. Conway, Morgan Deters, Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** Definitions of SMT-LIB (v1) constants. - **/ - -#include "parser/smt1/smt1.h" - -#include "api/cvc4cpp.h" -#include "expr/type.h" -#include "parser/parser.h" -#include "smt/command.h" - -namespace CVC4 { -namespace parser { - -std::unordered_map<std::string, Smt1::Logic> Smt1::newLogicMap() { - std::unordered_map<std::string, Smt1::Logic> logicMap; - logicMap["AUFLIA"] = AUFLIA; - logicMap["AUFLIRA"] = AUFLIRA; - logicMap["AUFNIRA"] = AUFNIRA; - logicMap["LRA"] = LRA; - logicMap["QF_AX"] = QF_AX; - logicMap["QF_BV"] = QF_BV; - logicMap["QF_IDL"] = QF_IDL; - logicMap["QF_LIA"] = QF_LIA; - logicMap["QF_LRA"] = QF_LRA; - logicMap["QF_NIA"] = QF_NIA; - logicMap["QF_NRA"] = QF_NRA; - logicMap["QF_RDL"] = QF_RDL; - logicMap["QF_S"] = QF_S; - logicMap["QF_SAT"] = QF_SAT; - logicMap["QF_UF"] = QF_UF; - logicMap["QF_UFIDL"] = QF_UFIDL; - logicMap["QF_UFBV"] = QF_UFBV; - logicMap["QF_UFLRA"] = QF_UFLRA; - logicMap["QF_UFLIA"] = QF_UFLIA; - logicMap["QF_UFLIRA"] = QF_UFLIRA; - logicMap["QF_UFNIA"] = QF_UFNIA; - logicMap["QF_UFNIRA"] = QF_UFNIRA; - logicMap["QF_UFNRA"] = QF_UFNRA; - logicMap["QF_ABV"] = QF_ABV; - logicMap["QF_AUFBV"] = QF_AUFBV; - logicMap["QF_AUFBVLIA"] = QF_AUFBVLIA; - logicMap["QF_AUFBVLRA"] = QF_AUFBVLRA; - logicMap["QF_UFNIRA"] = QF_UFNIRA; - logicMap["QF_AUFLIA"] = QF_AUFLIA; - logicMap["QF_AUFLIRA"] = QF_AUFLIRA; - logicMap["SAT"] = SAT; - logicMap["UFNIA"] = UFNIA; - logicMap["UFNIRA"] = UFNIRA; - logicMap["UFLRA"] = UFLRA; - logicMap["QF_ALL_SUPPORTED"] = QF_ALL_SUPPORTED; - logicMap["ALL_SUPPORTED"] = ALL_SUPPORTED; - logicMap["QF_ALL"] = QF_ALL_SUPPORTED; - logicMap["ALL"] = ALL_SUPPORTED; - logicMap["HORN"] = ALL_SUPPORTED; - return logicMap; -} - -Smt1::Logic Smt1::toLogic(const std::string& name) { - static std::unordered_map<std::string, Smt1::Logic> logicMap = newLogicMap(); - return logicMap[name]; -} - -Smt1::Smt1(api::Solver* solver, Input* input, bool strictMode, bool parseOnly) - : Parser(solver, input, strictMode, parseOnly), d_logic(UNSET) -{ - // Boolean symbols are always defined - addOperator(kind::AND); - addOperator(kind::EQUAL); - addOperator(kind::IMPLIES); - addOperator(kind::ITE); - addOperator(kind::NOT); - addOperator(kind::OR); - addOperator(kind::XOR); -} - -void Smt1::addArithmeticOperators() { - addOperator(kind::PLUS); - addOperator(kind::MINUS); - addOperator(kind::UMINUS); - addOperator(kind::MULT); - addOperator(kind::LT); - addOperator(kind::LEQ); - addOperator(kind::GT); - addOperator(kind::GEQ); -} - -void Smt1::addTheory(Theory theory) { - switch(theory) { - case THEORY_ARRAYS: - case THEORY_ARRAYS_EX: { - Type indexType = mkSort("Index"); - Type elementType = mkSort("Element"); - DeclarationSequence* seq = new DeclarationSequence(); - seq->addCommand(new DeclareTypeCommand("Index", 0, indexType)); - seq->addCommand(new DeclareTypeCommand("Element", 0, elementType)); - preemptCommand(seq); - - defineType("Array", getExprManager()->mkArrayType(indexType, elementType)); - - addOperator(kind::SELECT); - addOperator(kind::STORE); - break; - } - - case THEORY_BITVECTOR_ARRAYS_EX: { - // We don't define the "Array" symbol in this case; - // the parser creates the Array[m:n] types on the fly. - addOperator(kind::SELECT); - addOperator(kind::STORE); - break; - } - - case THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX: { - defineType("Array1", getExprManager()->mkArrayType(getSort("Int"), getSort("Real"))); - defineType("Array2", getExprManager()->mkArrayType(getSort("Int"), getSort("Array1"))); - addOperator(kind::SELECT); - addOperator(kind::STORE); - break; - } - - case THEORY_INT_ARRAYS: - case THEORY_INT_ARRAYS_EX: { - defineType("Array", getExprManager()->mkArrayType(getExprManager()->integerType(), getExprManager()->integerType())); - addOperator(kind::SELECT); - addOperator(kind::STORE); - break; - } - - case THEORY_EMPTY: { - Type sort = mkSort("U"); - preemptCommand(new DeclareTypeCommand("U", 0, sort)); - break; - } - - case THEORY_REALS_INTS: - defineType("Real", getExprManager()->realType()); - // falling-through on purpose, to add Ints part of RealsInts - - case THEORY_INTS: - defineType("Int", getExprManager()->integerType()); - addArithmeticOperators(); - break; - - case THEORY_REALS: - defineType("Real", getExprManager()->realType()); - addArithmeticOperators(); - break; - - case THEORY_BITVECTORS: - break; - - case THEORY_QUANTIFIERS: - break; - - default: - std::stringstream ss; - ss << "internal error: unsupported theory " << theory; - throw ParserException(ss.str()); - } -} - -bool Smt1::logicIsSet() { return d_logic != UNSET; } - -void Smt1::setLogic(const std::string& name) { - d_logic = toLogic(logicIsForced() ? getForcedLogic() : name); - - switch(d_logic) { - case UNSET: - throw ParserException("Logic cannot remain UNSET after being set."); - break; - - case QF_S: - throw ParserException( - "Strings theory unsupported in SMT-LIBv1 front-end; try SMT-LIBv2."); - break; - - case QF_AX: - addTheory(THEORY_ARRAYS_EX); - break; - - case QF_IDL: - case QF_LIA: - case QF_NIA: - addTheory(THEORY_INTS); - break; - - case QF_RDL: - case QF_LRA: - case QF_NRA: - addTheory(THEORY_REALS); - break; - - case QF_SAT: - /* no extra symbols needed */ - break; - case SAT: - addTheory(THEORY_QUANTIFIERS); - break; - - case QF_UFIDL: - case QF_UFLIA: - case QF_UFNIA: // nonstandard logic - addTheory(THEORY_INTS); - addOperator(kind::APPLY_UF); - break; - - case QF_UFLRA: - case QF_UFNRA: - addTheory(THEORY_REALS); - addOperator(kind::APPLY_UF); - break; - - case QF_UFLIRA: // nonstandard logic - case QF_UFNIRA: // nonstandard logic - addTheory(THEORY_INTS); - addTheory(THEORY_REALS); - addOperator(kind::APPLY_UF); - break; - - case QF_UF: - addTheory(THEORY_EMPTY); - addOperator(kind::APPLY_UF); - break; - - case QF_BV: - addTheory(THEORY_BITVECTORS); - break; - - case QF_ABV: // nonstandard logic - addTheory(THEORY_BITVECTOR_ARRAYS_EX); - addTheory(THEORY_BITVECTORS); - break; - - case QF_UFBV: - addOperator(kind::APPLY_UF); - addTheory(THEORY_BITVECTORS); - break; - - case QF_AUFBV: - addOperator(kind::APPLY_UF); - addTheory(THEORY_BITVECTOR_ARRAYS_EX); - addTheory(THEORY_BITVECTORS); - break; - - case QF_AUFBVLIA: // nonstandard logic - addOperator(kind::APPLY_UF); - addTheory(THEORY_ARRAYS_EX); - addTheory(THEORY_BITVECTORS); - addTheory(THEORY_INTS); - break; - - case QF_AUFBVLRA: // nonstandard logic - addOperator(kind::APPLY_UF); - addTheory(THEORY_ARRAYS_EX); - addTheory(THEORY_BITVECTORS); - addTheory(THEORY_REALS); - break; - - case QF_AUFLIA: - addTheory(THEORY_INT_ARRAYS_EX); // nonstandard logic - addOperator(kind::APPLY_UF); - addTheory(THEORY_INTS); - break; - - case QF_AUFLIRA: // nonstandard logic - addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX); - addOperator(kind::APPLY_UF); - addTheory(THEORY_INTS); - addTheory(THEORY_REALS); - break; - - case ALL_SUPPORTED: // nonstandard logic - addTheory(THEORY_QUANTIFIERS); - /* fall through */ - case QF_ALL_SUPPORTED: // nonstandard logic - addTheory(THEORY_ARRAYS_EX); - addOperator(kind::APPLY_UF); - addTheory(THEORY_INTS); - addTheory(THEORY_REALS); - addTheory(THEORY_BITVECTORS); - break; - - case AUFLIA: - addOperator(kind::APPLY_UF); - addTheory(THEORY_INTS); - addTheory(THEORY_INT_ARRAYS_EX); - addTheory(THEORY_QUANTIFIERS); - break; - - case AUFLIRA: - case AUFNIRA: - addOperator(kind::APPLY_UF); - addTheory(THEORY_INTS); - addTheory(THEORY_REALS); - addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX); - addTheory(THEORY_QUANTIFIERS); - break; - - case LRA: - addTheory(THEORY_REALS); - addTheory(THEORY_QUANTIFIERS); - break; - - case UFNIA: - addOperator(kind::APPLY_UF); - addTheory(THEORY_INTS); - addTheory(THEORY_QUANTIFIERS); - break; - case UFNIRA: - addOperator(kind::APPLY_UF); - addTheory(THEORY_INTS); - addTheory(THEORY_REALS); - addTheory(THEORY_QUANTIFIERS); - break; - - case UFLRA: - addOperator(kind::APPLY_UF); - addTheory(THEORY_REALS); - addTheory(THEORY_QUANTIFIERS); - break; - } -}/* Smt1::setLogic() */ - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ diff --git a/src/parser/smt1/smt1.h b/src/parser/smt1/smt1.h deleted file mode 100644 index 32867e692..000000000 --- a/src/parser/smt1/smt1.h +++ /dev/null @@ -1,133 +0,0 @@ -/********************* */ -/*! \file smt1.h - ** \verbatim - ** Top contributors (to current version): - ** Christopher L. Conway, Morgan Deters, Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** Definitions of SMT constants. - **/ - -#include "cvc4parser_private.h" - -#ifndef CVC4__PARSER__SMT1_H -#define CVC4__PARSER__SMT1_H - -#include <string> -#include <unordered_map> - -#include "parser/parser.h" - -namespace CVC4 { - -class SExpr; - -namespace api { -class Solver; -} - -namespace parser { - -class Smt1 : public Parser { - friend class ParserBuilder; - -public: - enum Logic { - UNSET = 0, // This indicates that the logic has not been set. - AUFLIA, // +p and -p? - AUFLIRA, - AUFNIRA, - LRA, - QF_ABV, - QF_AUFBV, - QF_AUFBVLIA, - QF_AUFBVLRA, - QF_AUFLIA, - QF_AUFLIRA, - QF_AX, - QF_BV, - QF_IDL, - QF_LIA, - QF_LRA, - QF_NIA, - QF_NRA, - QF_RDL, - QF_S, // nonstandard (for string theory) - QF_SAT, - QF_UF, - QF_UFIDL, - QF_UFBV, - QF_UFLIA, - QF_UFNIA, // nonstandard - QF_UFLRA, - QF_UFLIRA, // nonstandard - QF_UFNIRA, // nonstandard - QF_UFNRA, - SAT, - UFLRA, - UFNIRA, // nonstandard - UFNIA, - QF_ALL_SUPPORTED, // nonstandard - ALL_SUPPORTED // nonstandard - }; - - enum Theory { - THEORY_ARRAYS, - THEORY_ARRAYS_EX, - THEORY_BITVECTORS, - THEORY_BITVECTORS_32, - THEORY_BITVECTOR_ARRAYS_EX, - THEORY_EMPTY, - THEORY_INTS, - THEORY_INT_ARRAYS, - THEORY_INT_ARRAYS_EX, - THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX, - THEORY_REALS, - THEORY_REALS_INTS, - THEORY_STRINGS, - THEORY_QUANTIFIERS, - THEORY_CARDINALITY_CONSTRAINT - }; - -private: - Logic d_logic; - -protected: - Smt1(api::Solver* solver, - Input* input, - bool strictMode = false, - bool parseOnly = false); - -public: - /** - * Add theory symbols to the parser state. - * - * @param theory the theory to open (e.g., Core, Ints) - */ - void addTheory(Theory theory); - - bool logicIsSet() override; - - /** - * Sets the logic for the current benchmark. Declares any logic and theory symbols. - * - * @param name the name of the logic (e.g., QF_UF, AUFLIA) - */ - void setLogic(const std::string& name); - - static Logic toLogic(const std::string& name); - -private: - - void addArithmeticOperators(); - static std::unordered_map<std::string, Logic> newLogicMap(); -};/* class Smt1 */ - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ - -#endif /* CVC4__PARSER__SMT1_H */ diff --git a/src/parser/smt1/smt1_input.cpp b/src/parser/smt1/smt1_input.cpp deleted file mode 100644 index b8f476687..000000000 --- a/src/parser/smt1/smt1_input.cpp +++ /dev/null @@ -1,70 +0,0 @@ -/********************* */ -/*! \file smt1_input.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Christopher L. Conway - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add file-specific comments here ]]. - ** - ** [[ Add file-specific comments here ]] - **/ - -#include "parser/smt1/smt1_input.h" - -#include <antlr3.h> - -#include "expr/expr_manager.h" -#include "parser/input.h" -#include "parser/parser.h" -#include "parser/parser_exception.h" -#include "parser/smt1/Smt1Lexer.h" -#include "parser/smt1/Smt1Parser.h" - -namespace CVC4 { -namespace parser { - -/* Use lookahead=2 */ -Smt1Input::Smt1Input(AntlrInputStream& inputStream) : - AntlrInput(inputStream, 2) { - pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); - assert( input != NULL ); - - d_pSmt1Lexer = Smt1LexerNew(input); - if( d_pSmt1Lexer == NULL ) { - throw ParserException("Failed to create SMT lexer."); - } - - setAntlr3Lexer( d_pSmt1Lexer->pLexer ); - - pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); - assert( tokenStream != NULL ); - - d_pSmt1Parser = Smt1ParserNew(tokenStream); - if( d_pSmt1Parser == NULL ) { - throw ParserException("Failed to create SMT parser."); - } - - setAntlr3Parser(d_pSmt1Parser->pParser); -} - - -Smt1Input::~Smt1Input() { - d_pSmt1Lexer->free(d_pSmt1Lexer); - d_pSmt1Parser->free(d_pSmt1Parser); -} - -Command* Smt1Input::parseCommand() { - return d_pSmt1Parser->parseCommand(d_pSmt1Parser); -} - -Expr Smt1Input::parseExpr() { - return d_pSmt1Parser->parseExpr(d_pSmt1Parser); -} - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ diff --git a/src/parser/smt1/smt1_input.h b/src/parser/smt1/smt1_input.h deleted file mode 100644 index fcdc63ee2..000000000 --- a/src/parser/smt1/smt1_input.h +++ /dev/null @@ -1,85 +0,0 @@ -/********************* */ -/*! \file smt1_input.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Christopher L. Conway, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add file-specific comments here ]]. - ** - ** [[ Add file-specific comments here ]] - **/ - -#include "cvc4parser_private.h" - -#ifndef CVC4__PARSER__SMT1_INPUT_H -#define CVC4__PARSER__SMT1_INPUT_H - -#include "parser/antlr_input.h" -#include "parser/smt1/Smt1Lexer.h" -#include "parser/smt1/Smt1Parser.h" - -// extern void Smt1ParserSetAntlrParser(CVC4::parser::AntlrParser* newAntlrParser); - -namespace CVC4 { - -class Command; -class Expr; -class ExprManager; - -namespace parser { - -class Smt1Input : public AntlrInput { - - /** The ANTLR3 SMT lexer for the input. */ - pSmt1Lexer d_pSmt1Lexer; - - /** The ANTLR3 CVC parser for the input. */ - pSmt1Parser d_pSmt1Parser; - -public: - - /** - * Create an input. - * - * @param inputStream the input stream to use - */ - Smt1Input(AntlrInputStream& inputStream); - - /** Destructor. Frees the lexer and the parser. */ - virtual ~Smt1Input(); - - protected: - /** - * Parse a command from the input. Returns <code>NULL</code> if - * there is no command there to parse. - * - * @throws ParserException if an error is encountered during parsing. - */ - Command* parseCommand() override; - - /** - * Parse an expression from the input. Returns a null - * <code>Expr</code> if there is no expression there to parse. - * - * @throws ParserException if an error is encountered during parsing. - */ - Expr parseExpr() override; - - private: - /** - * Initialize the class. Called from the constructors once the input - * stream is initialized. - */ - void init(); - -};/* class Smt1Input */ - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ - -#endif /* CVC4__PARSER__SMT1_INPUT_H */ |