1		% (c) 2014-2016 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		parse_smtlib2(Source, ListOfCommands) :- debug_println(5,parsing_smtlib2(Source)),
15		commands(ListOfCommands,Source,[]),
16		debug_println(5,finished_parsing).
17
18		% meta magic
19		% at_least_once consumes rule A at least once and returns a list
20		% multiple_times consumes rule A zero or more times
21
22		:- meta_predicate multiple_times(3,-,-,-).
23		:- meta_predicate at_least_once(3,-,-,-).
24		at_least_once(A,[Partial|List]) -->
25		call(A,Partial), ws,
26		multiple_times(A,List).
27
28		multiple_times(A,List) -->
29		at_least_once(A,List).
30		multiple_times(_A,[],In,In).
31
32		:- meta_predicate multiple_times_no_whitespace(3,-,-,-).
33		:- meta_predicate at_least_once_no_whitespace(3,-,-,-).
34		at_least_once_no_whitespace(A,[Partial|List]) -->
35		call(A,Partial),
36		multiple_times_no_whitespace(A,List).
37
38		multiple_times_no_whitespace(A,List) -->
39		at_least_once_no_whitespace(A,List).
40		multiple_times_no_whitespace(_A,[],In,In).
41
42		% grammar rules
43		commands(Cmds) --> real_ws, !, commands(Cmds).
44		commands([Command|Commands]) -->
45		command(Command), {debug_println(5,command(Command))}, !,
46		commands(Commands).
47		commands(Commands) --> ";", any_chars_but_newline(_), newline, !, commands(Commands).
48		commands([]) --> "".
49		commands(_,_,_) :- line_counter(N), format("Syntax error on line ~w.~n",[N]),fail.
50
51		:- dynamic line_counter/1.
52		line_counter(0).
53		inc_line_counter :-
54		retract(line_counter(N)), debug_println(5,processed_line(N)),
55		N1 is N+1, assert(line_counter(N1)).
56		newline --> "\n", {inc_line_counter}.
57
58		command(set_logic(Logic)) --> "(set-logic", ws, symbol(Logic), ")".
59		command(set_option(Option)) --> "(set-option", ws, attribute(Option), ")".
60		command(set_info(Info)) --> "(set-info", ws, attribute(Info), ")".
61		command(set_info(Info)) --> "(meta-info", ws, attribute(Info), ")".
62		command(reset) --> "(reset)".
63		command(declare_sort(Name,Arrity)) --> "(declare-sort", ws, symbol(Name), ws, numeral(Arrity), ")".
64		command(define_sort(Name,Parameters,Sort)) --> "(define-sort", ws, symbol(Name), ws, "(", multiple_times(symbol,(Parameters)), ")", sort(Sort), ")".
65		command(declare_fun(Name,Parameters,Result)) --> "(declare-fun", ws, symbol(Name), ws, "(", multiple_times(sort,Parameters), ")", ws, sort(Result), ")".
66		command(define_fun(Name,Parameters,Result,Term)) --> "(define-fun", ws, symbol(Name), ws, "(", multiple_times(sorted_var,Parameters), ")", ws, sort(Result), ws, term(Term), ")".
67		command(push(Num)) --> "(push", ws, numeral(Num), ")".
68		command(pop(Num)) --> "(pop", ws, numeral(Num), ")".
69		command(assert(Term)) --> "(assert", ws, term(Term), ")".
70		command(check_sat) --> "(check-sat", ")".
71		command(get_assert) --> "(get-assert", ")".
72		command(get_proof) --> "(get-proof", ")".
73		command(get_model) --> "(get-model", ")".
74		command(get_unsat_core) --> "(get-unsat-core", ")".
75		command(get_value(Terms)) --> "(get-value", ws, "(", at_least_once(term,Terms), ")", ")".
76		command(get_assign) --> "(get-assign", ")".
77		command(get_option(Name)) --> "(get-option", ws, keyword(Name), ")".
78		command(get_info(Name)) --> "(get-info", ws, keyword(Name), ")".
79		command(exit) --> "(exit", ")".
80
81		%command(_,In,_) :- !, atom_codes(A,In), format('Parsing failed on: ~w~n',[A]), !, fail.
82
83		symbol(Symbol) --> (simplesymbol(Symbol) -> [] ; asciicomment(Symbol)).
84		simplesymbol(Symbol) --> single_symbol(Start), symbols_or_digits(Rest), {atom_codes(Symbol,[Start|Rest])}.
85		single_symbol(S) --> [S], {member(S,"abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ+-/*=%?!.$_~&^<>@")}.
86		single_symbol_or_digit(S) --> single_symbol(S) ; digit(S).
87		symbols_or_digits([H|T]) --> single_symbol_or_digit(H), symbols_or_digits(T).
88		symbols_or_digits([]) --> "".
89
90		asciicomment(string(Symbol)) --> "|", any_chars_but_pipe(Codes), "|", {atom_codes(Symbol,Codes)}.
91
92		any_chars_but_pipe([C|T]) --> [C], {C \= 124}, any_chars_but_pipe(T).
93		any_chars_but_pipe([]) --> "".
94
95		any_chars_but_newline([C|T]) --> [C], {C \= 10}, any_chars_but_newline(T).
96		any_chars_but_newline([]) --> "".
97
98		attribute(attribute(A,Value)) --> keyword(A), ws, attribute_value(Value).
99		attribute(attribute(A)) --> keyword(A).
100
101		attribute_value(Value) --> symbol(Value).
102		attribute_value(Value) --> spec_constant(Value).
103		attribute_value(Value) --> "(", at_least_once(sexpr,Value), ")".
104
105		numeral(0) --> "0".
106		numeral(N) --> digit_no_zero(D1), multiple_times_no_whitespace(digit,D), {number_codes(N,[D1|D])}.
107
108		decimal_numeral(D) --> numeral(D1), ".", numeral(D2),
109		{number_codes(D1,DC1), number_codes(D2,DC2),
110		append([DC1,".",DC2],Codes),
111		number_codes(D,Codes)}.
112
113		digit(D) --> [D], {[D]="0"} ; digit_no_zero(D).
114		digit_no_zero(D) --> [D], {member(D,"123456789")}.
115
116		sort(sort(S)) --> identifier(S).
117		sort(sort('BitVec',[Length])) --> "(_ BitVec ", numeral(Length), ")".
118		sort(sort(S,Params)) --> "(", identifier(S), ws, at_least_once(sort,Params), ")".
119
120		sorted_var(svar(Name,Sort)) --> "(", symbol(Name), ws, sort(Sort), ")".
121
122		term(let(Bindings,Term)) --> "(let", ws, "(", at_least_once(binding,Bindings), ")", ws, term(Term), ws, ")".
123		term(forall(Vars,Term)) --> "(forall", ws, "(", at_least_once(sorted_var,Vars), ")", ws, term(Term), ws, ")".
124		term(exists(Vars,Term)) --> "(exists", ws, "(", at_least_once(sorted_var,Vars), ")", ws, term(Term), ws, ")".
125		term(T) --> spec_constant(T).
126		term(T) --> qual_identifier(T).
127		term(id_term(Id,Terms)) --> "(", qual_identifier(Id), ws, at_least_once(term,Terms), ws, ")".
128		term(attributed_term(Term,Attributes)) --> "(", "!", ws, term(Term), ws, at_least_once(attribute,Attributes), ws, ")".
129
130		binding(bind(Symbol,Term)) --> "(", symbol(Symbol), ws, term(Term), ")".
131
132		qual_identifier(id(Id)) --> identifier(Id).
133		qual_identifier(id(Id,Sort)) --> "(as ", ws, identifier(Id), ws, sort(Sort), ")".
134		qual_identifier(id(sign_extend(Parameter))) --> "(_ sign_extend ", numeral(Parameter), ")".
135		qual_identifier(id(zero_extend(Parameter))) --> "(_ zero_extend ", numeral(Parameter), ")".
136		qual_identifier(id(extract(P1,P2))) --> "(_ extract ", numeral(P1), ws, numeral(P2), ")".
137
138
139		identifier(Id) --> symbol(Id).
140		%identifier(id_num(Id,Num)) --> "(", "_", symbol(Id), numeral(Num), ")".
141
142		keyword(KW) --> ":", symbols_or_digits(L), {atom_codes(KW,L)}.
143
144		sexpr(E) --> spec_constant(E).
145		sexpr(E) --> symbol(E).
146		sexpr(E) --> keyword(E).
147		sexpr(E) --> "(", multiple_times(sexpr,E), ")".
148
149		spec_constant(integer(I)) --> numeral(I).
150		spec_constant(decimal(D)) --> decimal_numeral(D).
151		spec_constant(string(S)) --> "\"", any_chars_but_quotations(SCodes), "\"", {atom_codes(S,SCodes)}.
152		spec_constant(bitvector(Val,Length)) --> "(_ bv", numeral(Val), " ", numeral(Length), ")".
153		spec_constant(bitvector(Binary)) --> "#b", binary_numbers(Binary).
154
155		binary_numbers([H|T]) --> binary_number(H), binary_numbers(T).
156		binary_numbers([N]) --> binary_number(N).
157		binary_number(0) --> "0".
158		binary_number(1) --> "1".
159
160		any_chars_but_quotations([C|T]) --> [C], {C \= 34}, any_chars_but_quotations(T).
161		% two quotations are allowed in smtlib 2.5
162		any_chars_but_quotations([C,C|T]) --> [C,C], {C = 34}, any_chars_but_quotations(T).
163		any_chars_but_quotations([]) --> "".
164
165		% whitespaces
166		ws --> " ", ws.
167		ws --> newline, ws.
168		ws --> "".
169
170		real_ws --> " ", ws.
171		real_ws --> newline, ws.