author | wenzelm |
Wed, 15 Jul 2009 23:48:21 +0200 | |
changeset 32010 | cb1a1c94b4cd |
parent 29269 | 5c25a2012975 |
child 32091 | 30e2ffbba718 |
permissions | -rw-r--r-- |
17618 | 1 |
(* Title: HOL/Tools/sat_funcs.ML |
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 | 4 |
|
5 |
Proof reconstruction from SAT solvers. |
|
6 |
||
7 |
Description: |
|
8 |
This file defines several tactics to invoke a proof-producing |
|
9 |
SAT solver on a propositional goal in clausal form. |
|
10 |
||
11 |
We use a sequent presentation of clauses to speed up resolution |
|
17695 | 12 |
proof reconstruction. |
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 | 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 | 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 | 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 | 47 |
*) |
48 |
||
49 |
signature SAT = |
|
50 |
sig |
|
21267 | 51 |
val trace_sat : bool ref (* input: print trace messages *) |
52 |
val solver : string ref (* input: name of SAT solver to be used *) |
|
53 |
val counter : int ref (* output: number of resolution steps during last proof replay *) |
|
54 |
val rawsat_thm : cterm list -> thm |
|
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset
|
55 |
val rawsat_tac : int -> Tactical.tactic |
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset
|
56 |
val sat_tac : int -> Tactical.tactic |
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset
|
57 |
val satx_tac : int -> Tactical.tactic |
17618 | 58 |
end |
59 |
||
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
60 |
functor SATFunc (structure cnf : CNF) : SAT = |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
61 |
struct |
17618 | 62 |
|
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
63 |
val trace_sat = ref false; |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
64 |
|
20170 | 65 |
val solver = ref "zchaff_with_proofs"; (* 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
|
66 |
|
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
67 |
val counter = ref 0; |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
68 |
|
32010 | 69 |
val resolution_thm = |
70 |
@{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)} |
|
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
71 |
|
32010 | 72 |
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
|
73 |
|
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 |
(* ------------------------------------------------------------------------- *) |
21768
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
75 |
(* 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
|
76 |
(* thereby treating integers that represent the same atom (positively *) |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
77 |
(* or negatively) as equal *) |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
78 |
(* ------------------------------------------------------------------------- *) |
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 |
fun lit_ord (i, j) = |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
81 |
int_ord (abs i, abs j); |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
82 |
|
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
83 |
(* ------------------------------------------------------------------------- *) |
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
|
84 |
(* 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
|
85 |
(* 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
|
86 |
(* 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
|
87 |
(* 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
|
88 |
(* 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
|
89 |
(* (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
|
90 |
(* 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
|
91 |
(* ------------------------------------------------------------------------- *) |
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 |
datatype CLAUSE = 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
|
94 |
| ORIG_CLAUSE of Thm.thm |
21768
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
95 |
| RAW_CLAUSE of Thm.thm * (int * Thm.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
|
96 |
|
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
97 |
(* ------------------------------------------------------------------------- *) |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
98 |
(* 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
|
99 |
(* 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
|
100 |
(* clauses *) |
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset
|
101 |
(* [P, x1, ..., a, ..., xn] |- False *) |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
102 |
(* and *) |
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset
|
103 |
(* [Q, y1, ..., a', ..., ym] |- False *) |
19976
aa35f8e27c73
comments fixed, minor optimization wrt. certifying terms
webertj
parents:
19553
diff
changeset
|
104 |
(* (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
|
105 |
(* to *) |
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset
|
106 |
(* [P, x1, ..., xn] |- a ==> False , *) |
19976
aa35f8e27c73
comments fixed, minor optimization wrt. certifying terms
webertj
parents:
19553
diff
changeset
|
107 |
(* 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
|
108 |
(* [Q, y1, ..., ym] |- a' ==> False *) |
19976
aa35f8e27c73
comments fixed, minor optimization wrt. certifying terms
webertj
parents:
19553
diff
changeset
|
109 |
(* and then perform resolution with *) |
aa35f8e27c73
comments fixed, minor optimization wrt. certifying terms
webertj
parents:
19553
diff
changeset
|
110 |
(* [| ?P ==> False; ~?P ==> False |] ==> False *) |
aa35f8e27c73
comments fixed, minor optimization wrt. certifying terms
webertj
parents:
19553
diff
changeset
|
111 |
(* to produce *) |
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset
|
112 |
(* [P, Q, x1, ..., xn, y1, ..., ym] |- False *) |
21768
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
113 |
(* 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
|
114 |
(* (positive for positive literals, negative for negative literals, and *) |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
115 |
(* 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
|
116 |
(* cterms. *) |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
117 |
(* ------------------------------------------------------------------------- *) |
17618 | 118 |
|
21768
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
119 |
(* (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
|
120 |
|
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
121 |
fun resolve_raw_clauses [] = |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
122 |
raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, []) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
123 |
| resolve_raw_clauses (c::cs) = |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
124 |
let |
21768
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
125 |
(* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *) |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
126 |
fun merge xs [] = xs |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
127 |
| merge [] ys = ys |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
128 |
| merge (x::xs) (y::ys) = |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
129 |
(case (lit_ord o pairself fst) (x, y) of |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
130 |
LESS => x :: merge xs (y::ys) |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
131 |
| EQUAL => x :: merge xs ys |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
132 |
| GREATER => y :: merge (x::xs) ys) |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
133 |
|
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
|
134 |
(* 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
|
135 |
(* (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
|
136 |
fun find_res_hyps ([], _) _ = |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
137 |
raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, []) |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
138 |
| find_res_hyps (_, []) _ = |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
139 |
raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, []) |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
140 |
| find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc = |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
141 |
(case (lit_ord o pairself fst) (h1, h2) of |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
142 |
LESS => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc) |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
143 |
| EQUAL => let |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
144 |
val (i1, chyp1) = h1 |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
145 |
val (i2, chyp2) = h2 |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
146 |
in |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
147 |
if i1 = ~ i2 then |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
148 |
(i1 < 0, chyp1, chyp2, rev acc @ merge hyps1 hyps2) |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
149 |
else (* i1 = i2 *) |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
150 |
find_res_hyps (hyps1, hyps2) (h1 :: acc) |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
151 |
end |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
152 |
| GREATER => find_res_hyps (h1 :: hyps1, hyps2) (h2 :: acc)) |
19976
aa35f8e27c73
comments fixed, minor optimization wrt. certifying terms
webertj
parents:
19553
diff
changeset
|
153 |
|
21768
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
154 |
(* 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
|
155 |
fun resolution (c1, hyps1) (c2, hyps2) = |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
156 |
let |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
157 |
val _ = if !trace_sat then |
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26931
diff
changeset
|
158 |
tracing ("Resolving clause: " ^ Display.string_of_thm c1 ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c1)) (#hyps (rep_thm c1)) |
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26931
diff
changeset
|
159 |
^ ")\nwith clause: " ^ Display.string_of_thm c2 ^ " (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
|
160 |
else () |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
161 |
|
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
|
162 |
(* the two literals used for resolution *) |
21768
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
163 |
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
|
164 |
|
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
|
165 |
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
|
166 |
val c2' = Thm.implies_intr hyp2 c2 (* Gamma2 |- hyp2 ==> False *) |
17618 | 167 |
|
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
|
168 |
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
|
169 |
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
|
170 |
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
|
171 |
in |
19976
aa35f8e27c73
comments fixed, minor optimization wrt. certifying terms
webertj
parents:
19553
diff
changeset
|
172 |
Thm.instantiate ([], [(cP, cLit)]) resolution_thm |
19236
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
173 |
end |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
174 |
|
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
175 |
val _ = if !trace_sat then |
26928 | 176 |
tracing ("Resolution theorem: " ^ Display.string_of_thm res_thm) |
19236
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
177 |
else () |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
178 |
|
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset
|
179 |
(* Gamma1, Gamma2 |- False *) |
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset
|
180 |
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
|
181 |
(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
|
182 |
(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
|
183 |
|
19236
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
184 |
val _ = if !trace_sat then |
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26931
diff
changeset
|
185 |
tracing ("Resulting clause: " ^ Display.string_of_thm c_new ^ " (hyps: " ^ ML_Syntax.print_list (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
|
186 |
else () |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
187 |
val _ = inc counter |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
188 |
in |
21768
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
189 |
(c_new, new_hyps) |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
190 |
end |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
191 |
in |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
192 |
fold resolution cs c |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
193 |
end; |
17618 | 194 |
|
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
195 |
(* ------------------------------------------------------------------------- *) |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
196 |
(* replay_proof: replays the resolution proof returned by the SAT solver; *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
197 |
(* cf. SatSolver.proof for details of the proof format. Updates the *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
198 |
(* 'clauses' array with derived clauses, and returns the derived clause *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
199 |
(* at index 'empty_id' (which should just be "False" if proof *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
200 |
(* 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
|
201 |
(* '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
|
202 |
(* 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
|
203 |
(* ------------------------------------------------------------------------- *) |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
204 |
|
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
|
205 |
(* int Termtab.table -> CLAUSE Array.array -> SatSolver.proof -> Thm.thm *) |
17618 | 206 |
|
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
|
207 |
fun replay_proof atom_table clauses (clause_table, empty_id) = |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
208 |
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
|
209 |
(* 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
|
210 |
fun index_of_literal chyp = ( |
21586
8da782143bde
clauses sorted according to term order (significant speedup in some cases)
webertj
parents:
21474
diff
changeset
|
211 |
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
|
212 |
(Const ("Not", _) $ atom) => |
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 |
SOME (~(valOf (Termtab.lookup atom_table atom))) |
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset
|
214 |
| atom => |
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 |
SOME (valOf (Termtab.lookup atom_table atom)) |
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset
|
216 |
) 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
|
217 |
|
21768
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
218 |
(* int -> Thm.thm * (int * Thm.cterm) list *) |
17623
ae4af66b3072
replay_proof optimized: now performs backwards proof search
webertj
parents:
17622
diff
changeset
|
219 |
fun prove_clause id = |
ae4af66b3072
replay_proof optimized: now performs backwards proof search
webertj
parents:
17622
diff
changeset
|
220 |
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
|
221 |
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
|
222 |
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
|
223 |
| 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
|
224 |
(* convert the original clause *) |
17623
ae4af66b3072
replay_proof optimized: now performs backwards proof search
webertj
parents:
17622
diff
changeset
|
225 |
let |
21768
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
226 |
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
|
227 |
val raw = cnf.clause2raw_thm thm |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
228 |
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
|
229 |
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
|
230 |
val clause = (raw, hyps) |
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset
|
231 |
val _ = Array.update (clauses, id, RAW_CLAUSE clause) |
17623
ae4af66b3072
replay_proof optimized: now performs backwards proof search
webertj
parents:
17622
diff
changeset
|
232 |
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
|
233 |
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
|
234 |
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
|
235 |
| 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
|
236 |
(* 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
|
237 |
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
|
238 |
val _ = if !trace_sat then tracing ("Proving clause #" ^ 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
|
239 |
val ids = valOf (Inttab.lookup clause_table id) |
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset
|
240 |
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
|
241 |
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
|
242 |
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
|
243 |
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
|
244 |
clause |
17623
ae4af66b3072
replay_proof optimized: now performs backwards proof search
webertj
parents:
17622
diff
changeset
|
245 |
end |
17618 | 246 |
|
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
247 |
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
|
248 |
val empty_clause = fst (prove_clause empty_id) |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
249 |
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
|
250 |
in |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
251 |
empty_clause |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
252 |
end; |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
253 |
|
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
|
254 |
(* ------------------------------------------------------------------------- *) |
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset
|
255 |
(* 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
|
256 |
(* 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
|
257 |
(* ------------------------------------------------------------------------- *) |
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset
|
258 |
|
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
259 |
(* 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
|
260 |
|
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
261 |
fun string_of_prop_formula PropLogic.True = "True" |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
262 |
| string_of_prop_formula PropLogic.False = "False" |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
263 |
| 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
|
264 |
| 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
|
265 |
| 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
|
266 |
| 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
|
267 |
|
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
268 |
(* ------------------------------------------------------------------------- *) |
21267 | 269 |
(* take_prefix: *) |
270 |
(* 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
|
271 |
(* ------------------------------------------------------------------------- *) |
17618 | 272 |
|
21267 | 273 |
(* int -> 'a list -> 'a list * 'a list *) |
274 |
||
275 |
fun take_prefix n xs = |
|
276 |
let |
|
277 |
fun take 0 (rxs, xs) = (rev rxs, xs) |
|
278 |
| take _ (rxs, []) = (rev rxs, []) |
|
279 |
| take n (rxs, x :: xs) = take (n-1) (x :: rxs, xs) |
|
280 |
in |
|
281 |
take n ([], xs) |
|
282 |
end; |
|
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
283 |
|
21267 | 284 |
(* ------------------------------------------------------------------------- *) |
285 |
(* rawsat_thm: run external SAT solver with the given clauses. Reconstructs *) |
|
286 |
(* a proof from the resulting proof trace of the SAT solver. The *) |
|
287 |
(* theorem returned is just "False" (with some of the given clauses as *) |
|
288 |
(* hyps). *) |
|
289 |
(* ------------------------------------------------------------------------- *) |
|
290 |
||
291 |
(* Thm.cterm list -> Thm.thm *) |
|
292 |
||
293 |
fun rawsat_thm clauses = |
|
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
294 |
let |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
295 |
(* remove premises that equal "True" *) |
21267 | 296 |
val clauses' = filter (fn clause => |
21586
8da782143bde
clauses sorted according to term order (significant speedup in some cases)
webertj
parents:
21474
diff
changeset
|
297 |
(not_equal HOLogic.true_const o HOLogic.dest_Trueprop o Thm.term_of) clause |
21267 | 298 |
handle TERM ("dest_Trueprop", _) => true) clauses |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
299 |
(* remove non-clausal premises -- of course this shouldn't actually *) |
21267 | 300 |
(* 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
|
301 |
(* premises have been converted to clauses *) |
21267 | 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 |
((cnf.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause |
21267 | 304 |
handle TERM ("dest_Trueprop", _) => false) |
305 |
orelse ( |
|
26928 | 306 |
warning ("Ignoring non-clausal premise " ^ Display.string_of_cterm clause); |
21267 | 307 |
false)) clauses' |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
308 |
(* remove trivial clauses -- this is necessary because zChaff removes *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
309 |
(* trivial clauses during preprocessing, and otherwise our clause *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
310 |
(* numbering would be off *) |
21586
8da782143bde
clauses sorted according to term order (significant speedup in some cases)
webertj
parents:
21474
diff
changeset
|
311 |
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
|
312 |
(* 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
|
313 |
(* useful because forming the union of hypotheses, as done by *) |
23533 | 314 |
(* 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
|
315 |
(* 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
|
316 |
(* sorted in ascending order *) |
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
27115
diff
changeset
|
317 |
val sorted_clauses = sort (TermOrd.fast_term_ord o pairself Thm.term_of) nontrivial_clauses |
21267 | 318 |
val _ = if !trace_sat then |
26931 | 319 |
tracing ("Sorted non-trivial clauses:\n" ^ cat_lines (map Display.string_of_cterm sorted_clauses)) |
19534 | 320 |
else () |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
321 |
(* 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
|
322 |
val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of) sorted_clauses Termtab.empty |
21267 | 323 |
val _ = if !trace_sat then |
26931 | 324 |
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
|
325 |
else () |
21586
8da782143bde
clauses sorted according to term order (significant speedup in some cases)
webertj
parents:
21474
diff
changeset
|
326 |
val fm = PropLogic.all fms |
17842
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
327 |
(* unit -> Thm.thm *) |
21267 | 328 |
fun make_quick_and_dirty_thm () = |
329 |
let |
|
330 |
val _ = if !trace_sat then |
|
331 |
tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead." |
|
332 |
else () |
|
333 |
val False_thm = SkipProof.make_thm (the_context ()) (HOLogic.Trueprop $ HOLogic.false_const) |
|
334 |
in |
|
21586
8da782143bde
clauses sorted according to term order (significant speedup in some cases)
webertj
parents:
21474
diff
changeset
|
335 |
(* '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
|
336 |
(* 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
|
337 |
(* clauses in ascending order (which is linear for *) |
23533 | 338 |
(* 'Conjunction.intr_balanced', used below) *) |
21586
8da782143bde
clauses sorted according to term order (significant speedup in some cases)
webertj
parents:
21474
diff
changeset
|
339 |
fold Thm.weaken (rev sorted_clauses) False_thm |
21267 | 340 |
end |
17618 | 341 |
in |
21268 | 342 |
case (tracing ("Invoking solver " ^ (!solver)); SatSolver.invoke_solver (!solver) fm) of |
17842
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
343 |
SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => ( |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
344 |
if !trace_sat then |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
345 |
tracing ("Proof trace from SAT solver:\n" ^ |
21756 | 346 |
"clauses: " ^ ML_Syntax.print_list (ML_Syntax.print_pair Int.toString (ML_Syntax.print_list Int.toString)) (Inttab.dest clause_table) ^ "\n" ^ |
21586
8da782143bde
clauses sorted according to term order (significant speedup in some cases)
webertj
parents:
21474
diff
changeset
|
347 |
"empty clause: " ^ Int.toString empty_id) |
17842
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
348 |
else (); |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
349 |
if !quick_and_dirty then |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
350 |
make_quick_and_dirty_thm () |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
351 |
else |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
352 |
let |
21267 | 353 |
(* optimization: convert the given clauses to "[c_1 && ... && c_n] |- c_i"; *) |
354 |
(* this avoids accumulation of hypotheses during resolution *) |
|
355 |
(* [c_1, ..., c_n] |- c_1 && ... && c_n *) |
|
23533 | 356 |
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
|
357 |
(* [c_1 && ... && c_n] |- c_1 && ... && c_n *) |
21267 | 358 |
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
|
359 |
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
|
360 |
(* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *) |
23533 | 361 |
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
|
362 |
(* initialize the clause array with the given clauses *) |
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset
|
363 |
val max_idx = valOf (Inttab.max_key clause_table) |
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset
|
364 |
val clause_arr = Array.array (max_idx + 1, NO_CLAUSE) |
21267 | 365 |
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
|
366 |
(* 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
|
367 |
(* [c_1 && ... && c_n] |- False *) |
21268 | 368 |
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
|
369 |
in |
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset
|
370 |
(* [c_1, ..., c_n] |- False *) |
21267 | 371 |
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
|
372 |
end) |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
373 |
| SatSolver.UNSATISFIABLE NONE => |
17842
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
374 |
if !quick_and_dirty then ( |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
375 |
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
|
376 |
make_quick_and_dirty_thm () |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
377 |
) else |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
378 |
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
|
379 |
| SatSolver.SATISFIABLE assignment => |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
380 |
let |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
381 |
val msg = "SAT solver found a countermodel:\n" |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
382 |
^ (commas |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
383 |
o map (fn (term, idx) => |
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26931
diff
changeset
|
384 |
Syntax.string_of_term_global (the_context ()) term ^ ": " |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
385 |
^ (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
|
386 |
(Termtab.dest atom_table) |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
387 |
in |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
388 |
raise THM (msg, 0, []) |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
389 |
end |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
390 |
| SatSolver.UNKNOWN => |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
391 |
raise THM ("SAT solver failed to decide the formula", 0, []) |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
392 |
end; |
17618 | 393 |
|
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
394 |
(* ------------------------------------------------------------------------- *) |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
395 |
(* Tactics *) |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
396 |
(* ------------------------------------------------------------------------- *) |
17618 | 397 |
|
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
398 |
(* ------------------------------------------------------------------------- *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
399 |
(* 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
|
400 |
(* should be of the form *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
401 |
(* [| c1; c2; ...; ck |] ==> False *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
402 |
(* 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
|
403 |
(* or "True" *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
404 |
(* ------------------------------------------------------------------------- *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
405 |
|
21267 | 406 |
fun rawsat_tac i = METAHYPS (fn prems => rtac (rawsat_thm (map cprop_of prems)) 1) i; |
17618 | 407 |
|
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
408 |
(* ------------------------------------------------------------------------- *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
409 |
(* pre_cnf_tac: converts the i-th subgoal *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
410 |
(* [| A1 ; ... ; An |] ==> B *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
411 |
(* to *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
412 |
(* [| A1; ... ; An ; ~B |] ==> False *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
413 |
(* (handling meta-logical connectives in B properly before negating), *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
414 |
(* then replaces meta-logical connectives in the premises (i.e. "==>", *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
415 |
(* "!!" 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
|
416 |
(* "-->", "!", 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
|
417 |
(* subgoal *) |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
418 |
(* ------------------------------------------------------------------------- *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
419 |
|
23533 | 420 |
val pre_cnf_tac = |
421 |
rtac ccontr THEN' |
|
23590
ad95084a5c63
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23533
diff
changeset
|
422 |
ObjectLogic.atomize_prems_tac THEN' |
23533 | 423 |
CONVERSION Drule.beta_eta_conversion; |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
424 |
|
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
425 |
(* ------------------------------------------------------------------------- *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
426 |
(* 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
|
427 |
(* 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
|
428 |
(* becomes a separate premise), then applies 'rawsat_tac' to solve the *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
429 |
(* subgoal *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
430 |
(* ------------------------------------------------------------------------- *) |
17697 | 431 |
|
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
|
432 |
fun cnfsat_tac i = |
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset
|
433 |
(etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac i); |
17618 | 434 |
|
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
435 |
(* ------------------------------------------------------------------------- *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
436 |
(* cnfxsat_tac: checks if the empty clause "False" occurs among the *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
437 |
(* premises; if not, eliminates conjunctions (i.e. each clause of the *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
438 |
(* CNF formula becomes a separate premise) and existential quantifiers, *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
439 |
(* then applies 'rawsat_tac' to solve the subgoal *) |
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 |
|
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
|
442 |
fun cnfxsat_tac i = |
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset
|
443 |
(etac FalseE i) ORELSE |
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset
|
444 |
(REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac i); |
17618 | 445 |
|
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
446 |
(* ------------------------------------------------------------------------- *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
447 |
(* 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
|
448 |
(* arbitrary formula. The input is translated to CNF, possibly causing *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
449 |
(* an exponential blowup. *) |
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 |
|
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
|
452 |
fun sat_tac i = |
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset
|
453 |
pre_cnf_tac i THEN cnf.cnf_rewrite_tac i THEN cnfsat_tac i; |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
454 |
|
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 |
(* 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
|
457 |
(* arbitrary formula. The input is translated to CNF, possibly *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
458 |
(* introducing new literals. *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
459 |
(* ------------------------------------------------------------------------- *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
460 |
|
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
|
461 |
fun satx_tac i = |
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset
|
462 |
pre_cnf_tac i THEN cnf.cnfx_rewrite_tac i THEN cnfxsat_tac i; |
17618 | 463 |
|
23533 | 464 |
end; |