1		% (c) 2014-2015 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]).
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		read_file(Stream,Out) :-
20		get_code(Stream,Code),
21		read_file(Code,Stream,Out).
22		read_file(-1,_Stream,[]) :- !.
23		read_file(Code,Stream,[Code|L]) :-
24		read_file(Stream,L).
25
26		smtlib2_file(Filename) :-
27		debug_println(10,processing_smt_file(Filename)),
28		% enable disprover mode to trigger modified treatment of wd conditions, etc.
29		% some default preferences
30		set_preference(disprover_mode,true),
31		set_preference(use_clpfd_solver,true),
32		set_preference(use_smt_mode,true),
33
34		debug_println(25,opening(Filename)),nl,
35		open(Filename,read,S),
36		read_file(S,Content),
37		close(S),
38		debug_println(25,parsing(Filename)),nl,
39		parse_smtlib2(Content,ListOfCommands),
40		!,
41		empty_env(EnvIn),
42		debug_println(25,interpreting_commands(ListOfCommands)),
43		on_exception(halt(0),
44		(interpret_l(ListOfCommands,EnvIn,EnvOut),
45		debug_println(25,finished_processing_and_starting_repl(Filename)),
46		smtlib2_repl(EnvOut)),
47		debug_println(25,finished_processing_exit(Filename))).
48		smtlib2_file(Filename) :-
49		add_error(smtlib2_cli,'Could not process file: ',Filename).
50
51		smtlib2_repl(EnvIn) :-
52		read_line(Line),
53		(Line = end_of_file -> halt(0) ; append(RealLine,".",Line)),
54		(parse_smtlib2(RealLine,Commands)
55		-> interpret_l(Commands,EnvIn,EnvOut)
56		; add_error(smtlib2_cli,'Parser error on line: ',RealLine)
57		),
58		smtlib2_repl(EnvOut).