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