src/HOL/Tools/sat_funcs.ML
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 21474 936edc65a3a5
child 21586 8da782143bde
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
webertj@17618
     1
(*  Title:      HOL/Tools/sat_funcs.ML
webertj@17618
     2
    ID:         $Id$
webertj@17618
     3
    Author:     Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
webertj@17622
     4
    Author:     Tjark Weber
webertj@19236
     5
    Copyright   2005-2006
webertj@17618
     6
webertj@17618
     7
webertj@17618
     8
Proof reconstruction from SAT solvers.
webertj@17618
     9
webertj@17618
    10
  Description:
webertj@17618
    11
    This file defines several tactics to invoke a proof-producing
webertj@17618
    12
    SAT solver on a propositional goal in clausal form.
webertj@17618
    13
webertj@17618
    14
    We use a sequent presentation of clauses to speed up resolution
webertj@17695
    15
    proof reconstruction.
webertj@17695
    16
    We call such clauses "raw clauses", which are of the form
webertj@20440
    17
          [x1, ..., xn, P] |- False
webertj@19236
    18
    (note the use of |- instead of ==>, i.e. of Isabelle's (meta-)hyps here),
webertj@20440
    19
    where each xi is a literal (see also comments in cnf_funcs.ML).
webertj@17618
    20
webertj@19236
    21
    This does not work for goals containing schematic variables!
webertj@19236
    22
webertj@20039
    23
      The tactic produces a clause representation of the given goal
webertj@20039
    24
      in DIMACS format and invokes a SAT solver, which should return
webertj@20039
    25
      a proof consisting of a sequence of resolution steps, indicating
webertj@20039
    26
      the two input clauses, and resulting in new clauses, leading to
webertj@20039
    27
      the empty clause (i.e. "False").  The tactic replays this proof
webertj@20039
    28
      in Isabelle and thus solves the overall goal.
webertj@17618
    29
webertj@20440
    30
  There are three SAT tactics available.  They differ in the CNF transformation
webertj@20039
    31
  used. "sat_tac" uses naive CNF transformation to transform the theorem to be
webertj@20039
    32
  proved before giving it to the SAT solver.  The naive transformation in the
webertj@20440
    33
  worst case can lead to an exponential blow up in formula size.  Another
webertj@20039
    34
  tactic, "satx_tac", uses "definitional CNF transformation" which attempts to
webertj@20039
    35
  produce a formula of linear size increase compared to the input formula, at
webertj@20039
    36
  the cost of possibly introducing new variables.  See cnf_funcs.ML for more
webertj@20440
    37
  comments on the CNF transformation.  "rawsat_tac" should be used with
webertj@20440
    38
  caution: no CNF transformation is performed, and the tactic's behavior is
webertj@20440
    39
  undefined if the subgoal is not already given as [| C1; ...; Cn |] ==> False,
webertj@20440
    40
  where each Ci is a disjunction.
webertj@17618
    41
webertj@20039
    42
  The SAT solver to be used can be set via the "solver" reference.  See
webertj@20039
    43
  sat_solvers.ML for possible values, and etc/settings for required (solver-
webertj@20039
    44
  dependent) configuration settings.  To replay SAT proofs in Isabelle, you
webertj@20039
    45
  must of course use a proof-producing SAT solver in the first place.
webertj@20039
    46
webertj@20039
    47
  Proofs are replayed only if "!quick_and_dirty" is false.  If
webertj@20039
    48
  "!quick_and_dirty" is true, the theorem (in case the SAT solver claims its
webertj@20039
    49
  negation to be unsatisfiable) is proved via an oracle.
webertj@17618
    50
*)
webertj@17618
    51
webertj@17618
    52
signature SAT =
webertj@17618
    53
sig
webertj@21267
    54
	val trace_sat  : bool ref    (* input: print trace messages *)
webertj@21267
    55
	val solver     : string ref  (* input: name of SAT solver to be used *)
webertj@21267
    56
	val counter    : int ref     (* output: number of resolution steps during last proof replay *)
webertj@21267
    57
	val rawsat_thm : cterm list -> thm
webertj@20440
    58
	val rawsat_tac : int -> Tactical.tactic
webertj@20440
    59
	val sat_tac    : int -> Tactical.tactic
webertj@20440
    60
	val satx_tac   : int -> Tactical.tactic
webertj@17618
    61
end
webertj@17618
    62
webertj@17622
    63
functor SATFunc (structure cnf : CNF) : SAT =
webertj@17622
    64
struct
webertj@17618
    65
webertj@17622
    66
val trace_sat = ref false;
webertj@17622
    67
webertj@20170
    68
val solver = ref "zchaff_with_proofs";  (* see HOL/Tools/sat_solver.ML for possible values *)
webertj@20039
    69
webertj@17622
    70
val counter = ref 0;
webertj@17622
    71
webertj@19236
    72
(* Thm.thm *)
webertj@21267
    73
val resolution_thm =  (* "[| ?P ==> False; ~ ?P ==> False |] ==> False" *)
webertj@19236
    74
	let
webertj@19236
    75
		val cterm = cterm_of (the_context ())
webertj@19236
    76
		val Q     = Var (("Q", 0), HOLogic.boolT)
webertj@19236
    77
		val False = HOLogic.false_const
webertj@19236
    78
	in
webertj@19236
    79
		Thm.instantiate ([], [(cterm Q, cterm False)]) case_split_thm
webertj@19236
    80
	end;
webertj@17622
    81
webertj@20278
    82
(* Thm.cterm *)
webertj@20278
    83
val cP = cterm_of (theory_of_thm resolution_thm) (Var (("P", 0), HOLogic.boolT));
webertj@20278
    84
webertj@20278
    85
(* ------------------------------------------------------------------------- *)
webertj@20278
    86
(* CLAUSE: during proof reconstruction, three kinds of clauses are           *)
webertj@20278
    87
(*      distinguished:                                                       *)
webertj@20278
    88
(*      1. NO_CLAUSE: clause not proved (yet)                                *)
webertj@20278
    89
(*      2. ORIG_CLAUSE: a clause as it occurs in the original problem        *)
webertj@20278
    90
(*      3. RAW_CLAUSE: a raw clause, with additional precomputed information *)
webertj@20278
    91
(*         (a mapping from int's to its literals) for faster proof           *)
webertj@20278
    92
(*         reconstruction                                                    *)
webertj@20278
    93
(* ------------------------------------------------------------------------- *)
webertj@20278
    94
webertj@20278
    95
datatype CLAUSE = NO_CLAUSE
webertj@20278
    96
                | ORIG_CLAUSE of Thm.thm
webertj@20278
    97
                | RAW_CLAUSE of Thm.thm * Thm.cterm Inttab.table;
webertj@20278
    98
webertj@17622
    99
(* ------------------------------------------------------------------------- *)
webertj@17809
   100
(* resolve_raw_clauses: given a non-empty list of raw clauses, we fold       *)
webertj@17809
   101
(*      resolution over the list (starting with its head), i.e. with two raw *)
webertj@17809
   102
(*      clauses                                                              *)
webertj@20440
   103
(*        [P, x1, ..., a, ..., xn] |- False                                  *)
webertj@17622
   104
(*      and                                                                  *)
webertj@20440
   105
(*        [Q, y1, ..., a', ..., ym] |- False                                 *)
webertj@19976
   106
(*      (where a and a' are dual to each other), we convert the first clause *)
webertj@19976
   107
(*      to                                                                   *)
webertj@20440
   108
(*        [P, x1, ..., xn] |- a ==> False ,                                  *)
webertj@19976
   109
(*      the second clause to                                                 *)
webertj@20440
   110
(*        [Q, y1, ..., ym] |- a' ==> False                                   *)
webertj@19976
   111
(*      and then perform resolution with                                     *)
webertj@19976
   112
(*        [| ?P ==> False; ~?P ==> False |] ==> False                        *)
webertj@19976
   113
(*      to produce                                                           *)
webertj@20440
   114
(*        [P, Q, x1, ..., xn, y1, ..., ym] |- False                          *)
webertj@20278
   115
(*      Each clause is accompanied with a table mapping integers (positive   *)
webertj@20278
   116
(*      for positive literals, negative for negative literals, and the same  *)
webertj@20278
   117
(*      absolute value for dual literals) to the actual literals as cterms.  *)
webertj@17622
   118
(* ------------------------------------------------------------------------- *)
webertj@17618
   119
webertj@20278
   120
(* (Thm.thm * Thm.cterm Inttab.table) list -> Thm.thm * Thm.cterm Inttab.table *)
webertj@17622
   121
webertj@17809
   122
fun resolve_raw_clauses [] =
webertj@17809
   123
	raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
webertj@17809
   124
  | resolve_raw_clauses (c::cs) =
webertj@17809
   125
	let
webertj@20278
   126
		(* find out which two hyps are used in the resolution *)
webertj@20278
   127
		local exception RESULT of int * Thm.cterm * Thm.cterm in
webertj@20278
   128
			(* Thm.cterm Inttab.table -> Thm.cterm Inttab.table -> int * Thm.cterm * Thm.cterm *)
webertj@20278
   129
			fun find_res_hyps hyp1_table hyp2_table = (
webertj@20278
   130
				Inttab.fold (fn (i, hyp1) => fn () =>
webertj@20278
   131
					case Inttab.lookup hyp2_table (~i) of
webertj@20278
   132
					  SOME hyp2 => raise RESULT (i, hyp1, hyp2)
webertj@20278
   133
					| NONE      => ()) hyp1_table ();
webertj@20278
   134
				raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
webertj@20278
   135
			) handle RESULT x => x
webertj@20278
   136
		end
webertj@19976
   137
webertj@20278
   138
		(* Thm.thm * Thm.cterm Inttab.table -> Thm.thm * Thm.cterm Inttab.table -> Thm.thm * Thm.cterm Inttab.table *)
webertj@20278
   139
		fun resolution (c1, hyp1_table) (c2, hyp2_table) =
webertj@17622
   140
		let
webertj@17622
   141
			val _ = if !trace_sat then
wenzelm@21474
   142
					tracing ("Resolving clause: " ^ string_of_thm c1 ^ " (hyps: " ^ ML_Syntax.str_of_list (Sign.string_of_term (theory_of_thm c1)) (#hyps (rep_thm c1))
wenzelm@21474
   143
						^ ")\nwith clause: " ^ string_of_thm c2 ^ " (hyps: " ^ ML_Syntax.str_of_list (Sign.string_of_term (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")")
webertj@17622
   144
				else ()
webertj@17809
   145
webertj@20278
   146
			(* the two literals used for resolution *)
webertj@20278
   147
			val (i1, hyp1, hyp2) = find_res_hyps hyp1_table hyp2_table
webertj@20278
   148
			val hyp1_is_neg      = i1 < 0
webertj@19236
   149
webertj@20278
   150
			val c1' = Thm.implies_intr hyp1 c1  (* Gamma1 |- hyp1 ==> False *)
webertj@20278
   151
			val c2' = Thm.implies_intr hyp2 c2  (* Gamma2 |- hyp2 ==> False *)
webertj@17618
   152
webertj@20278
   153
			val res_thm =  (* |- (lit ==> False) ==> (~lit ==> False) ==> False *)
webertj@19236
   154
				let
webertj@20278
   155
					val cLit = snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1))  (* strip Trueprop *)
webertj@19236
   156
				in
webertj@19976
   157
					Thm.instantiate ([], [(cP, cLit)]) resolution_thm
webertj@19236
   158
				end
webertj@19236
   159
webertj@19236
   160
			val _ = if !trace_sat then
webertj@19236
   161
					tracing ("Resolution theorem: " ^ string_of_thm res_thm)
webertj@19236
   162
				else ()
webertj@19236
   163
webertj@20440
   164
			(* Gamma1, Gamma2 |- False *)
webertj@20440
   165
			val c_new = Thm.implies_elim
webertj@20440
   166
				(Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1'))
webertj@20440
   167
				(if hyp1_is_neg then c1' else c2')
webertj@20278
   168
webertj@20278
   169
			(* since the mapping from integers to literals should be injective *)
webertj@20278
   170
			(* (over different clauses), 'K true' here should be equivalent to *)
webertj@20440
   171
			(* 'op=' (but slightly faster)                                     *)
webertj@20278
   172
			val hypnew_table = Inttab.merge (K true) (Inttab.delete i1 hyp1_table, Inttab.delete (~i1) hyp2_table)
webertj@19236
   173
webertj@19236
   174
			val _ = if !trace_sat then
wenzelm@21474
   175
					tracing ("Resulting clause: " ^ string_of_thm c_new ^ " (hyps: " ^ ML_Syntax.str_of_list (Sign.string_of_term (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
webertj@19236
   176
				else ()
webertj@17809
   177
			val _ = inc counter
webertj@17809
   178
		in
webertj@20278
   179
			(c_new, hypnew_table)
webertj@17809
   180
		end
webertj@17809
   181
	in
webertj@17809
   182
		fold resolution cs c
webertj@17809
   183
	end;
webertj@17618
   184
webertj@17622
   185
(* ------------------------------------------------------------------------- *)
webertj@17809
   186
(* replay_proof: replays the resolution proof returned by the SAT solver;    *)
webertj@17809
   187
(*      cf. SatSolver.proof for details of the proof format.  Updates the    *)
webertj@17809
   188
(*      'clauses' array with derived clauses, and returns the derived clause *)
webertj@17809
   189
(*      at index 'empty_id' (which should just be "False" if proof           *)
webertj@17809
   190
(*      reconstruction was successful, with the used clauses as hyps).       *)
webertj@20278
   191
(*      'atom_table' must contain an injective mapping from all atoms that   *)
webertj@20278
   192
(*      occur (as part of a literal) in 'clauses' to positive integers.      *)
webertj@17622
   193
(* ------------------------------------------------------------------------- *)
webertj@17622
   194
webertj@20278
   195
(* int Termtab.table -> CLAUSE Array.array -> SatSolver.proof -> Thm.thm *)
webertj@17618
   196
webertj@20278
   197
fun replay_proof atom_table clauses (clause_table, empty_id) =
webertj@17622
   198
let
webertj@20278
   199
	(* Thm.cterm -> int option *)
webertj@20278
   200
	fun index_of_literal chyp = (
webertj@20278
   201
		case (HOLogic.dest_Trueprop o term_of) chyp of
webertj@20278
   202
		  (Const ("Not", _) $ atom) =>
webertj@20278
   203
			SOME (~(valOf (Termtab.lookup atom_table atom)))
webertj@20278
   204
		| atom =>
webertj@20278
   205
			SOME (valOf (Termtab.lookup atom_table atom))
webertj@20278
   206
	) handle TERM _ => NONE;  (* 'chyp' is not a literal *)
webertj@20278
   207
webertj@20278
   208
	(* int -> Thm.thm * Thm.cterm Inttab.table *)
webertj@17623
   209
	fun prove_clause id =
webertj@17623
   210
		case Array.sub (clauses, id) of
webertj@20278
   211
		  RAW_CLAUSE clause =>
webertj@20278
   212
			clause
webertj@20278
   213
		| ORIG_CLAUSE thm =>
webertj@20278
   214
			(* convert the original clause *)
webertj@17623
   215
			let
webertj@20278
   216
				val _         = if !trace_sat then tracing ("Using original clause #" ^ string_of_int id) else ()
webertj@20278
   217
				val raw       = cnf.clause2raw_thm thm
webertj@20278
   218
				val lit_table = fold (fn chyp => fn lit_table => (case index_of_literal chyp of
webertj@20278
   219
					  SOME i => Inttab.update_new (i, chyp) lit_table
webertj@20278
   220
					| NONE   => lit_table)) (#hyps (Thm.crep_thm raw)) Inttab.empty
webertj@20278
   221
				val clause    = (raw, lit_table)
webertj@20278
   222
				val _         = Array.update (clauses, id, RAW_CLAUSE clause)
webertj@17623
   223
			in
webertj@20278
   224
				clause
webertj@20278
   225
			end
webertj@20278
   226
		| NO_CLAUSE =>
webertj@20278
   227
			(* prove the clause, using information from 'clause_table' *)
webertj@20278
   228
			let
webertj@20278
   229
				val _      = if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else ()
webertj@20278
   230
				val ids    = valOf (Inttab.lookup clause_table id)
webertj@20278
   231
				val clause = resolve_raw_clauses (map prove_clause ids)
webertj@20278
   232
				val _      = Array.update (clauses, id, RAW_CLAUSE clause)
webertj@20278
   233
				val _      = if !trace_sat then tracing ("Replay chain successful; clause stored at #" ^ string_of_int id) else ()
webertj@20278
   234
			in
webertj@20278
   235
				clause
webertj@17623
   236
			end
webertj@17618
   237
webertj@17809
   238
	val _            = counter := 0
webertj@20278
   239
	val empty_clause = fst (prove_clause empty_id)
webertj@17809
   240
	val _            = if !trace_sat then tracing ("Proof reconstruction successful; " ^ string_of_int (!counter) ^ " resolution step(s) total.") else ()
webertj@17622
   241
in
webertj@17809
   242
	empty_clause
webertj@17622
   243
end;
webertj@17622
   244
webertj@20278
   245
(* ------------------------------------------------------------------------- *)
webertj@20278
   246
(* string_of_prop_formula: return a human-readable string representation of  *)
webertj@20278
   247
(*      a 'prop_formula' (just for tracing)                                  *)
webertj@20278
   248
(* ------------------------------------------------------------------------- *)
webertj@20278
   249
webertj@17809
   250
(* PropLogic.prop_formula -> string *)
webertj@20278
   251
webertj@17809
   252
fun string_of_prop_formula PropLogic.True             = "True"
webertj@17809
   253
  | string_of_prop_formula PropLogic.False            = "False"
webertj@17809
   254
  | string_of_prop_formula (PropLogic.BoolVar i)      = "x" ^ string_of_int i
webertj@17809
   255
  | string_of_prop_formula (PropLogic.Not fm)         = "~" ^ string_of_prop_formula fm
webertj@17809
   256
  | string_of_prop_formula (PropLogic.Or (fm1, fm2))  = "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")"
webertj@17809
   257
  | string_of_prop_formula (PropLogic.And (fm1, fm2)) = "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")";
webertj@17622
   258
webertj@17622
   259
(* ------------------------------------------------------------------------- *)
webertj@21267
   260
(* take_prefix:                                                              *)
webertj@21267
   261
(*      take_prefix n [x_1, ..., x_k] = ([x_1, ..., x_n], [x_n+1, ..., x_k]) *)
webertj@17622
   262
(* ------------------------------------------------------------------------- *)
webertj@17618
   263
webertj@21267
   264
(* int -> 'a list -> 'a list * 'a list *)
webertj@21267
   265
webertj@21267
   266
fun take_prefix n xs =
webertj@21267
   267
let
webertj@21267
   268
	fun take 0 (rxs, xs)      = (rev rxs, xs)
webertj@21267
   269
	  | take _ (rxs, [])      = (rev rxs, [])
webertj@21267
   270
	  | take n (rxs, x :: xs) = take (n-1) (x :: rxs, xs)
webertj@21267
   271
in
webertj@21267
   272
	take n ([], xs)
webertj@21267
   273
end;
webertj@17809
   274
webertj@21267
   275
(* ------------------------------------------------------------------------- *)
webertj@21267
   276
(* rawsat_thm: run external SAT solver with the given clauses.  Reconstructs *)
webertj@21267
   277
(*      a proof from the resulting proof trace of the SAT solver.  The       *)
webertj@21267
   278
(*      theorem returned is just "False" (with some of the given clauses as  *)
webertj@21267
   279
(*      hyps).                                                               *)
webertj@21267
   280
(* ------------------------------------------------------------------------- *)
webertj@21267
   281
webertj@21267
   282
(* Thm.cterm list -> Thm.thm *)
webertj@21267
   283
webertj@21267
   284
fun rawsat_thm clauses =
webertj@17622
   285
let
webertj@17809
   286
	(* remove premises that equal "True" *)
webertj@21267
   287
	val clauses' = filter (fn clause =>
webertj@21267
   288
		(not_equal HOLogic.true_const o HOLogic.dest_Trueprop o term_of) clause
webertj@21267
   289
			handle TERM ("dest_Trueprop", _) => true) clauses
webertj@17809
   290
	(* remove non-clausal premises -- of course this shouldn't actually   *)
webertj@21267
   291
	(* remove anything as long as 'rawsat_tac' is only called after the   *)
webertj@17809
   292
	(* premises have been converted to clauses                            *)
webertj@21267
   293
	val clauses'' = filter (fn clause =>
webertj@21267
   294
		((cnf.is_clause o HOLogic.dest_Trueprop o term_of) clause
webertj@21267
   295
			handle TERM ("dest_Trueprop", _) => false)
webertj@21267
   296
		orelse (
webertj@21267
   297
			warning ("Ignoring non-clausal premise " ^ string_of_cterm clause);
webertj@21267
   298
			false)) clauses'
webertj@17809
   299
	(* remove trivial clauses -- this is necessary because zChaff removes *)
webertj@17809
   300
	(* trivial clauses during preprocessing, and otherwise our clause     *)
webertj@17809
   301
	(* numbering would be off                                             *)
webertj@21267
   302
	val clauses''' = filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o term_of) clauses''
webertj@21267
   303
	val _ = if !trace_sat then
webertj@21267
   304
			tracing ("Non-trivial clauses:\n" ^ space_implode "\n" (map string_of_cterm clauses'''))
webertj@19534
   305
		else ()
webertj@17809
   306
	(* translate clauses from HOL terms to PropLogic.prop_formula *)
webertj@21267
   307
	val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o term_of) clauses''' Termtab.empty
webertj@21267
   308
	val _ = if !trace_sat then
webertj@17809
   309
			tracing ("Invoking SAT solver on clauses:\n" ^ space_implode "\n" (map string_of_prop_formula fms))
webertj@17809
   310
		else ()
webertj@17809
   311
	val fm                = PropLogic.all fms
webertj@17842
   312
	(* unit -> Thm.thm *)
webertj@21267
   313
	fun make_quick_and_dirty_thm () =
webertj@21267
   314
	let
webertj@21267
   315
		val _ = if !trace_sat then
webertj@21267
   316
				tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
webertj@21267
   317
			else ()
webertj@21267
   318
		val False_thm = SkipProof.make_thm (the_context ()) (HOLogic.Trueprop $ HOLogic.false_const)
webertj@21267
   319
	in
webertj@21267
   320
		fold Thm.weaken clauses''' False_thm
webertj@21267
   321
	end
webertj@17618
   322
in
webertj@21268
   323
	case (tracing ("Invoking solver " ^ (!solver)); SatSolver.invoke_solver (!solver) fm) of
webertj@17842
   324
	  SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => (
webertj@17842
   325
		if !trace_sat then
webertj@17842
   326
			tracing ("Proof trace from SAT solver:\n" ^
wenzelm@21474
   327
				"clauses: " ^ ML_Syntax.str_of_list (ML_Syntax.str_of_pair string_of_int (ML_Syntax.str_of_list string_of_int)) (Inttab.dest clause_table) ^ "\n" ^
webertj@17842
   328
				"empty clause: " ^ string_of_int empty_id)
webertj@17842
   329
		else ();
webertj@17842
   330
		if !quick_and_dirty then
webertj@17842
   331
			make_quick_and_dirty_thm ()
webertj@17842
   332
		else
webertj@17842
   333
			let
webertj@21267
   334
				(* optimization: convert the given clauses to "[c_1 && ... && c_n] |- c_i";  *)
webertj@21267
   335
				(*               this avoids accumulation of hypotheses during resolution    *)
webertj@21267
   336
				(* [c_1, ..., c_n] |- c_1 && ... && c_n *)
webertj@21268
   337
				val clauses_thm = Conjunction.intr_list (map Thm.assume clauses''')
webertj@20440
   338
				(* [c_1 && ... && c_n] |- c_1 && ... && c_n *)
webertj@21267
   339
				val cnf_cterm = cprop_of clauses_thm
webertj@20440
   340
				val cnf_thm   = Thm.assume cnf_cterm
webertj@20440
   341
				(* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *)
webertj@21268
   342
				val cnf_clauses = Conjunction.elim_list cnf_thm
webertj@20278
   343
				(* initialize the clause array with the given clauses *)
webertj@20440
   344
				val max_idx    = valOf (Inttab.max_key clause_table)
webertj@20440
   345
				val clause_arr = Array.array (max_idx + 1, NO_CLAUSE)
webertj@21267
   346
				val _          = fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1)) cnf_clauses 0
webertj@19236
   347
				(* replay the proof to derive the empty clause *)
webertj@20440
   348
				(* [c_1 && ... && c_n] |- False *)
webertj@21268
   349
				val raw_thm = replay_proof atom_table clause_arr (clause_table, empty_id)
webertj@17842
   350
			in
webertj@20440
   351
				(* [c_1, ..., c_n] |- False *)
webertj@21267
   352
				Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm
webertj@17842
   353
			end)
webertj@17622
   354
	| SatSolver.UNSATISFIABLE NONE =>
webertj@17842
   355
		if !quick_and_dirty then (
webertj@17842
   356
			warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof";
webertj@17842
   357
			make_quick_and_dirty_thm ()
webertj@17842
   358
		) else
webertj@17842
   359
			raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, [])
webertj@17622
   360
	| SatSolver.SATISFIABLE assignment =>
webertj@17622
   361
		let
webertj@17622
   362
			val msg = "SAT solver found a countermodel:\n"
webertj@17809
   363
				^ (commas
webertj@17809
   364
					o map (fn (term, idx) =>
webertj@17809
   365
						Sign.string_of_term (the_context ()) term ^ ": "
webertj@17809
   366
							^ (case assignment idx of NONE => "arbitrary" | SOME true => "true" | SOME false => "false")))
webertj@17809
   367
					(Termtab.dest atom_table)
webertj@17622
   368
		in
webertj@17622
   369
			raise THM (msg, 0, [])
webertj@17622
   370
		end
webertj@17622
   371
	| SatSolver.UNKNOWN =>
webertj@17622
   372
		raise THM ("SAT solver failed to decide the formula", 0, [])
webertj@17622
   373
end;
webertj@17618
   374
webertj@17622
   375
(* ------------------------------------------------------------------------- *)
webertj@17622
   376
(* Tactics                                                                   *)
webertj@17622
   377
(* ------------------------------------------------------------------------- *)
webertj@17618
   378
webertj@17809
   379
(* ------------------------------------------------------------------------- *)
webertj@17809
   380
(* rawsat_tac: solves the i-th subgoal of the proof state; this subgoal      *)
webertj@17809
   381
(*      should be of the form                                                *)
webertj@17809
   382
(*        [| c1; c2; ...; ck |] ==> False                                    *)
webertj@17809
   383
(*      where each cj is a non-empty clause (i.e. a disjunction of literals) *)
webertj@17809
   384
(*      or "True"                                                            *)
webertj@17809
   385
(* ------------------------------------------------------------------------- *)
webertj@17809
   386
webertj@17809
   387
(* int -> Tactical.tactic *)
webertj@17809
   388
webertj@21267
   389
fun rawsat_tac i = METAHYPS (fn prems => rtac (rawsat_thm (map cprop_of prems)) 1) i;
webertj@17618
   390
webertj@17809
   391
(* ------------------------------------------------------------------------- *)
webertj@17809
   392
(* pre_cnf_tac: converts the i-th subgoal                                    *)
webertj@17809
   393
(*        [| A1 ; ... ; An |] ==> B                                          *)
webertj@17809
   394
(*      to                                                                   *)
webertj@17809
   395
(*        [| A1; ... ; An ; ~B |] ==> False                                  *)
webertj@17809
   396
(*      (handling meta-logical connectives in B properly before negating),   *)
webertj@17809
   397
(*      then replaces meta-logical connectives in the premises (i.e. "==>",  *)
webertj@17809
   398
(*      "!!" and "==") by connectives of the HOL object-logic (i.e. by       *)
webertj@19553
   399
(*      "-->", "!", and "="), then performs beta-eta-normalization on the    *)
webertj@19553
   400
(*      subgoal                                                              *)
webertj@17809
   401
(* ------------------------------------------------------------------------- *)
webertj@17809
   402
webertj@17809
   403
(* int -> Tactical.tactic *)
webertj@17809
   404
webertj@20278
   405
fun pre_cnf_tac i =
webertj@20278
   406
	rtac ccontr i THEN ObjectLogic.atomize_tac i THEN
webertj@20278
   407
		PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal i) (Drule.beta_eta_conversion)));
webertj@17809
   408
webertj@17809
   409
(* ------------------------------------------------------------------------- *)
webertj@17809
   410
(* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *)
webertj@17809
   411
(*      if not, eliminates conjunctions (i.e. each clause of the CNF formula *)
webertj@17809
   412
(*      becomes a separate premise), then applies 'rawsat_tac' to solve the  *)
webertj@17809
   413
(*      subgoal                                                              *)
webertj@17809
   414
(* ------------------------------------------------------------------------- *)
webertj@17697
   415
webertj@17809
   416
(* int -> Tactical.tactic *)
webertj@17809
   417
webertj@20278
   418
fun cnfsat_tac i =
webertj@20278
   419
	(etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac i);
webertj@17618
   420
webertj@17809
   421
(* ------------------------------------------------------------------------- *)
webertj@17809
   422
(* cnfxsat_tac: checks if the empty clause "False" occurs among the          *)
webertj@17809
   423
(*      premises; if not, eliminates conjunctions (i.e. each clause of the   *)
webertj@17809
   424
(*      CNF formula becomes a separate premise) and existential quantifiers, *)
webertj@17809
   425
(*      then applies 'rawsat_tac' to solve the subgoal                       *)
webertj@17809
   426
(* ------------------------------------------------------------------------- *)
webertj@17809
   427
webertj@17809
   428
(* int -> Tactical.tactic *)
webertj@17809
   429
webertj@20278
   430
fun cnfxsat_tac i =
webertj@20278
   431
	(etac FalseE i) ORELSE
webertj@20278
   432
		(REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac i);
webertj@17618
   433
webertj@17809
   434
(* ------------------------------------------------------------------------- *)
webertj@17809
   435
(* sat_tac: tactic for calling an external SAT solver, taking as input an    *)
webertj@17809
   436
(*      arbitrary formula.  The input is translated to CNF, possibly causing *)
webertj@17809
   437
(*      an exponential blowup.                                               *)
webertj@17809
   438
(* ------------------------------------------------------------------------- *)
webertj@17809
   439
webertj@17809
   440
(* int -> Tactical.tactic *)
webertj@17809
   441
webertj@20278
   442
fun sat_tac i =
webertj@20278
   443
	pre_cnf_tac i THEN cnf.cnf_rewrite_tac i THEN cnfsat_tac i;
webertj@17809
   444
webertj@17809
   445
(* ------------------------------------------------------------------------- *)
webertj@17809
   446
(* satx_tac: tactic for calling an external SAT solver, taking as input an   *)
webertj@17809
   447
(*      arbitrary formula.  The input is translated to CNF, possibly         *)
webertj@17809
   448
(*      introducing new literals.                                            *)
webertj@17809
   449
(* ------------------------------------------------------------------------- *)
webertj@17809
   450
webertj@17809
   451
(* int -> Tactical.tactic *)
webertj@17809
   452
webertj@20278
   453
fun satx_tac i =
webertj@20278
   454
	pre_cnf_tac i THEN cnf.cnfx_rewrite_tac i THEN cnfxsat_tac i;
webertj@17618
   455
webertj@20039
   456
end;  (* of structure SATFunc *)