author | webertj |
Mon, 10 Jul 2006 21:02:29 +0200 | |
changeset 20066 | b045b835cb3b |
parent 20039 | 4293f932fe83 |
child 20170 | 6ff853f82d73 |
permissions | -rw-r--r-- |
17618 | 1 |
(* Title: HOL/Tools/sat_funcs.ML |
2 |
ID: $Id$ |
|
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 | 6 |
|
7 |
||
8 |
Proof reconstruction from SAT solvers. |
|
9 |
||
10 |
Description: |
|
11 |
This file defines several tactics to invoke a proof-producing |
|
12 |
SAT solver on a propositional goal in clausal form. |
|
13 |
||
14 |
We use a sequent presentation of clauses to speed up resolution |
|
17695 | 15 |
proof reconstruction. |
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 | 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 | 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 | 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 | 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 | 52 |
zChaff version 2004.11.15 |
17695 | 53 |
- zChaff must have been compiled with proof generation enabled |
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 | 59 |
*) |
60 |
||
61 |
signature SAT = |
|
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 | 68 |
end |
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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 267 |
val _ = if !trace_sat then |
268 |
tracing ("Non-trivial clauses:\n" ^ space_implode "\n" (map (string_of_cterm o cprop_of) non_triv_clauses)) |
|
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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 411 |
|
20039
4293f932fe83
"solver" reference added to make the SAT solver configurable
webertj
parents:
19976
diff
changeset
|
412 |
end; (* of structure SATFunc *) |