author | wenzelm |
Tue, 22 Jul 2025 12:02:53 +0200 | |
changeset 82894 | a8e47bd31965 |
parent 76183 | 8089593a364a |
permissions | -rw-r--r-- |
76183 | 1 |
(* Title: HOL/Tools/SMT/verit_strategies.ML |
75956
1e2a9d2251b0
remove duplicate parsing for alethe; fix skolemization;
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
75561
diff
changeset
|
2 |
Author: Mathias Fleury, ENS Rennes, MPI, JKU, Freiburg University |
57704 | 3 |
|
4 |
VeriT proofs: parsing and abstract syntax tree. |
|
5 |
*) |
|
6 |
||
75956
1e2a9d2251b0
remove duplicate parsing for alethe; fix skolemization;
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
75561
diff
changeset
|
7 |
signature VERIT_STRATEGIES = |
57704 | 8 |
sig |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
9 |
(*Strategy related*) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
10 |
val veriT_strategy : string Config.T |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
11 |
val veriT_current_strategy : Context.generic -> string list |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
12 |
val all_veriT_stgies: Context.generic -> string list; |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
13 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
14 |
val select_veriT_stgy: string -> Context.generic -> Context.generic; |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
15 |
val valid_veriT_stgy: string -> Context.generic -> bool; |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
16 |
val verit_add_stgy: string * string list -> Context.generic -> Context.generic |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
17 |
val verit_rm_stgy: string -> Context.generic -> Context.generic |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
18 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
19 |
(*Global tactic*) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
20 |
val verit_tac: Proof.context -> thm list -> int -> tactic |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
21 |
val verit_tac_stgy: string -> Proof.context -> thm list -> int -> tactic |
57704 | 22 |
end; |
23 |
||
75956
1e2a9d2251b0
remove duplicate parsing for alethe; fix skolemization;
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
75561
diff
changeset
|
24 |
structure Verit_Strategies: VERIT_STRATEGIES = |
57704 | 25 |
struct |
26 |
||
58061 | 27 |
open SMTLIB_Proof |
57704 | 28 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
29 |
val veriT_strategy_default_name = "default"; (*FUDGE*) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
30 |
val veriT_strategy_del_insts_name = "del_insts"; (*FUDGE*) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
31 |
val veriT_strategy_rm_insts_name = "ccfv_SIG"; (*FUDGE*) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
32 |
val veriT_strategy_ccfv_insts_name = "ccfv_threshold"; (*FUDGE*) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
33 |
val veriT_strategy_best_name = "best"; (*FUDGE*) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
34 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
35 |
val veriT_strategy_best = ["--index-sorts", "--index-fresh-sorts", "--triggers-new", |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
36 |
"--triggers-sel-rm-specific"]; |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
37 |
val veriT_strategy_del_insts = ["--index-sorts", "--index-fresh-sorts", "--ccfv-breadth", |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
38 |
"--inst-deletion", "--index-SAT-triggers", "--inst-deletion-loops", "--inst-deletion-track-vars", |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
39 |
"--inst-deletion", "--index-SAT-triggers"]; |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
40 |
val veriT_strategy_rm_insts = ["--index-SIG", "--triggers-new", "--triggers-sel-rm-specific"]; |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
41 |
val veriT_strategy_ccfv_insts = ["--index-sorts", "--index-fresh-sorts", "--triggers-new", |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
42 |
"--triggers-sel-rm-specific", "--triggers-restrict-combine", "--inst-deletion", |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
43 |
"--index-SAT-triggers", "--inst-deletion-loops", "--inst-deletion-track-vars", "--inst-deletion", |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
44 |
"--index-SAT-triggers", "--inst-sorts-threshold=100000", "--ematch-exp=10000000", |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
45 |
"--ccfv-index=100000", "--ccfv-index-full=1000"] |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
46 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
47 |
val veriT_strategy_default = []; |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
48 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
49 |
type verit_strategy = {default_strategy: string, strategies: (string * string list) list} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
50 |
fun mk_verit_strategy default_strategy strategies : verit_strategy = {default_strategy=default_strategy,strategies=strategies} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
51 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
52 |
val empty_data = mk_verit_strategy veriT_strategy_best_name |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
53 |
[(veriT_strategy_default_name, veriT_strategy_default), |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
54 |
(veriT_strategy_del_insts_name, veriT_strategy_del_insts), |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
55 |
(veriT_strategy_rm_insts_name, veriT_strategy_rm_insts), |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
56 |
(veriT_strategy_ccfv_insts_name, veriT_strategy_ccfv_insts), |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
57 |
(veriT_strategy_best_name, veriT_strategy_best)] |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
58 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
59 |
fun merge_data ({strategies=strategies1,...}:verit_strategy, |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
60 |
{default_strategy,strategies=strategies2}:verit_strategy) : verit_strategy = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
61 |
mk_verit_strategy default_strategy (AList.merge (op =) (op =) (strategies1, strategies2)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
62 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
63 |
structure Data = Generic_Data |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
64 |
( |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
65 |
type T = verit_strategy |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
66 |
val empty = empty_data |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
67 |
val merge = merge_data |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
68 |
) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
69 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
70 |
fun veriT_current_strategy ctxt = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
71 |
let |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
72 |
val {default_strategy,strategies} = (Data.get ctxt) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
73 |
in |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
74 |
AList.lookup (op=) strategies default_strategy |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
75 |
|> the |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
76 |
end |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
77 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
78 |
val veriT_strategy = Attrib.setup_config_string \<^binding>\<open>smt_verit_strategy\<close> (K veriT_strategy_best_name); |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
79 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
80 |
fun valid_veriT_stgy stgy context = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
81 |
let |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
82 |
val {strategies,...} = Data.get context |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
83 |
in |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
84 |
AList.defined (op =) strategies stgy |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
85 |
end |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
86 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
87 |
fun select_veriT_stgy stgy context = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
88 |
let |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
89 |
val {strategies,...} = Data.get context |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
90 |
val upd = Data.map (K (mk_verit_strategy stgy strategies)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
91 |
in |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
92 |
if not (AList.defined (op =) strategies stgy) then |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
93 |
error ("Trying to select unknown veriT strategy: " ^ quote stgy) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
94 |
else upd context |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
95 |
end |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
96 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
97 |
fun verit_add_stgy stgy context = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
98 |
let |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
99 |
val {default_strategy,strategies} = Data.get context |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
100 |
in |
72908
6a26a955308e
improve and activate compression for veriT proof reconstruction
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72513
diff
changeset
|
101 |
Data.map |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
102 |
(K (mk_verit_strategy default_strategy (AList.update (op =) stgy strategies))) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
103 |
context |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
104 |
end |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
105 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
106 |
fun verit_rm_stgy stgy context = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
107 |
let |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
108 |
val {default_strategy,strategies} = Data.get context |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
109 |
in |
72908
6a26a955308e
improve and activate compression for veriT proof reconstruction
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72513
diff
changeset
|
110 |
Data.map |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
111 |
(K (mk_verit_strategy default_strategy (AList.delete (op =) stgy strategies))) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
112 |
context |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
113 |
end |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
114 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
115 |
fun all_veriT_stgies context = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
116 |
let |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
117 |
val {strategies,...} = Data.get context |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
118 |
in |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
119 |
map fst strategies |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
120 |
end |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
121 |
|
74817
1fd8705503b4
generate problems with correct logic for veriT
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
74561
diff
changeset
|
122 |
val select_verit = SMT_Config.select_solver "verit" |
1fd8705503b4
generate problems with correct logic for veriT
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
74561
diff
changeset
|
123 |
fun verit_tac ctxt = SMT_Solver.smt_tac (Config.put SMT_Config.native_bv false ((Context.proof_map select_verit ctxt))) |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
124 |
fun verit_tac_stgy stgy ctxt = verit_tac (Context.proof_of (select_veriT_stgy stgy (Context.Proof ctxt))) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
125 |
|
57704 | 126 |
end; |