diff options
Diffstat (limited to 'src/parser/cvc/CvcParser.g')
| -rw-r--r-- | src/parser/cvc/CvcParser.g | 111 |
1 files changed, 111 insertions, 0 deletions
diff --git a/src/parser/cvc/CvcParser.g b/src/parser/cvc/CvcParser.g new file mode 100644 index 000000000..625f2c381 --- /dev/null +++ b/src/parser/cvc/CvcParser.g @@ -0,0 +1,111 @@ +header "post_include_hpp" { +#include "parser/antlr_parser.h" +} + +header "post_include_cpp" { +#include <vector> + +using namespace std; +using namespace CVC4; +using namespace CVC4::parser; +} + +options { + language = "Cpp"; // C++ output for antlr + namespaceStd = "std"; // Cosmetic option to get rid of long defines in generated code + namespaceAntlr = "antlr"; // Cosmetic option to get rid of long defines in generated code + namespace = "CVC4::parser"; // Wrap everything in the smtparser namespace +} + +/** + * AntlrCvcParser class is the parser for the files in CVC format. + */ +class AntlrCvcParser extends Parser("AntlrParser"); +options { + genHashLines = true; // Include line number information + importVocab = CvcVocabulary; // Import the common vocabulary + defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions + k = 2; +} + +/** + * Matches a command of the input. If a declaration, it will return an empty + * command. + */ +command returns [CVC4::Command* cmd = 0] +{ + Expr f; + vector<string> ids; +} + : ASSERT f = formula { cmd = new AssertCommand(f); } + | QUERY f = formula { cmd = new QueryCommand(f); } + | CHECKSAT f = formula { cmd = new CheckSatCommand(f); } + | CHECKSAT { cmd = new CheckSatCommand(); } + | identifierList[ids] COLON type { + newPredicates(ids); + cmd = new EmptyCommand("Declaration"); + } + | EOF + ; + +identifierList[std::vector<std::string>& id_list] + : id1:IDENTIFIER { id_list.push_back(id1->getText()); } + ( + COMMA + id2:IDENTIFIER { id_list.push_back(id2->getText()); } + )* + ; + +type + : BOOLEAN + ; + +formula returns [CVC4::Expr formula] + : formula = bool_formula + ; + +bool_formula returns [CVC4::Expr formula] +{ + vector<Expr> formulas; + vector<Kind> kinds; + Expr f1, f2; + Kind k; +} + : f1 = primary_bool_formula { formulas.push_back(f1); } + ( k = bool_operator { kinds.push_back(k); } f2 = primary_bool_formula { formulas.push_back(f2); } )* + { + // Create the expression based on precedences + formula = createPrecedenceExpr(formulas, kinds); + } + ; + +primary_bool_formula returns [CVC4::Expr formula] + : formula = bool_atom + | NOT formula = primary_bool_formula { formula = newExpression(CVC4::NOT, formula); } + | LPAREN formula = bool_formula RPAREN + ; + +bool_operator returns [CVC4::Kind kind] + : IMPLIES { kind = CVC4::IMPLIES; } + | AND { kind = CVC4::AND; } + | OR { kind = CVC4::OR; } + | XOR { kind = CVC4::XOR; } + | IFF { kind = CVC4::IFF; } + ; + +bool_atom returns [CVC4::Expr atom] +{ + string p; +} + : p = predicate_sym {isDeclared(p, SYM_VARIABLE)}? { atom = getVariable(p); } + exception catch [antlr::SemanticException ex] { + rethrow(ex, "Undeclared variable " + p); + } + | TRUE { atom = getTrueExpr(); } + | FALSE { atom = getFalseExpr(); } + ; + +predicate_sym returns [std::string p] + : id:IDENTIFIER { p = id->getText(); } + ; +
\ No newline at end of file |