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