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.