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