1		% (c) 2014-2022 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(solver_handling,[clauses_on_level/4,
6		add_clauses_to_level/4,
7		in_solver_on_level/3,
8		solve/2, solve_negated/2,
9		initial_state/1]).
10
11		:- use_module(probsrc(module_information)).
12		:- module_info(group,symbolic_model_checker).
13		:- module_info(description,'Internal data structures for solver / prover').
14
15		:- use_module(library(avl)).
16		:- use_module(library(ordsets)).
17		:- use_module(library(lists)).
18
19		:- use_module(extension('counter/counter'),[inc_counter/1]).
20
21		:- use_module(smt_solvers_interface(smt_solvers_interface), [smt_solve_predicate/4]).
22
23		:- use_module(extrasrc(atelierb_provers_interface),[prove_predicate/3]).
24		:- use_module(probsrc(preferences), [get_preference/2,
25		temporary_set_preference/3,
26		reset_temporary_preference/2]).
27		:- use_module(probsrc(solver_interface), [solve_predicate/5]).
28		:- use_module(probsrc(translate), [print_bexpr/1]).
29		:- use_module(probsrc(bsyntaxtree), [disjunct_predicates/2,
30		conjunction_to_list/2,
31		conjunct_predicates/2]).
32
33		:- use_module(symbolic_model_checker(predicate_handling)).
34
35		initial_state(Pred) :-
36		get_initial_state_predicate(Init),
37		conjunct_predicates([Init,Pred],IandPred),
38		solve(IandPred,Result),
39		Result = solution(_).
40
41		add_clauses_to_level(Level,FramesIn,Clauses,FramesOut) :-
42		maplist(list_to_ord_set,Clauses,OrdClauses),
43		clauses_on_level(Level,FramesIn,F_To,ClausesTo),
44		list_to_ord_set(OrdClauses,SetToAdd),
45		ord_union(ClausesTo,SetToAdd,NewClauses),
46		exclude(is_subsumed(NewClauses),NewClauses,FilteredNewClauses),
47		avl_store(Level,FramesIn,frame(F_To,FilteredNewClauses),FramesOut).
48
49		is_subsumed(AllClauses,C) :-
50		member(C2,AllClauses),
51		C \= C2,
52		% C is subsumed by C2 if C = C2 + additional disjuncts
53		ord_subtract(C2,C,[]).
54
55		clauses_on_level(Level,Frames,F_K,Clauses) :-
56		avl_fetch(Level,Frames,frame(F_K,Clauses)).
57
58		in_solver_on_level(Level,Frames,InSolver) :-
59		clauses_on_level(Level,Frames,F_K,Clauses),
60		maplist(disjunct_predicates,Clauses,Conjuncts),
61		append(F_K,Conjuncts,InSolver).
62
63		% the version below retuns clauses as negated conjunctions
64		% for some reason this seems to aid the solver?
65		% in_solver_on_level(Level,Frames,InSolver) :-
66		% clauses_on_level(Level,Frames,F_K,Clauses),
67		% (Clauses = [] -> InSolver = F_K ;
68		% maplist(maplist(bsyntaxtree:create_negation),Clauses,T),
69		% maplist(bsyntaxtree:conjunct_predicates,T,T2),
70		% maplist(bsyntaxtree:create_negation,T2,Conjuncts),
71		% append(F_K,Conjuncts,InSolver)).
72
73		% if our constraint solver fails, we try the atelierb provers
74		try_further_solvers(no_solution_found(_)).
75		try_further_solvers(time_out).
76
77		throw_if_solvers_too_weak(X,Pred) :-
78		X \= contradiction_found(_), X \= solution(_), !,
79		format('Solvers too weak for predicate:~n',[]),
80		print_bexpr(Pred),nl,
81		%translate:nested_print_bexpr(Pred),nl,
82		throw(solver_and_provers_too_weak).
83		throw_if_solvers_too_weak(_,_).
84
85		print_result(Solver,FullResult) :-
86		functor(FullResult,SRForPrint,_),
87		format('solve/2: result of ~w: ~w~n',[Solver,SRForPrint]).
88
89		solve_negated(P,R) :-
90		create_negation_and_cleanup(P,NP), % despite the name does not do clean_up of AST?
91		solve(NP,R).
92
93		:- use_module(probsrc(b_ast_cleanup), [clean_up_pred/3]).
94		solve(Predicate,Result) :-
95		clean_up_pred(Predicate,_,CPredicate),
96		%nl,translate:nested_print_bexpr(CPredicate),nl,
97		% as we constructed Predicate by hand; better clean it up and optimise it
98		inc_counter(ic3solvercalls),
99		% debug output for all solver calls
100		% translate:translate_bexpression(Predicate,PPPredicate),
101		% format('Checking: ~w~n',[PPPredicate]),
102		% calls through the solver interface
103		% uses smt support and smt fallback
104		Options = ['SMT'], % for symbolic mc SMT option is typically useful due to the disjunctions in the transition pred
105		% we could also provide 'CHR' option
106		get_timeout_factor(Options,TimeoutFactor),
107		solve_prob(CPredicate,Options,TimeoutFactor,SolverResult),
108		print_result(prob,SolverResult),
109		solve2(CPredicate,SolverResult,Result).
110
111		% other options to try if prob alone did not find a suitable result
112		% corresponding timeout factors for portfolio / prob only
113		options_to_try(['KODKOD']).
114		options_to_try(['SMT_SUPPORTED_INTERPRETER']).
115
116		get_timeout_factor(['KODKOD'],TO) :- !, TO=0.25.
117		get_timeout_factor(['SMT_SUPPORTED_INTERPRETER'],TO) :- !, TO=0.35. % last 0,15 reserved for ml/pp
118		get_timeout_factor(_,Factor) :-
119		get_preference(symbolic_mc_try_other_solvers,false)
120		-> Factor = 1 ; Factor = 0.25.
121
122		solve2(Predicate,SolverResult,Result) :-
123		try_further_solvers(SolverResult),
124		get_preference(symbolic_mc_try_other_solvers,true),
125		options_to_try(Options), % backtracks into different options
126		inc_counter(ic3solvercalls),
127		get_timeout_factor(Options,TimeoutFactor),
128		solve_prob(Predicate,Options,TimeoutFactor,NewResult),
129		print_result(prob,NewResult),
130		\+ (try_further_solvers(NewResult)), !,
131		Result = NewResult.
132		solve2(Predicate,SolverResult,Result) :-
133		solve3(Predicate,SolverResult,Result).
134
135		solve3(Predicate,SolverResult,Result) :-
136		try_further_solvers(SolverResult),
137		get_preference(symbolic_mc_try_other_solvers,true),
138		smt_solve_predicate(z3,Predicate,_,contradiction_found), !,
139		print_result('smt_solve_predicate',contradiction_found),
140		Result = contradiction_found(Predicate).
141		solve3(Predicate,SolverResult,Result) :-
142		solve4(Predicate,SolverResult,Result).
143
144		solve4(Predicate,SolverResult,Result) :-
145		try_further_solvers(SolverResult),
146		get_preference(symbolic_mc_try_other_solvers,true), !,
147		solve_provers(Predicate,Result),
148		print_result('pp/ml',Result),
149		throw_if_solvers_too_weak(Result,Predicate).
150		solve4(Predicate,Result,Result) :-
151		throw_if_solvers_too_weak(Result,Predicate).
152
153		:- use_module(probsrc(debug),[debug_format/3]).
154		solve_prob(Predicate,Options,TimeoutFactor,ResultOut) :-
155		%temporary_set_preference(disprover_mode,true,Changed), % this seems dangerous, TODO: check if ok
156		% temporary_set_preference(smt_supported_interpreter,true),
157		debug_format(19,'Solving symbolic MC constraint with ProB and options ~w and timeout factor ~w~n',[Options, TimeoutFactor]),
158		%print('SOLVE:'),nl,translate:nested_print_bexpr(Predicate),nl,nl,
159		solve_predicate(Predicate,_State,TimeoutFactor,Options,Result), !,
160		%reset_temporary_preference(disprover_mode,Changed),
161		% reset_temporary_preference(smt_supported_interpreter),
162		(Result = contradiction_found -> ResultOut = contradiction_found(Predicate) ; % TODO: extract core
163		ResultOut = Result).
164
165		solve_provers(Predicate,Result) :-
166		conjunction_to_list(Predicate,Hyps),
167		% no hypotheses. might want to consider refactoring the predicate in order to find them
168		length(Hyps,L),write(len_of_hyps(L)),nl,
169		% (L=1 -> write(Predicate),nl ; true),
170		prove_predicate(Hyps,b(falsity,pred,[]),TResult), !,
171		(TResult = proved
172		-> Result = contradiction_found(Predicate) % TODO: extract core, etc.
173		; Result = no_solution_found(atbprover_unproved)).
174		solve_provers(_,no_solution_found). % in case prove_predicate fails