src/HOL/Tools/sat_funcs.ML
author haftmann
Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744 3daaf23b9ab4
parent 35625 9c818cab0dd0
child 38549 d0385f2764d8
permissions -rw-r--r--
tuned titles
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
    Author:     Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
29269
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents: 27115
diff changeset
     3
    Author:     Tjark Weber, TU Muenchen
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     4
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     5
Proof reconstruction from SAT solvers.
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
  Description:
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     8
    This file defines several tactics to invoke a proof-producing
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     9
    SAT solver on a propositional goal in clausal form.
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    10
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    11
    We use a sequent presentation of clauses to speed up resolution
17695
9c4887f7a9e3 comment fixed
webertj
parents: 17623
diff changeset
    12
    proof reconstruction.
9c4887f7a9e3 comment fixed
webertj
parents: 17623
diff changeset
    13
    We call such clauses "raw clauses", which are of the form
20440
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 20371
diff changeset
    14
          [x1, ..., xn, P] |- False
19236
150e8b0fb991 clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents: 17843
diff changeset
    15
    (note the use of |- instead of ==>, i.e. of Isabelle's (meta-)hyps here),
20440
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 20371
diff changeset
    16
    where each xi is a literal (see also comments in cnf_funcs.ML).
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    17
19236
150e8b0fb991 clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents: 17843
diff changeset
    18
    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
    19
20039
4293f932fe83 "solver" reference added to make the SAT solver configurable
webertj
parents: 19976
diff changeset
    20
      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
    21
      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
    22
      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
    23
      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
    24
      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
    25
      in Isabelle and thus solves the overall goal.
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    26
20440
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 20371
diff changeset
    27
  There are three SAT tactics available.  They differ in the CNF transformation
20039
4293f932fe83 "solver" reference added to make the SAT solver configurable
webertj
parents: 19976
diff changeset
    28
  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
    29
  proved before giving it to the SAT solver.  The naive transformation in the
20440
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 20371
diff changeset
    30
  worst case can lead to an exponential blow up in formula size.  Another
20039
4293f932fe83 "solver" reference added to make the SAT solver configurable
webertj
parents: 19976
diff changeset
    31
  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
    32
  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
    33
  the cost of possibly introducing new variables.  See cnf_funcs.ML for more
20440
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 20371
diff changeset
    34
  comments on the CNF transformation.  "rawsat_tac" should be used with
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 20371
diff changeset
    35
  caution: no CNF transformation is performed, and the tactic's behavior is
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 20371
diff changeset
    36
  undefined if the subgoal is not already given as [| C1; ...; Cn |] ==> False,
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 20371
diff changeset
    37
  where each Ci is a disjunction.
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    38
20039
4293f932fe83 "solver" reference added to make the SAT solver configurable
webertj
parents: 19976
diff changeset
    39
  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
    40
  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
    41
  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
    42
  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
    43
4293f932fe83 "solver" reference added to make the SAT solver configurable
webertj
parents: 19976
diff changeset
    44
  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
    45
  "!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
    46
  negation to be unsatisfiable) is proved via an oracle.
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    47
*)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    48
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    49
signature SAT =
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    50
sig
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32432
diff changeset
    51
	val trace_sat: bool Unsynchronized.ref    (* input: print trace messages *)
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32432
diff changeset
    52
	val solver: string Unsynchronized.ref  (* input: name of SAT solver to be used *)
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32432
diff changeset
    53
	val counter: int Unsynchronized.ref     (* output: number of resolution steps during last proof replay *)
32432
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32283
diff changeset
    54
	val rawsat_thm: Proof.context -> cterm list -> thm
32232
6c394343360f proper context for SAT tactics;
wenzelm
parents: 32231
diff changeset
    55
	val rawsat_tac: Proof.context -> int -> tactic
6c394343360f proper context for SAT tactics;
wenzelm
parents: 32231
diff changeset
    56
	val sat_tac: Proof.context -> int -> tactic
6c394343360f proper context for SAT tactics;
wenzelm
parents: 32231
diff changeset
    57
	val satx_tac: Proof.context -> int -> 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
32232
6c394343360f proper context for SAT tactics;
wenzelm
parents: 32231
diff changeset
    60
functor SATFunc(cnf : CNF) : SAT =
17622
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
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32432
diff changeset
    63
val trace_sat = Unsynchronized.ref false;
17622
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
    64
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32432
diff changeset
    65
val solver = Unsynchronized.ref "zchaff_with_proofs";
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32432
diff changeset
    66
  (*see HOL/Tools/sat_solver.ML for possible values*)
20039
4293f932fe83 "solver" reference added to make the SAT solver configurable
webertj
parents: 19976
diff changeset
    67
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32432
diff changeset
    68
val counter = Unsynchronized.ref 0;
17622
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
    69
32010
cb1a1c94b4cd more antiquotations;
wenzelm
parents: 29269
diff changeset
    70
val resolution_thm =
cb1a1c94b4cd more antiquotations;
wenzelm
parents: 29269
diff changeset
    71
  @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)}
17622
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
    72
32010
cb1a1c94b4cd more antiquotations;
wenzelm
parents: 29269
diff changeset
    73
val cP = cterm_of @{theory} (Var (("P", 0), HOLogic.boolT));
20278
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
    74
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
    75
(* ------------------------------------------------------------------------- *)
21768
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
    76
(* lit_ord: an order on integers that considers their absolute values only,  *)
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
    77
(*      thereby treating integers that represent the same atom (positively   *)
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
    78
(*      or negatively) as equal                                              *)
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
    79
(* ------------------------------------------------------------------------- *)
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
    80
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
    81
fun lit_ord (i, j) =
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
    82
	int_ord (abs i, abs j);
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
    83
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
    84
(* ------------------------------------------------------------------------- *)
20278
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
    85
(* CLAUSE: during proof reconstruction, three kinds of clauses are           *)
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
    86
(*      distinguished:                                                       *)
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
    87
(*      1. NO_CLAUSE: clause not proved (yet)                                *)
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
    88
(*      2. ORIG_CLAUSE: a clause as it occurs in the original problem        *)
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
    89
(*      3. RAW_CLAUSE: a raw clause, with additional precomputed information *)
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
    90
(*         (a mapping from int's to its literals) for faster proof           *)
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
    91
(*         reconstruction                                                    *)
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
    92
(* ------------------------------------------------------------------------- *)
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
    93
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
    94
datatype CLAUSE = NO_CLAUSE
33243
17014b1b9353 normalized basic type abbreviations;
wenzelm
parents: 33228
diff changeset
    95
                | ORIG_CLAUSE of thm
17014b1b9353 normalized basic type abbreviations;
wenzelm
parents: 33228
diff changeset
    96
                | RAW_CLAUSE of thm * (int * cterm) list;
20278
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
    97
17622
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
    98
(* ------------------------------------------------------------------------- *)
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
    99
(* 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
   100
(*      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
   101
(*      clauses                                                              *)
20440
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 20371
diff changeset
   102
(*        [P, x1, ..., a, ..., xn] |- False                                  *)
17622
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   103
(*      and                                                                  *)
20440
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 20371
diff changeset
   104
(*        [Q, y1, ..., a', ..., ym] |- False                                 *)
19976
aa35f8e27c73 comments fixed, minor optimization wrt. certifying terms
webertj
parents: 19553
diff changeset
   105
(*      (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
   106
(*      to                                                                   *)
20440
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 20371
diff changeset
   107
(*        [P, x1, ..., xn] |- a ==> False ,                                  *)
19976
aa35f8e27c73 comments fixed, minor optimization wrt. certifying terms
webertj
parents: 19553
diff changeset
   108
(*      the second clause to                                                 *)
20440
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 20371
diff changeset
   109
(*        [Q, y1, ..., ym] |- a' ==> False                                   *)
19976
aa35f8e27c73 comments fixed, minor optimization wrt. certifying terms
webertj
parents: 19553
diff changeset
   110
(*      and then perform resolution with                                     *)
aa35f8e27c73 comments fixed, minor optimization wrt. certifying terms
webertj
parents: 19553
diff changeset
   111
(*        [| ?P ==> False; ~?P ==> False |] ==> False                        *)
aa35f8e27c73 comments fixed, minor optimization wrt. certifying terms
webertj
parents: 19553
diff changeset
   112
(*      to produce                                                           *)
20440
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 20371
diff changeset
   113
(*        [P, Q, x1, ..., xn, y1, ..., ym] |- False                          *)
21768
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   114
(*      Each clause is accompanied with an association list mapping integers *)
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   115
(*      (positive for positive literals, negative for negative literals, and *)
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   116
(*      the same absolute value for dual literals) to the actual literals as *)
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   117
(*      cterms.                                                              *)
17622
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   118
(* ------------------------------------------------------------------------- *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   119
21768
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   120
(* (Thm.thm * (int * Thm.cterm) list) list -> Thm.thm * (int * Thm.cterm) list *)
17622
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   121
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   122
fun resolve_raw_clauses [] =
32091
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32010
diff changeset
   123
      raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   124
  | resolve_raw_clauses (c::cs) =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   125
	let
21768
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   126
		(* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *)
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   127
		fun merge xs      []      = xs
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   128
		  | merge []      ys      = ys
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   129
		  | merge (x::xs) (y::ys) =
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   130
			(case (lit_ord o pairself fst) (x, y) of
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   131
			  LESS    => x :: merge xs (y::ys)
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   132
			| EQUAL   => x :: merge xs ys
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   133
			| GREATER => y :: merge (x::xs) ys)
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   134
20278
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   135
		(* find out which two hyps are used in the resolution *)
21768
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   136
		(* (int * Thm.cterm) list * (int * Thm.cterm) list -> (int * Thm.cterm) list -> bool * Thm.cterm * Thm.cterm * (int * Thm.cterm) list *)
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   137
		fun find_res_hyps ([], _) _ =
32091
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32010
diff changeset
   138
          raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
21768
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   139
		  | find_res_hyps (_, []) _ =
32091
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32010
diff changeset
   140
          raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
21768
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   141
		  | find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc =
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   142
			(case (lit_ord o pairself fst) (h1, h2) of
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   143
			  LESS  => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc)
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   144
			| EQUAL => let
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   145
				val (i1, chyp1) = h1
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   146
				val (i2, chyp2) = h2
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   147
			in
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   148
				if i1 = ~ i2 then
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   149
					(i1 < 0, chyp1, chyp2, rev acc @ merge hyps1 hyps2)
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   150
				else (* i1 = i2 *)
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   151
					find_res_hyps (hyps1, hyps2) (h1 :: acc)
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   152
			end
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   153
			| GREATER => find_res_hyps (h1 :: hyps1, hyps2) (h2 :: acc))
19976
aa35f8e27c73 comments fixed, minor optimization wrt. certifying terms
webertj
parents: 19553
diff changeset
   154
21768
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   155
		(* Thm.thm * (int * Thm.cterm) list -> Thm.thm * (int * Thm.cterm) list -> Thm.thm * (int * Thm.cterm) list *)
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   156
		fun resolution (c1, hyps1) (c2, hyps2) =
17622
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   157
		let
32091
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32010
diff changeset
   158
			val _ =
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32010
diff changeset
   159
			  if ! trace_sat then
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32010
diff changeset
   160
					tracing ("Resolving clause: " ^ Display.string_of_thm_without_context c1 ^
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32010
diff changeset
   161
					  " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c1)) (#hyps (rep_thm c1))
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32010
diff changeset
   162
						^ ")\nwith clause: " ^ Display.string_of_thm_without_context c2 ^
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32010
diff changeset
   163
						" (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")")
17622
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   164
				else ()
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   165
20278
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   166
			(* the two literals used for resolution *)
21768
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   167
			val (hyp1_is_neg, hyp1, hyp2, new_hyps) = find_res_hyps (hyps1, hyps2) []
19236
150e8b0fb991 clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents: 17843
diff changeset
   168
20278
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   169
			val c1' = Thm.implies_intr hyp1 c1  (* Gamma1 |- hyp1 ==> False *)
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   170
			val c2' = Thm.implies_intr hyp2 c2  (* Gamma2 |- hyp2 ==> False *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   171
20278
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   172
			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
   173
				let
20278
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   174
					val cLit = snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1))  (* strip Trueprop *)
19236
150e8b0fb991 clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents: 17843
diff changeset
   175
				in
19976
aa35f8e27c73 comments fixed, minor optimization wrt. certifying terms
webertj
parents: 19553
diff changeset
   176
					Thm.instantiate ([], [(cP, cLit)]) resolution_thm
19236
150e8b0fb991 clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents: 17843
diff changeset
   177
				end
150e8b0fb991 clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents: 17843
diff changeset
   178
32091
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32010
diff changeset
   179
			val _ =
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32010
diff changeset
   180
			  if !trace_sat then
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32010
diff changeset
   181
					tracing ("Resolution theorem: " ^ Display.string_of_thm_without_context res_thm)
19236
150e8b0fb991 clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents: 17843
diff changeset
   182
				else ()
150e8b0fb991 clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents: 17843
diff changeset
   183
20440
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 20371
diff changeset
   184
			(* Gamma1, Gamma2 |- False *)
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 20371
diff changeset
   185
			val c_new = Thm.implies_elim
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 20371
diff changeset
   186
				(Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1'))
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 20371
diff changeset
   187
				(if hyp1_is_neg then c1' else c2')
20278
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   188
32091
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32010
diff changeset
   189
			val _ =
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32010
diff changeset
   190
			  if !trace_sat then
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32010
diff changeset
   191
					tracing ("Resulting clause: " ^ Display.string_of_thm_without_context c_new ^
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32010
diff changeset
   192
					  " (hyps: " ^ ML_Syntax.print_list
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32010
diff changeset
   193
					      (Syntax.string_of_term_global (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
19236
150e8b0fb991 clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents: 17843
diff changeset
   194
				else ()
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32432
diff changeset
   195
			val _ = Unsynchronized.inc counter
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   196
		in
21768
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   197
			(c_new, new_hyps)
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   198
		end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   199
	in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   200
		fold resolution cs c
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   201
	end;
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   202
17622
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   203
(* ------------------------------------------------------------------------- *)
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   204
(* replay_proof: replays the resolution proof returned by the SAT solver;    *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   205
(*      cf. SatSolver.proof for details of the proof format.  Updates the    *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   206
(*      'clauses' array with derived clauses, and returns the derived clause *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   207
(*      at index 'empty_id' (which should just be "False" if proof           *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   208
(*      reconstruction was successful, with the used clauses as hyps).       *)
20278
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   209
(*      'atom_table' must contain an injective mapping from all atoms that   *)
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   210
(*      occur (as part of a literal) in 'clauses' to positive integers.      *)
17622
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   211
(* ------------------------------------------------------------------------- *)
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   212
20278
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   213
(* int Termtab.table -> CLAUSE Array.array -> SatSolver.proof -> Thm.thm *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   214
20278
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   215
fun replay_proof atom_table clauses (clause_table, empty_id) =
17622
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   216
let
20278
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   217
	(* Thm.cterm -> int option *)
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   218
	fun index_of_literal chyp = (
21586
8da782143bde clauses sorted according to term order (significant speedup in some cases)
webertj
parents: 21474
diff changeset
   219
		case (HOLogic.dest_Trueprop o Thm.term_of) chyp of
20278
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   220
		  (Const ("Not", _) $ atom) =>
33035
15eab423e573 standardized basic operations on type option;
wenzelm
parents: 32970
diff changeset
   221
			SOME (~ (the (Termtab.lookup atom_table atom)))
20278
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   222
		| atom =>
33035
15eab423e573 standardized basic operations on type option;
wenzelm
parents: 32970
diff changeset
   223
			SOME (the (Termtab.lookup atom_table atom))
20278
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   224
	) handle TERM _ => NONE;  (* 'chyp' is not a literal *)
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   225
21768
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   226
	(* int -> Thm.thm * (int * Thm.cterm) list *)
17623
ae4af66b3072 replay_proof optimized: now performs backwards proof search
webertj
parents: 17622
diff changeset
   227
	fun prove_clause id =
ae4af66b3072 replay_proof optimized: now performs backwards proof search
webertj
parents: 17622
diff changeset
   228
		case Array.sub (clauses, id) of
20278
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   229
		  RAW_CLAUSE clause =>
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   230
			clause
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   231
		| ORIG_CLAUSE thm =>
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   232
			(* convert the original clause *)
17623
ae4af66b3072 replay_proof optimized: now performs backwards proof search
webertj
parents: 17622
diff changeset
   233
			let
21768
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   234
				val _      = if !trace_sat then tracing ("Using original clause #" ^ string_of_int id) else ()
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   235
				val raw    = cnf.clause2raw_thm thm
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   236
				val hyps   = sort (lit_ord o pairself fst) (map_filter (fn chyp =>
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   237
					Option.map (rpair chyp) (index_of_literal chyp)) (#hyps (Thm.crep_thm raw)))
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   238
				val clause = (raw, hyps)
69165d27b55b ordered lists instead of tables for resolving hyps; speedup
webertj
parents: 21756
diff changeset
   239
				val _      = Array.update (clauses, id, RAW_CLAUSE clause)
17623
ae4af66b3072 replay_proof optimized: now performs backwards proof search
webertj
parents: 17622
diff changeset
   240
			in
20278
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   241
				clause
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   242
			end
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   243
		| NO_CLAUSE =>
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   244
			(* prove the clause, using information from 'clause_table' *)
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   245
			let
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   246
				val _      = if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else ()
33035
15eab423e573 standardized basic operations on type option;
wenzelm
parents: 32970
diff changeset
   247
				val ids    = the (Inttab.lookup clause_table id)
20278
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   248
				val clause = resolve_raw_clauses (map prove_clause ids)
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   249
				val _      = Array.update (clauses, id, RAW_CLAUSE clause)
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   250
				val _      = if !trace_sat then tracing ("Replay chain successful; clause stored at #" ^ string_of_int id) else ()
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   251
			in
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   252
				clause
17623
ae4af66b3072 replay_proof optimized: now performs backwards proof search
webertj
parents: 17622
diff changeset
   253
			end
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   254
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   255
	val _            = counter := 0
20278
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   256
	val empty_clause = fst (prove_clause empty_id)
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   257
	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
   258
in
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   259
	empty_clause
17622
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   260
end;
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   261
20278
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   262
(* ------------------------------------------------------------------------- *)
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   263
(* string_of_prop_formula: return a human-readable string representation of  *)
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   264
(*      a 'prop_formula' (just for tracing)                                  *)
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   265
(* ------------------------------------------------------------------------- *)
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   266
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   267
(* PropLogic.prop_formula -> string *)
20278
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   268
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   269
fun string_of_prop_formula PropLogic.True             = "True"
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   270
  | string_of_prop_formula PropLogic.False            = "False"
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   271
  | 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
   272
  | 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
   273
  | 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
   274
  | 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
   275
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   276
(* ------------------------------------------------------------------------- *)
21267
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   277
(* take_prefix:                                                              *)
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   278
(*      take_prefix n [x_1, ..., x_k] = ([x_1, ..., x_n], [x_n+1, ..., x_k]) *)
17622
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   279
(* ------------------------------------------------------------------------- *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   280
21267
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   281
(* int -> 'a list -> 'a list * 'a list *)
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   282
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   283
fun take_prefix n xs =
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   284
let
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   285
	fun take 0 (rxs, xs)      = (rev rxs, xs)
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   286
	  | take _ (rxs, [])      = (rev rxs, [])
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   287
	  | take n (rxs, x :: xs) = take (n-1) (x :: rxs, xs)
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   288
in
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   289
	take n ([], xs)
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   290
end;
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   291
21267
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   292
(* ------------------------------------------------------------------------- *)
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   293
(* rawsat_thm: run external SAT solver with the given clauses.  Reconstructs *)
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   294
(*      a proof from the resulting proof trace of the SAT solver.  The       *)
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   295
(*      theorem returned is just "False" (with some of the given clauses as  *)
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   296
(*      hyps).                                                               *)
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   297
(* ------------------------------------------------------------------------- *)
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   298
32432
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32283
diff changeset
   299
fun rawsat_thm ctxt clauses =
17622
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   300
let
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   301
	(* remove premises that equal "True" *)
21267
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   302
	val clauses' = filter (fn clause =>
21586
8da782143bde clauses sorted according to term order (significant speedup in some cases)
webertj
parents: 21474
diff changeset
   303
		(not_equal HOLogic.true_const o HOLogic.dest_Trueprop o Thm.term_of) clause
21267
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   304
			handle TERM ("dest_Trueprop", _) => true) clauses
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   305
	(* remove non-clausal premises -- of course this shouldn't actually   *)
21267
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   306
	(* remove anything as long as 'rawsat_tac' is only called after the   *)
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   307
	(* premises have been converted to clauses                            *)
21267
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   308
	val clauses'' = filter (fn clause =>
21586
8da782143bde clauses sorted according to term order (significant speedup in some cases)
webertj
parents: 21474
diff changeset
   309
		((cnf.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause
21267
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   310
			handle TERM ("dest_Trueprop", _) => false)
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   311
		orelse (
32432
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32283
diff changeset
   312
			warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause));
21267
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   313
			false)) clauses'
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   314
	(* remove trivial clauses -- this is necessary because zChaff removes *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   315
	(* trivial clauses during preprocessing, and otherwise our clause     *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   316
	(* numbering would be off                                             *)
21586
8da782143bde clauses sorted according to term order (significant speedup in some cases)
webertj
parents: 21474
diff changeset
   317
	val nontrivial_clauses = filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o Thm.term_of) clauses''
8da782143bde clauses sorted according to term order (significant speedup in some cases)
webertj
parents: 21474
diff changeset
   318
	(* sort clauses according to the term order -- an optimization,       *)
8da782143bde clauses sorted according to term order (significant speedup in some cases)
webertj
parents: 21474
diff changeset
   319
	(* useful because forming the union of hypotheses, as done by         *)
23533
b86b764d5764 Conjunction.intr/elim_balanced;
wenzelm
parents: 22900
diff changeset
   320
	(* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *)
21586
8da782143bde clauses sorted according to term order (significant speedup in some cases)
webertj
parents: 21474
diff changeset
   321
	(* terms sorted in descending order, while only linear for terms      *)
8da782143bde clauses sorted according to term order (significant speedup in some cases)
webertj
parents: 21474
diff changeset
   322
	(* sorted in ascending order                                          *)
35408
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 33243
diff changeset
   323
	val sorted_clauses = sort (Term_Ord.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
21267
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   324
	val _ = if !trace_sat then
32432
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32283
diff changeset
   325
			tracing ("Sorted non-trivial clauses:\n" ^
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32283
diff changeset
   326
			  cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses))
19534
1724ec4032c5 beta_eta_conversion added to pre_cnf_tac
webertj
parents: 19236
diff changeset
   327
		else ()
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   328
	(* translate clauses from HOL terms to PropLogic.prop_formula *)
21586
8da782143bde clauses sorted according to term order (significant speedup in some cases)
webertj
parents: 21474
diff changeset
   329
	val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of) sorted_clauses Termtab.empty
21267
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   330
	val _ = if !trace_sat then
26931
aa226d8405a8 cat_lines;
wenzelm
parents: 26928
diff changeset
   331
			tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms))
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   332
		else ()
21586
8da782143bde clauses sorted according to term order (significant speedup in some cases)
webertj
parents: 21474
diff changeset
   333
	val fm = PropLogic.all fms
17842
e661a78472f0 no proof reconstruction when quick_and_dirty is set
webertj
parents: 17809
diff changeset
   334
	(* unit -> Thm.thm *)
21267
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   335
	fun make_quick_and_dirty_thm () =
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   336
	let
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   337
		val _ = if !trace_sat then
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   338
				tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   339
			else ()
32970
fbd2bb2489a8 operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
wenzelm
parents: 32740
diff changeset
   340
		val False_thm = Skip_Proof.make_thm @{theory} (HOLogic.Trueprop $ HOLogic.false_const)
21267
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   341
	in
21586
8da782143bde clauses sorted according to term order (significant speedup in some cases)
webertj
parents: 21474
diff changeset
   342
		(* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold    *)
8da782143bde clauses sorted according to term order (significant speedup in some cases)
webertj
parents: 21474
diff changeset
   343
		(* Thm.weaken sorted_clauses' would be quadratic, since we sorted   *)
8da782143bde clauses sorted according to term order (significant speedup in some cases)
webertj
parents: 21474
diff changeset
   344
		(* clauses in ascending order (which is linear for                  *)
23533
b86b764d5764 Conjunction.intr/elim_balanced;
wenzelm
parents: 22900
diff changeset
   345
		(* 'Conjunction.intr_balanced', used below)                         *)
21586
8da782143bde clauses sorted according to term order (significant speedup in some cases)
webertj
parents: 21474
diff changeset
   346
		fold Thm.weaken (rev sorted_clauses) False_thm
21267
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   347
	end
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   348
in
33228
cf8da4f3f92b more thread-safe access to global refs;
wenzelm
parents: 33035
diff changeset
   349
	case
cf8da4f3f92b more thread-safe access to global refs;
wenzelm
parents: 33035
diff changeset
   350
	  let val the_solver = ! solver
cf8da4f3f92b more thread-safe access to global refs;
wenzelm
parents: 33035
diff changeset
   351
	  in (tracing ("Invoking solver " ^ the_solver); SatSolver.invoke_solver the_solver fm) end
cf8da4f3f92b more thread-safe access to global refs;
wenzelm
parents: 33035
diff changeset
   352
	of
17842
e661a78472f0 no proof reconstruction when quick_and_dirty is set
webertj
parents: 17809
diff changeset
   353
	  SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => (
e661a78472f0 no proof reconstruction when quick_and_dirty is set
webertj
parents: 17809
diff changeset
   354
		if !trace_sat then
e661a78472f0 no proof reconstruction when quick_and_dirty is set
webertj
parents: 17809
diff changeset
   355
			tracing ("Proof trace from SAT solver:\n" ^
33228
cf8da4f3f92b more thread-safe access to global refs;
wenzelm
parents: 33035
diff changeset
   356
				"clauses: " ^ ML_Syntax.print_list
cf8da4f3f92b more thread-safe access to global refs;
wenzelm
parents: 33035
diff changeset
   357
				  (ML_Syntax.print_pair Int.toString (ML_Syntax.print_list Int.toString))
cf8da4f3f92b more thread-safe access to global refs;
wenzelm
parents: 33035
diff changeset
   358
				  (Inttab.dest clause_table) ^ "\n" ^
21586
8da782143bde clauses sorted according to term order (significant speedup in some cases)
webertj
parents: 21474
diff changeset
   359
				"empty clause: " ^ Int.toString empty_id)
17842
e661a78472f0 no proof reconstruction when quick_and_dirty is set
webertj
parents: 17809
diff changeset
   360
		else ();
e661a78472f0 no proof reconstruction when quick_and_dirty is set
webertj
parents: 17809
diff changeset
   361
		if !quick_and_dirty then
e661a78472f0 no proof reconstruction when quick_and_dirty is set
webertj
parents: 17809
diff changeset
   362
			make_quick_and_dirty_thm ()
e661a78472f0 no proof reconstruction when quick_and_dirty is set
webertj
parents: 17809
diff changeset
   363
		else
e661a78472f0 no proof reconstruction when quick_and_dirty is set
webertj
parents: 17809
diff changeset
   364
			let
21267
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   365
				(* optimization: convert the given clauses to "[c_1 && ... && c_n] |- c_i";  *)
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   366
				(*               this avoids accumulation of hypotheses during resolution    *)
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   367
				(* [c_1, ..., c_n] |- c_1 && ... && c_n *)
23533
b86b764d5764 Conjunction.intr/elim_balanced;
wenzelm
parents: 22900
diff changeset
   368
				val clauses_thm = Conjunction.intr_balanced (map Thm.assume sorted_clauses)
20440
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 20371
diff changeset
   369
				(* [c_1 && ... && c_n] |- c_1 && ... && c_n *)
21267
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   370
				val cnf_cterm = cprop_of clauses_thm
20440
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 20371
diff changeset
   371
				val cnf_thm   = Thm.assume cnf_cterm
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 20371
diff changeset
   372
				(* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *)
23533
b86b764d5764 Conjunction.intr/elim_balanced;
wenzelm
parents: 22900
diff changeset
   373
				val cnf_clauses = Conjunction.elim_balanced (length sorted_clauses) cnf_thm
20278
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   374
				(* initialize the clause array with the given clauses *)
33035
15eab423e573 standardized basic operations on type option;
wenzelm
parents: 32970
diff changeset
   375
				val max_idx    = the (Inttab.max_key clause_table)
20440
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 20371
diff changeset
   376
				val clause_arr = Array.array (max_idx + 1, NO_CLAUSE)
21267
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   377
				val _          = fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1)) cnf_clauses 0
19236
150e8b0fb991 clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents: 17843
diff changeset
   378
				(* replay the proof to derive the empty clause *)
20440
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 20371
diff changeset
   379
				(* [c_1 && ... && c_n] |- False *)
21268
7a6299a17386 timing/tracing code removed
webertj
parents: 21267
diff changeset
   380
				val raw_thm = replay_proof atom_table clause_arr (clause_table, empty_id)
17842
e661a78472f0 no proof reconstruction when quick_and_dirty is set
webertj
parents: 17809
diff changeset
   381
			in
20440
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 20371
diff changeset
   382
				(* [c_1, ..., c_n] |- False *)
21267
5294ecae6708 interpreters for fst and snd added
webertj
parents: 20486
diff changeset
   383
				Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm
17842
e661a78472f0 no proof reconstruction when quick_and_dirty is set
webertj
parents: 17809
diff changeset
   384
			end)
17622
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   385
	| SatSolver.UNSATISFIABLE NONE =>
17842
e661a78472f0 no proof reconstruction when quick_and_dirty is set
webertj
parents: 17809
diff changeset
   386
		if !quick_and_dirty then (
e661a78472f0 no proof reconstruction when quick_and_dirty is set
webertj
parents: 17809
diff changeset
   387
			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
   388
			make_quick_and_dirty_thm ()
e661a78472f0 no proof reconstruction when quick_and_dirty is set
webertj
parents: 17809
diff changeset
   389
		) else
e661a78472f0 no proof reconstruction when quick_and_dirty is set
webertj
parents: 17809
diff changeset
   390
			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
   391
	| SatSolver.SATISFIABLE assignment =>
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   392
		let
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   393
			val msg = "SAT solver found a countermodel:\n"
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   394
				^ (commas
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   395
					o map (fn (term, idx) =>
33228
cf8da4f3f92b more thread-safe access to global refs;
wenzelm
parents: 33035
diff changeset
   396
						Syntax.string_of_term_global @{theory} term ^ ": " ^
cf8da4f3f92b more thread-safe access to global refs;
wenzelm
parents: 33035
diff changeset
   397
						  (case assignment idx of NONE => "arbitrary"
cf8da4f3f92b more thread-safe access to global refs;
wenzelm
parents: 33035
diff changeset
   398
							| SOME true => "true" | SOME false => "false")))
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   399
					(Termtab.dest atom_table)
17622
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   400
		in
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   401
			raise THM (msg, 0, [])
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   402
		end
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   403
	| SatSolver.UNKNOWN =>
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   404
		raise THM ("SAT solver failed to decide the formula", 0, [])
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   405
end;
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   406
17622
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   407
(* ------------------------------------------------------------------------- *)
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   408
(* Tactics                                                                   *)
5d03a69481b6 code reformatted and restructured, many minor modifications
webertj
parents: 17618
diff changeset
   409
(* ------------------------------------------------------------------------- *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   410
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   411
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   412
(* 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
   413
(*      should be of the form                                                *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   414
(*        [| c1; c2; ...; ck |] ==> False                                    *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   415
(*      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
   416
(*      or "True"                                                            *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   417
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   418
32232
6c394343360f proper context for SAT tactics;
wenzelm
parents: 32231
diff changeset
   419
fun rawsat_tac ctxt i =
32432
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32283
diff changeset
   420
  Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32283
diff changeset
   421
    rtac (rawsat_thm ctxt' (map cprop_of prems)) 1) ctxt i;
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   422
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   423
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   424
(* pre_cnf_tac: converts the i-th subgoal                                    *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   425
(*        [| A1 ; ... ; An |] ==> B                                          *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   426
(*      to                                                                   *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   427
(*        [| A1; ... ; An ; ~B |] ==> False                                  *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   428
(*      (handling meta-logical connectives in B properly before negating),   *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   429
(*      then replaces meta-logical connectives in the premises (i.e. "==>",  *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   430
(*      "!!" 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
   431
(*      "-->", "!", 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
   432
(*      subgoal                                                              *)
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   433
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   434
23533
b86b764d5764 Conjunction.intr/elim_balanced;
wenzelm
parents: 22900
diff changeset
   435
val pre_cnf_tac =
b86b764d5764 Conjunction.intr/elim_balanced;
wenzelm
parents: 22900
diff changeset
   436
        rtac ccontr THEN'
35625
9c818cab0dd0 modernized structure Object_Logic;
wenzelm
parents: 35408
diff changeset
   437
        Object_Logic.atomize_prems_tac THEN'
23533
b86b764d5764 Conjunction.intr/elim_balanced;
wenzelm
parents: 22900
diff changeset
   438
        CONVERSION Drule.beta_eta_conversion;
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   439
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   440
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   441
(* 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
   442
(*      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
   443
(*      becomes a separate premise), then applies 'rawsat_tac' to solve the  *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   444
(*      subgoal                                                              *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   445
(* ------------------------------------------------------------------------- *)
17697
005218b2ee6b pre_sat_tac moved towards end of file
webertj
parents: 17695
diff changeset
   446
32232
6c394343360f proper context for SAT tactics;
wenzelm
parents: 32231
diff changeset
   447
fun cnfsat_tac ctxt i =
6c394343360f proper context for SAT tactics;
wenzelm
parents: 32231
diff changeset
   448
	(etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac ctxt i);
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   449
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   450
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   451
(* cnfxsat_tac: checks if the empty clause "False" occurs among the          *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   452
(*      premises; if not, eliminates conjunctions (i.e. each clause of the   *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   453
(*      CNF formula becomes a separate premise) and existential quantifiers, *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   454
(*      then applies 'rawsat_tac' to solve the subgoal                       *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   455
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   456
32232
6c394343360f proper context for SAT tactics;
wenzelm
parents: 32231
diff changeset
   457
fun cnfxsat_tac ctxt i =
20278
28be10991666 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents: 20170
diff changeset
   458
	(etac FalseE i) ORELSE
32232
6c394343360f proper context for SAT tactics;
wenzelm
parents: 32231
diff changeset
   459
		(REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac ctxt i);
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   460
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   461
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   462
(* 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
   463
(*      arbitrary formula.  The input is translated to CNF, possibly causing *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   464
(*      an exponential blowup.                                               *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   465
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   466
32232
6c394343360f proper context for SAT tactics;
wenzelm
parents: 32231
diff changeset
   467
fun sat_tac ctxt i =
6c394343360f proper context for SAT tactics;
wenzelm
parents: 32231
diff changeset
   468
	pre_cnf_tac i THEN cnf.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i;
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   469
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   470
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   471
(* 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
   472
(*      arbitrary formula.  The input is translated to CNF, possibly         *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   473
(*      introducing new literals.                                            *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   474
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17697
diff changeset
   475
32232
6c394343360f proper context for SAT tactics;
wenzelm
parents: 32231
diff changeset
   476
fun satx_tac ctxt i =
6c394343360f proper context for SAT tactics;
wenzelm
parents: 32231
diff changeset
   477
	pre_cnf_tac i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i;
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   478
23533
b86b764d5764 Conjunction.intr/elim_balanced;
wenzelm
parents: 22900
diff changeset
   479
end;