smtlib2_interpreter

add_error_if_result_unexpected(unknown) :- % in non-strict mode: no message, we simple failed to establish a result
    get_preference(strict_raise_warnings,false),!.

add_error_if_result_unexpected(Actual) :-
    expected_result(Expected),!,
    (Actual = Expected -> true
    ; Expected = unknown -> true
    ; Actual = unknown ->
    add_warning(smtlib2_interpreter,'Result unknown; could not establish expected result: ',Expected)
    ; add_error(smtlib2_interpreter, 'Actual result differs from expected result: ','/='(Actual,Expected))).

add_error_if_result_unexpected(_). % no expected result stored

compare_prob_cdclt_results(no_solution_found(_), contradiction_found) :-
    !.

compare_prob_cdclt_results(solution(_), CdcltFullResult) :-
    functor(CdcltFullResult, Functor, 1),
    Functor == solution,
    !.

compare_prob_cdclt_results(ProBResult, CdcltFullResult) :-
    (ProBResult == unknown; ProBResult == time_out),
    CdcltFullResult == time_out,!.

create_set_term(Name,deferred_set(none,Name)).

interpret(exit,E,E) :- !, throw(halt(0)).

interpret(reset,_,E) :- !, empty_env(E).

interpret(set_logic(_X),E,E) :- !,
    % TODO: only accept supported logics.
    true.

interpret(set_info(X),E,E) :- !,
    set_info(X).

interpret(declare_fun(Id,[],sort('Array',[Index,Element])),EIn,EOut) :- !,
    smt_type_to_prob_type(Index,EIn,BIndex),
    smt_type_to_prob_type(Element,EIn,BElement),
    FullType = set(couple(BIndex,BElement)),
    add_identifier(EIn,Id,FullType,ETemp),
    % however, an array is a partial function. thus, we have to add a constraint
    typing_constraint(svar(Id,sort('Array',[Index,Element])),AdditionalConstraint),
    add_assertion(ETemp,AdditionalConstraint,EOut).

interpret(declare_fun(Id,[],sort('BitVec',[Length])),EIn,EOut) :- !,
    FullType = set(couple(integer,integer)),
    add_identifier(EIn,Id,FullType,ETemp),
    % however, an array is a partial function. thus, we have to add a constraint
    typing_constraint(svar(Id,sort('BitVec',[Length])),AdditionalConstraint),
    add_assertion(ETemp,AdditionalConstraint,EOut).

interpret(declare_fun(Id,[],Type),EIn,EOut) :- !,
    smt_type_to_prob_type(Type,EIn,BType),
    add_identifier(EIn,Id,BType,EOut).

interpret(declare_fun(Id,Params,Return),EIn,EOut) :- !,
    maplist(smt_type_to_prob_type_maplist(EIn),Params,BParams),
    smt_type_to_prob_type(Return,EIn,BReturn),
    couplise_list(BParams,BParamsCoupled),
    Fulltype = set(couple(BParamsCoupled,BReturn)),
    add_identifier(EIn,Id,Fulltype,ETemp),
    is_function_constraint(Id,Fulltype,Constraint),
    add_assertion(ETemp,Constraint,EOut).

interpret(declare_sort(Name,0),EIn,EOut) :- !,
    add_custom_type(EIn,Name,EOut).

interpret(define_fun(ID,Params,Return,Definition),EIn,EOut) :- !,
    smt_type_to_prob_type(Return,EIn,BReturn),
    maplist(smt_term_to_prob_term_maplist(EIn),Params,BParams),
    create_local_env(EIn,BParams,LocalEnv),
    smt_term_to_prob_term(Definition,LocalEnv,BDefinition),
    add_function(EIn,ID,BParams,BReturn,BDefinition,EOut).

interpret(assert(Term),EIn,EOut) :- !,
    smt_term_to_prob_term(Term,EIn,BTerm),
    bool_to_pred(BTerm,PredBTerm),
    add_assertion(EIn,PredBTerm,EOut).

interpret(push(Num),EIn,EOut) :- !,
    push_assertion_stack(EIn,Num,EOut).

interpret(pop(Num),EIn,EOut) :- !,
    pop_assertion_stack(EIn,Num,EOut).

interpret(set_option(Opt),EIn,EOut) :- !,
    format('Ignoring set_option(~w) !~n',[Opt]), EOut=EIn.

interpret(check_sat,E,E) :- !,
    get_assertions(E,BTerms),
    get_custom_types(E,CT),
    conjunct_predicates(BTerms,Assertions),
    QuantifiedAssertions = Assertions,
    load_sets_for_cbc(CT), % will set animation minor mode to event_b
    unset_animation_minor_modes(_),
    start_animation,
    start_ms_timer(TimerProB),
    my_solve_predicate(QuantifiedAssertions,FullResult),
    stop_ms_timer(TimerProB),!,
    % CDCL(T) benchmarks
    %statistics(walltime, [TimerCdcltStart|_]),
    %cdclt_solve_predicate(QuantifiedAssertions,CdcltFullResult),
    %statistics(walltime, [TimerCdcltStop|_]),!,
    %( compare_prob_cdclt_results(FullResult, CdcltFullResult)
    %; add_error(smtlib2_interpreter, 'Result of CDCL(T) differs from ProB: ', [FullResult,CdcltFullResult])
    %),
    %WalltimeCdclt is TimerCdcltStop - TimerCdcltStart,
    %nl,print(State),nl,
    %format('CDCL(T) Solver walltime: ~d ms~n', [WalltimeCdclt]),
    format('ProB result:~n', []), print_prob_result(FullResult),
    %format('CDCL(T) result: ~w~n', [CdcltFullResult]),
    try_provers(FullResult,E,QuantifiedAssertions).

interpret(get_model,E,E) :- !, print_model(E). % this command is not part of the smtlib2 language anymore

interpret(X,_,_) :- !, format('Not supported by SMT intepreter: ~w~n',[X]),fail.

interpret_l([],Env,Env).

interpret_l([H|T],EnvIn,EnvOut) :-
    interpret(H,EnvIn,EnvT),
    interpret_l(T,EnvT,EnvOut).

load_sets_for_cbc(Sets) :-
    remove_dups(Sets,SetOfSets),
    load_sets_for_cbc_aux(SetOfSets).

load_sets_for_cbc_aux([]) :-
    load_event_b_project([],[event_b_context(none,'CBCSets',[])],[exporter_version(3)],[]), !.

load_sets_for_cbc_aux(SetOfSets) :-
    maplist(create_set_term,SetOfSets,SetTerms),
    load_event_b_project([],[event_b_context(none,'CBCSets',[sets(none,SetTerms)])],[exporter_version(3)],[]).

my_solve_predicate(Pred,FullResult) :-
    %strip_outer_exists(Pred,NewPred), % can be useful in improving solving performance, e.g., public_examples/SMT/QF_IDL/queens_bench/n_queen/queen3-1.smt2
    TimeoutFactor = 4,
    (get_preference(smtlib2b_cleanup_predicate,true)
    -> clean_up(Pred,[],CPred) % can for the moment be very expensive !! e.g. for public_examples/SMT/QF_IDL/mathsat/fischer/FISCHER3-2-ninc.smt2 and so on
    %,bsyntaxtree:check_ast(CPred)
    ; CPred = Pred
    ),
    (debug_mode(on)
    -> print('Solving predicate: '),nl, nested_print_bexpr(CPred),nl ; true),
    solve_predicate(CPred,_State,TimeoutFactor,FullResult).

print_binding(E,binding(V,_,PP)) :-
    get_type(V,E,Type),
    type_for_print(Type,TypeForPrint),
    format('(define-fun ~w () ~w ~w)~n',[V,TypeForPrint,PP]).

print_model(E) :-
    stored_model(M), !,
    print('(model'), nl,
    maplist(print_binding(E),M),
    print(')'), nl.

print_model(_) :- write('no model generated\n').

print_prob_binding(binding(ID,_Val,VS)) :- !, format(' ~w = ~w ~n',[ID,VS]).

print_prob_binding(X) :- format(' ~w ',[X]).

print_prob_result(solution(L)) :- !,maplist(print_prob_binding,L),nl.

print_prob_result(S) :- print(S),nl.

set_attribute('smt-lib-version',decimal(2.0)) :- !.

set_attribute('smt-lib-version',decimal(2.5)) :- !.

set_attribute('smt-lib-version',decimal(2.6)) :- !.

set_attribute(category,string(_S)) :- !.

set_attribute(notes,string(_S)) :- !.

set_attribute(status,S) :- !, nonvar(S),
    memberchk(S,[unknown,sat,unsat]),
    retractall(expected_result(_)),
    assertz(expected_result(S)).

set_attribute(source,string(_S)) :- !.

set_attribute(A,V) :- !,
    format('missing in set_attribute: ~w to ~w~n',[A,V]), fail.

set_info(attribute(A,V)) :- !,
    set_attribute(A,V).

set_info(X) :- !, format('missing in set_info: ~w~n',[X]), fail.

try_provers(solution(S),E,_) :- !,
    assertz(stored_model(S)),
    (debug_mode(on) -> print_model(E) ; true),
    add_error_if_result_unexpected(sat),
    write('sat\n').

try_provers(contradiction_found,_,_) :- !, add_error_if_result_unexpected(unsat), write('unsat\n').

try_provers(_,_,Assertions) :-
    get_preference(try_atb_provers,true),
    % we suspect that the solver failed to identify a contradiction
    % disprove predicate might fail, i.e. if the provers are not installed
    debug_println(20,'Trying to run Atelier-B provers'),
    disprove_predicate(Assertions,Result),!,
    write_final_result(Result).

try_provers(_,_,_) :- add_error_if_result_unexpected(unknown), write('unknown\n').

type_for_print(integer,'Int') :- !.

type_for_print(X,X).

write_final_result(proved) :- add_error_if_result_unexpected(unsat), write('unsat\n').

write_final_result(_) :- add_error_if_result_unexpected(unknown), write('unknown\n').