author | boehmes |

Sun May 04 16:17:53 2014 +0200 (2014-05-04) | |

changeset 56845 | 691da43fbdd4 |

parent 56844 | 52e5bf245b2a |

child 56846 | 9df717fef2bb |

removed obsolete internal SAT solvers

1.1 --- a/NEWS Sat May 03 23:15:00 2014 +0200 1.2 +++ b/NEWS Sun May 04 16:17:53 2014 +0200 1.3 @@ -351,6 +351,9 @@ 1.4 * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy 1.5 1.6 * New internal SAT solver "dpll_p" that produces models and proof traces. 1.7 + This solver replaces the internal SAT solvers "enumerate" and "dpll". 1.8 + Applications that explicitly used one of these two SAT solvers should 1.9 + use "dpll_p" instead. Minor INCOMPATIBILITY. 1.10 1.11 * SMT module: 1.12 * A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2

2.1 --- a/src/HOL/Library/refute.ML Sat May 03 23:15:00 2014 +0200 2.2 +++ b/src/HOL/Library/refute.ML Sun May 04 16:17:53 2014 +0200 2.3 @@ -1068,7 +1068,7 @@ 2.4 val fm_ax = Prop_Logic.all (map toTrue (tl intrs)) 2.5 val fm = Prop_Logic.all [#wellformed args, fm_ax, fm_u] 2.6 val _ = 2.7 - (if member (op =) ["dpll_p", "dpll", "enumerate"] satsolver then 2.8 + (if member (op =) ["dpll_p"] satsolver then 2.9 warning ("Using SAT solver " ^ quote satsolver ^ 2.10 "; for better performance, consider installing an \ 2.11 \external solver.")

3.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Sat May 03 23:15:00 2014 +0200 3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Sun May 04 16:17:53 2014 +0200 3.3 @@ -574,7 +574,7 @@ 3.4 (* use the first ML solver (to avoid startup overhead) *) 3.5 val (ml_solvers, nonml_solvers) = 3.6 SatSolver.get_solvers () 3.7 - |> List.partition (member (op =) ["dptsat", "dpll_p", "dpll"] o fst) 3.8 + |> List.partition (member (op =) ["dptsat", "dpll_p"] o fst) 3.9 val res = 3.10 if null nonml_solvers then 3.11 TimeLimit.timeLimit tac_timeout (snd (hd ml_solvers)) prop

4.1 --- a/src/HOL/Tools/sat_solver.ML Sat May 03 23:15:00 2014 +0200 4.2 +++ b/src/HOL/Tools/sat_solver.ML Sun May 04 16:17:53 2014 +0200 4.3 @@ -384,130 +384,11 @@ 4.4 (* ------------------------------------------------------------------------- *) 4.5 4.6 (* ------------------------------------------------------------------------- *) 4.7 -(* Internal SAT solver, available as 'SatSolver.invoke_solver "enumerate"' *) 4.8 -(* -- simply enumerates assignments until a satisfying assignment is found *) 4.9 -(* ------------------------------------------------------------------------- *) 4.10 - 4.11 -let 4.12 - fun enum_solver fm = 4.13 - let 4.14 - val indices = Prop_Logic.indices fm 4.15 - (* binary increment: list 'xs' of current bits, list 'ys' of all bits (lower bits first) *) 4.16 - fun next_list _ ([]:int list) = 4.17 - NONE 4.18 - | next_list [] (y::ys) = 4.19 - SOME [y] 4.20 - | next_list (x::xs) (y::ys) = 4.21 - if x=y then 4.22 - (* reset the bit, continue *) 4.23 - next_list xs ys 4.24 - else 4.25 - (* set the lowest bit that wasn't set before, keep the higher bits *) 4.26 - SOME (y::x::xs) 4.27 - fun assignment_from_list xs i = 4.28 - member (op =) xs i 4.29 - fun solver_loop xs = 4.30 - if Prop_Logic.eval (assignment_from_list xs) fm then 4.31 - SatSolver.SATISFIABLE (SOME o (assignment_from_list xs)) 4.32 - else 4.33 - (case next_list xs indices of 4.34 - SOME xs' => solver_loop xs' 4.35 - | NONE => SatSolver.UNSATISFIABLE NONE) 4.36 - in 4.37 - (* start with the "first" assignment (all variables are interpreted as 'false') *) 4.38 - solver_loop [] 4.39 - end 4.40 -in 4.41 - SatSolver.add_solver ("enumerate", enum_solver) 4.42 -end; 4.43 - 4.44 -(* ------------------------------------------------------------------------- *) 4.45 -(* Internal SAT solver, available as 'SatSolver.invoke_solver "dpll"' -- a *) 4.46 -(* simple implementation of the DPLL algorithm (cf. L. Zhang, S. Malik: "The *) 4.47 -(* Quest for Efficient Boolean Satisfiability Solvers", July 2002, Fig. 1). *) 4.48 -(* ------------------------------------------------------------------------- *) 4.49 - 4.50 -let 4.51 - local 4.52 - open Prop_Logic 4.53 - in 4.54 - fun dpll_solver fm = 4.55 - let 4.56 - (* We could use 'Prop_Logic.defcnf fm' instead of 'Prop_Logic.nnf fm' *) 4.57 - (* but that sometimes leads to worse performance due to the *) 4.58 - (* introduction of additional variables. *) 4.59 - val fm' = Prop_Logic.nnf fm 4.60 - val indices = Prop_Logic.indices fm' 4.61 - fun partial_var_eval [] i = BoolVar i 4.62 - | partial_var_eval (x::xs) i = if x=i then True else if x=(~i) then False else partial_var_eval xs i 4.63 - fun partial_eval xs True = True 4.64 - | partial_eval xs False = False 4.65 - | partial_eval xs (BoolVar i) = partial_var_eval xs i 4.66 - | partial_eval xs (Not fm) = SNot (partial_eval xs fm) 4.67 - | partial_eval xs (Or (fm1, fm2)) = SOr (partial_eval xs fm1, partial_eval xs fm2) 4.68 - | partial_eval xs (And (fm1, fm2)) = SAnd (partial_eval xs fm1, partial_eval xs fm2) 4.69 - fun forced_vars True = [] 4.70 - | forced_vars False = [] 4.71 - | forced_vars (BoolVar i) = [i] 4.72 - | forced_vars (Not (BoolVar i)) = [~i] 4.73 - | forced_vars (Or (fm1, fm2)) = inter (op =) (forced_vars fm1) (forced_vars fm2) 4.74 - | forced_vars (And (fm1, fm2)) = union (op =) (forced_vars fm1) (forced_vars fm2) 4.75 - (* Above, i *and* ~i may be forced. In this case the first occurrence takes *) 4.76 - (* precedence, and the next partial evaluation of the formula returns 'False'. *) 4.77 - | forced_vars _ = error "formula is not in negation normal form" 4.78 - fun eval_and_force xs fm = 4.79 - let 4.80 - val fm' = partial_eval xs fm 4.81 - val xs' = forced_vars fm' 4.82 - in 4.83 - if null xs' then 4.84 - (xs, fm') 4.85 - else 4.86 - eval_and_force (xs@xs') fm' (* xs and xs' should be distinct, so '@' here should have *) 4.87 - (* the same effect as 'union_int' *) 4.88 - end 4.89 - fun fresh_var xs = 4.90 - find_first (fn i => not (member (op =) xs i) andalso not (member (op =) xs (~i))) indices 4.91 - (* partial assignment 'xs' *) 4.92 - fun dpll xs fm = 4.93 - let 4.94 - val (xs', fm') = eval_and_force xs fm 4.95 - in 4.96 - case fm' of 4.97 - True => SOME xs' 4.98 - | False => NONE 4.99 - | _ => 4.100 - let 4.101 - val x = the (fresh_var xs') (* a fresh variable must exist since 'fm' did not evaluate to 'True'/'False' *) 4.102 - in 4.103 - case dpll (x::xs') fm' of (* passing fm' rather than fm should save some simplification work *) 4.104 - SOME xs'' => SOME xs'' 4.105 - | NONE => dpll ((~x)::xs') fm' (* now try interpreting 'x' as 'False' *) 4.106 - end 4.107 - end 4.108 - fun assignment_from_list [] i = 4.109 - NONE (* the DPLL procedure didn't provide a value for this variable *) 4.110 - | assignment_from_list (x::xs) i = 4.111 - if x=i then (SOME true) 4.112 - else if x=(~i) then (SOME false) 4.113 - else assignment_from_list xs i 4.114 - in 4.115 - (* initially, no variable is interpreted yet *) 4.116 - case dpll [] fm' of 4.117 - SOME assignment => SatSolver.SATISFIABLE (assignment_from_list assignment) 4.118 - | NONE => SatSolver.UNSATISFIABLE NONE 4.119 - end 4.120 - end (* local *) 4.121 -in 4.122 - SatSolver.add_solver ("dpll", dpll_solver) 4.123 -end; 4.124 - 4.125 -(* ------------------------------------------------------------------------- *) 4.126 (* Internal SAT solver, available as 'SatSolver.invoke_solver "dpll_p"' -- *) 4.127 -(* a simple, slightly more efficient implementation of the DPLL algorithm *) 4.128 -(* (cf. L. Zhang, S. Malik: "The Quest for Efficient Boolean Satisfiability *) 4.129 -(* Solvers", July 2002, Fig. 2). In contrast to the other two ML solvers *) 4.130 -(* above, this solver produces proof traces. *) 4.131 +(* a simplified implementation of the conflict-driven clause-learning *) 4.132 +(* algorithm (cf. L. Zhang, S. Malik: "The Quest for Efficient Boolean *) 4.133 +(* Satisfiability Solvers", July 2002, Fig. 2). This solver produces models *) 4.134 +(* and proof traces. *) 4.135 (* ------------------------------------------------------------------------- *) 4.136 4.137 let

5.1 --- a/src/HOL/ex/Refute_Examples.thy Sat May 03 23:15:00 2014 +0200 5.2 +++ b/src/HOL/ex/Refute_Examples.thy Sun May 04 16:17:53 2014 +0200 5.3 @@ -20,7 +20,7 @@ 5.4 refute [expect = genuine] -- {* equivalent to 'refute 1' *} 5.5 -- {* here 'refute 3' would cause an exception, since we only have 2 subgoals *} 5.6 refute [maxsize = 5, expect = genuine] -- {* we can override parameters ... *} 5.7 -refute [satsolver = "dpll", expect = genuine] 2 5.8 +refute [satsolver = "dpll_p", expect = genuine] 2 5.9 -- {* ... and specify a subgoal at the same time *} 5.10 oops 5.11