diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-27 22:04:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-27 22:04:38 +0000 |
commit | ad0a71e2782bc291ba9f808d24df2e1d8ca1b41e (patch) | |
tree | 744a9ae0f10f6dd8837d7e0dcd8bd2b25d34e481 /src/parser/smt1 | |
parent | 51daaee8eb1ee55ee3323c5395a95fd121fe87a8 (diff) |
* Rename SMT parts (printer, parser) to SMT1
* Change --lang smt to mean SMT-LIBv2
* --lang smt1 now means SMT-LIBv1
* SMT-LIBv2 parser now gives helpful error if input looks like v1
* SMT-LIBv1 parser now gives helpful error if input looks like v2
* CVC presentation language parser now gives helpful error if input
looks like either SMT-LIB v1 or v2
* Other associated changes
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/parser/smt1')
-rw-r--r-- | src/parser/smt1/Makefile | 4 | ||||
-rw-r--r-- | src/parser/smt1/Makefile.am | 65 | ||||
-rw-r--r-- | src/parser/smt1/Smt1.g | 817 | ||||
-rw-r--r-- | src/parser/smt1/smt1.cpp | 328 | ||||
-rw-r--r-- | src/parser/smt1/smt1.h | 125 | ||||
-rw-r--r-- | src/parser/smt1/smt1_input.cpp | 73 | ||||
-rw-r--r-- | src/parser/smt1/smt1_input.h | 96 |
7 files changed, 1508 insertions, 0 deletions
diff --git a/src/parser/smt1/Makefile b/src/parser/smt1/Makefile new file mode 100644 index 000000000..7e97ed357 --- /dev/null +++ b/src/parser/smt1/Makefile @@ -0,0 +1,4 @@ +topdir = ../../.. +srcdir = src/parser/smt + +include $(topdir)/Makefile.subdir diff --git a/src/parser/smt1/Makefile.am b/src/parser/smt1/Makefile.am new file mode 100644 index 000000000..34b979ef9 --- /dev/null +++ b/src/parser/smt1/Makefile.am @@ -0,0 +1,65 @@ +AM_CPPFLAGS = \ + -D__BUILDING_CVC4PARSERLIB \ + -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. $(ANTLR_INCLUDES) +AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -Wno-unused-function -Wno-unused-variable + +# Compile generated C files using C++ compiler +AM_CFLAGS = $(AM_CXXFLAGS) +CC=$(CXX) + +ANTLR_OPTS = + +# hide this included makefile from automake +@mk_include@ @srcdir@/../Makefile.antlr_tracing + +noinst_LTLIBRARIES = libparsersmt1.la + +ANTLR_TOKEN_STUFF = \ + generated/Smt1.tokens +ANTLR_LEXER_STUFF = \ + generated/Smt1Lexer.h \ + generated/Smt1Lexer.c \ + $(ANTLR_TOKEN_STUFF) +ANTLR_PARSER_STUFF = \ + generated/Smt1Parser.h \ + generated/Smt1Parser.c +ANTLR_STUFF = \ + $(ANTLR_LEXER_STUFF) \ + $(ANTLR_PARSER_STUFF) + +libparsersmt1_la_SOURCES = \ + Smt1.g \ + smt1.h \ + smt1.cpp \ + smt1_input.h \ + smt1_input.cpp \ + $(ANTLR_STUFF) + +BUILT_SOURCES = \ + generated/Smt1.tokens \ + generated/Smt1Lexer.h \ + generated/Smt1Lexer.c \ + generated/Smt1Parser.h \ + generated/Smt1Parser.c \ + stamp-generated + +DISTCLEANFILES = $(ANTLR_STUFF) +distclean-local: + -$(AM_V_at)rmdir generated + -$(AM_V_at)rm -f stamp-generated + +stamp-generated: + $(AM_V_at)mkdir -p generated + $(AM_V_at)touch stamp-generated + +# antlr doesn't overwrite output files, it just leaves them. So we have to delete them first. +generated/Smt1Lexer.h: Smt1.g stamp-generated + -$(AM_V_at)rm -f $(ANTLR_STUFF) + @if test -z "$(ANTLR)"; then echo "ERROR: antlr parser generator cannot be found, cannot generate the parser" >&2; exit 1; fi + $(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "generated" "@srcdir@/Smt1.g" + +# These don't actually depend on Smt1Lexer.h, but if we're doing parallel +# make and the lexer needs to be rebuilt, we have to keep the rules +# from running in parallel (since the token files will be deleted & +# recreated) +generated/Smt1Lexer.c generated/Smt1Parser.h generated/Smt1Parser.c $(ANTLR_TOKEN_STUFF): generated/Smt1Lexer.h diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g new file mode 100644 index 000000000..b228fb9ec --- /dev/null +++ b/src/parser/smt1/Smt1.g @@ -0,0 +1,817 @@ +/* ******************* */ +/*! \file Smt1.g + ** \verbatim + ** Original author: cconway + ** Major contributors: dejan, mdeters + ** Minor contributors (to current version): taking + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 <stdint.h> + +#include "expr/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 "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/output.h" +#include "util/rational.h" +#include <vector> + +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 = NULL] + : b = benchmark { $cmd = b; } + | 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 returns [CVC4::Command* cmd = NULL] + : LPAREN_TOK BENCHMARK_TOK IDENTIFIER c = benchAttributes RPAREN_TOK + { $cmd = c; } + | EOF { $cmd = 0; } + ; + +/** + * Matches a sequence of benchmark attributes and returns a pointer to a + * command sequence. + * @return the command sequence + */ +benchAttributes returns [CVC4::CommandSequence* cmd_seq = NULL] +@init { + cmd_seq = new CommandSequence(); +} + : (cmd = benchAttribute { if (cmd) cmd_seq->addCommand(cmd); } )+ + ; + +/** + * Matches a benchmark attribute, such as ':logic', ':formula', and returns + * a corresponding command + * @return a command corresponding to the attribute + */ +benchAttribute returns [CVC4::Command* smt_command = NULL] +@declarations { + std::string name; + BenchmarkStatus b_status; + Expr expr; + Command* c; +} + : LOGIC_TOK identifier[name,CHECK_NONE,SYM_VARIABLE] + { PARSER_STATE->preemptCommand(new SetBenchmarkLogicCommand(name)); + PARSER_STATE->setLogic(name); + smt_command = new EmptyCommand(); + } + | ASSUMPTION_TOK annotatedFormula[expr] + { smt_command = new AssertCommand(expr); } + | FORMULA_TOK annotatedFormula[expr] + { smt_command = new CheckSatCommand(expr); } + | STATUS_TOK status[b_status] + { smt_command = new SetBenchmarkStatusCommand(b_status); } + | EXTRAFUNS_TOK LPAREN_TOK + { smt_command = new CommandSequence(); } + ( functionDeclaration[c] + { ((CommandSequence*) smt_command)->addCommand(c); } + )+ RPAREN_TOK + | EXTRAPREDS_TOK LPAREN_TOK + ( { smt_command = new CommandSequence(); } + predicateDeclaration[c] + { ((CommandSequence*) smt_command)->addCommand(c); } + )+ RPAREN_TOK + | EXTRASORTS_TOK LPAREN_TOK + ( { smt_command = new CommandSequence(); } + sortDeclaration[c] + { ((CommandSequence*) smt_command)->addCommand(c); } + )+ RPAREN_TOK + | NOTES_TOK STRING_LITERAL + { smt_command = 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] RPAREN_TOK + { 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 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); + } + } + + | /* 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] RPAREN_TOK + { args2.push_back( MK_EXPR( kind::BOUND_VAR_LIST, args ) ); + args2.push_back(expr); + expr = MK_EXPR(kind, args2); + 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] RPAREN_TOK + // TODO: check arity + { expr = MK_EXPR(op,args); } + + | /* 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); } + RPAREN_TOK + { expr = MK_EXPR(CVC4::kind::ITE, args); } + + | /* 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] + 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) ); } + // 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::IFF; } + | 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] + { PARSER_STATE->checkFunctionLike(name); + fun = PARSER_STATE->getVariable(name); } + ; + +/** + * Matches an attribute name from the input (:attribute_name). + */ +attribute[std::string& s] + : ATTR_IDENTIFIER + { s = AntlrInput::tokenText($ATTR_IDENTIFIER); } + ; + +functionDeclaration[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 = new DeclareFunctionCommand(name, func, t); + } + ; + +/** + * Matches the declaration of a predicate and declares it + */ +predicateDeclaration[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 = new DeclareFunctionCommand(name, func, t); + } + ; + +sortDeclaration[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 = 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 + */ +annotation[CVC4::Command*& smt_command] +@init { + std::string key; + smt_command = NULL; +} + : attribute[key] + ( USER_VALUE + { std::string value = AntlrInput::tokenText($USER_VALUE); + Assert(*value.begin() == '{'); + Assert(*value.rbegin() == '}'); + // trim whitespace + value.erase(value.begin(), value.begin() + 1); + value.erase(value.begin(), std::find_if(value.begin(), value.end(), std::not1(std::ptr_fun<int, int>(std::isspace)))); + value.erase(value.end() - 1); + value.erase(std::find_if(value.rbegin(), value.rend(), std::not1(std::ptr_fun<int, int>(std::isspace))).base(), value.end()); + smt_command = new SetInfoCommand(key.c_str() + 1, value); } + )? + { if(smt_command == NULL) { + smt_command = new EmptyCommand(std::string("annotation: ") + 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 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. + */ +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 new file mode 100644 index 000000000..c91743226 --- /dev/null +++ b/src/parser/smt1/smt1.cpp @@ -0,0 +1,328 @@ +/********************* */ +/*! \file smt1.cpp + ** \verbatim + ** Original author: cconway + ** Major contributors: mdeters + ** Minor contributors (to current version): dejan + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** Definitions of SMT-LIB (v1) constants. + **/ + +#include <ext/hash_map> +namespace std { + using namespace __gnu_cxx; +} + +#include "expr/type.h" +#include "expr/command.h" +#include "parser/parser.h" +#include "parser/smt1/smt1.h" + +namespace CVC4 { +namespace parser { + +std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> Smt1::newLogicMap() { + std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> 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_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["UFNIA"] = UFNIA; + logicMap["UFNIRA"] = UFNIRA; + logicMap["UFLRA"] = UFLRA; + logicMap["QF_ALL_SUPPORTED"] = QF_ALL_SUPPORTED; + logicMap["ALL_SUPPORTED"] = ALL_SUPPORTED; + return logicMap; +} + +Smt1::Logic Smt1::toLogic(const std::string& name) { + static std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> logicMap = newLogicMap(); + return logicMap[name]; +} + +Smt1::Smt1(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) : + Parser(exprManager,input,strictMode,parseOnly), + d_logicSet(false) { + + // Boolean symbols are always defined + addOperator(kind::AND); + addOperator(kind::EQUAL); + addOperator(kind::IFF); + 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: { + Unimplemented("Cannot yet handle SMT-LIBv1 bitvector arrays (i.e., the BitVector_ArraysEx theory)"); + //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: + Unhandled(theory); + } +} + +bool Smt1::logicIsSet() { + return d_logicSet; +} + +void Smt1::setLogic(const std::string& name) { + d_logicSet = true; + d_logic = toLogic(name); + + switch(d_logic) { + 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 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: + addTheory(THEORY_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_ARRAYS_EX); + addTheory(THEORY_BITVECTORS); + break; + + case QF_AUFBVLIA: + addOperator(kind::APPLY_UF); + addTheory(THEORY_ARRAYS_EX); + addTheory(THEORY_BITVECTORS); + addTheory(THEORY_INTS); + break; + + case QF_AUFBVLRA: + addOperator(kind::APPLY_UF); + addTheory(THEORY_ARRAYS_EX); + addTheory(THEORY_BITVECTORS); + addTheory(THEORY_REALS); + break; + + case QF_AUFLIA: + addTheory(THEORY_INT_ARRAYS_EX); + addOperator(kind::APPLY_UF); + addTheory(THEORY_INTS); + break; + + case QF_AUFLIRA: + addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX); + addOperator(kind::APPLY_UF); + addTheory(THEORY_INTS); + addTheory(THEORY_REALS); + break; + + case ALL_SUPPORTED: + addTheory(THEORY_QUANTIFIERS); + /* fall through */ + case QF_ALL_SUPPORTED: + 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 new file mode 100644 index 000000000..f6c99da04 --- /dev/null +++ b/src/parser/smt1/smt1.h @@ -0,0 +1,125 @@ +/********************* */ +/*! \file smt1.h + ** \verbatim + ** Original author: cconway + ** Major contributors: mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 <ext/hash_map> +namespace std { using namespace __gnu_cxx; } + +#include "util/hash.h" +#include "parser/parser.h" + +namespace CVC4 { + +class SExpr; + +namespace parser { + +class Smt1 : public Parser { + friend class ParserBuilder; + +public: + enum Logic { + 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_SAT, + QF_UF, + QF_UFIDL, + QF_UFBV, + QF_UFLIA, + QF_UFNIA, // nonstandard + QF_UFLRA, + QF_UFLIRA, // nonstandard + QF_UFNIRA, // nonstandard + QF_UFNRA, + 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_QUANTIFIERS + }; + +private: + bool d_logicSet; + Logic d_logic; + +protected: + Smt1(ExprManager* exprManager, 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(); + + /** + * 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::hash_map<const std::string, Logic, CVC4::StringHashFunction> 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 new file mode 100644 index 000000000..4987cd793 --- /dev/null +++ b/src/parser/smt1/smt1_input.cpp @@ -0,0 +1,73 @@ +/********************* */ +/*! \file smt1_input.cpp + ** \verbatim + ** Original author: cconway + ** Major contributors: mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 <antlr3.h> + +#include "parser/smt1/smt1_input.h" +#include "expr/expr_manager.h" +#include "parser/input.h" +#include "parser/parser.h" +#include "parser/parser_exception.h" +#include "parser/smt1/generated/Smt1Lexer.h" +#include "parser/smt1/generated/Smt1Parser.h" + +namespace CVC4 { +namespace parser { + +/* Use lookahead=2 */ +Smt1Input::Smt1Input(AntlrInputStream& inputStream) : + AntlrInput(inputStream, 2) { + pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); + AlwaysAssert( 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(); + AlwaysAssert( 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() + throw (ParserException, TypeCheckingException, AssertionException) { + return d_pSmt1Parser->parseCommand(d_pSmt1Parser); +} + +Expr Smt1Input::parseExpr() + throw (ParserException, TypeCheckingException, AssertionException) { + 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 new file mode 100644 index 000000000..77d6f4b50 --- /dev/null +++ b/src/parser/smt1/smt1_input.h @@ -0,0 +1,96 @@ +/********************* */ +/*! \file smt_input.h + ** \verbatim + ** Original author: cconway + ** Major contributors: mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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/generated/Smt1Lexer.h" +#include "parser/smt1/generated/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(); + + /** Get the language that this Input is reading. */ + InputLanguage getLanguage() const throw() { + return language::input::LANG_SMTLIB_V1; + } + +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() + throw(ParserException, TypeCheckingException, AssertionException); + + /** + * 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() + throw(ParserException, TypeCheckingException, AssertionException); + +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 */ |