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