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). |