| 1 | % (c) 2014-2026 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, smtlib2_result/1]). | |
| 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(tools_strings),[ajoin/2]). | |
| 24 | :- use_module(probsrc(error_manager), [add_error/3, add_warning/3, add_message/3]). | |
| 25 | :- use_module(probsrc(preferences), [get_preference/2]). | |
| 26 | :- use_module(probsrc(debug), [debug_println/2, debug_mode/1]). | |
| 27 | :- use_module(probsrc(specfile), [unset_animation_minor_modes/1]). | |
| 28 | ||
| 29 | :- dynamic expected_result/1. | |
| 30 | :- volatile expected_result/1. | |
| 31 | ||
| 32 | interpret_l([],Env,Env). | |
| 33 | interpret_l([H|T],EnvIn,EnvOut) :- | |
| 34 | (interpret(H,EnvIn,EnvT) -> true | |
| 35 | ; add_error(smtlib2_interpreter,'SMTLib command failed: ',H), | |
| 36 | EnvT=EnvIn), | |
| 37 | interpret_l(T,EnvT,EnvOut). | |
| 38 | ||
| 39 | interpret(exit,E,E) :- !, throw(halt(0)). % is caught in smtlib2_file | |
| 40 | interpret(reset,_,E) :- !, empty_env(E). | |
| 41 | interpret(set_logic(_X),E,E) :- !, | |
| 42 | % TODO: only accept supported logics. | |
| 43 | true. | |
| 44 | interpret(set_info(X),E,E) :- !, | |
| 45 | set_info(X). | |
| 46 | % special case for array logics, sets up an additional constraint | |
| 47 | interpret(declare_fun(Id,[],sort('Array',[Index,Element])),EIn,EOut) :- !, | |
| 48 | smt_type_to_prob_type(Index,EIn,BIndex), | |
| 49 | smt_type_to_prob_type(Element,EIn,BElement), | |
| 50 | FullType = set(couple(BIndex,BElement)), | |
| 51 | add_identifier(EIn,Id,FullType,ETemp), | |
| 52 | % however, an array is a partial function. thus, we have to add a constraint | |
| 53 | typing_constraint(svar(Id,sort('Array',[Index,Element])),AdditionalConstraint), | |
| 54 | add_assertion(ETemp,AdditionalConstraint,EOut). | |
| 55 | % special case for bit vectors, sets up an additional constraint | |
| 56 | interpret(declare_fun(Id,[],sort('BitVec',[Length])),EIn,EOut) :- !, | |
| 57 | FullType = set(couple(integer,integer)), | |
| 58 | add_identifier(EIn,Id,FullType,ETemp), | |
| 59 | % however, an array is a partial function. thus, we have to add a constraint | |
| 60 | typing_constraint(svar(Id,sort('BitVec',[Length])),AdditionalConstraint), | |
| 61 | add_assertion(ETemp,AdditionalConstraint,EOut). | |
| 62 | interpret(declare_fun(Id,[],Type),EIn,EOut) :- !, | |
| 63 | smt_type_to_prob_type(Type,EIn,BType), | |
| 64 | add_identifier(EIn,Id,BType,EOut). | |
| 65 | interpret(declare_fun(Id,Params,Return),EIn,EOut) :- !, | |
| 66 | maplist(smt_type_to_prob_type_maplist(EIn),Params,BParams), | |
| 67 | smt_type_to_prob_type(Return,EIn,BReturn), | |
| 68 | couplise_list(BParams,BParamsCoupled), | |
| 69 | Fulltype = set(couple(BParamsCoupled,BReturn)), | |
| 70 | add_identifier(EIn,Id,Fulltype,ETemp), | |
| 71 | is_function_constraint(Id,Fulltype,Constraint), | |
| 72 | add_assertion(ETemp,Constraint,EOut). | |
| 73 | interpret(declare_sort(Name,0),EIn,EOut) :- !, | |
| 74 | add_custom_type(EIn,Name,EOut). | |
| 75 | interpret(define_fun(ID,Params,Return,Definition),EIn,EOut) :- !, | |
| 76 | smt_type_to_prob_type(Return,EIn,BReturn), | |
| 77 | maplist(smt_term_to_prob_term_maplist(EIn),Params,BParams), | |
| 78 | create_local_env(EIn,BParams,LocalEnv), | |
| 79 | smt_term_to_prob_term(Definition,LocalEnv,BDefinition), | |
| 80 | add_function(EIn,ID,BParams,BReturn,BDefinition,EOut). | |
| 81 | interpret(assert(Term),EIn,EOut) :- !, | |
| 82 | smt_term_to_prob_term(Term,EIn,BTerm), | |
| 83 | bool_to_pred(BTerm,PredBTerm), | |
| 84 | add_assertion(EIn,PredBTerm,EOut). | |
| 85 | interpret(push(Num),EIn,EOut) :- !, | |
| 86 | push_assertion_stack(EIn,Num,EOut). | |
| 87 | interpret(pop(Num),EIn,EOut) :- !, | |
| 88 | pop_assertion_stack(EIn,Num,EOut). | |
| 89 | interpret(set_option(Opt),EIn,EOut) :- !, | |
| 90 | format('Ignoring set_option(~w) !~n',[Opt]), EOut=EIn. | |
| 91 | interpret(check_sat,E,E) :- !, | |
| 92 | get_assertions(E,BTerms), | |
| 93 | get_custom_types(E,CT), | |
| 94 | conjunct_predicates(BTerms,Assertions), | |
| 95 | QuantifiedAssertions = Assertions, | |
| 96 | load_sets_for_cbc(CT), % will set animation minor mode to event_b | |
| 97 | unset_animation_minor_modes(_), | |
| 98 | start_animation, | |
| 99 | start_ms_timer(TimerProB), | |
| 100 | (my_solve_predicate(QuantifiedAssertions,FullResult) | |
| 101 | -> stop_ms_timer(TimerProB), | |
| 102 | % CDCL(T) benchmarks | |
| 103 | %statistics(walltime, [TimerCdcltStart|_]), | |
| 104 | %cdclt_solve_predicate(QuantifiedAssertions,CdcltFullResult), | |
| 105 | %statistics(walltime, [TimerCdcltStop|_]),!, | |
| 106 | %( compare_prob_cdclt_results(FullResult, CdcltFullResult) | |
| 107 | %; add_error(smtlib2_interpreter, 'Result of CDCL(T) differs from ProB: ', [FullResult,CdcltFullResult]) | |
| 108 | %), | |
| 109 | %WalltimeCdclt is TimerCdcltStop - TimerCdcltStart, | |
| 110 | %nl,print(State),nl, | |
| 111 | %format('CDCL(T) Solver walltime: ~d ms~n', [WalltimeCdclt]), | |
| 112 | format('ProB result:~n', []), print_prob_result(FullResult), | |
| 113 | %format('CDCL(T) result: ~w~n', [CdcltFullResult]), | |
| 114 | try_provers(FullResult,E,QuantifiedAssertions) | |
| 115 | ; stop_ms_timer(TimerProB), | |
| 116 | add_error(smtlib2_interpreter,'Solving failed:',QuantifiedAssertions) | |
| 117 | ). | |
| 118 | interpret(get_model,E,E) :- !, print_model(E). % this command is not part of the smtlib2 language anymore | |
| 119 | interpret(get_value(IDList),E,E) :- !, get_model_values(IDList,E). | |
| 120 | interpret(X,_,_) :- !, format('Not supported by SMT intepreter: ~w~n',[X]),fail. | |
| 121 | ||
| 122 | load_sets_for_cbc(Sets) :- | |
| 123 | remove_dups(Sets,SetOfSets), | |
| 124 | load_sets_for_cbc_aux(SetOfSets). | |
| 125 | %initialise_specification. % now has to be called afterwards | |
| 126 | load_sets_for_cbc_aux([]) :- | |
| 127 | load_event_b_project([],[event_b_context(none,'CBCSets',[])],[exporter_version(3)],[]), !. | |
| 128 | load_sets_for_cbc_aux(SetOfSets) :- | |
| 129 | maplist(create_set_term,SetOfSets,SetTerms), | |
| 130 | load_event_b_project([],[event_b_context(none,'CBCSets',[sets(none,SetTerms)])],[exporter_version(3)],[]). | |
| 131 | ||
| 132 | create_set_term(Name,deferred_set(none,Name)). | |
| 133 | ||
| 134 | :- use_module(probsrc(tools_printing), [format_with_colour_nl/4]). | |
| 135 | print_prob_result(solution(L)) :- !,maplist(print_prob_binding,L). | |
| 136 | print_prob_result(contradiction_found) :- !, format_with_colour_nl(user_output,[red],' ~w',[contradiction_found]). | |
| 137 | print_prob_result(S) :- format_with_colour_nl(user_output,[orange],' ~w',[S]). | |
| 138 | print_prob_binding(binding(ID,_Val,VS)) :- !, format_with_colour_nl(user_output,[green],' ~w = ~w',[ID,VS]). | |
| 139 | print_prob_binding(X) :- format_with_colour_nl(user_output,[green],' ~w ',[X]). | |
| 140 | ||
| 141 | :- use_module(probsrc(b_ast_cleanup), [clean_up/3]). | |
| 142 | %:- use_module(probsrc(solver_interface), [strip_outer_exists/2]). | |
| 143 | my_solve_predicate(Pred,FullResult) :- | |
| 144 | %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 | |
| 145 | TimeoutFactor = 4, | |
| 146 | (get_preference(smtlib2b_cleanup_predicate,true) | |
| 147 | -> 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 | |
| 148 | %,bsyntaxtree:check_ast(CPred) | |
| 149 | % but it is required for reals ! | |
| 150 | ; CPred = Pred | |
| 151 | ), | |
| 152 | (debug_mode(on) | |
| 153 | -> print('Solving predicate: '),nl, nested_print_bexpr(CPred),nl | |
| 154 | %,bsyntaxtree:check_ast(CPred) | |
| 155 | ; true), | |
| 156 | solve_predicate(CPred,_State,TimeoutFactor,FullResult). | |
| 157 | ||
| 158 | :- public compare_prob_cdclt_results/2. % for debugging | |
| 159 | compare_prob_cdclt_results(no_solution_found(_), contradiction_found) :- | |
| 160 | !. | |
| 161 | % CdcltFullResult == contradiction_found; CdcltFullResult == time_out. | |
| 162 | compare_prob_cdclt_results(solution(_), CdcltFullResult) :- | |
| 163 | functor(CdcltFullResult, Functor, 1), | |
| 164 | Functor == solution, | |
| 165 | !. | |
| 166 | compare_prob_cdclt_results(ProBResult, CdcltFullResult) :- | |
| 167 | (ProBResult == unknown; ProBResult == time_out), | |
| 168 | CdcltFullResult == time_out,!. | |
| 169 | ||
| 170 | try_provers(solution(S),E,_) :- !, | |
| 171 | assertz(stored_model(S)), | |
| 172 | (debug_mode(on) -> print_model(E) ; true), | |
| 173 | add_error_if_result_unexpected(sat), | |
| 174 | write_smtlib_result('sat'). | |
| 175 | try_provers(contradiction_found,_,_) :- !, add_error_if_result_unexpected(unsat), | |
| 176 | write_smtlib_result('unsat'). | |
| 177 | try_provers(_,_,Assertions) :- | |
| 178 | get_preference(try_atb_provers,true), | |
| 179 | % we suspect that the solver failed to identify a contradiction | |
| 180 | % disprove predicate might fail, i.e. if the provers are not installed | |
| 181 | debug_println(20,'Trying to run Atelier-B provers'), | |
| 182 | disprove_predicate(Assertions,Result),!, | |
| 183 | write_final_result(Result). | |
| 184 | try_provers(_,_,_) :- add_error_if_result_unexpected(unknown), | |
| 185 | write_smtlib_result('unknown'). | |
| 186 | ||
| 187 | write_final_result(proved) :- add_error_if_result_unexpected(unsat), write_smtlib_result('unsat'). | |
| 188 | write_final_result(_) :- add_error_if_result_unexpected(unknown), write_smtlib_result('unknown'). | |
| 189 | ||
| 190 | :- dynamic smtlib2_result/1. | |
| 191 | ||
| 192 | :- use_module(probsrc(eventhandling),[register_event_listener/3]). | |
| 193 | :- register_event_listener(clear_specification,clear_smtlib_result, | |
| 194 | 'Reset SMTLib2 result.'). | |
| 195 | clear_smtlib_result :- retractall(smtlib2_result(_)), retractall(stored_model(_)). | |
| 196 | ||
| 197 | ||
| 198 | write_smtlib_result(Result) :- | |
| 199 | assert(smtlib2_result(Result)),nl, | |
| 200 | format('~w~n',[Result]). | |
| 201 | ||
| 202 | add_error_if_result_unexpected(Actual) :- | |
| 203 | expected_result(Expected),!, | |
| 204 | (Actual = Expected -> true | |
| 205 | ; Expected = unknown -> | |
| 206 | add_warn_or_msg('Expected result was unknown but obtained: ',Actual) | |
| 207 | ; Actual = unknown -> | |
| 208 | add_warn_or_msg('Result unknown; could not establish expected result: ',Expected) | |
| 209 | ; ajoin(['Actual result ',Actual,' differs from expected result: '],Msg), | |
| 210 | add_error(smtlib2_interpreter,Msg,Expected)). | |
| 211 | add_error_if_result_unexpected(_). % no expected result stored | |
| 212 | ||
| 213 | add_warn_or_msg(Msg,T) :- get_preference(strict_raise_warnings,false),!, | |
| 214 | add_message(smtlib2_interpreter,Msg,T). | |
| 215 | add_warn_or_msg(Msg,T) :- | |
| 216 | add_warning(smtlib2_interpreter,Msg,T). | |
| 217 | ||
| 218 | :- dynamic stored_model/1. | |
| 219 | ||
| 220 | print_binding(E,binding(V,_,PP)) :- !, | |
| 221 | (get_type(V,E,Type) -> type_for_print(Type,TypeForPrint) | |
| 222 | ; add_error(smtlib2_interpreter,'Unknown identifier in get_model:',V), | |
| 223 | TypeForPrint = '?' | |
| 224 | ), | |
| 225 | format('(define-fun ~w () ~w ~w)~n',[V,TypeForPrint,PP]). | |
| 226 | print_binding(_,B) :- add_error(smtlib2_interpreter,'Illegal binding:',B). | |
| 227 | ||
| 228 | print_model(E) :- | |
| 229 | stored_model(M), !, | |
| 230 | print('(model'), nl, | |
| 231 | maplist(print_binding(E),M), | |
| 232 | print(')'), nl. | |
| 233 | print_model(_) :- write('no model generated\n'). | |
| 234 | ||
| 235 | type_for_print(integer,'Int') :- !. | |
| 236 | type_for_print(X,X). | |
| 237 | ||
| 238 | get_model_values(List,E) :- stored_model(M),!, print_vals(List,M,E). | |
| 239 | get_model_values(List,_) :- add_error(smtlib2_interpreter,'No model stored for get_value of: ',List). | |
| 240 | ||
| 241 | print_vals([],_,_). | |
| 242 | print_vals([id(ID)|T],M,E) :- member(binding(ID,Val,PP),M),!, print_binding(E,binding(ID,Val,PP)), | |
| 243 | print_vals(T,M,E). | |
| 244 | get_vals([id(ID)|_],_,_) :- add_error(smtlib2_interpreter,'No value stored for get_value of: ',ID). | |
| 245 | ||
| 246 | set_info(attribute(A,V)) :- !, | |
| 247 | set_attribute(A,V). | |
| 248 | set_info(X) :- !, format('missing in set_info: ~w~n',[X]), fail. | |
| 249 | ||
| 250 | ||
| 251 | :- use_module(probsrc(preferences), [set_preference/2]). | |
| 252 | set_attribute('smt-lib-version',decimal(2.0)) :- !. | |
| 253 | set_attribute('smt-lib-version',decimal(2.5)) :- !. | |
| 254 | set_attribute('smt-lib-version',decimal(2.6)) :- !. | |
| 255 | set_attribute(category,string(_S)) :- !. | |
| 256 | set_attribute(notes,string(_S)) :- !. | |
| 257 | set_attribute(status,S) :- !, nonvar(S), | |
| 258 | memberchk(S,[unknown,sat,unsat]), | |
| 259 | retractall(expected_result(_)), | |
| 260 | assertz(expected_result(S)). | |
| 261 | set_attribute(source,string(_S)) :- !. | |
| 262 | set_attribute(precision,decimal(D)) :- !, set_preference(real_solver_precision,D). | |
| 263 | set_attribute(A,V) :- | |
| 264 | add_warning(smtlib2_interpreter,'Missing case in set_attribute:',[A,V]). |