src/HOL/Library/Old_SMT/old_smtlib_interface.ML
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 58058 1a0b18176548
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     1
(*  Title:      HOL/Library/Old_SMT/old_smtlib_interface.ML
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     3
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     4
Interface to SMT solvers based on the SMT-LIB format.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     5
*)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     6
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     7
signature OLD_SMTLIB_INTERFACE =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     8
sig
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     9
  val smtlibC: Old_SMT_Utils.class
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    10
  val add_logic: int * (term list -> string option) -> Context.generic ->
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    11
    Context.generic
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    12
  val translate_config: Proof.context -> Old_SMT_Translate.config
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    13
  val setup: theory -> theory
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    14
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    15
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    16
structure Old_SMTLIB_Interface: OLD_SMTLIB_INTERFACE =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    17
struct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    18
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    19
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    20
val smtlibC = ["smtlib"]
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    21
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    22
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    23
(* builtins *)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    24
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    25
local
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    26
  fun int_num _ i = SOME (string_of_int i)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    27
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    28
  fun is_linear [t] = Old_SMT_Utils.is_number t
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    29
    | is_linear [t, u] = Old_SMT_Utils.is_number t orelse Old_SMT_Utils.is_number u
41280
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41127
diff changeset
    30
    | is_linear _ = false
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41127
diff changeset
    31
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
    32
  fun times _ _ ts =
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
    33
    let val mk = Term.list_comb o pair @{const times (int)}
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
    34
    in if is_linear ts then SOME ("*", 2, ts, mk) else NONE end
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    35
in
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    36
41072
9f9bc1bdacef be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents: 41059
diff changeset
    37
val setup_builtins =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    38
  Old_SMT_Builtin.add_builtin_typ smtlibC (@{typ int}, K (SOME "Int"), int_num) #>
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    39
  fold (Old_SMT_Builtin.add_builtin_fun' smtlibC) [
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    40
    (@{const True}, "true"),
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    41
    (@{const False}, "false"),
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    42
    (@{const Not}, "not"),
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    43
    (@{const HOL.conj}, "and"),
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    44
    (@{const HOL.disj}, "or"),
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    45
    (@{const HOL.implies}, "implies"),
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    46
    (@{const HOL.eq (bool)}, "iff"),
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    47
    (@{const HOL.eq ('a)}, "="),
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    48
    (@{const If (bool)}, "if_then_else"),
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    49
    (@{const If ('a)}, "ite"),
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    50
    (@{const less (int)}, "<"),
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    51
    (@{const less_eq (int)}, "<="),
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    52
    (@{const uminus (int)}, "~"),
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    53
    (@{const plus (int)}, "+"),
41280
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41127
diff changeset
    54
    (@{const minus (int)}, "-") ] #>
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    55
  Old_SMT_Builtin.add_builtin_fun smtlibC
47155
ade3fc826af3 dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct
boehmes
parents: 41473
diff changeset
    56
    (Term.dest_Const @{const times (int)}, times)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    57
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    58
end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    59
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    60
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    61
(* serialization *)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    62
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    63
(** header **)
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    64
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    65
fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    66
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    67
structure Logics = Generic_Data
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    68
(
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    69
  type T = (int * (term list -> string option)) list
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    70
  val empty = []
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    71
  val extend = I
41473
3717fc42ebe9 Ord_List.merge convenience;
wenzelm
parents: 41426
diff changeset
    72
  fun merge data = Ord_List.merge fst_int_ord data
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    73
)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    74
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    75
fun add_logic pf = Logics.map (Ord_List.insert fst_int_ord pf)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    76
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    77
fun choose_logic ctxt ts =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    78
  let
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    79
    fun choose [] = "AUFLIA"
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    80
      | choose ((_, f) :: fs) = (case f ts of SOME s => s | NONE => choose fs)
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    81
  in [":logic " ^ choose (Logics.get (Context.Proof ctxt))] end
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    82
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    83
41072
9f9bc1bdacef be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents: 41059
diff changeset
    84
(** serialization **)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    85
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    86
val add = Buffer.add
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    87
fun sep f = add " " #> f
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    88
fun enclose l r f = sep (add l #> f #> add r)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    89
val par = enclose "(" ")"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    90
fun app n f = (fn [] => sep (add n) | xs => par (add n #> fold f xs))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    91
fun line f = f #> add "\n"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    92
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    93
fun var i = add "?v" #> add (string_of_int i)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    94
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    95
fun sterm l (Old_SMT_Translate.SVar i) = sep (var (l - i - 1))
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    96
  | sterm l (Old_SMT_Translate.SApp (n, ts)) = app n (sterm l) ts
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    97
  | sterm _ (Old_SMT_Translate.SLet _) =
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41281
diff changeset
    98
      raise Fail "SMT-LIB: unsupported let expression"
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    99
  | sterm l (Old_SMT_Translate.SQua (q, ss, ps, w, t)) =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   100
      let
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   101
        fun quant Old_SMT_Translate.SForall = add "forall"
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   102
          | quant Old_SMT_Translate.SExists = add "exists"
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   103
        val vs = map_index (apfst (Integer.add l)) ss
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   104
        fun var_decl (i, s) = par (var i #> sep (add s))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   105
        val sub = sterm (l + length ss)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   106
        fun pat kind ts = sep (add kind #> enclose "{" " }" (fold sub ts))
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   107
        fun pats (Old_SMT_Translate.SPat ts) = pat ":pat" ts
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   108
          | pats (Old_SMT_Translate.SNoPat ts) = pat ":nopat" ts
40664
e023788a91a1 added support for quantifier weight annotations
boehmes
parents: 40274
diff changeset
   109
        fun weight NONE = I
e023788a91a1 added support for quantifier weight annotations
boehmes
parents: 40274
diff changeset
   110
          | weight (SOME i) =
e023788a91a1 added support for quantifier weight annotations
boehmes
parents: 40274
diff changeset
   111
              sep (add ":weight { " #> add (string_of_int i) #> add " }")
e023788a91a1 added support for quantifier weight annotations
boehmes
parents: 40274
diff changeset
   112
      in
e023788a91a1 added support for quantifier weight annotations
boehmes
parents: 40274
diff changeset
   113
        par (quant q #> fold var_decl vs #> sub t #> fold pats ps #> weight w)
e023788a91a1 added support for quantifier weight annotations
boehmes
parents: 40274
diff changeset
   114
      end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   115
37155
e3f18cfc9829 sort signature in SMT-LIB output (improves sharing of SMT certificates: goals of the same logical structure are translated into equal SMT-LIB benchmarks)
boehmes
parents: 36936
diff changeset
   116
fun ssort sorts = sort fast_string_ord sorts
e3f18cfc9829 sort signature in SMT-LIB output (improves sharing of SMT certificates: goals of the same logical structure are translated into equal SMT-LIB benchmarks)
boehmes
parents: 36936
diff changeset
   117
fun fsort funcs = sort (prod_ord fast_string_ord (K EQUAL)) funcs
e3f18cfc9829 sort signature in SMT-LIB output (improves sharing of SMT certificates: goals of the same logical structure are translated into equal SMT-LIB benchmarks)
boehmes
parents: 36936
diff changeset
   118
39298
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 38864
diff changeset
   119
fun sdatatypes decls =
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 38864
diff changeset
   120
  let
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   121
    fun con (n, []) = sep (add n)
39298
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 38864
diff changeset
   122
      | con (n, sels) = par (add n #>
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   123
          fold (fn (n, s) => par (add n #> sep (add s))) sels)
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   124
    fun dtyp (n, decl) = add n #> fold con decl
39298
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 38864
diff changeset
   125
  in line (add ":datatypes " #> par (fold (par o dtyp) decls)) end
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 38864
diff changeset
   126
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 38864
diff changeset
   127
fun serialize comments {header, sorts, dtyps, funcs} ts =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   128
  Buffer.empty
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   129
  |> line (add "(benchmark Isabelle")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   130
  |> line (add ":status unknown")
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   131
  |> fold (line o add) header
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   132
  |> length sorts > 0 ?
37155
e3f18cfc9829 sort signature in SMT-LIB output (improves sharing of SMT certificates: goals of the same logical structure are translated into equal SMT-LIB benchmarks)
boehmes
parents: 36936
diff changeset
   133
       line (add ":extrasorts" #> par (fold (sep o add) (ssort sorts)))
39298
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 38864
diff changeset
   134
  |> fold sdatatypes dtyps
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   135
  |> length funcs > 0 ? (
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   136
       line (add ":extrafuns" #> add " (") #>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   137
       fold (fn (f, (ss, s)) =>
37155
e3f18cfc9829 sort signature in SMT-LIB output (improves sharing of SMT certificates: goals of the same logical structure are translated into equal SMT-LIB benchmarks)
boehmes
parents: 36936
diff changeset
   138
         line (sep (app f (sep o add) (ss @ [s])))) (fsort funcs) #>
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   139
       line (add ")"))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   140
  |> fold (fn t => line (add ":assumption" #> sterm 0 t)) ts
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   141
  |> line (add ":formula true)")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   142
  |> fold (fn str => line (add "; " #> add str)) comments
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   143
  |> Buffer.content
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   144
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   145
41072
9f9bc1bdacef be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents: 41059
diff changeset
   146
(* interface *)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   147
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
   148
fun translate_config ctxt = {
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
   149
  prefixes = {
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
   150
    sort_prefix = "S",
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
   151
    func_prefix = "f"},
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
   152
  header = choose_logic ctxt,
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
   153
  is_fol = true,
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
   154
  has_datatypes = false,
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
   155
  serialize = serialize}
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   156
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
   157
val setup = Context.theory_map (
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
   158
  setup_builtins #>
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   159
  Old_SMT_Translate.add_config (smtlibC, translate_config))
41072
9f9bc1bdacef be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents: 41059
diff changeset
   160
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   161
end