src/HOL/Tools/SMT/verit_strategies.ML
author wenzelm
Tue, 22 Jul 2025 12:02:53 +0200
changeset 82894 a8e47bd31965
parent 76183 8089593a364a
permissions -rw-r--r--
back to more basic defaults, independently on the accidental L&F: e.g. relevant for editor_style=false, and session_graph.pdf;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
76183
8089593a364a proper file headers;
wenzelm
parents: 75956
diff changeset
     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
c0da3fc313e3 Basic support for the SMT prover veriT.
fleury
parents:
diff changeset
     3
c0da3fc313e3 Basic support for the SMT prover veriT.
fleury
parents:
diff changeset
     4
VeriT proofs: parsing and abstract syntax tree.
c0da3fc313e3 Basic support for the SMT prover veriT.
fleury
parents:
diff changeset
     5
*)
c0da3fc313e3 Basic support for the SMT prover veriT.
fleury
parents:
diff changeset
     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
c0da3fc313e3 Basic support for the SMT prover veriT.
fleury
parents:
diff changeset
     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
c0da3fc313e3 Basic support for the SMT prover veriT.
fleury
parents:
diff changeset
    22
end;
c0da3fc313e3 Basic support for the SMT prover veriT.
fleury
parents:
diff changeset
    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
c0da3fc313e3 Basic support for the SMT prover veriT.
fleury
parents:
diff changeset
    25
struct
c0da3fc313e3 Basic support for the SMT prover veriT.
fleury
parents:
diff changeset
    26
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57762
diff changeset
    27
open SMTLIB_Proof
57704
c0da3fc313e3 Basic support for the SMT prover veriT.
fleury
parents:
diff changeset
    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
c0da3fc313e3 Basic support for the SMT prover veriT.
fleury
parents:
diff changeset
   126
end;