removed obsolete internal SAT solvers
authorboehmes
Sun May 04 16:17:53 2014 +0200 (2014-05-04)
changeset 56845691da43fbdd4
parent 56844 52e5bf245b2a
child 56846 9df717fef2bb
removed obsolete internal SAT solvers
NEWS
src/HOL/Library/refute.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/sat_solver.ML
src/HOL/ex/Refute_Examples.thy
     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