# HG changeset patch # User webertj # Date 1087502483 -7200 # Node ID 7155b319eafa85f42f5c3337d64c3afd4305fd23 # Parent 2c1456d705e9812d462eac5f10921a79f1afa1a1 new SAT solver interface diff -r 2c1456d705e9 -r 7155b319eafa src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Thu Jun 17 21:58:51 2004 +0200 +++ b/src/HOL/Tools/refute.ML Thu Jun 17 22:01:23 2004 +0200 @@ -3,10 +3,10 @@ Author: Tjark Weber Copyright 2003-2004 -Finite model generation for HOL formulae, using a SAT solver. +Finite model generation for HOL formulas, using a SAT solver. *) -(* TODO: case, rec, size for IDTs are not supported yet *) +(* TODO: case, recursion, size for IDTs are not supported yet *) (* ------------------------------------------------------------------------- *) (* Declares the 'REFUTE' signature as well as a structure 'Refute'. *) @@ -59,7 +59,7 @@ structure Refute : REFUTE = struct - (* FIXME comptibility -- should avoid std_output altogether *) + (* FIXME compatibility -- should avoid std_output altogether *) val std_output = Output.std_output o Output.output; open PropLogic; @@ -903,16 +903,16 @@ val fm = PropLogic.all [#wellformed args, fm_ax, fm_t] in std_output " invoking SAT solver..."; - case SatSolver.invoke_solver satsolver fm of - None => - error ("SAT solver " ^ quote satsolver ^ " not configured.") - | Some None => + (case SatSolver.invoke_solver satsolver fm of + SatSolver.SATISFIABLE assignment => + writeln ("\n*** Model found: ***\n" ^ print_model thy model (fn i => case assignment i of Some b => b | None => true)) + | _ => (* SatSolver.UNSATISFIABLE, SatSolver.UNKNOWN *) (std_output " no model found.\n"; case next_universe universe sizes minsize maxsize of Some universe' => find_model_loop universe' - | None => writeln "Search terminated, no larger universe within the given limits.") - | Some (Some assignment) => - writeln ("\n*** Model found: ***\n" ^ print_model thy model assignment) + | None => writeln "Search terminated, no larger universe within the given limits.")) + handle SatSolver.NOT_CONFIGURED => + error ("SAT solver " ^ quote satsolver ^ " is not configured.") end handle MAXVARS_EXCEEDED => writeln ("\nSearch terminated, number of Boolean variables (" ^ string_of_int maxvars ^ " allowed) exceeded.") | CANNOT_INTERPRET t' => @@ -931,14 +931,12 @@ writeln ("Trying to find a model that " ^ (if negate then "refutes" else "satisfies") ^ ": " ^ Sign.string_of_term (sign_of thy) t); if maxtime>0 then - (* TODO: this only works with SML/NJ *) - ((*TimeLimit.timeLimit (Time.fromSeconds (Int32.fromInt maxtime))*) + (TimeLimit.timeLimit (Time.fromSeconds (Int.toLarge maxtime)) wrapper () - (*handle TimeLimit.TimeOut => + handle TimeLimit.TimeOut => writeln ("\nSearch terminated, time limit (" - ^ string_of_int maxtime ^ " second" - ^ (if maxtime=1 then "" else "s") - ^ ") exceeded.")*)) + ^ string_of_int maxtime ^ (if maxtime=1 then " second" else " seconds") + ^ ") exceeded.")) else wrapper () end; diff -r 2c1456d705e9 -r 7155b319eafa src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Thu Jun 17 21:58:51 2004 +0200 +++ b/src/HOL/Tools/sat_solver.ML Thu Jun 17 22:01:23 2004 +0200 @@ -8,14 +8,19 @@ signature SAT_SOLVER = sig - type solver (* PropLogic.prop_formula -> (int -> bool) option option *) + exception NOT_CONFIGURED - (* external SAT solvers *) + type assignment = int -> bool option + datatype result = SATISFIABLE of assignment + | UNSATISFIABLE + | UNKNOWN + type solver = PropLogic.prop_formula -> result + + (* auxiliary functions to create external SAT solvers *) val write_dimacs_cnf_file : Path.T -> PropLogic.prop_formula -> unit val write_dimacs_sat_file : Path.T -> PropLogic.prop_formula -> unit - val parse_std_result_file : Path.T -> string -> (int -> bool) option - val make_external_solver : string -> (PropLogic.prop_formula -> unit) -> (unit -> (int -> bool) option) - -> PropLogic.prop_formula -> (int -> bool) option + val parse_std_result_file : Path.T -> string * string * string -> result + val make_external_solver : string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver (* generic interface *) val solvers : (string * solver) list ref @@ -29,20 +34,41 @@ open PropLogic; (* ------------------------------------------------------------------------- *) -(* Type of SAT solvers: given a propositional formula, a satisfying *) -(* assignment may be returned *) -(* - 'Some None' means that no satisfying assignment was found *) -(* - 'None' means that the solver was not configured/installed properly *) +(* should be raised by an external SAT solver to indicate that the solver is *) +(* not configured properly *) +(* ------------------------------------------------------------------------- *) + + exception NOT_CONFIGURED; + +(* ------------------------------------------------------------------------- *) +(* type of partial (satisfying) assignments: 'a i = None' means that 'a' is *) +(* a satisfying assigment regardless of the value of variable 'i' *) (* ------------------------------------------------------------------------- *) - type solver = prop_formula -> (int -> bool) option option; + type assignment = int -> bool option; + +(* ------------------------------------------------------------------------- *) +(* return type of SAT solvers: if the result is 'SATISFIABLE', a satisfying *) +(* assignment must be returned as well *) +(* ------------------------------------------------------------------------- *) + + datatype result = SATISFIABLE of assignment + | UNSATISFIABLE + | UNKNOWN; + +(* ------------------------------------------------------------------------- *) +(* type of SAT solvers: given a propositional formula, a satisfying *) +(* assignment may be returned *) +(* ------------------------------------------------------------------------- *) + + type solver = prop_formula -> result; (* ------------------------------------------------------------------------- *) (* write_dimacs_cnf_file: serializes a formula 'fm' of propositional logic *) (* to a file in DIMACS CNF format (see "Satisfiability Suggested *) (* Format", May 8 1993, Section 2.1) *) (* Note: 'fm' must not contain a variable index less than 1. *) -(* Note: 'fm' is converted into (definitional) CNF. *) +(* Note: 'fm' must be given in CNF. *) (* ------------------------------------------------------------------------- *) (* Path.T -> prop_formula -> unit *) @@ -70,22 +96,23 @@ (assert (i>=1) "formula contains a variable index less than 1"; string_of_int i) | cnf_string (Not fm) = - "-" ^ (cnf_string fm) + "-" ^ cnf_string fm | cnf_string (Or (fm1,fm2)) = - (cnf_string fm1) ^ " " ^ (cnf_string fm2) + cnf_string fm1 ^ " " ^ cnf_string fm2 | cnf_string (And (fm1,fm2)) = - (cnf_string fm1) ^ " 0\n" ^ (cnf_string fm2) + cnf_string fm1 ^ " 0\n" ^ cnf_string fm2 in File.write path (let - val cnf = (cnf_True_False_elim o defcnf) fm (* conversion into def. CNF *) - val number_of_vars = maxidx cnf - val number_of_clauses = cnf_number_of_clauses cnf + val fm' = cnf_True_False_elim fm + val number_of_vars = maxidx fm' + val number_of_clauses = cnf_number_of_clauses fm' + val cnfstring = cnf_string fm' in "c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^ "c (c) Tjark Weber\n" ^ - "p cnf " ^ (string_of_int number_of_vars) ^ " " ^ (string_of_int number_of_clauses) ^ "\n" ^ - (cnf_string cnf) ^ "\n" + "p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n" ^ + cnfstring ^ " 0\n" end) end; @@ -109,11 +136,11 @@ (assert (i>=1) "formula contains a variable index less than 1"; string_of_int i) | sat_string (Not fm) = - "-(" ^ (sat_string fm) ^ ")" + "-(" ^ sat_string fm ^ ")" | sat_string (Or (fm1,fm2)) = - "+(" ^ (sat_string fm1) ^ " " ^ (sat_string fm2) ^ ")" + "+(" ^ sat_string fm1 ^ " " ^ sat_string fm2 ^ ")" | sat_string (And (fm1,fm2)) = - "*(" ^ (sat_string fm1) ^ " " ^ (sat_string fm2) ^ ")" + "*(" ^ sat_string fm1 ^ " " ^ sat_string fm2 ^ ")" in File.write path (let @@ -121,29 +148,28 @@ in "c This file was generated by SatSolver.write_dimacs_sat_file\n" ^ "c (c) Tjark Weber\n" ^ - "p sat " ^ (string_of_int number_of_vars) ^ "\n" ^ - "(" ^ (sat_string fm) ^ ")\n" + "p sat " ^ string_of_int number_of_vars ^ "\n" ^ + "(" ^ sat_string fm ^ ")\n" end) end; (* ------------------------------------------------------------------------- *) (* parse_std_result_file: scans a SAT solver's output file for a satisfying *) -(* variable assignment. Returns the assignment, or 'None' if the SAT *) -(* solver did not find one. The file format must be as follows: *) -(* ,----- *) -(* | 0 or more lines not containing 'success' *) -(* | A line containing 'success' as a substring *) -(* | A line ASSIGNMENT containing integers, separated by " " *) -(* | 0 or more lines *) -(* `----- *) -(* If variable i is contained in ASSIGNMENT, then i is interpreted as *) -(* 'true'. If ~i is contained in ASSIGNMENT, then i is interpreted as *) -(* 'false'. *) +(* variable assignment. Returns the assignment, or 'UNSATISFIABLE' if *) +(* the file contains 'unsatisfiable', or 'UNKNOWN' if the file contains *) +(* neither 'satisfiable' nor 'unsatisfiable'. Empty lines are ignored. *) +(* The assignment must be given in one or more lines immediately after *) +(* the line that contains 'satisfiable'. These lines must begin with *) +(* 'assignment_prefix'. Variables must be separated by " ". Non- *) +(* integer strings are ignored. If variable i is contained in the *) +(* assignment, then i is interpreted as 'true'. If ~i is contained in *) +(* the assignment, then i is interpreted as 'false'. Otherwise the *) +(* value of i is taken to be unspecified. *) (* ------------------------------------------------------------------------- *) - (* Path.T -> string -> (int -> bool) option *) + (* Path.T -> string * string * string -> result *) - fun parse_std_result_file path success = + fun parse_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) = let (* 'a option -> 'a Library.option *) fun option (SOME a) = @@ -153,13 +179,21 @@ (* string -> int list *) fun int_list_from_string s = mapfilter (option o Int.fromString) (space_explode " " s) - (* int list -> int -> bool *) + (* int list -> assignment *) fun assignment_from_list [] i = - false (* could be 'true' just as well; the SAT solver didn't provide a value for this variable *) + None (* the SAT solver didn't provide a value for this variable *) | assignment_from_list (x::xs) i = - if x=i then true - else if x=(~i) then false + if x=i then (Some true) + else if x=(~i) then (Some false) else assignment_from_list xs i + (* int list -> string list -> assignment *) + fun parse_assignment xs [] = + assignment_from_list xs + | parse_assignment xs (line::lines) = + if String.isPrefix assignment_prefix line then + parse_assignment (xs @ int_list_from_string line) lines + else + assignment_from_list xs (* string -> string -> bool *) fun is_substring needle haystack = let @@ -172,29 +206,28 @@ true else is_substring needle (String.substring (haystack, 1, length2-1)) end - (* string list -> int list option *) + (* string list -> result *) fun parse_lines [] = - None + UNKNOWN | parse_lines (line::lines) = - if is_substring success line then - (* the next line must be a list of integers *) - (Some o assignment_from_list o int_list_from_string o hd) lines + if is_substring satisfiable line then + SATISFIABLE (parse_assignment [] lines) + else if is_substring unsatisfiable line then + UNSATISFIABLE else parse_lines lines in - (parse_lines o split_lines o File.read) path + (parse_lines o (filter (fn l => l <> "")) o split_lines o File.read) path end; (* ------------------------------------------------------------------------- *) (* make_external_solver: call 'writefn', execute 'cmd', call 'readfn' *) (* ------------------------------------------------------------------------- *) - (* string -> (prop_formula -> unit) -> (unit -> (int -> bool) option) -> prop_formula -> (int -> bool) option *) + (* string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver *) fun make_external_solver cmd writefn readfn fm = - (writefn fm; - assert ((system cmd)=0) ("system command " ^ quote cmd ^ " failed (make sure the SAT solver is installed)"); - readfn ()); + (writefn fm; system cmd; readfn ()); (* ------------------------------------------------------------------------- *) (* solvers: a (reference to a) table of all registered SAT solvers *) @@ -255,20 +288,20 @@ (* int list -> int -> bool *) fun assignment_from_list xs i = i mem xs - (* int list -> (int -> bool) option *) + (* int list -> SatSolver.result *) fun solver_loop xs = if PropLogic.eval (assignment_from_list xs) fm then - Some (assignment_from_list xs) + SatSolver.SATISFIABLE (Some o (assignment_from_list xs)) else (case next_list xs indices of Some xs' => solver_loop xs' - | None => None) + | None => SatSolver.UNSATISFIABLE) in - (* start with the "first" assignment (all variables are interpreted as 'False') *) + (* start with the "first" assignment (all variables are interpreted as 'false') *) solver_loop [] end in - SatSolver.add_solver ("enumerate", Some o enum_solver) + SatSolver.add_solver ("enumerate", enum_solver) end; (* ------------------------------------------------------------------------- *) @@ -283,9 +316,9 @@ in fun dpll_solver fm = let - (* We could use 'PropLogic.defcnf fm' instead of 'nnf fm', but that *) - (* sometimes introduces more boolean variables than we can handle *) - (* efficiently. *) + (* We could use 'PropLogic.defcnf fm' instead of 'PropLogic.nnf fm' *) + (* but that sometimes introduces more boolean variables than we can *) + (* handle efficiently. *) val fm' = PropLogic.nnf fm (* int list *) val indices = PropLogic.indices fm' @@ -342,66 +375,132 @@ | None => dpll ((~x)::xs') fm' (* now try interpreting 'x' as 'False' *) end end - (* int list -> int -> bool *) + (* int list -> assignment *) fun assignment_from_list [] i = - false (* could be 'true' just as well; the DPLL procedure didn't provide a value for this variable *) + None (* the DPLL procedure didn't provide a value for this variable *) | assignment_from_list (x::xs) i = - if x=i then true - else if x=(~i) then false + 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 *) - apsome assignment_from_list (dpll [] fm') + case dpll [] fm' of + Some assignment => SatSolver.SATISFIABLE (assignment_from_list assignment) + | None => SatSolver.UNSATISFIABLE end end (* local *) in - SatSolver.add_solver ("dpll", Some o dpll_solver) + SatSolver.add_solver ("dpll", dpll_solver) end; (* ------------------------------------------------------------------------- *) (* Internal SAT solver, available as 'SatSolver.invoke_solver "auto"': uses *) -(* the first installed solver (other than "auto" itself) *) +(* all installed solvers (other than "auto" itself) until one returns either *) +(* SATISFIABLE or UNSATISFIABLE *) (* ------------------------------------------------------------------------- *) let fun auto_solver fm = - get_first (fn (name,solver) => + let + fun loop [] = + SatSolver.UNKNOWN + | loop ((name, solver)::solvers) = if name="auto" then - None + (* do not call solver "auto" from within "auto" *) + loop solvers else - ((if name="dpll" orelse name="enumerate" then + ( + (if name="dpll" orelse name="enumerate" then warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.") else ()); - solver fm)) (rev (!SatSolver.solvers)) + (* apply 'solver' to 'fm' *) + (case solver fm of + SatSolver.SATISFIABLE a => SatSolver.SATISFIABLE a + | SatSolver.UNSATISFIABLE => SatSolver.UNSATISFIABLE + | SatSolver.UNKNOWN => loop solvers) + handle SatSolver.NOT_CONFIGURED => loop solvers + ) + in + loop (rev (!SatSolver.solvers)) + end in SatSolver.add_solver ("auto", auto_solver) end; (* ------------------------------------------------------------------------- *) -(* ZChaff, Version 2003.12.04 *) +(* ZChaff, Version 2003.12.04 (http://www.princeton.edu/~chaff/zchaff.html) *) (* ------------------------------------------------------------------------- *) let fun zchaff fm = let - val inname = "isabelle.cnf" - val outname = "result" - val inpath = File.tmp_path (Path.unpack inname) - val outpath = File.tmp_path (Path.unpack outname) + val _ = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () + val inpath = File.tmp_path (Path.unpack "isabelle.cnf") + val outpath = File.tmp_path (Path.unpack "result") val cmd = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath) - fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm - fun readfn () = SatSolver.parse_std_result_file outpath "Verify Solution successful. Instance satisfiable" + fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) + fun readfn () = SatSolver.parse_std_result_file outpath ("Verify Solution successful. Instance satisfiable", "", "Instance unsatisfiable") val _ = assert (not (File.exists inpath)) ("file " ^ quote (Path.pack inpath) ^ " exists, please delete (will not overwrite)") val _ = assert (not (File.exists outpath)) ("file " ^ quote (Path.pack outpath) ^ " exists, please delete (will not overwrite)") - val assignment = SatSolver.make_external_solver cmd writefn readfn fm + val result = SatSolver.make_external_solver cmd writefn readfn fm val _ = (File.rm inpath handle _ => ()) val _ = (File.rm outpath handle _ => ()) in - assignment + result end in - SatSolver.add_solver ("zchaff", (fn fm => if getenv "ZCHAFF_HOME" <> "" then Some (zchaff fm) else None)) + SatSolver.add_solver ("zchaff", zchaff) +end; + +(* ------------------------------------------------------------------------- *) +(* BerkMin 561 (http://eigold.tripod.com/BerkMin.html) *) +(* ------------------------------------------------------------------------- *) + +let + fun berkmin fm = + let + val _ = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else () + val inpath = File.tmp_path (Path.unpack "isabelle.cnf") + val outpath = File.tmp_path (Path.unpack "result") + val cmd = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath) + fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) + fun readfn () = SatSolver.parse_std_result_file outpath ("Satisfiable !!", "solution =", "UNSATISFIABLE !!") + val _ = assert (not (File.exists inpath)) ("file " ^ quote (Path.pack inpath) ^ " exists, please delete (will not overwrite)") + val _ = assert (not (File.exists outpath)) ("file " ^ quote (Path.pack outpath) ^ " exists, please delete (will not overwrite)") + val result = SatSolver.make_external_solver cmd writefn readfn fm + val _ = (File.rm inpath handle _ => ()) + val _ = (File.rm outpath handle _ => ()) + in + result + end +in + SatSolver.add_solver ("berkmin", berkmin) +end; + +(* ------------------------------------------------------------------------- *) +(* Jerusat 1.3 (http://www.cs.tau.ac.il/~ale1/) *) +(* ------------------------------------------------------------------------- *) + +let + fun jerusat fm = + let + val _ = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () + val inpath = File.tmp_path (Path.unpack "isabelle.cnf") + val outpath = File.tmp_path (Path.unpack "result") + val cmd = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath) + fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) + fun readfn () = SatSolver.parse_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE") + val _ = assert (not (File.exists inpath)) ("file " ^ quote (Path.pack inpath) ^ " exists, please delete (will not overwrite)") + val _ = assert (not (File.exists outpath)) ("file " ^ quote (Path.pack outpath) ^ " exists, please delete (will not overwrite)") + val result = SatSolver.make_external_solver cmd writefn readfn fm + val _ = (File.rm inpath handle _ => ()) + val _ = (File.rm outpath handle _ => ()) + in + result + end +in + SatSolver.add_solver ("jerusat", jerusat) end; (* ------------------------------------------------------------------------- *) @@ -412,7 +511,7 @@ let fun mysolver fm = ... in - SatSolver.add_solver ("myname", (fn fm => if mysolver_is_installed then Some (mysolver fm) else None)); -- register the solver + SatSolver.add_solver ("myname", (fn fm => if mysolver_is_configured then mysolver fm else raise SatSolver.NOT_CONFIGURED)); -- register the solver end; -- the solver is now available as SatSolver.invoke_solver "myname"