1 | % (c) 2014-2015 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(probsrc(solver_interface), [solve_predicate/4]). | |
14 | :- use_module(probsrc(atelierb_provers_interface), [disprove_predicate/2]). | |
15 | :- use_module(probsrc(bsyntaxtree), [conjunct_predicates/2]). | |
16 | :- use_module(probsrc(btypechecker), [couplise_list/2]). | |
17 | :- use_module(probsrc(eclipse_interface), [load_sets_for_cbc/1]). | |
18 | :- use_module(probsrc(prob2_interface), [start_animation/0]). | |
19 | :- use_module(probsrc(translate), [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 | ||
27 | :- dynamic expected_result/1. | |
28 | :- volatile expected_result/1. | |
29 | ||
30 | interpret_l([],Env,Env). | |
31 | interpret_l([H|T],EnvIn,EnvOut) :- | |
32 | interpret(H,EnvIn,EnvT), | |
33 | interpret_l(T,EnvT,EnvOut). | |
34 | ||
35 | interpret(exit,E,E) :- !, throw(halt(0)). | |
36 | interpret(reset,_,E) :- !, empty_env(E). | |
37 | interpret(set_logic(_X),E,E) :- !, | |
38 | % TODO: only accept supported logics. | |
39 | true. | |
40 | interpret(set_info(X),E,E) :- !, | |
41 | set_info(X). | |
42 | % special case for array logics, sets up an additional constraint | |
43 | interpret(declare_fun(Id,[],sort('Array',[Index,Element])),EIn,EOut) :- !, | |
44 | smt_type_to_prob_type(Index,EIn,BIndex), | |
45 | smt_type_to_prob_type(Element,EIn,BElement), | |
46 | FullType = set(couple(BIndex,BElement)), | |
47 | add_identifier(EIn,Id,FullType,ETemp), | |
48 | % however, an array is a partial function. thus, we have to add a constraint | |
49 | typing_constraint(svar(Id,sort('Array',[Index,Element])),AdditionalConstraint), | |
50 | add_assertion(ETemp,AdditionalConstraint,EOut). | |
51 | % special case for bit vectors, sets up an additional constraint | |
52 | interpret(declare_fun(Id,[],sort('BitVec',[Length])),EIn,EOut) :- !, | |
53 | FullType = set(couple(integer,integer)), | |
54 | add_identifier(EIn,Id,FullType,ETemp), | |
55 | % however, an array is a partial function. thus, we have to add a constraint | |
56 | typing_constraint(svar(Id,sort('BitVec',[Length])),AdditionalConstraint), | |
57 | add_assertion(ETemp,AdditionalConstraint,EOut). | |
58 | interpret(declare_fun(Id,[],Type),EIn,EOut) :- !, | |
59 | smt_type_to_prob_type(Type,EIn,BType), | |
60 | add_identifier(EIn,Id,BType,EOut). | |
61 | interpret(declare_fun(Id,Params,Return),EIn,EOut) :- !, | |
62 | maplist(smt_type_to_prob_type_maplist(EIn),Params,BParams), | |
63 | smt_type_to_prob_type(Return,EIn,BReturn), | |
64 | couplise_list(BParams,BParamsCoupled), | |
65 | Fulltype = set(couple(BParamsCoupled,BReturn)), | |
66 | add_identifier(EIn,Id,Fulltype,ETemp), | |
67 | is_function_constraint(Id,Fulltype,Constraint), | |
68 | add_assertion(ETemp,Constraint,EOut). | |
69 | interpret(declare_sort(Name,0),EIn,EOut) :- !, | |
70 | add_custom_type(EIn,Name,EOut). | |
71 | interpret(define_fun(ID,Params,Return,Definition),EIn,EOut) :- !, | |
72 | smt_type_to_prob_type(Return,EIn,BReturn), | |
73 | maplist(smt_term_to_prob_term_maplist(EIn),Params,BParams), | |
74 | create_local_env(EIn,BParams,LocalEnv), | |
75 | smt_term_to_prob_term(Definition,LocalEnv,BDefinition), | |
76 | add_function(EIn,ID,BParams,BReturn,BDefinition,EOut). | |
77 | interpret(assert(Term),EIn,EOut) :- !, | |
78 | smt_term_to_prob_term(Term,EIn,BTerm), | |
79 | bool_to_pred(BTerm,PredBTerm), | |
80 | add_assertion(EIn,PredBTerm,EOut). | |
81 | interpret(push(Num),EIn,EOut) :- !, | |
82 | push_assertion_stack(EIn,Num,EOut). | |
83 | interpret(pop(Num),EIn,EOut) :- !, | |
84 | pop_assertion_stack(EIn,Num,EOut). | |
85 | interpret(set_option(Opt),EIn,EOut) :- !, | |
86 | format('Ignoring set_option(~w) !~n',[Opt]), EOut=EIn. | |
87 | interpret(check_sat,E,E) :- !, | |
88 | get_assertions(E,BTerms), | |
89 | get_custom_types(E,CT), | |
90 | conjunct_predicates(BTerms,Assertions), | |
91 | QuantifiedAssertions = Assertions, | |
92 | load_sets_for_cbc(CT), | |
93 | start_animation, | |
94 | (debug_mode(on) -> print('Solving: '),nl, | |
95 | print_bexpr(QuantifiedAssertions),nl | |
96 | ; true), | |
97 | start_ms_timer(Timer), | |
98 | solve_predicate(QuantifiedAssertions,_State,4,FullResult), !, | |
99 | %nl,print(State),nl, | |
100 | (debug_mode(on) -> print('ProB Solver walltime: '),stop_ms_timer(Timer) ; true), | |
101 | try_provers(FullResult,E,QuantifiedAssertions). | |
102 | interpret(get_model,E,E) :- !, print_model(E). % this command is not part of the smtlib2 language anymore | |
103 | interpret(X,_,_) :- !, format('missing in interpret: ~w~n',[X]), fail. | |
104 | ||
105 | try_provers(solution(S),E,_) :- !, | |
106 | assert(stored_model(S)), | |
107 | (debug_mode(on) -> print_model(E) ; true), | |
108 | add_error_if_result_unexpected(sat), | |
109 | write('sat\n'). | |
110 | try_provers(contradiction_found,_,_) :- !, add_error_if_result_unexpected(unsat), write('unsat\n'). | |
111 | try_provers(_,_,Assertions) :- | |
112 | get_preference(try_atb_provers,true), | |
113 | % we suspect that the solver failed to identify a contradiction | |
114 | % disprove predicate might fail, i.e. if the provers are not installed | |
115 | debug_println(20,'Trying to run Atelier-B provers'), | |
116 | disprove_predicate(Assertions,Result),!, | |
117 | write_final_result(Result). | |
118 | try_provers(_,_,_) :- add_error_if_result_unexpected(unknown), write('unknown\n'). | |
119 | ||
120 | write_final_result(proved) :- add_error_if_result_unexpected(unsat), write('unsat\n'). | |
121 | write_final_result(_) :- add_error_if_result_unexpected(unknown), write('unknown\n'). | |
122 | ||
123 | add_error_if_result_unexpected(unknown) :- % in non-strict mode: no message, we simple failed to establish a result | |
124 | get_preference(strict_raise_warnings,false),!. | |
125 | add_error_if_result_unexpected(Actual) :- | |
126 | expected_result(Expected),!, | |
127 | (Actual = Expected -> true | |
128 | ; Expected = unknown -> true | |
129 | ; Actual = unknown -> | |
130 | add_warning(smtlib2_interpreter,'Result unknown; could not establish expected result: ',Expected) | |
131 | ; add_error(smtlib2_interpreter, 'Actual result differs from expected result: ','/='(Actual,Expected))). | |
132 | add_error_if_result_unexpected(_). % no expected result stored | |
133 | ||
134 | :- dynamic stored_model/1. | |
135 | ||
136 | print_binding(E,binding(V,_,PP)) :- | |
137 | get_type(V,E,Type), | |
138 | type_for_print(Type,TypeForPrint), | |
139 | format('(define-fun ~w () ~w ~w)~n',[V,TypeForPrint,PP]). | |
140 | print_model(E) :- | |
141 | stored_model(M), !, | |
142 | print('(model'), nl, | |
143 | maplist(print_binding(E),M), | |
144 | print(')'), nl. | |
145 | print_model(_) :- write('no model generated\n'). | |
146 | ||
147 | type_for_print(integer,'Int') :- !. | |
148 | type_for_print(X,X). | |
149 | ||
150 | set_info(attribute(A,V)) :- !, | |
151 | set_attribute(A,V). | |
152 | set_info(X) :- !, format('missing in set_info: ~w~n',[X]), fail. | |
153 | ||
154 | ||
155 | set_attribute('smt-lib-version',decimal(2.0)) :- !. | |
156 | set_attribute('smt-lib-version',decimal(2.5)) :- !. | |
157 | set_attribute('smt-lib-version',decimal(2.6)) :- !. | |
158 | set_attribute(category,string(_S)) :- !. | |
159 | set_attribute(notes,string(_S)) :- !. | |
160 | set_attribute(status,S) :- !, | |
161 | member(S,[unknown,sat,unsat]), | |
162 | retractall(expected_result(_)), | |
163 | assert(expected_result(S)). | |
164 | set_attribute(source,string(_S)) :- !. | |
165 | set_attribute(A,V) :- !, | |
166 | format('missing in set_attribute: ~w to ~w~n',[A,V]), fail. |