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.