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 |