blob: 864719cfa7681e4fda812abe5a2fa5053dda380f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
|
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 {
// [chris 12/15/2009] FIXME: decls may not be BOOLEAN
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(); }
;
|
