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(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(probsrc(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),
91		solve(NP,R).
92		solve(Predicate,Result) :-
93		inc_counter(ic3solvercalls),
94		% debug output for all solver calls
95		% translate:translate_bexpression(Predicate,PPPredicate),
96		% format('Checking: ~w~n',[PPPredicate]),
97		% calls through the solver interface
98		% uses smt support and smt fallback
99		Options = [],
100		get_timeout_factor(Options,TimeoutFactor),
101		solve_prob(Predicate,Options,TimeoutFactor,SolverResult),
102		print_result(prob,SolverResult),
103		solve2(Predicate,SolverResult,Result).
104
105		% other options to try if prob alone did not find a suitable result
106		% corresponding timeout factors for portfolio / prob only
107		options_to_try(['KODKOD']).
108		options_to_try(['SMT_SUPPORTED_INTERPRETER']).
109
110		get_timeout_factor([],Factor) :-
111		get_preference(symbolic_mc_try_other_solvers,false)
112		-> Factor = 1 ; Factor = 0.25.
113		get_timeout_factor(['KODKOD'],0.25).
114		get_timeout_factor(['SMT_SUPPORTED_INTERPRETER'],0.35). % last 0,15 reserved for ml/pp
115
116		solve2(Predicate,SolverResult,Result) :-
117		try_further_solvers(SolverResult),
118		get_preference(symbolic_mc_try_other_solvers,true),
119		options_to_try(Options), % backtracks into different options
120		inc_counter(ic3solvercalls),
121		get_timeout_factor(Options,TimeoutFactor),
122		solve_prob(Predicate,Options,TimeoutFactor,NewResult),
123		print_result(prob,NewResult),
124		\+ (try_further_solvers(NewResult)), !,
125		Result = NewResult.
126		solve2(Predicate,SolverResult,Result) :-
127		solve3(Predicate,SolverResult,Result).
128
129		solve3(Predicate,SolverResult,Result) :-
130		try_further_solvers(SolverResult),
131		get_preference(symbolic_mc_try_other_solvers,true),
132		smt_solve_predicate(z3,Predicate,_,contradiction_found), !,
133		print_result('smt_solve_predicate',contradiction_found),
134		Result = contradiction_found(Predicate).
135		solve3(Predicate,SolverResult,Result) :-
136		solve4(Predicate,SolverResult,Result).
137
138		solve4(Predicate,SolverResult,Result) :-
139		try_further_solvers(SolverResult),
140		get_preference(symbolic_mc_try_other_solvers,true), !,
141		solve_provers(Predicate,Result),
142		print_result('pp/ml',Result),
143		throw_if_solvers_too_weak(Result,Predicate).
144		solve4(Predicate,Result,Result) :-
145		throw_if_solvers_too_weak(Result,Predicate).
146
147		solve_prob(Predicate,Options,TimeoutFactor,ResultOut) :-
148		temporary_set_preference(disprover_mode,true,Changed),
149		% temporary_set_preference(smt_supported_interpreter,true),
150		solve_predicate(Predicate,_State,TimeoutFactor,Options,Result), !,
151		reset_temporary_preference(disprover_mode,Changed),
152		% reset_temporary_preference(smt_supported_interpreter),
153		(Result = contradiction_found -> ResultOut = contradiction_found(Predicate) ; % TODO: extract core
154		otherwise -> ResultOut = Result).
155
156		solve_provers(Predicate,Result) :-
157		conjunction_to_list(Predicate,Hyps),
158		% no hypotheses. might want to consider refactoring the predicate in order to find them
159		length(Hyps,L),write(len_of_hyps(L)),nl,
160		% (L=1 -> write(Predicate),nl ; true),
161		prove_predicate(Hyps,b(falsity,pred,[]),TResult), !,
162		(TResult = proved
163		-> Result = contradiction_found(Predicate) % TODO: extract core, etc.
164		; Result = no_solution_found(atbprover_unproved)).
165		solve_provers(_,no_solution_found). % in case prove_predicate fails