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_cli,[smtlib2_file/1, smtlib2_file/2]).
6
7		:- use_module(probsrc(module_information),[module_info/2]).
8		:- module_info(group,smtlib).
9		:- module_info(description,'Command line interface and REPL for SMT-LIB 2 files.').
10
11		:- use_module(smtlib_solver(smtlib2_interpreter)).
12		:- use_module(smtlib_solver(smtlib2_parser)).
13		:- use_module(smtlib_solver(smtlib2_environment)).
14
15		:- use_module(probsrc(debug),[debug_println/2]).
16		:- use_module(probsrc(preferences), [set_preference/2]).
17		:- use_module(probsrc(error_manager),[add_error/3]).
18
19		:- set_prolog_flag(double_quotes, codes).
20
21		read_file(Stream,Out) :-
22		get_code(Stream,Code),
23		read_file(Code,Stream,Out).
24		read_file(-1,_Stream,[]) :- !.
25		read_file(Code,Stream,[Code|L]) :-
26		read_file(Stream,L).
27
28		smtlib2_file(Filename) :- smtlib2_file(Filename,[]).
29
30		smtlib2_file(Filename,Options) :-
31		debug_println(10,processing_smt_file(Filename)),
32		% enable disprover mode to trigger modified treatment of wd conditions, etc.
33		% some default preferences
34		set_preference(disprover_mode,true),
35		set_preference(use_clpfd_solver,true),
36		set_preference(use_smt_mode,true),
37
38		debug_println(25,opening(Filename)),
39		open(Filename,read,S),
40		read_file(S,Content),
41		close(S),
42		debug_println(25,parsing(Filename)),
43		parse_smtlib2(Content,ListOfCommands),
44		!,
45		empty_env(EnvIn),
46		debug_println(25,interpreting_commands(ListOfCommands)),
47		catch(
48		(
49		interpret_l(ListOfCommands,EnvIn,EnvOut),
50		(member(repl,Options)
51		-> debug_println(25,finished_processing_and_starting_repl(Filename)),
52		repl_help,
53		smtlib2_repl(EnvOut)
54		; true)
55		),
56		halt(0),
57		debug_println(25,finished_processing_exit(Filename))
58		).
59		smtlib2_file(Filename,_) :-
60		add_error(smtlib2_cli,'Could not process file: ',Filename).
61
62		:- use_module(probsrc(tools_printing),[format_with_colour/4]).
63
64		repl_help :-
65		format_with_colour(user_output,[blue],'Starting SMTLIB REPL~n',[]),
66		format_with_colour(user_output,[blue],'Available commands:~n',[]),
67		format_with_colour(user_output,[blue],' (get-model)~n',[]),
68		format_with_colour(user_output,[blue],' (check-sat)~n',[]),
69		format_with_colour(user_output,[blue],' (set-info I Val)~n',[]),
70		format_with_colour(user_output,[blue],' (push Num)~n',[]),
71		format_with_colour(user_output,[blue],' (pop Num)~n',[]),
72		format_with_colour(user_output,[blue],' (assert Term)~n',[]),
73		format_with_colour(user_output,[blue],' (reset)~n',[]),
74		format_with_colour(user_output,[blue],' (exit)~n',[]),
75		format_with_colour(user_output,[blue],' define-fun, declare-sort,....~n~n',[]).
76
77		smtlib2_repl(EnvIn) :-
78		write('SMT>>>'),flush_output(user_output),
79		read_line(Line),
80		(Line = end_of_file -> halt(0)
81		; append(RealLine,".",Line) -> true
82		; RealLine = Line
83		),
84		(parse_smtlib2(RealLine,Commands)
85		-> (interpret_l(Commands,EnvIn,EnvOut) -> true
86		; format_with_colour(user_output,[red],'Could not process SMT commands: ~w~n',[Commands])
87		)
88		; atom_codes(RL,RealLine),
89		add_error(smtlib2_cli,'Parser error on line: ',RL)
90		),
91		smtlib2_repl(EnvOut).