src/HOL/Tools/sat_solver.ML
changeset 14753 f40b45db8cf0
parent 14703 837d7180c39a
child 14805 eff7b9df27e9
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Mon May 17 11:02:16 2004 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Mon May 17 14:05:06 2004 +0200
     1.3 @@ -230,8 +230,8 @@
     1.4  (* ------------------------------------------------------------------------- *)
     1.5  
     1.6  (* ------------------------------------------------------------------------- *)
     1.7 -(* Internal SAT solver, available as 'SatSolver.solve "enumerate"' -- simply *)
     1.8 -(* enumerates assignments until a satisfying assignment is found             *)
     1.9 +(* Internal SAT solver, available as 'SatSolver.invoke_solver "enumerate"'   *)
    1.10 +(* -- simply enumerates assignments until a satisfying assignment is found   *)
    1.11  (* ------------------------------------------------------------------------- *)
    1.12  
    1.13  let
    1.14 @@ -272,9 +272,9 @@
    1.15  end;
    1.16  
    1.17  (* ------------------------------------------------------------------------- *)
    1.18 -(* Internal SAT solver, available as 'SatSolver.solve "dpll"' -- a simple    *)
    1.19 -(* implementation of the DPLL algorithm (cf. L. Zhang, S. Malik: "The Quest  *)
    1.20 -(* for Efficient Boolean Satisfiability Solvers", July 2002, Fig. 1).        *)
    1.21 +(* Internal SAT solver, available as 'SatSolver.invoke_solver "dpll"' -- a   *)
    1.22 +(* simple implementation of the DPLL algorithm (cf. L. Zhang, S. Malik: "The *)
    1.23 +(* Quest for Efficient Boolean Satisfiability Solvers", July 2002, Fig. 1).  *)
    1.24  (* ------------------------------------------------------------------------- *)
    1.25  
    1.26  let
    1.27 @@ -359,8 +359,8 @@
    1.28  end;
    1.29  
    1.30  (* ------------------------------------------------------------------------- *)
    1.31 -(* Internal SAT solver, available as 'SatSolver.solve "auto"': uses the      *)
    1.32 -(* first installed solver (other than "auto" itself)                         *)
    1.33 +(* Internal SAT solver, available as 'SatSolver.invoke_solver "auto"': uses  *)
    1.34 +(* the first installed solver (other than "auto" itself)                     *)
    1.35  (* ------------------------------------------------------------------------- *)
    1.36  
    1.37  let