src/HOL/Tools/sat_funcs.ML

code reformatted and restructured, many minor modifications

(*  Title:      HOL/Tools/sat_funcs.ML
    ID:         $Id$
    Author:     Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
    Author:     Tjark Weber
    Copyright   2005


Proof reconstruction from SAT solvers.

  Description:
    This file defines several tactics to invoke a proof-producing
    SAT solver on a propositional goal in clausal form.

    We use a sequent presentation of clauses to speed up resolution
    proof reconstruction. 
    We call such clauses as "raw clauses", which are of the form
          [| c1; c2; ...; ck |] ==> False
    where each clause ci is of the form
          [|l1,  l2,  ..., lm |] ==> False,
    where li is a literal  (see also comments in cnf_funcs.ML).

    -- observe that this is the "dualized" version of the standard
       clausal form
           l1' \/ l2' \/ ... \/ lm', where li is the negation normal
       form of ~li'.
       The tactic produces a clause representation of the given goal
       in DIMACS format and invokes a SAT solver, which should return
       a proof consisting of a sequence of resolution steps, indicating
       the two input clauses and the variable resolved upon, and resulting
       in new clauses, leading to the empty clause (i.e., False).
       The tactic replays this proof in Isabelle and thus solves the
       overall goal.

   There are two SAT tactics available. They differ in the CNF transformation
   used. The "sat_tac" uses naive CNF transformation to transform the theorem
   to be proved before giving it to SAT solver. The naive transformation in 
   some worst case can lead to explonential blow up in formula size.
   The other tactic, the "satx_tac" uses the "definitional CNF transformation"
   which produces formula of linear size increase compared to the input formula.
   This transformation introduces new variables. See also cnf_funcs.ML for
   more comments.

 Notes for the current revision:
   - The current version supports only zChaff prover.
   - The environment variable ZCHAFF_HOME must be set to point to
     the directory where zChaff executable resides
   - The environment variable ZCHAFF_VERSION must be set according to
     the version of zChaff used. Current supported version of zChaff:
     zChaff version 2004.11.15
*)

signature SAT =
sig
	val trace_sat : bool ref  (* print trace messages *)
	val sat_tac   : Tactical.tactic
	val satx_tac  : Tactical.tactic
end

functor SATFunc (structure cnf : CNF) : SAT =
struct

val trace_sat = ref false;

val counter = ref 0;

(* ------------------------------------------------------------------------- *)
(* rev_lookup: look up the Isabelle/HOL atom corresponding to a DIMACS       *)
(*      variable index in the dictionary.  This index should exist in the    *)
(*      dictionary, otherwise exception Option is raised.                    *)
(* ------------------------------------------------------------------------- *)

(* 'b -> ('a * 'b) list -> 'a *)

fun rev_lookup idx []                   = raise Option
  | rev_lookup idx ((key, entry)::dict) = if entry=idx then key else rev_lookup idx dict;

(* ------------------------------------------------------------------------- *)
(* swap_prem: convert rules of the form                                      *)
(*       l1 ==> l2 ==> .. ==> li ==> .. ==> False                            *)
(*     to                                                                    *)
(*       l1 ==> l2 ==> .... ==> ~li                                          *)
(* ------------------------------------------------------------------------- *)

fun swap_prem rslv c =
let
	val thm1 = rule_by_tactic (metacut_tac c 1 THEN (atac 1) THEN (REPEAT_SOME atac)) rslv
in
	rule_by_tactic (ALLGOALS (cnf.weakening_tac)) thm1
end;

(* ------------------------------------------------------------------------- *)
(* is_dual: check if two atoms are dual to each other                        *)
(* ------------------------------------------------------------------------- *)

(* Term.term -> Term.term -> bool *)

fun is_dual (Const ("Trueprop", _) $ x) y = is_dual x y
  | is_dual x (Const ("Trueprop", _) $ y) = is_dual x y
  | is_dual (Const ("Not", _) $ x) y      = (x = y)
  | is_dual x (Const ("Not", _) $ y)      = (x = y)
  | is_dual x y                           = false;

(* ------------------------------------------------------------------------- *)
(* dual_mem: check if an atom has a dual in a list of atoms                  *)
(* ------------------------------------------------------------------------- *)

(* Term.term -> Term.term list -> bool *)

fun dual_mem x []      = false
  | dual_mem x (y::ys) = is_dual x y orelse dual_mem x ys;

(* ------------------------------------------------------------------------- *)
(* replay_chain: proof reconstruction: given two clauses                     *)
(*        [| x1 ; .. ; a ; .. ; xn |] ==> False                              *)
(*      and                                                                  *)
(*        [| y1 ; .. ; ~a ; .. ; ym |] ==> False ,                           *)
(*      we first convert the first clause into                               *)
(*        [| x1 ; ... ; xn |] ==> ~a     (using swap_prem)                   *)
(*      and do a resolution with the second clause to produce                *)
(*        [| y1 ; ... ; x1 ; ... ; xn ; ... ; yn |] ==> False                *)
(* ------------------------------------------------------------------------- *)

(* Theory.theory -> Thm.thm option Array.array -> int -> int list -> unit *)

fun replay_chain sg clauses idx (c::cs) =
let
	val (SOME fc) = Array.sub (clauses, c)

	fun strip_neg (Const ("Trueprop", _) $ x) = strip_neg x
	  | strip_neg (Const ("Not", _) $ x)      = x
	  | strip_neg x                           = x

	(* find out which atom (literal) is used in the resolution *)
	fun res_atom []      _  = raise THM ("Proof reconstruction failed!", 0, [])
	  | res_atom (x::xs) ys = if dual_mem x ys then strip_neg x else res_atom xs ys

	fun replay old []        =
		old
	  | replay old (cl::cls) =
		let
			val icl  = (valOf o Array.sub) (clauses, cl)
			val var  = res_atom (prems_of old) (prems_of icl)
			val atom = cterm_of sg var
			val rslv = instantiate' [] [SOME atom] notI
			val _ = if !trace_sat then
					tracing ("Resolving clause: " ^ string_of_thm old ^
						"\nwith clause: " ^ string_of_thm icl ^
						"\nusing literal " ^ string_of_cterm atom ^ ".")
				else ()
			val thm1 = (rule_by_tactic (REPEAT_SOME (rtac (swap_prem rslv old))) icl
				handle THM _ => rule_by_tactic (REPEAT_SOME (rtac (swap_prem rslv icl))) old)
			val new  = rule_by_tactic distinct_subgoals_tac thm1
			val _    = if !trace_sat then tracing ("Resulting clause: " ^ string_of_thm new) else ()
			val _    = inc counter
		in
			replay new cls
		end

	val _ = Array.update (clauses, idx, SOME (replay fc cs))

	val _ = if !trace_sat then
			tracing ("Replay chain successful; clause stored at #" ^ string_of_int idx)
		else ()
in
	()
end;

(* ------------------------------------------------------------------------- *)
(* replay_proof: replay the resolution proof returned by the SAT solver; cf. *)
(*      SatSolver.proof for details of the proof format.  Returns the        *)
(*      theorem established by the proof (which is just False).              *)
(* ------------------------------------------------------------------------- *)

(* Theory.theory -> Thm.thm option Array.array -> SatSolver.proof -> Thm.thm *)

fun replay_proof sg clauses (clause_table, empty_id) =
let
	fun complete []      =
		true
	  | complete (x::xs) =
		(isSome o Array.sub) (clauses, x) andalso complete xs

	fun do_chains []        =
		()
	  | do_chains (ch::chs) =
		let
			val (idx, cls) = ch
		in
			if complete cls then (
				replay_chain sg clauses idx cls;
				do_chains chs
			) else
				do_chains (chs @ [ch])
		end

	val _ = do_chains (Inttab.dest clause_table)

	val _ = if !trace_sat then
			tracing (string_of_int (!counter) ^ " resolution steps total.")
		else ()
in
	(valOf o Array.sub) (clauses, empty_id)
end;

(* ------------------------------------------------------------------------- *)
(* Functions to build the sat tactic                                         *)
(* ------------------------------------------------------------------------- *)

(* A trivial tactic, used in preprocessing before calling the main tactic *)
val pre_sat_tac = (REPEAT (etac conjE 1)) THEN (REPEAT ((atac 1) ORELSE (etac FalseE 1)));

fun collect_atoms (Const ("Trueprop", _) $ x) ls = collect_atoms x ls
  | collect_atoms (Const ("op |", _) $ x $ y) ls = collect_atoms x (collect_atoms y ls)
  | collect_atoms x                           ls = x ins ls;

fun has_duals []      = false
  | has_duals (x::xs) = dual_mem x xs orelse has_duals xs;

fun is_trivial_clause (Const ("True", _)) = true
  | is_trivial_clause c                   = has_duals (collect_atoms c []);

(* ------------------------------------------------------------------------- *)
(* rawsat_thm: run external SAT solver with the given clauses.  Reconstructs *)
(*      a proof from the resulting proof trace of the SAT solver.            *)
(* ------------------------------------------------------------------------- *)

fun rawsat_thm sg prems =
let
	val thms       = filter (not o is_trivial_clause o term_of o cprop_of) prems  (* remove trivial clauses *)
	val (fm, dict) = cnf.cnf2prop thms
	val _          = if !trace_sat then tracing "Invoking SAT solver ..." else ()
in
	case SatSolver.invoke_solver "zchaff_with_proofs" fm of
	  SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) =>
		let
			val _         = if !trace_sat then
					tracing ("Proof trace from SAT solver:\n" ^
						"clauses: [" ^ commas (map (fn (c, cs) =>
							"(" ^ string_of_int c ^ ", [" ^ commas (map string_of_int cs) ^ "])") (Inttab.dest clause_table)) ^ "]\n" ^
						"empty clause: " ^ string_of_int empty_id)
				else ()
			val raw_thms  = cnf.cnf2raw_thms thms
			val raw_thms' = map (rule_by_tactic distinct_subgoals_tac) raw_thms
			(* initialize the clause array with the original clauses *)
			val max_idx   = valOf (Inttab.max_key clause_table)
			val clauses   = Array.array (max_idx + 1, NONE)
			val _         = fold (fn thm => fn idx => (Array.update (clauses, idx, SOME thm); idx+1)) raw_thms' 0
		in
			replay_proof sg clauses (clause_table, empty_id)
		end
	| SatSolver.UNSATISFIABLE NONE =>
		raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, [])
	| SatSolver.SATISFIABLE assignment =>
		let
			val msg = "SAT solver found a countermodel:\n"
				^ (enclose "{" "}"
					o commas
					o map (Sign.string_of_term sg o fst)
					o filter (fn (_, idx) => getOpt (assignment idx, false))) dict
		in
			raise THM (msg, 0, [])
		end
	| SatSolver.UNKNOWN =>
		raise THM ("SAT solver failed to decide the formula", 0, [])
end;

(* ------------------------------------------------------------------------- *)
(* Tactics                                                                   *)
(* ------------------------------------------------------------------------- *)

fun cnfsat_basic_tac state =
let
	val sg = Thm.sign_of_thm state
in
	METAHYPS (fn prems => rtac (rawsat_thm sg prems) 1) 1 state
end;

(* Tactic for calling external SAT solver, taking as input CNF clauses *)
val cnfsat_tac = pre_sat_tac THEN (IF_UNSOLVED cnfsat_basic_tac);

(* Tactic for calling external SAT solver, taking as input arbitrary formula *)
val sat_tac = cnf.cnf_thin_tac THEN cnfsat_tac;

(*
  Tactic for calling external SAT solver, taking as input arbitrary formula.
  The input is translated to CNF (in primitive form), possibly introducing
  new literals.
*)
val satx_tac = cnf.cnfx_thin_tac THEN cnfsat_tac;

end;  (* of structure *)