src/HOL/Library/Old_SMT/old_z3_interface.ML
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 63950 cdc1e59aa513
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_z3_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 Z3 based on a relaxed version of SMT-LIB.
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_Z3_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 smtlib_z3C: Old_SMT_Utils.class
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40681
diff changeset
    10
  val setup: theory -> theory
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    11
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    12
  datatype sym = Sym of string * sym list
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    13
  type mk_builtins = {
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    14
    mk_builtin_typ: sym -> typ option,
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    15
    mk_builtin_num: theory -> int -> typ -> cterm option,
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    16
    mk_builtin_fun: theory -> sym -> cterm list -> cterm option }
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    17
  val add_mk_builtins: mk_builtins -> Context.generic -> Context.generic
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    18
  val mk_builtin_typ: Proof.context -> sym -> typ option
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    19
  val mk_builtin_num: Proof.context -> int -> typ -> cterm option
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    20
  val mk_builtin_fun: Proof.context -> sym -> cterm list -> cterm option
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    21
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    22
  val is_builtin_theory_term: Proof.context -> term -> bool
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    23
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    24
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    25
structure Old_Z3_Interface: OLD_Z3_INTERFACE =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    26
struct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    27
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    28
val smtlib_z3C = Old_SMTLIB_Interface.smtlibC @ ["z3"]
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    29
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    30
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    31
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40681
diff changeset
    32
(* interface *)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    33
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    34
local
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
    35
  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
    36
    let
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
    37
      val {prefixes, header, is_fol, serialize, ...} =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    38
        Old_SMTLIB_Interface.translate_config ctxt
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
    39
    in
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
    40
      {prefixes=prefixes, header=header, is_fol=is_fol, serialize=serialize,
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
    41
        has_datatypes=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
    42
    end
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    43
60352
d46de31a50c4 separate class for division operator, with particular syntax added in more specific classes
haftmann
parents: 59634
diff changeset
    44
  fun is_div_mod @{const divide (int)} = true
63950
cdc1e59aa513 syntactic type class for operation mod named after mod;
haftmann
parents: 60352
diff changeset
    45
    | is_div_mod @{const modulo (int)} = true
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
    46
    | is_div_mod _ = 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
    47
41302
0485186839a7 re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
boehmes
parents: 41280
diff changeset
    48
  val div_by_z3div = @{lemma
0485186839a7 re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
boehmes
parents: 41280
diff changeset
    49
    "ALL k l. k div l = (
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
    50
      if k = 0 | l = 0 then 0
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41127
diff changeset
    51
      else if (0 < k & 0 < l) | (k < 0 & 0 < l) then z3div k l
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41127
diff changeset
    52
      else z3div (-k) (-l))"
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
    53
    by (simp add: z3div_def)}
37151
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 36899
diff changeset
    54
41302
0485186839a7 re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
boehmes
parents: 41280
diff changeset
    55
  val mod_by_z3mod = @{lemma
0485186839a7 re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
boehmes
parents: 41280
diff changeset
    56
    "ALL k l. k mod l = (
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
    57
      if l = 0 then k
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41127
diff changeset
    58
      else if k = 0 then 0
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41127
diff changeset
    59
      else if (0 < k & 0 < l) | (k < 0 & 0 < l) then z3mod k l
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41127
diff changeset
    60
      else - z3mod (-k) (-l))"
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41127
diff changeset
    61
    by (simp add: z3mod_def)}
37151
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 36899
diff changeset
    62
41302
0485186839a7 re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
boehmes
parents: 41280
diff changeset
    63
  val have_int_div_mod =
0485186839a7 re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
boehmes
parents: 41280
diff changeset
    64
    exists (Term.exists_subterm is_div_mod o Thm.prop_of)
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
    65
41302
0485186839a7 re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
boehmes
parents: 41280
diff changeset
    66
  fun add_div_mod _ (thms, extra_thms) =
0485186839a7 re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
boehmes
parents: 41280
diff changeset
    67
    if have_int_div_mod thms orelse have_int_div_mod extra_thms then
0485186839a7 re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
boehmes
parents: 41280
diff changeset
    68
      (thms, div_by_z3div :: mod_by_z3mod :: extra_thms)
0485186839a7 re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
boehmes
parents: 41280
diff changeset
    69
    else (thms, extra_thms)
41072
9f9bc1bdacef be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents: 41059
diff changeset
    70
9f9bc1bdacef be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents: 41059
diff changeset
    71
  val setup_builtins =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    72
    Old_SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const times (int)}, "*") #>
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    73
    Old_SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const z3div}, "div") #>
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    74
    Old_SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const z3mod}, "mod")
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    75
in
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    76
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41124
diff changeset
    77
val setup = Context.theory_map (
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41124
diff changeset
    78
  setup_builtins #>
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    79
  Old_SMT_Normalize.add_extra_norm (smtlib_z3C, add_div_mod) #>
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    80
  Old_SMT_Translate.add_config (smtlib_z3C, translate_config))
41072
9f9bc1bdacef be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents: 41059
diff changeset
    81
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    82
end
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    83
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    84
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    85
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40681
diff changeset
    86
(* constructors *)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    87
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    88
datatype sym = Sym of string * sym list
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    89
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    90
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40681
diff changeset
    91
(** additional constructors **)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    92
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    93
type mk_builtins = {
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    94
  mk_builtin_typ: sym -> typ option,
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    95
  mk_builtin_num: theory -> int -> typ -> cterm option,
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    96
  mk_builtin_fun: theory -> sym -> cterm list -> cterm option }
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    97
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    98
fun chained _ [] = NONE
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    99
  | chained f (b :: bs) = (case f b of SOME y => SOME y | NONE => chained f bs)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   100
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   101
fun chained_mk_builtin_typ bs sym =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   102
  chained (fn {mk_builtin_typ=mk, ...} : mk_builtins => mk sym) bs
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   103
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   104
fun chained_mk_builtin_num ctxt bs i T =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 41761
diff changeset
   105
  let val thy = Proof_Context.theory_of ctxt
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   106
  in chained (fn {mk_builtin_num=mk, ...} : mk_builtins => mk thy i T) bs end
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   107
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   108
fun chained_mk_builtin_fun ctxt bs s cts =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 41761
diff changeset
   109
  let val thy = Proof_Context.theory_of ctxt
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   110
  in chained (fn {mk_builtin_fun=mk, ...} : mk_builtins => mk thy s cts) bs end
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   111
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40681
diff changeset
   112
fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2)
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40681
diff changeset
   113
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   114
structure Mk_Builtins = Generic_Data
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   115
(
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   116
  type T = (int * mk_builtins) list
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   117
  val empty = []
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   118
  val extend = I
41473
3717fc42ebe9 Ord_List.merge convenience;
wenzelm
parents: 41302
diff changeset
   119
  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
   120
)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   121
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   122
fun add_mk_builtins mk =
39687
4e9b6ada3a21 modernized structure Ord_List;
wenzelm
parents: 39298
diff changeset
   123
  Mk_Builtins.map (Ord_List.insert fst_int_ord (serial (), mk))
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   124
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   125
fun get_mk_builtins ctxt = map snd (Mk_Builtins.get (Context.Proof ctxt))
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   126
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   127
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40681
diff changeset
   128
(** basic and additional constructors **)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   129
49720
6279490e0438 newer versions of Z3 call it "Bool" not "bool"
blanchet
parents: 47965
diff changeset
   130
fun mk_builtin_typ _ (Sym ("Bool", _)) = SOME @{typ bool}
40516
516a367eb38c preliminary support for newer versions of Z3
boehmes
parents: 40274
diff changeset
   131
  | mk_builtin_typ _ (Sym ("Int", _)) = SOME @{typ int}
49720
6279490e0438 newer versions of Z3 call it "Bool" not "bool"
blanchet
parents: 47965
diff changeset
   132
  | mk_builtin_typ _ (Sym ("bool", _)) = SOME @{typ bool}  (*FIXME: legacy*)
6279490e0438 newer versions of Z3 call it "Bool" not "bool"
blanchet
parents: 47965
diff changeset
   133
  | mk_builtin_typ _ (Sym ("int", _)) = SOME @{typ int}  (*FIXME: legacy*)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   134
  | mk_builtin_typ ctxt sym = chained_mk_builtin_typ (get_mk_builtins ctxt) sym
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   135
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   136
fun mk_builtin_num _ i @{typ int} = SOME (Numeral.mk_cnumber @{ctyp int} i)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   137
  | mk_builtin_num ctxt i T =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   138
      chained_mk_builtin_num ctxt (get_mk_builtins ctxt) i T
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   139
59634
4b94cc030ba0 clarified context;
wenzelm
parents: 59621
diff changeset
   140
val mk_true = Thm.cterm_of @{context} (@{const Not} $ @{const False})
4b94cc030ba0 clarified context;
wenzelm
parents: 59621
diff changeset
   141
val mk_false = Thm.cterm_of @{context} @{const False}
4b94cc030ba0 clarified context;
wenzelm
parents: 59621
diff changeset
   142
val mk_not = Thm.apply (Thm.cterm_of @{context} @{const Not})
4b94cc030ba0 clarified context;
wenzelm
parents: 59621
diff changeset
   143
val mk_implies = Thm.mk_binop (Thm.cterm_of @{context} @{const HOL.implies})
4b94cc030ba0 clarified context;
wenzelm
parents: 59621
diff changeset
   144
val mk_iff = Thm.mk_binop (Thm.cterm_of @{context} @{const HOL.eq (bool)})
4b94cc030ba0 clarified context;
wenzelm
parents: 59621
diff changeset
   145
val conj = Thm.cterm_of @{context} @{const HOL.conj}
4b94cc030ba0 clarified context;
wenzelm
parents: 59621
diff changeset
   146
val disj = Thm.cterm_of @{context} @{const HOL.disj}
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   147
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   148
fun mk_nary _ cu [] = cu
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   149
  | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   150
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   151
val eq = Old_SMT_Utils.mk_const_pat @{theory} @{const_name HOL.eq} Old_SMT_Utils.destT1
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   152
fun mk_eq ct cu = Thm.mk_binop (Old_SMT_Utils.instT' ct eq) ct cu
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   153
41691
8f0531cf34f8 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41473
diff changeset
   154
val if_term =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   155
  Old_SMT_Utils.mk_const_pat @{theory} @{const_name If}
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   156
    (Old_SMT_Utils.destT1 o Old_SMT_Utils.destT2)
41691
8f0531cf34f8 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41473
diff changeset
   157
fun mk_if cc ct cu =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   158
  Thm.mk_binop (Thm.apply (Old_SMT_Utils.instT' ct if_term) cc) ct cu
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   159
41691
8f0531cf34f8 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41473
diff changeset
   160
val nil_term =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   161
  Old_SMT_Utils.mk_const_pat @{theory} @{const_name Nil} Old_SMT_Utils.destT1
41691
8f0531cf34f8 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41473
diff changeset
   162
val cons_term =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   163
  Old_SMT_Utils.mk_const_pat @{theory} @{const_name Cons} Old_SMT_Utils.destT1
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   164
fun mk_list cT cts =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   165
  fold_rev (Thm.mk_binop (Old_SMT_Utils.instT cT cons_term)) cts
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   166
    (Old_SMT_Utils.instT cT nil_term)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   167
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   168
val distinct = Old_SMT_Utils.mk_const_pat @{theory} @{const_name distinct}
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   169
  (Old_SMT_Utils.destT1 o Old_SMT_Utils.destT1)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   170
fun mk_distinct [] = mk_true
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   171
  | mk_distinct (cts as (ct :: _)) =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   172
      Thm.apply (Old_SMT_Utils.instT' ct distinct)
59586
ddf6deaadfe8 clarified signature;
wenzelm
parents: 58058
diff changeset
   173
        (mk_list (Thm.ctyp_of_cterm ct) cts)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   174
41691
8f0531cf34f8 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41473
diff changeset
   175
val access =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   176
  Old_SMT_Utils.mk_const_pat @{theory} @{const_name fun_app} Old_SMT_Utils.destT1
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   177
fun mk_access array = Thm.apply (Old_SMT_Utils.instT' array access) array
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   178
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   179
val update = Old_SMT_Utils.mk_const_pat @{theory} @{const_name fun_upd}
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   180
  (Thm.dest_ctyp o Old_SMT_Utils.destT1)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   181
fun mk_update array index value =
59586
ddf6deaadfe8 clarified signature;
wenzelm
parents: 58058
diff changeset
   182
  let val cTs = Thm.dest_ctyp (Thm.ctyp_of_cterm array)
41691
8f0531cf34f8 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41473
diff changeset
   183
  in
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   184
    Thm.apply (Thm.mk_binop (Old_SMT_Utils.instTs cTs update) array index) value
41691
8f0531cf34f8 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41473
diff changeset
   185
  end
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   186
59634
4b94cc030ba0 clarified context;
wenzelm
parents: 59621
diff changeset
   187
val mk_uminus = Thm.apply (Thm.cterm_of @{context} @{const uminus (int)})
4b94cc030ba0 clarified context;
wenzelm
parents: 59621
diff changeset
   188
val add = Thm.cterm_of @{context} @{const plus (int)}
47965
8ba6438557bc extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
boehmes
parents: 46497
diff changeset
   189
val int0 = Numeral.mk_cnumber @{ctyp int} 0
59634
4b94cc030ba0 clarified context;
wenzelm
parents: 59621
diff changeset
   190
val mk_sub = Thm.mk_binop (Thm.cterm_of @{context} @{const minus (int)})
4b94cc030ba0 clarified context;
wenzelm
parents: 59621
diff changeset
   191
val mk_mul = Thm.mk_binop (Thm.cterm_of @{context} @{const times (int)})
4b94cc030ba0 clarified context;
wenzelm
parents: 59621
diff changeset
   192
val mk_div = Thm.mk_binop (Thm.cterm_of @{context} @{const z3div})
4b94cc030ba0 clarified context;
wenzelm
parents: 59621
diff changeset
   193
val mk_mod = Thm.mk_binop (Thm.cterm_of @{context} @{const z3mod})
4b94cc030ba0 clarified context;
wenzelm
parents: 59621
diff changeset
   194
val mk_lt = Thm.mk_binop (Thm.cterm_of @{context} @{const less (int)})
4b94cc030ba0 clarified context;
wenzelm
parents: 59621
diff changeset
   195
val mk_le = Thm.mk_binop (Thm.cterm_of @{context} @{const less_eq (int)})
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   196
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   197
fun mk_builtin_fun ctxt sym cts =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   198
  (case (sym, cts) of
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   199
    (Sym ("true", _), []) => SOME mk_true
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   200
  | (Sym ("false", _), []) => SOME mk_false
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   201
  | (Sym ("not", _), [ct]) => SOME (mk_not ct)
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 40516
diff changeset
   202
  | (Sym ("and", _), _) => SOME (mk_nary conj mk_true cts)
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 40516
diff changeset
   203
  | (Sym ("or", _), _) => SOME (mk_nary disj mk_false cts)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   204
  | (Sym ("implies", _), [ct, cu]) => SOME (mk_implies ct cu)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   205
  | (Sym ("iff", _), [ct, cu]) => SOME (mk_iff ct cu)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   206
  | (Sym ("~", _), [ct, cu]) => SOME (mk_iff ct cu)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   207
  | (Sym ("xor", _), [ct, cu]) => SOME (mk_not (mk_iff ct cu))
41761
2dc75bae5226 more explicit errors to inform users about problems related to SMT solvers;
boehmes
parents: 41691
diff changeset
   208
  | (Sym ("if", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3)
2dc75bae5226 more explicit errors to inform users about problems related to SMT solvers;
boehmes
parents: 41691
diff changeset
   209
  | (Sym ("ite", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3) (* FIXME: remove *)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   210
  | (Sym ("=", _), [ct, cu]) => SOME (mk_eq ct cu)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   211
  | (Sym ("distinct", _), _) => SOME (mk_distinct cts)
46497
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 42361
diff changeset
   212
  | (Sym ("select", _), [ca, ck]) => SOME (Thm.apply (mk_access ca) ck)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   213
  | (Sym ("store", _), [ca, ck, cv]) => SOME (mk_update ca ck cv)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   214
  | _ =>
59586
ddf6deaadfe8 clarified signature;
wenzelm
parents: 58058
diff changeset
   215
    (case (sym, try (Thm.typ_of_cterm o hd) cts, cts) of
47965
8ba6438557bc extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
boehmes
parents: 46497
diff changeset
   216
      (Sym ("+", _), SOME @{typ int}, _) => SOME (mk_nary add int0 cts)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   217
    | (Sym ("-", _), SOME @{typ int}, [ct]) => SOME (mk_uminus ct)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   218
    | (Sym ("-", _), SOME @{typ int}, [ct, cu]) => SOME (mk_sub ct cu)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   219
    | (Sym ("*", _), SOME @{typ int}, [ct, cu]) => SOME (mk_mul ct cu)
37151
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 36899
diff changeset
   220
    | (Sym ("div", _), SOME @{typ int}, [ct, cu]) => SOME (mk_div ct cu)
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 36899
diff changeset
   221
    | (Sym ("mod", _), SOME @{typ int}, [ct, cu]) => SOME (mk_mod ct cu)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   222
    | (Sym ("<", _), SOME @{typ int}, [ct, cu]) => SOME (mk_lt ct cu)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   223
    | (Sym ("<=", _), SOME @{typ int}, [ct, cu]) => SOME (mk_le ct cu)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   224
    | (Sym (">", _), SOME @{typ int}, [ct, cu]) => SOME (mk_lt cu ct)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   225
    | (Sym (">=", _), SOME @{typ int}, [ct, cu]) => SOME (mk_le cu ct)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   226
    | _ => chained_mk_builtin_fun ctxt (get_mk_builtins ctxt) sym cts))
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   227
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   228
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   229
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40681
diff changeset
   230
(* abstraction *)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   231
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   232
fun is_builtin_theory_term ctxt t =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   233
  if Old_SMT_Builtin.is_builtin_num ctxt t then true
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40681
diff changeset
   234
  else
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40681
diff changeset
   235
    (case Term.strip_comb t of
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   236
      (Const c, ts) => Old_SMT_Builtin.is_builtin_fun ctxt c ts
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40681
diff changeset
   237
    | _ => false)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   238
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   239
end