1 | | % (c) 2014-2022 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, |
2 | | % Heinrich Heine Universitaet Duesseldorf |
3 | | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) |
4 | | |
5 | | :- module(smtlib2_parser,[parse_smtlib2/2]). |
6 | | |
7 | | :- use_module(probsrc(module_information),[module_info/2]). |
8 | | :- module_info(group,smtlib). |
9 | | :- module_info(description,'The SMT-LIB 2 Interpreter - Parser'). |
10 | | |
11 | | :- use_module(library(lists),[append/2]). |
12 | | :- use_module(probsrc(debug),[debug_println/2]). |
13 | | |
14 | | :- set_prolog_flag(double_quotes, codes). |
15 | | |
16 | | parse_smtlib2(Source, ListOfCommands) :- |
17 | | debug_println(5,parsing_smtlib2(Source)), |
18 | | reset_parser, |
19 | | phrase(commands(ListOfCommands),Source), |
20 | | debug_println(5,finished_parsing). |
21 | | |
22 | | % meta magic |
23 | | % at_least_once consumes rule A at least once and returns a list |
24 | | % multiple_times consumes rule A zero or more times |
25 | | |
26 | | :- meta_predicate multiple_times(3,-,-,-). |
27 | | :- meta_predicate at_least_once(3,-,-,-). |
28 | | at_least_once(A,[Partial|List]) --> |
29 | ? | call(A,Partial), ws, |
30 | | !, |
31 | ? | multiple_times(A,List). |
32 | | at_least_once(A,_) --> err_message(A). |
33 | | |
34 | | err_message(Expected) --> {line_counter(N), format_with_colour_nl(user_error,[red],"! Unrecognized ~w on line ~w.",[Expected,N]),fail}. |
35 | | err_message(_) --> any_chars_but_newline(S), !, {format_with_colour_nl(user_error,[red],"! '~s'",[S]),fail}. |
36 | | |
37 | | multiple_times(A,[Partial|List]) --> |
38 | ? | call(A,Partial), ws, |
39 | ? | multiple_times(A,List). |
40 | | multiple_times(_A,[],In,In). |
41 | | |
42 | | :- meta_predicate multiple_times_no_whitespace(3,-,-,-). |
43 | | :- meta_predicate at_least_once_no_whitespace(3,-,-,-). |
44 | | at_least_once_no_whitespace(A,[Partial|List]) --> |
45 | ? | call(A,Partial), |
46 | | multiple_times_no_whitespace(A,List). |
47 | | |
48 | | multiple_times_no_whitespace(A,List) --> |
49 | ? | at_least_once_no_whitespace(A,List). |
50 | | multiple_times_no_whitespace(_A,[],In,In). |
51 | | |
52 | | :- use_module(probsrc(tools_printing),[format_with_colour_nl/4]). |
53 | | |
54 | | % grammar rules |
55 | | commands(Cmds) --> real_ws, !, commands(Cmds). |
56 | | commands([Command|Commands]) --> |
57 | ? | command(Command), {debug_println(5,command(Command))}, !, |
58 | | commands(Commands). |
59 | ? | commands(Commands) --> ";", any_chars_but_newline(_), newline, !, commands(Commands). |
60 | | commands([]) --> !. |
61 | | commands(_) --> err_message(command). |
62 | | |
63 | | reset_parser :- retractall(line_counter(_)), assertz(line_counter(1)). |
64 | | :- dynamic line_counter/1. |
65 | | line_counter(1). |
66 | | inc_line_counter :- |
67 | | retract(line_counter(N)), debug_println(5,processed_line(N)), |
68 | | N1 is N+1, assertz(line_counter(N1)). |
69 | | |
70 | | newline --> [10],!, {inc_line_counter}. |
71 | | newline --> [13],!, {inc_line_counter}. |
72 | | |
73 | ? | command(Command) --> "(", ws, !, command1(Command). |
74 | | command(exit) --> ":x",!. % for ProB REPL compatibility |
75 | | |
76 | | command1(set_logic(Logic)) --> "set-logic", !, ws, symbol(Logic), close_paren(set_logic). |
77 | | command1(set_option(Option)) --> "set-option", !, ws, attribute(Option), close_paren(set_option). |
78 | ? | command1(set_info(Info)) --> "set-info", !, ws, attribute(Info), close_paren(set_info). |
79 | | command1(set_info(Info)) --> "meta-info", !, ws, attribute(Info), close_paren(meta_info). |
80 | | command1(reset) --> "reset", !, close_paren(reset). |
81 | | command1(declare_sort(Name,Arity)) --> "declare-sort", !, ws, |
82 | | symbol(Name), ws, numeral(Arity), close_paren(declare_sort). |
83 | | command1(define_sort(Name,Parameters,Sort)) --> "define-sort", !, ws, |
84 | | symbol(Name), ws, "(", multiple_times(symbol,(Parameters)), ")", ws, |
85 | | !, |
86 | | must_be_smt_sort(Sort), close_paren(define_sort). |
87 | | command1(declare_fun(Name,Parameters,Result)) --> "declare-fun", ws, !, |
88 | | must_be_symbol(Name), ws, |
89 | | "(", multiple_times(smt_sort,Parameters), ws, ")", ws, |
90 | | must_be_smt_sort(Result), close_paren(declare_fun). |
91 | | command1(define_fun(Name,Parameters,Result,Term)) --> "define-fun", ws, !, |
92 | | symbol(Name), ws, "(", multiple_times(sorted_var,Parameters), ")", ws, |
93 | | !, |
94 | | must_be_smt_sort(Result), ws, must_be_term(Term), close_paren(define_fun). |
95 | | command1(push(Num)) --> "push", !, ws, numeral(Num), close_paren(push). |
96 | | command1(pop(Num)) --> "pop", !, ws, numeral(Num), close_paren(pop). |
97 | | command1(assert(Term)) --> "assert", ws, !, |
98 | | must_be_term(Term), close_paren(assert). |
99 | | command1(check_sat) --> "check-sat", !, close_paren(check_sat). |
100 | | command1(get_assert) --> "get-assert", !, close_paren(get_assert). |
101 | | command1(get_proof) --> "get-proof", !, close_paren(get_proof). |
102 | | command1(get_model) --> "get-model", !, close_paren(get_model). |
103 | | command1(get_unsat_core) --> "get-unsat-core", !, close_paren(get_unsat_core). |
104 | | command1(get_value(Terms)) --> "get-value", ws, !, "(", at_least_once(term,Terms), ")", close_paren(get_value). |
105 | | command1(get_assign) --> "get-assign", !, close_paren(get_assign). |
106 | | command1(get_option(Name)) --> "get-option", ws, !, keyword(Name), close_paren(get_option). |
107 | | command1(get_info(Name)) --> "get-info", ws, !, keyword(Name), close_paren(get_info). |
108 | | command1(exit) --> "exit", !, close_paren(exit). |
109 | | command1(_) --> err_message(command). |
110 | | |
111 | | close_paren(Ctxt) --> real_ws, !, close_paren(Ctxt). |
112 | | close_paren(_) --> ")",!. |
113 | | close_paren(Ctxt) --> err_message(closing_parenthesis(Ctxt)). |
114 | | |
115 | | %command(_,In,_) :- !, atom_codes(A,In), format('Parsing failed on: ~w~n',[A]), !, fail. |
116 | | |
117 | ? | symbol(Symbol) --> (simplesymbol(Symbol) -> [] ; asciicomment(Symbol)). |
118 | ? | simplesymbol(Symbol) --> single_symbol(Start), symbols_or_digits(Rest), {atom_codes(Symbol,[Start|Rest])}. |
119 | ? | single_symbol(S) --> [S], {member(S,"abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ+-/*=%?!.$_~&^<>@")}. |
120 | ? | single_symbol_or_digit(S) --> single_symbol(S) ; digit(S). |
121 | ? | symbols_or_digits([H|T]) --> single_symbol_or_digit(H), symbols_or_digits(T). |
122 | | symbols_or_digits([]) --> "". |
123 | | |
124 | ? | asciicomment(string(Symbol)) --> "|", any_chars_but_pipe(Codes), "|", {atom_codes(Symbol,Codes)}. |
125 | | |
126 | ? | any_chars_but_pipe([C|T]) --> [C], {C \= 124}, any_chars_but_pipe(T). |
127 | | any_chars_but_pipe([]) --> "". |
128 | | |
129 | ? | any_chars_but_newline([C|T]) --> [C], {C \= 10}, any_chars_but_newline(T). |
130 | | any_chars_but_newline([]) --> "". |
131 | | |
132 | ? | attribute(attribute(A,Value)) --> keyword(A), real_ws, attribute_value(Value). |
133 | | attribute(attribute(A)) --> keyword(A). |
134 | | |
135 | ? | attribute_value(Value) --> symbol(Value). |
136 | ? | attribute_value(Value) --> spec_constant(Value). |
137 | | attribute_value(Value) --> "(", at_least_once(sexpr,Value), ")". |
138 | | |
139 | | numeral(0) --> "0". |
140 | ? | numeral(N) --> digit_no_zero(D1), multiple_times_no_whitespace(digit,D), {number_codes(N,[D1|D])}. |
141 | | |
142 | ? | decimal_numeral(D) --> numeral(D1), ".", numeral(D2), |
143 | | {number_codes(D1,DC1), number_codes(D2,DC2), |
144 | | append([DC1,".",DC2],Codes), |
145 | | number_codes(D,Codes)}. |
146 | | |
147 | ? | digit(D) --> [D], {[D]="0"} ; digit_no_zero(D). |
148 | ? | digit_no_zero(D) --> [D], {member(D,"123456789")}. |
149 | | |
150 | | smt_sort(sort(S)) --> identifier(S). |
151 | | smt_sort(sort(S)) --> numeral(S). % not yet supported in Translation, what does it mean? |
152 | | smt_sort(sort('BitVec',[Length])) --> "(_ BitVec ", numeral(Length), ")". |
153 | | smt_sort(sort(S,Params)) --> "(", identifier(S), ws, !, |
154 | ? | at_least_once(smt_sort,Params), close_paren(sort). |
155 | | % like smt_sort, but throw error message: |
156 | ? | must_be_smt_sort(T) --> smt_sort(T),!. |
157 | | must_be_smt_sort(_) --> err_message(sort). |
158 | | |
159 | ? | sorted_var(svar(Name,Sort)) --> "(", symbol(Name), ws, smt_sort(Sort), ")". |
160 | | |
161 | | term(let(Bindings,Term)) --> |
162 | ? | "(let", ws, !, "(", at_least_once(binding,Bindings), ")", ws, !, must_be_term(Term), !, close_paren(let). |
163 | | term(forall(Vars,Term)) --> |
164 | | "(forall", ws, !, "(", at_least_once(sorted_var,Vars), ")", ws, !, must_be_term(Term), !, close_paren(forall). |
165 | | term(exists(Vars,Term)) --> |
166 | | "(exists", ws, !, "(", at_least_once(sorted_var,Vars), ")", ws, !, must_be_term(Term), !, close_paren(exists). |
167 | ? | term(T) --> spec_constant(T),!. |
168 | ? | term(T) --> qual_identifier(T),!. |
169 | | term(attributed_term(Term,Attributes)) --> "(", "!", ws, !, |
170 | | must_be_term(Term), ws, !, |
171 | | at_least_once(attribute,Attributes), close_paren(attributed_term). |
172 | ? | term(id_term(Id,Terms)) --> "(", qual_identifier(Id), ws, !, at_least_once(term,Terms), close_paren(id_term). |
173 | | |
174 | | % term which raises error if it cannot be found |
175 | ? | must_be_term(T) --> term(T),!. |
176 | | must_be_term(_) --> err_message(term). |
177 | | |
178 | | binding(bind(Symbol,Term)) --> "(", must_be_symbol(Symbol), ws, !, must_be_term(Term), close_paren(bind). |
179 | | % binding which raises error if it cannot be found |
180 | | must_be_symbol(T) --> symbol(T),!. |
181 | | must_be_symbol(_) --> err_message(symbol). |
182 | | |
183 | | qual_identifier(id(Id)) --> identifier(Id). |
184 | | qual_identifier(id(Id,Sort)) --> "(as ", ws, !, identifier(Id), ws, smt_sort(Sort), ")". |
185 | | qual_identifier(id(sign_extend(Parameter))) --> "(_ sign_extend ", !, numeral(Parameter), ")". |
186 | | qual_identifier(id(zero_extend(Parameter))) --> "(_ zero_extend ", !, numeral(Parameter), ")". |
187 | | qual_identifier(id(extract(P1,P2))) --> "(_ extract ", !, numeral(P1), ws, numeral(P2), ")". |
188 | | |
189 | | |
190 | | identifier(Id) --> symbol(Id). |
191 | | %identifier(id_num(Id,Num)) --> "(", "_", symbol(Id), numeral(Num), ")". |
192 | | |
193 | ? | keyword(KW) --> ":", symbols_or_digits(L), {atom_codes(KW,L)}. |
194 | | |
195 | | sexpr(E) --> spec_constant(E). |
196 | | sexpr(E) --> symbol(E). |
197 | | sexpr(E) --> keyword(E). |
198 | | sexpr(E) --> "(", multiple_times(sexpr,E), ")". |
199 | | |
200 | ? | spec_constant(decimal(D)) --> decimal_numeral(D). |
201 | ? | spec_constant(integer(I)) --> numeral(I). |
202 | ? | spec_constant(string(S)) --> "\"", any_chars_but_quotations(SCodes), "\"", {atom_codes(S,SCodes)}. |
203 | | spec_constant(bitvector(Val,Length)) --> "(_ bv", numeral(Val), " ", numeral(Length), ")". |
204 | | spec_constant(bitvector(Binary)) --> "#b", binary_numbers(Binary). |
205 | | |
206 | | binary_numbers([H|T]) --> binary_number(H), binary_numbers(T). |
207 | | binary_numbers([N]) --> binary_number(N). |
208 | | binary_number(0) --> "0". |
209 | | binary_number(1) --> "1". |
210 | | |
211 | ? | any_chars_but_quotations([C|T]) --> [C], {C \= 34}, any_chars_but_quotations(T). |
212 | | % two quotations are allowed in smtlib 2.5 |
213 | | any_chars_but_quotations([C,C|T]) --> [C,C], {C = 34}, any_chars_but_quotations(T). |
214 | | any_chars_but_quotations([]) --> "". |
215 | | |
216 | | % whitespaces |
217 | | ws --> " ", !, ws. |
218 | | ws --> [9], !, ws. % tab |
219 | | ws --> newline, !, ws. |
220 | | ws --> "". |
221 | | |
222 | | real_ws --> " ", !, ws. |
223 | | real_ws --> [9], !, ws. |
224 | | real_ws --> newline, ws. |