src/HOL/Tools/sat_funcs.ML
author haftmann
Tue May 09 10:09:37 2006 +0200 (2006-05-09)
changeset 19599 a5c7eb37d14f
parent 19553 9d15911f1893
child 19976 aa35f8e27c73
permissions -rw-r--r--
added DatatypeHooks
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@19236
    17
          x1; ...; xn; c1; c2; ...; ck |- False
webertj@19236
    18
    (note the use of |- instead of ==>, i.e. of Isabelle's (meta-)hyps here),
webertj@17618
    19
    where each clause ci is of the form
webertj@19236
    20
          ~ (l1 | l2 | ... | lm) ==> False,
webertj@19236
    21
    where each xi and each li is a literal (see also comments in cnf_funcs.ML).
webertj@17618
    22
webertj@19236
    23
    This does not work for goals containing schematic variables!
webertj@19236
    24
webertj@17618
    25
       The tactic produces a clause representation of the given goal
webertj@17618
    26
       in DIMACS format and invokes a SAT solver, which should return
webertj@17618
    27
       a proof consisting of a sequence of resolution steps, indicating
webertj@17695
    28
       the two input clauses, and resulting in new clauses, leading to
webertj@17695
    29
       the empty clause (i.e., False).  The tactic replays this proof
webertj@17695
    30
       in Isabelle and thus solves the overall goal.
webertj@17618
    31
webertj@17618
    32
   There are two SAT tactics available. They differ in the CNF transformation
webertj@17618
    33
   used. The "sat_tac" uses naive CNF transformation to transform the theorem
webertj@17695
    34
   to be proved before giving it to SAT solver. The naive transformation in
webertj@17618
    35
   some worst case can lead to explonential blow up in formula size.
webertj@17618
    36
   The other tactic, the "satx_tac" uses the "definitional CNF transformation"
webertj@17618
    37
   which produces formula of linear size increase compared to the input formula.
webertj@17618
    38
   This transformation introduces new variables. See also cnf_funcs.ML for
webertj@17618
    39
   more comments.
webertj@17618
    40
webertj@17618
    41
 Notes for the current revision:
webertj@17618
    42
   - The current version supports only zChaff prover.
webertj@17618
    43
   - The environment variable ZCHAFF_HOME must be set to point to
webertj@17618
    44
     the directory where zChaff executable resides
webertj@17618
    45
   - The environment variable ZCHAFF_VERSION must be set according to
webertj@17618
    46
     the version of zChaff used. Current supported version of zChaff:
webertj@17618
    47
     zChaff version 2004.11.15
webertj@17695
    48
   - zChaff must have been compiled with proof generation enabled
webertj@17695
    49
     (#define VERIFY_ON).
webertj@17618
    50
*)
webertj@17618
    51
webertj@17618
    52
signature SAT =
webertj@17618
    53
sig
webertj@17622
    54
	val trace_sat : bool ref  (* print trace messages *)
webertj@17809
    55
	val sat_tac   : int -> Tactical.tactic
webertj@17809
    56
	val satx_tac  : int -> Tactical.tactic
webertj@17843
    57
	val counter   : int ref  (* number of resolution steps during last proof replay *)
webertj@17618
    58
end
webertj@17618
    59
webertj@17622
    60
functor SATFunc (structure cnf : CNF) : SAT =
webertj@17622
    61
struct
webertj@17618
    62
webertj@17622
    63
val trace_sat = ref false;
webertj@17622
    64
webertj@17622
    65
val counter = ref 0;
webertj@17622
    66
webertj@19236
    67
(* Thm.thm *)
webertj@19236
    68
val resolution_thm =  (* "[| P ==> False; ~P ==> False |] ==> False" *)
webertj@19236
    69
	let
webertj@19236
    70
		val cterm = cterm_of (the_context ())
webertj@19236
    71
		val Q     = Var (("Q", 0), HOLogic.boolT)
webertj@19236
    72
		val False = HOLogic.false_const
webertj@19236
    73
	in
webertj@19236
    74
		Thm.instantiate ([], [(cterm Q, cterm False)]) case_split_thm
webertj@19236
    75
	end;
webertj@17622
    76
webertj@17622
    77
(* ------------------------------------------------------------------------- *)
webertj@17809
    78
(* resolve_raw_clauses: given a non-empty list of raw clauses, we fold       *)
webertj@17809
    79
(*      resolution over the list (starting with its head), i.e. with two raw *)
webertj@17809
    80
(*      clauses                                                              *)
webertj@17809
    81
(*        [| x1; ... ; a; ...; xn |] ==> False                               *)
webertj@17622
    82
(*      and                                                                  *)
webertj@17809
    83
(*        [| y1; ... ; a'; ...; ym |] ==> False                              *)
webertj@17809
    84
(*      (where a and a' are dual to each other), we first convert the first  *)
webertj@17809
    85
(*      clause to                                                            *)
webertj@17809
    86
(*        [| x1; ...; xn |] ==> a'                                           *)
webertj@17809
    87
(*      (using swap_prem and perhaps notnotD), and then do a resolution with *)
webertj@17809
    88
(*      the second clause to produce                                         *)
webertj@17809
    89
(*        [| y1; ...; x1; ...; xn; ...; yn |] ==> False                      *)
webertj@17809
    90
(*      amd finally remove duplicate literals.                               *)
webertj@17622
    91
(* ------------------------------------------------------------------------- *)
webertj@17618
    92
webertj@17809
    93
(* Thm.thm list -> Thm.thm *)
webertj@17622
    94
webertj@17809
    95
fun resolve_raw_clauses [] =
webertj@17809
    96
	raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
webertj@17809
    97
  | resolve_raw_clauses (c::cs) =
webertj@17809
    98
	let
webertj@17809
    99
		fun dual (Const ("Not", _) $ x) = x
webertj@17809
   100
		  | dual x                      = HOLogic.Not $ x
webertj@17809
   101
webertj@17809
   102
		fun is_neg (Const ("Not", _) $ _) = true
webertj@17809
   103
		  | is_neg _                      = false
webertj@17622
   104
webertj@19236
   105
		(* find out which two hyps are used in the resolution *)
webertj@19236
   106
		(* Term.term list -> Term.term list -> Term.term * Term.term *)
webertj@19236
   107
		fun res_hyps [] _ =
webertj@19236
   108
			raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
webertj@19236
   109
		  | res_hyps _ [] =
webertj@17809
   110
			raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
webertj@19236
   111
		  | res_hyps ((Const ("Trueprop", _) $ x) :: xs) ys =
webertj@19236
   112
			let val dx = dual x in
webertj@19236
   113
				(* hyps are implemented as ordered list in the kernel, and *)
webertj@19236
   114
				(* stripping 'Trueprop' should not change the order        *)
webertj@19236
   115
				if OrdList.member Term.fast_term_ord ys dx then
webertj@19236
   116
					(x, dx)
webertj@17809
   117
				else
webertj@19236
   118
					res_hyps xs ys
webertj@17809
   119
			end
webertj@19236
   120
		  | res_hyps (_ :: xs) ys =
webertj@19236
   121
			(* hyps are implemented as ordered list in the kernel, all hyps are of *)
webertj@19236
   122
			(* the form 'Trueprop $ lit' or 'implies $ (negated clause) $ False',  *)
webertj@19236
   123
			(* and the former are LESS than the latter according to the order --   *)
webertj@19236
   124
			(* therefore there is no need to continue the search via               *)
webertj@19236
   125
			(* 'res_hyps xs ys' here                                               *)
webertj@19236
   126
			raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
webertj@17622
   127
webertj@17809
   128
		(* Thm.thm -> Thm.thm -> Thm.thm *)
webertj@17809
   129
		fun resolution c1 c2 =
webertj@17622
   130
		let
webertj@17622
   131
			val _ = if !trace_sat then
webertj@19236
   132
					tracing ("Resolving clause: " ^ string_of_thm c1 ^ " (hyps: " ^ space_implode ", " (map (Sign.string_of_term (theory_of_thm c1)) (#hyps (rep_thm c1)))
webertj@19236
   133
						^ ")\nwith clause: " ^ string_of_thm c2 ^ " (hyps: " ^ space_implode ", " (map (Sign.string_of_term (theory_of_thm c2)) (#hyps (rep_thm c2))) ^ ")")
webertj@17622
   134
				else ()
webertj@17809
   135
webertj@19236
   136
			(* Term.term list -> Term.term list *)
webertj@19236
   137
			fun dest_filter_Trueprop []                                  = []
webertj@19236
   138
			  | dest_filter_Trueprop ((Const ("Trueprop", _) $ x) :: xs) = x :: dest_filter_Trueprop xs
webertj@19236
   139
			  | dest_filter_Trueprop (_ :: xs)                           =      dest_filter_Trueprop xs
webertj@19236
   140
webertj@19236
   141
			val hyps1    =                        (#hyps o rep_thm) c1
webertj@19236
   142
			(* minor optimization: dest/filter over the second list outside 'res_hyps' to do it only once *)
webertj@19236
   143
			val hyps2    = (dest_filter_Trueprop o #hyps o rep_thm) c2
webertj@19236
   144
webertj@19236
   145
			val (l1, l2) = res_hyps hyps1 hyps2  (* the two literals used for resolution, with 'Trueprop' stripped *)
webertj@19236
   146
			val is_neg   = is_neg l1
webertj@19236
   147
webertj@19236
   148
			val c1'      = Thm.implies_intr (cterm_of (theory_of_thm c1) (HOLogic.mk_Trueprop l1)) c1  (* Gamma1 |- l1 ==> False *)
webertj@19236
   149
			val c2'      = Thm.implies_intr (cterm_of (theory_of_thm c2) (HOLogic.mk_Trueprop l2)) c2  (* Gamma2 |- l2 ==> False *)
webertj@17618
   150
webertj@19236
   151
			val res_thm  =  (* |- (lit ==> False) ==> (~lit ==> False) ==> False *)
webertj@19236
   152
				let
webertj@19236
   153
					val P          = Var (("P", 0), HOLogic.boolT)
webertj@19236
   154
					val (lit, thy) = if is_neg then (l2, theory_of_thm c2') else (l1, theory_of_thm c1')
webertj@19236
   155
					val cterm      = cterm_of thy
webertj@19236
   156
				in
webertj@19236
   157
					Thm.instantiate ([], [(cterm P, cterm lit)]) 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@19236
   164
			val c_new    = Thm.implies_elim (Thm.implies_elim res_thm (if is_neg then c2' else c1')) (if is_neg then c1' else c2')  (* Gamma1, Gamma2 |- False *)
webertj@19236
   165
webertj@19236
   166
			val _ = if !trace_sat then
webertj@19236
   167
					tracing ("Resulting clause: " ^ string_of_thm c_new ^ " (hyps: " ^ space_implode ", " (map (Sign.string_of_term (theory_of_thm c_new)) (#hyps (rep_thm c_new))) ^ ")")
webertj@19236
   168
				else ()
webertj@17809
   169
			val _ = inc counter
webertj@17809
   170
		in
webertj@17809
   171
			c_new
webertj@17809
   172
		end
webertj@17809
   173
	in
webertj@17809
   174
		fold resolution cs c
webertj@17809
   175
	end;
webertj@17618
   176
webertj@17622
   177
(* ------------------------------------------------------------------------- *)
webertj@17809
   178
(* replay_proof: replays the resolution proof returned by the SAT solver;    *)
webertj@17809
   179
(*      cf. SatSolver.proof for details of the proof format.  Updates the    *)
webertj@17809
   180
(*      'clauses' array with derived clauses, and returns the derived clause *)
webertj@17809
   181
(*      at index 'empty_id' (which should just be "False" if proof           *)
webertj@17809
   182
(*      reconstruction was successful, with the used clauses as hyps).       *)
webertj@17622
   183
(* ------------------------------------------------------------------------- *)
webertj@17622
   184
webertj@17809
   185
(* Thm.thm option Array.array -> SatSolver.proof -> Thm.thm *)
webertj@17618
   186
webertj@17809
   187
fun replay_proof clauses (clause_table, empty_id) =
webertj@17622
   188
let
webertj@17809
   189
	(* int -> Thm.thm *)
webertj@17623
   190
	fun prove_clause id =
webertj@17623
   191
		case Array.sub (clauses, id) of
webertj@17809
   192
		  SOME thm =>
webertj@17809
   193
			thm
webertj@17809
   194
		| NONE     =>
webertj@17623
   195
			let
webertj@17809
   196
				val _   = if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else ()
webertj@17623
   197
				val ids = valOf (Inttab.lookup clause_table id)
webertj@17809
   198
				val thm = resolve_raw_clauses (map prove_clause ids)
webertj@17809
   199
				val _   = Array.update (clauses, id, SOME thm)
webertj@17809
   200
				val _   = if !trace_sat then tracing ("Replay chain successful; clause stored at #" ^ string_of_int id) else ()
webertj@17623
   201
			in
webertj@17809
   202
				thm
webertj@17623
   203
			end
webertj@17618
   204
webertj@17809
   205
	val _            = counter := 0
webertj@17809
   206
	val empty_clause = prove_clause empty_id
webertj@17809
   207
	val _            = if !trace_sat then tracing ("Proof reconstruction successful; " ^ string_of_int (!counter) ^ " resolution step(s) total.") else ()
webertj@17622
   208
in
webertj@17809
   209
	empty_clause
webertj@17622
   210
end;
webertj@17622
   211
webertj@17809
   212
(* PropLogic.prop_formula -> string *)
webertj@17809
   213
fun string_of_prop_formula PropLogic.True             = "True"
webertj@17809
   214
  | string_of_prop_formula PropLogic.False            = "False"
webertj@17809
   215
  | string_of_prop_formula (PropLogic.BoolVar i)      = "x" ^ string_of_int i
webertj@17809
   216
  | string_of_prop_formula (PropLogic.Not fm)         = "~" ^ string_of_prop_formula fm
webertj@17809
   217
  | string_of_prop_formula (PropLogic.Or (fm1, fm2))  = "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")"
webertj@17809
   218
  | string_of_prop_formula (PropLogic.And (fm1, fm2)) = "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")";
webertj@17622
   219
webertj@17622
   220
(* ------------------------------------------------------------------------- *)
webertj@17622
   221
(* rawsat_thm: run external SAT solver with the given clauses.  Reconstructs *)
webertj@17809
   222
(*      a proof from the resulting proof trace of the SAT solver.  Each      *)
webertj@17809
   223
(*      premise in 'prems' that is not a clause is ignored, and the theorem  *)
webertj@17809
   224
(*      returned is just "False" (with some clauses as hyps).                *)
webertj@17622
   225
(* ------------------------------------------------------------------------- *)
webertj@17618
   226
webertj@17809
   227
(* Thm.thm list -> Thm.thm *)
webertj@17809
   228
webertj@17809
   229
fun rawsat_thm prems =
webertj@17622
   230
let
webertj@17809
   231
	(* remove premises that equal "True" *)
webertj@17809
   232
	val non_triv_prems    = filter (fn thm =>
webertj@17809
   233
		(not_equal HOLogic.true_const o HOLogic.dest_Trueprop o prop_of) thm
webertj@17809
   234
			handle TERM ("dest_Trueprop", _) => true) prems
webertj@17809
   235
	(* remove non-clausal premises -- of course this shouldn't actually   *)
webertj@17809
   236
	(* remove anything as long as 'rawsat_thm' is only called after the   *)
webertj@17809
   237
	(* premises have been converted to clauses                            *)
webertj@17809
   238
	val clauses           = filter (fn thm =>
webertj@17809
   239
		((cnf.is_clause o HOLogic.dest_Trueprop o prop_of) thm handle TERM ("dest_Trueprop", _) => false)
webertj@17809
   240
		orelse (warning ("Ignoring non-clausal premise " ^ (string_of_cterm o cprop_of) thm); false)) non_triv_prems
webertj@17809
   241
	(* remove trivial clauses -- this is necessary because zChaff removes *)
webertj@17809
   242
	(* trivial clauses during preprocessing, and otherwise our clause     *)
webertj@17809
   243
	(* numbering would be off                                             *)
webertj@17809
   244
	val non_triv_clauses  = filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o prop_of) clauses
webertj@19534
   245
	val _                 = if !trace_sat then
webertj@19534
   246
			tracing ("Non-trivial clauses:\n" ^ space_implode "\n" (map (string_of_cterm o cprop_of) non_triv_clauses))
webertj@19534
   247
		else ()
webertj@17809
   248
	(* translate clauses from HOL terms to PropLogic.prop_formula *)
webertj@17809
   249
	val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o prop_of) non_triv_clauses Termtab.empty
webertj@17809
   250
	val _                 = if !trace_sat then
webertj@17809
   251
			tracing ("Invoking SAT solver on clauses:\n" ^ space_implode "\n" (map string_of_prop_formula fms))
webertj@17809
   252
		else ()
webertj@17809
   253
	val fm                = PropLogic.all fms
webertj@17842
   254
	(* unit -> Thm.thm *)
webertj@17842
   255
	fun make_quick_and_dirty_thm () = (
webertj@17842
   256
		if !trace_sat then
webertj@17842
   257
			tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
webertj@17842
   258
		else ();
webertj@17842
   259
		(* of course just returning "False" is unsound; what we should return *)
webertj@17842
   260
		(* instead is "False" with all 'non_triv_clauses' as hyps -- but this *)
webertj@17842
   261
		(* might be rather slow, and it makes no real difference as long as   *)
webertj@17842
   262
		(* 'rawsat_thm' is only called from 'rawsat_tac'                      *)
webertj@17842
   263
		SkipProof.make_thm (the_context ()) (HOLogic.Trueprop $ HOLogic.false_const)
webertj@17842
   264
	)
webertj@17618
   265
in
webertj@17622
   266
	case SatSolver.invoke_solver "zchaff_with_proofs" fm of
webertj@17842
   267
	  SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => (
webertj@17842
   268
		if !trace_sat then
webertj@17842
   269
			tracing ("Proof trace from SAT solver:\n" ^
webertj@17842
   270
				"clauses: [" ^ commas (map (fn (c, cs) =>
webertj@17842
   271
					"(" ^ string_of_int c ^ ", [" ^ commas (map string_of_int cs) ^ "])") (Inttab.dest clause_table)) ^ "]\n" ^
webertj@17842
   272
				"empty clause: " ^ string_of_int empty_id)
webertj@17842
   273
		else ();
webertj@17842
   274
		if !quick_and_dirty then
webertj@17842
   275
			make_quick_and_dirty_thm ()
webertj@17842
   276
		else
webertj@17842
   277
			let
webertj@17842
   278
				(* initialize the clause array with the given clauses, *)
webertj@17842
   279
				(* but converted to raw clause format                  *)
webertj@17842
   280
				val max_idx     = valOf (Inttab.max_key clause_table)
webertj@17842
   281
				val clause_arr  = Array.array (max_idx + 1, NONE)
webertj@19236
   282
				val raw_clauses = map cnf.clause2raw_thm non_triv_clauses
webertj@19236
   283
				(* Every raw clause has only its literals and itself as hyp, and hyps are *)
webertj@19236
   284
				(* accumulated during resolution steps.  Experimental results indicate    *)
webertj@19236
   285
				(* that it is NOT faster to weaken all raw_clauses to contain every       *)
webertj@19236
   286
				(* clause in the hyps beforehand.                                         *)
webertj@17842
   287
				val _           = fold (fn thm => fn idx => (Array.update (clause_arr, idx, SOME thm); idx+1)) raw_clauses 0
webertj@19236
   288
				(* replay the proof to derive the empty clause *)
webertj@19236
   289
				val FalseThm    = replay_proof clause_arr (clause_table, empty_id)
webertj@17842
   290
			in
webertj@19236
   291
				(* convert the hyps back to the original format *)
webertj@19236
   292
				cnf.rawhyps2clausehyps_thm FalseThm
webertj@17842
   293
			end)
webertj@17622
   294
	| SatSolver.UNSATISFIABLE NONE =>
webertj@17842
   295
		if !quick_and_dirty then (
webertj@17842
   296
			warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof";
webertj@17842
   297
			make_quick_and_dirty_thm ()
webertj@17842
   298
		) else
webertj@17842
   299
			raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, [])
webertj@17622
   300
	| SatSolver.SATISFIABLE assignment =>
webertj@17622
   301
		let
webertj@17622
   302
			val msg = "SAT solver found a countermodel:\n"
webertj@17809
   303
				^ (commas
webertj@17809
   304
					o map (fn (term, idx) =>
webertj@17809
   305
						Sign.string_of_term (the_context ()) term ^ ": "
webertj@17809
   306
							^ (case assignment idx of NONE => "arbitrary" | SOME true => "true" | SOME false => "false")))
webertj@17809
   307
					(Termtab.dest atom_table)
webertj@17622
   308
		in
webertj@17622
   309
			raise THM (msg, 0, [])
webertj@17622
   310
		end
webertj@17622
   311
	| SatSolver.UNKNOWN =>
webertj@17622
   312
		raise THM ("SAT solver failed to decide the formula", 0, [])
webertj@17622
   313
end;
webertj@17618
   314
webertj@17622
   315
(* ------------------------------------------------------------------------- *)
webertj@17622
   316
(* Tactics                                                                   *)
webertj@17622
   317
(* ------------------------------------------------------------------------- *)
webertj@17618
   318
webertj@17809
   319
(* ------------------------------------------------------------------------- *)
webertj@17809
   320
(* rawsat_tac: solves the i-th subgoal of the proof state; this subgoal      *)
webertj@17809
   321
(*      should be of the form                                                *)
webertj@17809
   322
(*        [| c1; c2; ...; ck |] ==> False                                    *)
webertj@17809
   323
(*      where each cj is a non-empty clause (i.e. a disjunction of literals) *)
webertj@17809
   324
(*      or "True"                                                            *)
webertj@17809
   325
(* ------------------------------------------------------------------------- *)
webertj@17809
   326
webertj@17809
   327
(* int -> Tactical.tactic *)
webertj@17809
   328
webertj@17809
   329
fun rawsat_tac i = METAHYPS (fn prems => rtac (rawsat_thm prems) 1) i;
webertj@17618
   330
webertj@17809
   331
(* ------------------------------------------------------------------------- *)
webertj@17809
   332
(* pre_cnf_tac: converts the i-th subgoal                                    *)
webertj@17809
   333
(*        [| A1 ; ... ; An |] ==> B                                          *)
webertj@17809
   334
(*      to                                                                   *)
webertj@17809
   335
(*        [| A1; ... ; An ; ~B |] ==> False                                  *)
webertj@17809
   336
(*      (handling meta-logical connectives in B properly before negating),   *)
webertj@17809
   337
(*      then replaces meta-logical connectives in the premises (i.e. "==>",  *)
webertj@17809
   338
(*      "!!" and "==") by connectives of the HOL object-logic (i.e. by       *)
webertj@19553
   339
(*      "-->", "!", and "="), then performs beta-eta-normalization on the    *)
webertj@19553
   340
(*      subgoal                                                              *)
webertj@17809
   341
(* ------------------------------------------------------------------------- *)
webertj@17809
   342
webertj@17809
   343
(* int -> Tactical.tactic *)
webertj@17809
   344
webertj@19534
   345
fun pre_cnf_tac i = rtac ccontr i THEN ObjectLogic.atomize_tac i THEN
webertj@19553
   346
                      PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal i) (Drule.beta_eta_conversion)));
webertj@17809
   347
webertj@17809
   348
(* ------------------------------------------------------------------------- *)
webertj@17809
   349
(* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *)
webertj@17809
   350
(*      if not, eliminates conjunctions (i.e. each clause of the CNF formula *)
webertj@17809
   351
(*      becomes a separate premise), then applies 'rawsat_tac' to solve the  *)
webertj@17809
   352
(*      subgoal                                                              *)
webertj@17809
   353
(* ------------------------------------------------------------------------- *)
webertj@17697
   354
webertj@17809
   355
(* int -> Tactical.tactic *)
webertj@17809
   356
webertj@17809
   357
fun cnfsat_tac i = (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac i);
webertj@17618
   358
webertj@17809
   359
(* ------------------------------------------------------------------------- *)
webertj@17809
   360
(* cnfxsat_tac: checks if the empty clause "False" occurs among the          *)
webertj@17809
   361
(*      premises; if not, eliminates conjunctions (i.e. each clause of the   *)
webertj@17809
   362
(*      CNF formula becomes a separate premise) and existential quantifiers, *)
webertj@17809
   363
(*      then applies 'rawsat_tac' to solve the subgoal                       *)
webertj@17809
   364
(* ------------------------------------------------------------------------- *)
webertj@17809
   365
webertj@17809
   366
(* int -> Tactical.tactic *)
webertj@17809
   367
webertj@17809
   368
fun cnfxsat_tac i = (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac i);
webertj@17618
   369
webertj@17809
   370
(* ------------------------------------------------------------------------- *)
webertj@17809
   371
(* sat_tac: tactic for calling an external SAT solver, taking as input an    *)
webertj@17809
   372
(*      arbitrary formula.  The input is translated to CNF, possibly causing *)
webertj@17809
   373
(*      an exponential blowup.                                               *)
webertj@17809
   374
(* ------------------------------------------------------------------------- *)
webertj@17809
   375
webertj@17809
   376
(* int -> Tactical.tactic *)
webertj@17809
   377
webertj@17809
   378
fun sat_tac i = pre_cnf_tac i THEN cnf.cnf_rewrite_tac i THEN cnfsat_tac i;
webertj@17809
   379
webertj@17809
   380
(* ------------------------------------------------------------------------- *)
webertj@17809
   381
(* satx_tac: tactic for calling an external SAT solver, taking as input an   *)
webertj@17809
   382
(*      arbitrary formula.  The input is translated to CNF, possibly         *)
webertj@17809
   383
(*      introducing new literals.                                            *)
webertj@17809
   384
(* ------------------------------------------------------------------------- *)
webertj@17809
   385
webertj@17809
   386
(* int -> Tactical.tactic *)
webertj@17809
   387
webertj@17809
   388
fun satx_tac i = pre_cnf_tac i THEN cnf.cnfx_rewrite_tac i THEN cnfxsat_tac i;
webertj@17618
   389
webertj@17622
   390
end;  (* of structure *)