| 1 | % (c) 2014-2022 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_interpreter,[interpret_l/3]). | |
| 6 | ||
| 7 | :- use_module(probsrc(module_information),[module_info/2]). | |
| 8 | :- module_info(group,smtlib). | |
| 9 | :- module_info(description,'The SMT-LIB 2 Interpreter - Main Interpreter'). | |
| 10 | ||
| 11 | :- use_module(library(lists)). | |
| 12 | ||
| 13 | %:- use_module(cdclt_solver('cdclt_solver'), [cdclt_solve_predicate/2]). | |
| 14 | :- use_module(probsrc(solver_interface), [solve_predicate/4]). | |
| 15 | :- use_module(extrasrc(atelierb_provers_interface), [disprove_predicate/2]). | |
| 16 | :- use_module(probsrc(bsyntaxtree), [conjunct_predicates/2]). | |
| 17 | :- use_module(probsrc(btypechecker), [couplise_list/2]). | |
| 18 | :- use_module(probsrc(prob2_interface), [load_event_b_project/4, start_animation/0]). | |
| 19 | :- use_module(probsrc(translate), [nested_print_bexpr/1]). | |
| 20 | :- use_module(smtlib_solver(smtlib2_environment)). | |
| 21 | :- use_module(smtlib_solver(smtlib2_translation)). | |
| 22 | :- use_module(probsrc(tools),[start_ms_timer/1, stop_ms_timer/1]). | |
| 23 | :- use_module(probsrc(error_manager), [add_error/3, add_warning/3]). | |
| 24 | :- use_module(probsrc(preferences), [get_preference/2]). | |
| 25 | :- use_module(probsrc(debug), [debug_println/2, debug_mode/1]). | |
| 26 | :- use_module(probsrc(specfile), [unset_animation_minor_modes/1]). | |
| 27 | ||
| 28 | :- dynamic expected_result/1. | |
| 29 | :- volatile expected_result/1. | |
| 30 | ||
| 31 | interpret_l([],Env,Env). | |
| 32 | interpret_l([H|T],EnvIn,EnvOut) :- | |
| 33 | interpret(H,EnvIn,EnvT), | |
| 34 | interpret_l(T,EnvT,EnvOut). | |
| 35 | ||
| 36 | interpret(exit,E,E) :- !, throw(halt(0)). | |
| 37 | interpret(reset,_,E) :- !, empty_env(E). | |
| 38 | interpret(set_logic(_X),E,E) :- !, | |
| 39 | % TODO: only accept supported logics. | |
| 40 | true. | |
| 41 | interpret(set_info(X),E,E) :- !, | |
| 42 | set_info(X). | |
| 43 | % special case for array logics, sets up an additional constraint | |
| 44 | interpret(declare_fun(Id,[],sort('Array',[Index,Element])),EIn,EOut) :- !, | |
| 45 | smt_type_to_prob_type(Index,EIn,BIndex), | |
| 46 | smt_type_to_prob_type(Element,EIn,BElement), | |
| 47 | FullType = set(couple(BIndex,BElement)), | |
| 48 | add_identifier(EIn,Id,FullType,ETemp), | |
| 49 | % however, an array is a partial function. thus, we have to add a constraint | |
| 50 | typing_constraint(svar(Id,sort('Array',[Index,Element])),AdditionalConstraint), | |
| 51 | add_assertion(ETemp,AdditionalConstraint,EOut). | |
| 52 | % special case for bit vectors, sets up an additional constraint | |
| 53 | interpret(declare_fun(Id,[],sort('BitVec',[Length])),EIn,EOut) :- !, | |
| 54 | FullType = set(couple(integer,integer)), | |
| 55 | add_identifier(EIn,Id,FullType,ETemp), | |
| 56 | % however, an array is a partial function. thus, we have to add a constraint | |
| 57 | typing_constraint(svar(Id,sort('BitVec',[Length])),AdditionalConstraint), | |
| 58 | add_assertion(ETemp,AdditionalConstraint,EOut). | |
| 59 | interpret(declare_fun(Id,[],Type),EIn,EOut) :- !, | |
| 60 | smt_type_to_prob_type(Type,EIn,BType), | |
| 61 | add_identifier(EIn,Id,BType,EOut). | |
| 62 | interpret(declare_fun(Id,Params,Return),EIn,EOut) :- !, | |
| 63 | maplist(smt_type_to_prob_type_maplist(EIn),Params,BParams), | |
| 64 | smt_type_to_prob_type(Return,EIn,BReturn), | |
| 65 | couplise_list(BParams,BParamsCoupled), | |
| 66 | Fulltype = set(couple(BParamsCoupled,BReturn)), | |
| 67 | add_identifier(EIn,Id,Fulltype,ETemp), | |
| 68 | is_function_constraint(Id,Fulltype,Constraint), | |
| 69 | add_assertion(ETemp,Constraint,EOut). | |
| 70 | interpret(declare_sort(Name,0),EIn,EOut) :- !, | |
| 71 | add_custom_type(EIn,Name,EOut). | |
| 72 | interpret(define_fun(ID,Params,Return,Definition),EIn,EOut) :- !, | |
| 73 | smt_type_to_prob_type(Return,EIn,BReturn), | |
| 74 | maplist(smt_term_to_prob_term_maplist(EIn),Params,BParams), | |
| 75 | create_local_env(EIn,BParams,LocalEnv), | |
| 76 | smt_term_to_prob_term(Definition,LocalEnv,BDefinition), | |
| 77 | add_function(EIn,ID,BParams,BReturn,BDefinition,EOut). | |
| 78 | interpret(assert(Term),EIn,EOut) :- !, | |
| 79 | smt_term_to_prob_term(Term,EIn,BTerm), | |
| 80 | bool_to_pred(BTerm,PredBTerm), | |
| 81 | add_assertion(EIn,PredBTerm,EOut). | |
| 82 | interpret(push(Num),EIn,EOut) :- !, | |
| 83 | push_assertion_stack(EIn,Num,EOut). | |
| 84 | interpret(pop(Num),EIn,EOut) :- !, | |
| 85 | pop_assertion_stack(EIn,Num,EOut). | |
| 86 | interpret(set_option(Opt),EIn,EOut) :- !, | |
| 87 | format('Ignoring set_option(~w) !~n',[Opt]), EOut=EIn. | |
| 88 | interpret(check_sat,E,E) :- !, | |
| 89 | get_assertions(E,BTerms), | |
| 90 | get_custom_types(E,CT), | |
| 91 | conjunct_predicates(BTerms,Assertions), | |
| 92 | QuantifiedAssertions = Assertions, | |
| 93 | load_sets_for_cbc(CT), % will set animation minor mode to event_b | |
| 94 | unset_animation_minor_modes(_), | |
| 95 | start_animation, | |
| 96 | start_ms_timer(TimerProB), | |
| 97 | my_solve_predicate(QuantifiedAssertions,FullResult), | |
| 98 | stop_ms_timer(TimerProB),!, | |
| 99 | % CDCL(T) benchmarks | |
| 100 | %statistics(walltime, [TimerCdcltStart|_]), | |
| 101 | %cdclt_solve_predicate(QuantifiedAssertions,CdcltFullResult), | |
| 102 | %statistics(walltime, [TimerCdcltStop|_]),!, | |
| 103 | %( compare_prob_cdclt_results(FullResult, CdcltFullResult) | |
| 104 | %; add_error(smtlib2_interpreter, 'Result of CDCL(T) differs from ProB: ', [FullResult,CdcltFullResult]) | |
| 105 | %), | |
| 106 | %WalltimeCdclt is TimerCdcltStop - TimerCdcltStart, | |
| 107 | %nl,print(State),nl, | |
| 108 | %format('CDCL(T) Solver walltime: ~d ms~n', [WalltimeCdclt]), | |
| 109 | format('ProB result:~n', []), print_prob_result(FullResult), | |
| 110 | %format('CDCL(T) result: ~w~n', [CdcltFullResult]), | |
| 111 | try_provers(FullResult,E,QuantifiedAssertions). | |
| 112 | interpret(get_model,E,E) :- !, print_model(E). % this command is not part of the smtlib2 language anymore | |
| 113 | interpret(X,_,_) :- !, format('Not supported by SMT intepreter: ~w~n',[X]),fail. | |
| 114 | ||
| 115 | load_sets_for_cbc(Sets) :- | |
| 116 | remove_dups(Sets,SetOfSets), | |
| 117 | load_sets_for_cbc_aux(SetOfSets). | |
| 118 | %initialise_specification. % now has to be called afterwards | |
| 119 | load_sets_for_cbc_aux([]) :- | |
| 120 | load_event_b_project([],[event_b_context(none,'CBCSets',[])],[exporter_version(3)],[]), !. | |
| 121 | load_sets_for_cbc_aux(SetOfSets) :- | |
| 122 | maplist(create_set_term,SetOfSets,SetTerms), | |
| 123 | load_event_b_project([],[event_b_context(none,'CBCSets',[sets(none,SetTerms)])],[exporter_version(3)],[]). | |
| 124 | ||
| 125 | create_set_term(Name,deferred_set(none,Name)). | |
| 126 | ||
| 127 | print_prob_result(solution(L)) :- !,maplist(print_prob_binding,L),nl. | |
| 128 | print_prob_result(S) :- print(S),nl. | |
| 129 | print_prob_binding(binding(ID,_Val,VS)) :- !, format(' ~w = ~w ~n',[ID,VS]). | |
| 130 | print_prob_binding(X) :- format(' ~w ',[X]). | |
| 131 | ||
| 132 | :- use_module(probsrc(b_ast_cleanup), [clean_up/3]). | |
| 133 | %:- use_module(probsrc(solver_interface), [strip_outer_exists/2]). | |
| 134 | my_solve_predicate(Pred,FullResult) :- | |
| 135 | %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 | |
| 136 | TimeoutFactor = 4, | |
| 137 | (get_preference(smtlib2b_cleanup_predicate,true) | |
| 138 | -> 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 | |
| 139 | %,bsyntaxtree:check_ast(CPred) | |
| 140 | ; CPred = Pred | |
| 141 | ), | |
| 142 | (debug_mode(on) | |
| 143 | -> print('Solving predicate: '),nl, nested_print_bexpr(CPred),nl ; true), | |
| 144 | solve_predicate(CPred,_State,TimeoutFactor,FullResult). | |
| 145 | ||
| 146 | :- public compare_prob_cdclt_results/2. % for debugging | |
| 147 | compare_prob_cdclt_results(no_solution_found(_), contradiction_found) :- | |
| 148 | !. | |
| 149 | % CdcltFullResult == contradiction_found; CdcltFullResult == time_out. | |
| 150 | compare_prob_cdclt_results(solution(_), CdcltFullResult) :- | |
| 151 | functor(CdcltFullResult, Functor, 1), | |
| 152 | Functor == solution, | |
| 153 | !. | |
| 154 | compare_prob_cdclt_results(ProBResult, CdcltFullResult) :- | |
| 155 | (ProBResult == unknown; ProBResult == time_out), | |
| 156 | CdcltFullResult == time_out,!. | |
| 157 | ||
| 158 | try_provers(solution(S),E,_) :- !, | |
| 159 | assertz(stored_model(S)), | |
| 160 | (debug_mode(on) -> print_model(E) ; true), | |
| 161 | add_error_if_result_unexpected(sat), | |
| 162 | write('sat\n'). | |
| 163 | try_provers(contradiction_found,_,_) :- !, add_error_if_result_unexpected(unsat), write('unsat\n'). | |
| 164 | try_provers(_,_,Assertions) :- | |
| 165 | get_preference(try_atb_provers,true), | |
| 166 | % we suspect that the solver failed to identify a contradiction | |
| 167 | % disprove predicate might fail, i.e. if the provers are not installed | |
| 168 | debug_println(20,'Trying to run Atelier-B provers'), | |
| 169 | disprove_predicate(Assertions,Result),!, | |
| 170 | write_final_result(Result). | |
| 171 | try_provers(_,_,_) :- add_error_if_result_unexpected(unknown), write('unknown\n'). | |
| 172 | ||
| 173 | write_final_result(proved) :- add_error_if_result_unexpected(unsat), write('unsat\n'). | |
| 174 | write_final_result(_) :- add_error_if_result_unexpected(unknown), write('unknown\n'). | |
| 175 | ||
| 176 | add_error_if_result_unexpected(unknown) :- % in non-strict mode: no message, we simple failed to establish a result | |
| 177 | get_preference(strict_raise_warnings,false),!. | |
| 178 | add_error_if_result_unexpected(Actual) :- | |
| 179 | expected_result(Expected),!, | |
| 180 | (Actual = Expected -> true | |
| 181 | ; Expected = unknown -> true | |
| 182 | ; Actual = unknown -> | |
| 183 | add_warning(smtlib2_interpreter,'Result unknown; could not establish expected result: ',Expected) | |
| 184 | ; add_error(smtlib2_interpreter, 'Actual result differs from expected result: ','/='(Actual,Expected))). | |
| 185 | add_error_if_result_unexpected(_). % no expected result stored | |
| 186 | ||
| 187 | :- dynamic stored_model/1. | |
| 188 | ||
| 189 | print_binding(E,binding(V,_,PP)) :- | |
| 190 | get_type(V,E,Type), | |
| 191 | type_for_print(Type,TypeForPrint), | |
| 192 | format('(define-fun ~w () ~w ~w)~n',[V,TypeForPrint,PP]). | |
| 193 | print_model(E) :- | |
| 194 | stored_model(M), !, | |
| 195 | print('(model'), nl, | |
| 196 | maplist(print_binding(E),M), | |
| 197 | print(')'), nl. | |
| 198 | print_model(_) :- write('no model generated\n'). | |
| 199 | ||
| 200 | type_for_print(integer,'Int') :- !. | |
| 201 | type_for_print(X,X). | |
| 202 | ||
| 203 | set_info(attribute(A,V)) :- !, | |
| 204 | set_attribute(A,V). | |
| 205 | set_info(X) :- !, format('missing in set_info: ~w~n',[X]), fail. | |
| 206 | ||
| 207 | ||
| 208 | set_attribute('smt-lib-version',decimal(2.0)) :- !. | |
| 209 | set_attribute('smt-lib-version',decimal(2.5)) :- !. | |
| 210 | set_attribute('smt-lib-version',decimal(2.6)) :- !. | |
| 211 | set_attribute(category,string(_S)) :- !. | |
| 212 | set_attribute(notes,string(_S)) :- !. | |
| 213 | set_attribute(status,S) :- !, nonvar(S), | |
| 214 | memberchk(S,[unknown,sat,unsat]), | |
| 215 | retractall(expected_result(_)), | |
| 216 | assertz(expected_result(S)). | |
| 217 | set_attribute(source,string(_S)) :- !. | |
| 218 | set_attribute(A,V) :- !, | |
| 219 | format('missing in set_attribute: ~w to ~w~n',[A,V]), fail. |