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_cli,[smtlib2_file/1, smtlib2_file/2, get_smtlib2_result_infos/1]).
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		smtlib2_file(Filename,Content,Options).
43		smtlib2_file(Filename,_) :-
44		add_error(smtlib2_cli,'Could not read SMTLib file: ',Filename).
45
46		smtlib2_file(Filename,Content,Options) :-
47		debug_println(25,parsing(Filename)),
48		parse_smtlib2(Content,ListOfCommands),
49		!,
50		empty_env(EnvIn),
51		debug_println(25,interpreting_commands(ListOfCommands)),
52		catch(
53		(
54		interpret_l(ListOfCommands,EnvIn,EnvOut),
55		(member(repl,Options)
56		-> debug_println(25,finished_processing_and_starting_repl(Filename)),
57		repl_help,
58		smtlib2_repl(EnvOut)
59		; true)
60		),
61		halt(0),
62		debug_println(25,finished_processing_exit(Filename))
63		).
64		smtlib2_file(Filename,_,_) :-
65		add_error(smtlib2_cli,'Could not parse SMTLib file: ',Filename).
66
67		:- use_module(probsrc(tools_printing),[format_with_colour/4]).
68
69		repl_help :-
70		format_with_colour(user_output,[blue],'Starting SMTLIB REPL~n',[]),
71		format_with_colour(user_output,[blue],'Available commands:~n',[]),
72		format_with_colour(user_output,[blue],' (get-model)~n',[]),
73		format_with_colour(user_output,[blue],' (check-sat)~n',[]),
74		format_with_colour(user_output,[blue],' (set-info I Val)~n',[]),
75		format_with_colour(user_output,[blue],' (push Num)~n',[]),
76		format_with_colour(user_output,[blue],' (pop Num)~n',[]),
77		format_with_colour(user_output,[blue],' (assert Term)~n',[]),
78		format_with_colour(user_output,[blue],' (reset)~n',[]),
79		format_with_colour(user_output,[blue],' (exit)~n',[]),
80		format_with_colour(user_output,[blue],' define-fun, declare-sort,....~n~n',[]).
81
82		smtlib2_repl(EnvIn) :-
83		write('SMT>>>'),flush_output(user_output),
84		read_line(Line),
85		(Line = end_of_file -> halt(0)
86		; append(RealLine,".",Line) -> true
87		; RealLine = Line
88		),
89		(parse_smtlib2(RealLine,Commands)
90		-> (interpret_l(Commands,EnvIn,EnvOut) -> true
91		; format_with_colour(user_output,[red],'Could not process SMT commands: ~w~n',[Commands])
92		)
93		; atom_codes(RL,RealLine),
94		add_error(smtlib2_cli,'Parser error on line: ',RL)
95		),
96		smtlib2_repl(EnvOut).
97
98
99
100		% get result in format for accumulate_infos of prob_cli
101		get_smtlib2_result_infos([lines-L,sat-S,unsat-U,unknown-UK]) :-
102		smtlib2_result(Res),!, get_smtlib_lines_read(L),
103		(Res = sat -> S=1,U=0,UK=0
104		; Res=unsat -> S=0, U=1, UK=0
105		; UK=1, S=0, U=0).
106		get_smtlib2_result_infos([lines-L,sat-0,unsat-0,unknown-0]) :- get_smtlib_lines_read(L).