--- a/NEWS Sat May 03 23:15:00 2014 +0200
+++ b/NEWS Sun May 04 16:17:53 2014 +0200
@@ -351,6 +351,9 @@
* Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy
* New internal SAT solver "dpll_p" that produces models and proof traces.
+ This solver replaces the internal SAT solvers "enumerate" and "dpll".
+ Applications that explicitly used one of these two SAT solvers should
+ use "dpll_p" instead. Minor INCOMPATIBILITY.
* SMT module:
* A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2
--- a/src/HOL/Library/refute.ML Sat May 03 23:15:00 2014 +0200
+++ b/src/HOL/Library/refute.ML Sun May 04 16:17:53 2014 +0200
@@ -1068,7 +1068,7 @@
val fm_ax = Prop_Logic.all (map toTrue (tl intrs))
val fm = Prop_Logic.all [#wellformed args, fm_ax, fm_u]
val _ =
- (if member (op =) ["dpll_p", "dpll", "enumerate"] satsolver then
+ (if member (op =) ["dpll_p"] satsolver then
warning ("Using SAT solver " ^ quote satsolver ^
"; for better performance, consider installing an \
\external solver.")
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Sat May 03 23:15:00 2014 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Sun May 04 16:17:53 2014 +0200
@@ -574,7 +574,7 @@
(* use the first ML solver (to avoid startup overhead) *)
val (ml_solvers, nonml_solvers) =
SatSolver.get_solvers ()
- |> List.partition (member (op =) ["dptsat", "dpll_p", "dpll"] o fst)
+ |> List.partition (member (op =) ["dptsat", "dpll_p"] o fst)
val res =
if null nonml_solvers then
TimeLimit.timeLimit tac_timeout (snd (hd ml_solvers)) prop
--- a/src/HOL/Tools/sat_solver.ML Sat May 03 23:15:00 2014 +0200
+++ b/src/HOL/Tools/sat_solver.ML Sun May 04 16:17:53 2014 +0200
@@ -384,130 +384,11 @@
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
-(* Internal SAT solver, available as 'SatSolver.invoke_solver "enumerate"' *)
-(* -- simply enumerates assignments until a satisfying assignment is found *)
-(* ------------------------------------------------------------------------- *)
-
-let
- fun enum_solver fm =
- let
- val indices = Prop_Logic.indices fm
- (* binary increment: list 'xs' of current bits, list 'ys' of all bits (lower bits first) *)
- fun next_list _ ([]:int list) =
- NONE
- | next_list [] (y::ys) =
- SOME [y]
- | next_list (x::xs) (y::ys) =
- if x=y then
- (* reset the bit, continue *)
- next_list xs ys
- else
- (* set the lowest bit that wasn't set before, keep the higher bits *)
- SOME (y::x::xs)
- fun assignment_from_list xs i =
- member (op =) xs i
- fun solver_loop xs =
- if Prop_Logic.eval (assignment_from_list xs) fm then
- SatSolver.SATISFIABLE (SOME o (assignment_from_list xs))
- else
- (case next_list xs indices of
- SOME xs' => solver_loop xs'
- | NONE => SatSolver.UNSATISFIABLE NONE)
- in
- (* start with the "first" assignment (all variables are interpreted as 'false') *)
- solver_loop []
- end
-in
- SatSolver.add_solver ("enumerate", enum_solver)
-end;
-
-(* ------------------------------------------------------------------------- *)
-(* Internal SAT solver, available as 'SatSolver.invoke_solver "dpll"' -- a *)
-(* simple implementation of the DPLL algorithm (cf. L. Zhang, S. Malik: "The *)
-(* Quest for Efficient Boolean Satisfiability Solvers", July 2002, Fig. 1). *)
-(* ------------------------------------------------------------------------- *)
-
-let
- local
- open Prop_Logic
- in
- fun dpll_solver fm =
- let
- (* We could use 'Prop_Logic.defcnf fm' instead of 'Prop_Logic.nnf fm' *)
- (* but that sometimes leads to worse performance due to the *)
- (* introduction of additional variables. *)
- val fm' = Prop_Logic.nnf fm
- val indices = Prop_Logic.indices fm'
- fun partial_var_eval [] i = BoolVar i
- | partial_var_eval (x::xs) i = if x=i then True else if x=(~i) then False else partial_var_eval xs i
- fun partial_eval xs True = True
- | partial_eval xs False = False
- | partial_eval xs (BoolVar i) = partial_var_eval xs i
- | partial_eval xs (Not fm) = SNot (partial_eval xs fm)
- | partial_eval xs (Or (fm1, fm2)) = SOr (partial_eval xs fm1, partial_eval xs fm2)
- | partial_eval xs (And (fm1, fm2)) = SAnd (partial_eval xs fm1, partial_eval xs fm2)
- fun forced_vars True = []
- | forced_vars False = []
- | forced_vars (BoolVar i) = [i]
- | forced_vars (Not (BoolVar i)) = [~i]
- | forced_vars (Or (fm1, fm2)) = inter (op =) (forced_vars fm1) (forced_vars fm2)
- | forced_vars (And (fm1, fm2)) = union (op =) (forced_vars fm1) (forced_vars fm2)
- (* Above, i *and* ~i may be forced. In this case the first occurrence takes *)
- (* precedence, and the next partial evaluation of the formula returns 'False'. *)
- | forced_vars _ = error "formula is not in negation normal form"
- fun eval_and_force xs fm =
- let
- val fm' = partial_eval xs fm
- val xs' = forced_vars fm'
- in
- if null xs' then
- (xs, fm')
- else
- eval_and_force (xs@xs') fm' (* xs and xs' should be distinct, so '@' here should have *)
- (* the same effect as 'union_int' *)
- end
- fun fresh_var xs =
- find_first (fn i => not (member (op =) xs i) andalso not (member (op =) xs (~i))) indices
- (* partial assignment 'xs' *)
- fun dpll xs fm =
- let
- val (xs', fm') = eval_and_force xs fm
- in
- case fm' of
- True => SOME xs'
- | False => NONE
- | _ =>
- let
- val x = the (fresh_var xs') (* a fresh variable must exist since 'fm' did not evaluate to 'True'/'False' *)
- in
- case dpll (x::xs') fm' of (* passing fm' rather than fm should save some simplification work *)
- SOME xs'' => SOME xs''
- | NONE => dpll ((~x)::xs') fm' (* now try interpreting 'x' as 'False' *)
- end
- end
- fun assignment_from_list [] i =
- NONE (* the DPLL procedure didn't provide a value for this variable *)
- | assignment_from_list (x::xs) i =
- if x=i then (SOME true)
- else if x=(~i) then (SOME false)
- else assignment_from_list xs i
- in
- (* initially, no variable is interpreted yet *)
- case dpll [] fm' of
- SOME assignment => SatSolver.SATISFIABLE (assignment_from_list assignment)
- | NONE => SatSolver.UNSATISFIABLE NONE
- end
- end (* local *)
-in
- SatSolver.add_solver ("dpll", dpll_solver)
-end;
-
-(* ------------------------------------------------------------------------- *)
(* Internal SAT solver, available as 'SatSolver.invoke_solver "dpll_p"' -- *)
-(* a simple, slightly more efficient implementation of the DPLL algorithm *)
-(* (cf. L. Zhang, S. Malik: "The Quest for Efficient Boolean Satisfiability *)
-(* Solvers", July 2002, Fig. 2). In contrast to the other two ML solvers *)
-(* above, this solver produces proof traces. *)
+(* a simplified implementation of the conflict-driven clause-learning *)
+(* algorithm (cf. L. Zhang, S. Malik: "The Quest for Efficient Boolean *)
+(* Satisfiability Solvers", July 2002, Fig. 2). This solver produces models *)
+(* and proof traces. *)
(* ------------------------------------------------------------------------- *)
let
--- a/src/HOL/ex/Refute_Examples.thy Sat May 03 23:15:00 2014 +0200
+++ b/src/HOL/ex/Refute_Examples.thy Sun May 04 16:17:53 2014 +0200
@@ -20,7 +20,7 @@
refute [expect = genuine] -- {* equivalent to 'refute 1' *}
-- {* here 'refute 3' would cause an exception, since we only have 2 subgoals *}
refute [maxsize = 5, expect = genuine] -- {* we can override parameters ... *}
-refute [satsolver = "dpll", expect = genuine] 2
+refute [satsolver = "dpll_p", expect = genuine] 2
-- {* ... and specify a subgoal at the same time *}
oops