1		% (c) 2014-2026 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, get_smtlib_lines_read/1]).
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		:- use_module(probsrc(error_manager),[add_error/3, add_warning/3, add_message/3]).
14
15		:- set_prolog_flag(double_quotes, codes).
16
17		parse_smtlib2(Source, ListOfCommands) :-
18		debug_println(5,parsing_smtlib2(Source)),
19		reset_parser,
20		(phrase(commands(ListOfCommands),Source)
21		-> debug_println(5,finished_parsing)
22		; line_counter(Line),
23		add_error(smtlib2_parser,'Parsing failed at line:',Line),
24		fail
25		).
26
27		% meta magic
28		% at_least_once consumes rule A at least once and returns a list
29		% multiple_times consumes rule A zero or more times
30
31		:- meta_predicate multiple_times(3,-,-,-).
32		:- meta_predicate at_least_once(3,-,-,-).
33		at_least_once(A,[Partial|List]) -->
34	?	call(A,Partial), ws,
35		!,
36	?	multiple_times(A,List).
37		at_least_once(A,_) --> err_message(A).
38
39		err_message(Expected) --> err_message('Unrecognized',Expected).
40		err_message(Kind,Expected) -->
41		{line_counter(N), format_with_colour_nl(user_error,[red],"! ~w ~w on line ~w.",[Kind,Expected,N]),fail}.
42		err_message(_,_) --> any_chars_but_newline(S), !, {format_with_colour_nl(user_error,[red],"! '~s'",[S]),fail}.
43
44		multiple_times(A,[Partial|List]) -->
45	?	call(A,Partial), ws,
46	?	multiple_times(A,List).
47		multiple_times(_A,[],In,In).
48
49
50		:- use_module(probsrc(tools_printing),[format_with_colour_nl/4]).
51
52		% grammar rules
53	?	commands(Cmds) --> real_ws, !, commands(Cmds).
54		commands(Commands) --> comment(_),
55		{debug_println(19,comment_line)},!,
56		commands(Commands).
57		commands([Command|Commands]) -->
58	?	command(Command), {debug_println(19,command(Command))}, !,
59		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		get_smtlib_lines_read(Nr) :- (line_counter(N) -> Nr is N-1 ; Nr = 0).
67
68		inc_line_counter :-
69		retract(line_counter(N)), debug_println(5,processed_line(N)),
70		N1 is N+1, assertz(line_counter(N1)).
71
72		newline --> [10],!, {inc_line_counter}.
73		newline --> [13],!, {inc_line_counter}.
74
75	?	command(Command) --> "(", ws, !, command1(Command).
76		command(exit) --> ":x",!. % for ProB REPL compatibility
77
78
79		command1(set_logic(Logic)) --> "set-logic", !, ws, symbol(Logic), close_paren(set_logic).
80		command1(set_option(Option)) --> "set-option", !, ws, attribute(Option), close_paren(set_option).
81	?	command1(set_info(Info)) --> "set-info", !, ws, attribute(Info), close_paren(set_info(Info)).
82		command1(set_info(Info)) --> "meta-info", !, ws, attribute(Info), close_paren(meta_info(Info)).
83		command1(reset) --> "reset", !, close_paren(reset).
84		command1(declare_sort(Name,Arity)) --> "declare-sort", !, ws,
85		symbol(Name), ws, numeral(Arity), close_paren(declare_sort).
86		command1(define_sort(Name,Parameters,Sort)) --> "define-sort", !, ws,
87		symbol(Name),
88		open_paren(define_sort_params(Name)),
89		multiple_times(symbol,(Parameters)),close_paren(define_sort_params(Name)), ws,
90		must_be_smt_sort(Sort), close_paren(define_sort).
91		command1(declare_fun(Name,Parameters,Result)) --> "declare-fun", ws, !,
92		must_be_symbol(Name),
93		open_paren(declare_fun_params(Name)),
94		multiple_times(smt_sort,Parameters), ws, close_paren(declare_fun_params(Name)), ws,
95		must_be_smt_sort(Result),
96		close_paren(declare_fun).
97		command1(declare_fun(Name,[],Result)) --> "declare-const", ws, !,
98		must_be_symbol(Name), ws,
99		must_be_smt_sort(Result), close_paren(declare_fun).
100		command1(define_fun(Name,Parameters,Result,Term)) --> "define-fun", ws, !,
101		must_be_symbol(Name),
102		open_paren(define_fun_params(Name)),
103		multiple_times(sorted_var,Parameters),
104		close_paren(define_fun_params(Name)), ws,
105		must_be_smt_sort(Result), ws, must_be_term(Term), close_paren(define_fun).
106		command1(push(Num)) --> "push", !, ws, numeral(Num), close_paren(push).
107		command1(pop(Num)) --> "pop", !, ws, numeral(Num), close_paren(pop).
108		command1(assert(Term)) --> "assert", ws, !,
109		must_be_term(Term), close_paren(assert).
110		command1(check_sat) --> "check-sat", !, close_paren(check_sat).
111		command1(get_assert) --> "get-assert", !, close_paren(get_assert).
112		command1(get_proof) --> "get-proof", !, close_paren(get_proof).
113		command1(get_model) --> "get-model", !, close_paren(get_model).
114		command1(get_unsat_core) --> "get-unsat-core", !, close_paren(get_unsat_core).
115		command1(get_value(Terms)) --> "get-value", !, open_paren(get_value_arguments), at_least_once(term,Terms),
116		close_paren(get_value_arguments), close_paren(get_value).
117		command1(get_assign) --> "get-assign", !, close_paren(get_assign).
118		command1(get_option(Name)) --> "get-option", ws, !, keyword(Name), close_paren(get_option).
119		command1(get_info(Name)) --> "get-info", ws, !, keyword(Name), close_paren(get_info).
120		command1(minimize(Term)) --> "minimize", ws, !, must_be_term(Term), close_paren(minimize).
121		command1(maximize(Term)) --> "maximize", ws, !, must_be_term(Term), close_paren(minimize).
122		command1(exit) --> "exit", !, close_paren(exit).
123		% TODO: declare-datatype
124		command1(_) --> err_message(command).
125
126	?	close_paren(Ctxt) --> real_ws, !, close_paren(Ctxt).
127		close_paren(_) --> ")",!.
128		close_paren(Ctxt) --> err_message('Missing',closing_parenthesis(Ctxt)).
129
130		open_paren(Ctxt) --> real_ws, !, open_paren(Ctxt).
131		open_paren(_) --> "(",!.
132		open_paren(Ctxt) --> err_message('Missing',opening_parenthesis(Ctxt)).
133
134		close_bracket(Ctxt) --> real_ws, !, close_bracket(Ctxt).
135		close_bracket(_) --> "]",!.
136		close_bracket(Ctxt) --> err_message('Missing',closing_square_bracket(Ctxt)).
137
138
139		%command(_,In,_) :- !, atom_codes(A,In), format('Parsing failed on: ~w~n',[A]), !, fail.
140
141	?	symbol(Symbol) --> (simplesymbol(Symbol) -> [] ; asciicomment(Symbol)).
142	?	simplesymbol(Symbol) --> single_symbol(Start), symbols_or_digits(Rest), {atom_codes(Symbol,[Start|Rest])}.
143	?	single_symbol(S) --> [S], {member(S,"abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ+-/*=%?!.$_~&^<>@")}.
144	?	single_symbol_or_digit(S) --> single_symbol(S) ; digit(S).
145	?	symbols_or_digits([H|T]) --> single_symbol_or_digit(H), symbols_or_digits(T).
146		symbols_or_digits([]) --> "".
147
148	?	asciicomment(string(Symbol)) --> "|", any_chars_but_pipe(Codes), "|", {atom_codes(Symbol,Codes)}.
149
150	?	any_chars_but_pipe([C|T]) --> [C], {C \= 124}, any_chars_but_pipe(T).
151		any_chars_but_pipe([]) --> "".
152
153	?	any_chars_but_newline([C|T]) --> [C], {C \= 10}, any_chars_but_newline(T).
154		any_chars_but_newline([]) --> "".
155
156	?	attribute(Attr) --> keyword(A), attribute_aux(Attr,A).
157
158	?	attribute_aux(attribute(A,Value),A) --> real_ws, attribute_value(Value),!.
159		attribute_aux(attribute(A),A) --> [].
160
161	?	attribute_value(Value) --> symbol(Value).
162	?	attribute_value(Value) --> spec_constant(Value).
163		attribute_value(Value) --> "(", at_least_once(sexpr,Value), ")".
164
165		signed_numeral(N) --> "-",!, numeral(N1), {N is -N1}.
166	?	signed_numeral(N) --> numeral(N).
167
168		numeral(0) --> "0".
169		numeral(N) --> digit_no_zero(D1), digits(D), {number_codes(N,[D1|D])}.
170
171		digits1([D|T]) --> digit(D),!,digits(T).
172		digits([D|T]) --> digit(D),!,digits(T).
173		digits([]) --> "".
174		hex_digits(Val) --> hex_digits(0,Val).
175		hex_digits(ValIn,ValOut) --> hex_digit(_D,ValD),!,{V1 is ValIn*16+ValD}, hex_digits(V1,ValOut).
176		hex_digits(Val,Val) --> "".
177
178		% hex digits after a point
179		hex_digits_after(Val) --> hex_digit(_D,ValD),!, hex_digits_after(ValT), {Val is ValT/16+ValD}.
180		hex_digits_after(0.0) --> "".
181
182		signed_decimal_numeral(D) --> "-", !, decimal_numeral(D1), {D is -D1}.
183		signed_decimal_numeral(N) --> decimal_numeral(N).
184	?	decimal_numeral(DResult) --> numeral(D1), ".", !, digits1(DC2), decimal_exponent(DE),
185		{number_codes(D1,DC1),
186		append([DC1,".",DC2,DE],Codes),
187		number_codes(DResult,Codes)}.
188		decimal_numeral(DResult) --> ("0x" ; "+0x"),hex_digits(Val1), hex_numeral_rest1(Val1,DResult).
189
190		decimal_exponent([0'e,S|D]) --> ("e" ; "E"), exp_sign(S), !,digits1(D).
191		decimal_exponent([]) --> "".
192		exp_sign(D) --> [D], {D = 0'- ; D=0'+},!.
193		exp_sign(0'+) --> "".
194
195		hex_numeral_rest1(V1,DResult) --> ".",hex_digits_after(V2), !, {V is V1+V2},hex_numeral_rest2(V,DResult).
196		hex_numeral_rest1(V1,DResult) --> hex_numeral_rest2(V1,DResult).
197		hex_numeral_rest2(V,DResult) --> "p+",digits1(ExpS),!,
198		{number_codes(Exp,ExpS), DResult is V*2^Exp}. % TODO: process hexadecimal literal
199		hex_numeral_rest2(V,V) --> "".
200
201		digit(D) --> [D], {D >= 48, D =< 57}.
202		digit_no_zero(D) --> [D], {D >= 49, D =< 57}.
203		hex_digit(D,Val) --> [D], {D >= 48, (D =< 57, Val is D-38 ; D >= 65, D =< 70, Val is D-65)}.
204
205		smt_sort(sort(Sort)) --> identifier(SortName),!,optional_range(SortName,Sort).
206		smt_sort(sort(S)) --> numeral(S). % not yet supported in Translation, what does it mean?
207		smt_sort(sort('BitVec',[Length])) --> "(_ BitVec ", numeral(Length), ")".
208	?	smt_sort(Sort) --> "(", !, smt_sort_after_paren(Sort).
209
210		smt_sort_after_paren(sort(smt_fun(Params))) --> "->", !, % something like (-> Int Bool)
211		ws, at_least_once(smt_sort,Params), close_paren(sort).
212	?	smt_sort_after_paren(sort(S,Params)) --> identifier(S), ws, at_least_once(smt_sort,Params), close_paren(sort).
213
214		% like smt_sort, but throw error message:
215	?	must_be_smt_sort(T) --> smt_sort(T),!.
216		must_be_smt_sort(_) --> err_message(sort).
217
218		% integer or real range [0, 5] or default value [0.5]
219		% these are model annotations for preferred values, but do not force any constraint
220		optional_range(Sort,ResultingSort) --> real_ws,!,optional_range(Sort,ResultingSort).
221		optional_range(Sort,Sort) --> % should be sort('Int') or sort('Real');
222		% these return range in type and add constraints in interpreter
223		"[", !,
224		signed_number(range,From),
225		range_list_rest(Rest),
226		close_bracket(range),
227		{add_message(smtlib_parser,'Ignoring default range declaration: ',[From|Rest])}. % TODO: line_counter(N)
228		optional_range(Sort,Sort) --> "".
229
230		range_list_rest([H|T]) --> comma(range), !, signed_number(range,H), range_list_rest(T).
231		range_list_rest([]) --> "".
232
233		comma(Ctxt) --> real_ws, !, comma(Ctxt).
234		comma(_) --> ",",!.
235
236		signed_number(Ctxt,N) --> real_ws, !, signed_number(Ctxt,N).
237		signed_number(_,N) --> signed_decimal_numeral(N),!.
238		signed_number(_,N) --> signed_numeral(N),!.
239		signed_number(Ctxt,_) --> err_message('Missing',number(Ctxt)).
240
241		sorted_var(S) --> real_ws,!, sorted_var(S).
242	?	sorted_var(svar(Name,Sort)) --> "(", symbol(Name), ws, smt_sort(Sort), ")".
243
244		term(let(Bindings,Term)) -->
245	?	"(let", ws, !, "(", at_least_once(binding,Bindings), ")", ws, !, must_be_term(Term), !, close_paren(let).
246		term(forall(Vars,Term)) -->
247		"(forall", ws, !, "(", at_least_once(sorted_var,Vars), ")", ws, !, must_be_term(Term), !, close_paren(forall).
248		term(exists(Vars,Term)) -->
249		"(exists", ws, !, "(", at_least_once(sorted_var,Vars), ")", ws, !, must_be_term(Term), !, close_paren(exists).
250	?	term(T) --> spec_constant(T),!.
251	?	term(T) --> qual_identifier(T),!.
252		term(attributed_term(Term,Attributes)) --> "(", "!", ws, !,
253		must_be_term(Term), ws, !,
254		at_least_once(attribute,Attributes), close_paren(attributed_term).
255	?	term(id_term(Id,Terms)) --> "(", ws, qual_identifier(Id), ws, !, at_least_once(term,Terms), close_paren(id_term).
256
257		% term which raises error if it cannot be found
258	?	must_be_term(T) --> term(T),!.
259		must_be_term(_) --> err_message(term).
260
261		binding(bind(Symbol,Term)) --> "(", must_be_symbol(Symbol), ws, !, must_be_term(Term), close_paren(bind).
262		% binding which raises error if it cannot be found
263		must_be_symbol(T) --> symbol(T),!.
264		must_be_symbol(_) --> err_message(symbol).
265
266		qual_identifier(id(Id)) --> identifier(Id).
267		qual_identifier(id(Id,Sort)) --> "(as ", ws, !, identifier(Id), ws, smt_sort(Sort), ")".
268		qual_identifier(id(sign_extend(Parameter))) --> "(_ sign_extend ", !, numeral(Parameter), ")".
269		qual_identifier(id(zero_extend(Parameter))) --> "(_ zero_extend ", !, numeral(Parameter), ")".
270		qual_identifier(id(extract(P1,P2))) --> "(_ extract ", !, numeral(P1), ws, numeral(P2), ")".
271
272
273		identifier(Id) --> symbol(Id).
274		%identifier(id_num(Id,Num)) --> "(", "_", symbol(Id), numeral(Num), ")".
275
276	?	keyword(KW) --> ":", symbols_or_digits(L), {atom_codes(KW,L)}.
277
278		sexpr(E) --> spec_constant(E).
279		sexpr(E) --> symbol(E).
280		sexpr(E) --> keyword(E).
281		sexpr(E) --> "(", multiple_times(sexpr,E), ")".
282
283		spec_constant(decimal(D)) --> signed_decimal_numeral(D).
284	?	spec_constant(integer(I)) --> signed_numeral(I).
285	?	spec_constant(string(S)) --> "\"", any_chars_but_quotations(SCodes), "\"", {atom_codes(S,SCodes)}.
286		spec_constant(bitvector(Val,Length)) --> "(_ bv", numeral(Val), " ", numeral(Length), ")".
287		spec_constant(bitvector(Binary)) --> "#b", binary_numbers(Binary).
288
289		binary_numbers([H|T]) --> binary_number(H), binary_numbers(T).
290		binary_numbers([N]) --> binary_number(N).
291		binary_number(0) --> "0".
292		binary_number(1) --> "1".
293
294	?	any_chars_but_quotations([C|T]) --> [C], {C \= 34}, any_chars_but_quotations(T).
295		% two quotations are allowed in smtlib 2.5
296		any_chars_but_quotations([C,C|T]) --> [C,C], {C = 34}, any_chars_but_quotations(T).
297		any_chars_but_quotations([]) --> "".
298
299		% whitespaces
300		ws --> " ", !, ws.
301		ws --> [9], !, ws. % tab
302		ws --> newline, !, ws.
303	?	ws --> comment(_),!,ws.
304		ws --> "".
305
306		real_ws --> " ", !, ws.
307		real_ws --> [9], !, ws.
308		real_ws --> newline, ws.
309	?	real_ws --> comment(_),!,ws.
310
311	?	comment(Chars) --> ";", any_chars_but_newline(Chars), newline.