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