From: Christopher L. Conway Date: Tue, 27 Apr 2010 16:54:39 +0000 (+0000) Subject: Adding a bit of documentation to the SMT parser X-Git-Tag: cvc5-1.0.0~9107 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=130b814916c096f4b898a26c9df5056270af78d0;p=cvc5.git Adding a bit of documentation to the SMT parser --- diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp index 57914c9de..827d5fcaa 100644 --- a/src/parser/parser_state.cpp +++ b/src/parser/parser_state.cpp @@ -46,7 +46,6 @@ ParserState::ParserState(ExprManager* exprManager, const std::string& filename, Expr ParserState::getSymbol(const std::string& name, SymbolType type) { Assert( isDeclared(name, type) ); - switch( type ) { case SYM_VARIABLE: // Functions share var namespace @@ -125,15 +124,6 @@ ParserState::undefineVar(const std::string& name) { } */ -void -ParserState::setLogic(const std::string& name) { - if( name == "QF_UF" ) { - mkSort("U"); - } else { - Unhandled(name); - } -} - Type ParserState::mkSort(const std::string& name) { Debug("parser") << "newSort(" << name << ")" << std::endl; diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 15f0c8844..67290ada2 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -77,6 +77,22 @@ using namespace CVC4::parser; #define MK_EXPR EXPR_MANAGER->mkExpr #undef MK_CONST #define MK_CONST EXPR_MANAGER->mkConst + +/** + * Sets the logic for the current benchmark. Declares any logic symbols. + * + * @param parserState pointer to the current parser state + * @param name the name of the logic (e.g., QF_UF, AUFLIA) + */ +void +setLogic(ParserState *parserState, const std::string& name) { + if( name == "QF_UF" ) { + parserState->mkSort("U"); + } else { + // NOTE: Theory types go here + Unhandled(name); + } +} } @@ -131,7 +147,7 @@ benchAttribute returns [CVC4::Command* smt_command] Expr expr; } : LOGIC_TOK identifier[name,CHECK_NONE,SYM_VARIABLE] - { PARSER_STATE->setLogic(name); + { setLogic(PARSER_STATE,name); smt_command = new SetBenchmarkLogicCommand(name); } | ASSUMPTION_TOK annotatedFormula[expr] { smt_command = new AssertCommand(expr); } @@ -183,7 +199,7 @@ annotatedFormula[CVC4::Expr& expr] { expr = MK_EXPR(CVC4::kind::APPLY_UF,args); } | /* An ite expression */ - LPAREN_TOK (ITE_TOK | IF_THEN_ELSE_TOK) + LPAREN_TOK ITE_TOK annotatedFormula[expr] { args.push_back(expr); } annotatedFormula[expr] @@ -213,6 +229,7 @@ annotatedFormula[CVC4::Expr& expr] /* constants */ | TRUE_TOK { expr = MK_CONST(true); } | FALSE_TOK { expr = MK_CONST(false); } + // NOTE: Theory constants go here /* TODO: let, flet, quantifiers, arithmetic constants */ ; @@ -229,8 +246,7 @@ annotatedFormulas[std::vector& formulas, CVC4::Expr& expr] ; /** -* Matches on of the unary Boolean connectives. -* @return the kind of the Bollean connective +* Matches a builtin operator symbol and sets kind to its associated Expr kind. */ builtinOp[CVC4::Kind& kind] @init { @@ -244,6 +260,7 @@ builtinOp[CVC4::Kind& kind] | IFF_TOK { $kind = CVC4::kind::IFF; } | EQUAL_TOK { $kind = CVC4::kind::EQUAL; } | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; } + // NOTE: Theory operators go here /* TODO: lt, gt, plus, minus, etc. */ ; @@ -410,72 +427,65 @@ flet_identifier[std::string& id, PARSER_STATE->checkDeclaration(id, check); } ; - // Base SMT-LIB tokens -DISTINCT_TOK : 'distinct'; -ITE_TOK : 'ite'; -IF_THEN_ELSE_TOK : 'if_then_else'; -TRUE_TOK : 'true'; -FALSE_TOK : 'false'; -NOT_TOK : 'not'; -IMPLIES_TOK : 'implies'; -AND_TOK : 'and'; -OR_TOK : 'or'; -XOR_TOK : 'xor'; -IFF_TOK : 'iff'; -EXISTS_TOK : 'exists'; -FORALL_TOK : 'forall'; -LET_TOK : 'let'; -FLET_TOK : 'flet'; -THEORY_TOK : 'theory'; -SAT_TOK : 'sat'; -UNSAT_TOK : 'unsat'; -UNKNOWN_TOK : 'unknown'; -BENCHMARK_TOK : 'benchmark'; - -// The SMT attribute tokens -LOGIC_TOK : ':logic'; ASSUMPTION_TOK : ':assumption'; -FORMULA_TOK : ':formula'; -STATUS_TOK : ':status'; -EXTRASORTS_TOK : ':extrasorts'; +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'; -// arithmetic symbols -EQUAL_TOK : '='; -LESS_THAN_TOK : '<'; -GREATER_THAN_TOK : '>'; +// operators (NOTE: theory symbols go here) AMPERSAND_TOK : '&'; +AND_TOK : 'and'; AT_TOK : '@'; -POUND_TOK : '#'; -PLUS_TOK : '+'; -MINUS_TOK : '-'; -STAR_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 : '#'; +STAR_TOK : '*'; TILDE_TOK : '~'; +XOR_TOK : 'xor'; -// Language meta-symbols -//QUESTION_TOK : '?'; -//DOLLAR_TOK : '$'; -LPAREN_TOK : '('; -RPAREN_TOK : ')'; /** * Matches an identifier from the input. An identifier is a sequence of letters, * digits and "_", "'", "." symbols, starting with a letter. */ -IDENTIFIER /*options { paraphrase = 'an identifier'; testLiterals = true; }*/ +IDENTIFIER : ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')* ; /** * Matches an identifier starting with a colon. */ -ATTR_IDENTIFIER /*options { paraphrase = 'an identifier starting with a colon'; testLiterals = true; }*/ +ATTR_IDENTIFIER : ':' IDENTIFIER ; @@ -507,14 +517,14 @@ USER_VALUE /** * Matches and skips whitespace in the input. */ -WHITESPACE /*options { paraphrase = 'whitespace'; }*/ +WHITESPACE : (' ' | '\t' | '\f' | '\r' | '\n')+ { $channel = HIDDEN;; } ; /** * Matches a numeral from the input (non-empty sequence of digits). */ -NUMERAL_TOK /*options { paraphrase = 'a numeral'; }*/ +NUMERAL_TOK : (DIGIT)+ ; @@ -522,14 +532,14 @@ NUMERAL_TOK /*options { paraphrase = 'a numeral'; }*/ * Matches a double quoted string literal. Escaping is supported, and escape * character '\' has to be escaped. */ -STRING_LITERAL /*options { paraphrase = 'a string literal'; }*/ +STRING_LITERAL : '"' (ESCAPE | ~('"'|'\\'))* '"' ; /** * Matches the comments and ignores them */ -COMMENT /*options { paraphrase = 'comment'; }*/ +COMMENT : ';' (~('\n' | '\r'))* { $channel = HIDDEN;; } ; @@ -538,7 +548,7 @@ COMMENT /*options { paraphrase = 'comment'; }*/ * Matches any letter ('a'-'z' and 'A'-'Z'). */ fragment -ALPHA /*options { paraphrase = 'a letter'; }*/ +ALPHA : 'a'..'z' | 'A'..'Z' ; @@ -546,16 +556,11 @@ ALPHA /*options { paraphrase = 'a letter'; }*/ /** * Matches the digits (0-9) */ -fragment -DIGIT /*options { paraphrase = 'a digit'; }*/ - : '0'..'9' - ; +fragment DIGIT : '0'..'9'; /** * Matches an allowed escaped character. */ -fragment ESCAPE - : '\\' ('"' | '\\' | 'n' | 't' | 'r') - ; +fragment ESCAPE : '\\' ('"' | '\\' | 'n' | 't' | 'r');