smtlib2_cli

read_file(Stream,Out) :-
    get_code(Stream,Code),
    read_file(Code,Stream,Out).

read_file(-1,_Stream,[]) :- !.

read_file(Code,Stream,[Code|L]) :-
    read_file(Stream,L).

repl_help :-
    format_with_colour(user_output,[blue],'Starting SMTLIB REPL~n',[]),
    format_with_colour(user_output,[blue],'Available commands:~n',[]),
    format_with_colour(user_output,[blue],' (get-model)~n',[]),
    format_with_colour(user_output,[blue],' (check-sat)~n',[]),
    format_with_colour(user_output,[blue],' (set-info I Val)~n',[]),
    format_with_colour(user_output,[blue],' (push Num)~n',[]),
    format_with_colour(user_output,[blue],' (pop Num)~n',[]),
    format_with_colour(user_output,[blue],' (assert Term)~n',[]),
    format_with_colour(user_output,[blue],' (reset)~n',[]),
    format_with_colour(user_output,[blue],' (exit)~n',[]),
    format_with_colour(user_output,[blue],' define-fun, declare-sort,....~n~n',[]).

smtlib2_file(Filename) :- smtlib2_file(Filename,[]).

smtlib2_file(Filename,Options) :-
    debug_println(10,processing_smt_file(Filename)),
    % enable disprover mode to trigger modified treatment of wd conditions, etc.
    % some default preferences
    set_preference(disprover_mode,true),
    set_preference(use_clpfd_solver,true),
    set_preference(use_smt_mode,true),
   
    debug_println(25,opening(Filename)),
    open(Filename,read,S),
    read_file(S,Content),
    close(S),
    debug_println(25,parsing(Filename)),
    parse_smtlib2(Content,ListOfCommands),
    !,
    empty_env(EnvIn),
    debug_println(25,interpreting_commands(ListOfCommands)),
    catch(
    (
    interpret_l(ListOfCommands,EnvIn,EnvOut),
    (member(repl,Options)
    -> debug_println(25,finished_processing_and_starting_repl(Filename)),
    repl_help,
    smtlib2_repl(EnvOut)
    ; true)
    ),
    halt(0),
    debug_println(25,finished_processing_exit(Filename))
).

smtlib2_file(Filename,_) :-
    add_error(smtlib2_cli,'Could not process file: ',Filename).

smtlib2_repl(EnvIn) :-
    write('SMT>>>'),flush_output(user_output),
    read_line(Line),
    (Line = end_of_file -> halt(0)
    ; append(RealLine,".",Line) -> true
    ; RealLine = Line
    ),
    (parse_smtlib2(RealLine,Commands)
    -> (interpret_l(Commands,EnvIn,EnvOut) -> true
    ; format_with_colour(user_output,[red],'Could not process SMT commands: ~w~n',[Commands])
    )
    ; atom_codes(RL,RealLine),
    add_error(smtlib2_cli,'Parser error on line: ',RL)
    ),
    smtlib2_repl(EnvOut).