src/HOL/Tools/SMT/smt_real.ML
author wenzelm
Sun, 30 Jan 2011 13:02:18 +0100
changeset 41648 6d736d983d5c
parent 41439 a31c451183e6
child 41691 8f0531cf34f8
permissions -rw-r--r--
clarified example settings for Proof General;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     1
(*  Title:      HOL/Tools/SMT/smt_real.ML
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     3
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     4
SMT setup for reals.
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     5
*)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     6
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     7
signature SMT_REAL =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     8
sig
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     9
  val setup: theory -> theory
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    10
end
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    11
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    12
structure SMT_Real: SMT_REAL =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    13
struct
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    14
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    15
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    16
(* SMT-LIB logic *)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    17
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    18
fun smtlib_logic ts =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    19
  if exists (Term.exists_type (Term.exists_subtype (equal @{typ real}))) ts
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    20
  then SOME "AUFLIRA"
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    21
  else NONE
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    22
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    23
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40579
diff changeset
    24
(* SMT-LIB and Z3 built-ins *)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    25
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    26
local
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40579
diff changeset
    27
  fun real_num _ i = SOME (string_of_int i ^ ".0")
41280
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41072
diff changeset
    28
41439
a31c451183e6 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41302
diff changeset
    29
  fun is_linear [t] = SMT_Utils.is_number t
a31c451183e6 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41302
diff changeset
    30
    | is_linear [t, u] = SMT_Utils.is_number t orelse 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: 41072
diff changeset
    31
    | is_linear _ = false
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41072
diff changeset
    32
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
    33
  fun mk_times ts = Term.list_comb (@{const times (real)}, 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
    34
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
    35
  fun times _ T ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE
41280
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41072
diff changeset
    36
    | times _ _ _  = NONE
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    37
in
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    38
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40579
diff changeset
    39
val setup_builtins =
41439
a31c451183e6 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41302
diff changeset
    40
  SMT_Builtin.add_builtin_typ SMTLIB_Interface.smtlibC
a31c451183e6 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41302
diff changeset
    41
    (@{typ real}, K (SOME "Real"), real_num) #>
a31c451183e6 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41302
diff changeset
    42
  fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC) [
41280
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41072
diff changeset
    43
    (@{const less (real)}, "<"),
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41072
diff changeset
    44
    (@{const less_eq (real)}, "<="),
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40579
diff changeset
    45
    (@{const uminus (real)}, "~"),
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40579
diff changeset
    46
    (@{const plus (real)}, "+"),
41280
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41072
diff changeset
    47
    (@{const minus (real)}, "-") ] #>
41439
a31c451183e6 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41302
diff changeset
    48
  SMT_Builtin.add_builtin_fun SMTLIB_Interface.smtlibC
41280
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41072
diff changeset
    49
    (Term.dest_Const @{const times (real)}, times) #>
41439
a31c451183e6 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41302
diff changeset
    50
  SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C
a31c451183e6 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41302
diff changeset
    51
    (@{const times (real)}, "*") #>
a31c451183e6 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41302
diff changeset
    52
  SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C
a31c451183e6 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41302
diff changeset
    53
    (@{const divide (real)}, "/")
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    54
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    55
end
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    56
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    57
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    58
(* Z3 constructors *)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    59
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    60
local
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    61
  structure I = Z3_Interface
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    62
40516
516a367eb38c preliminary support for newer versions of Z3
boehmes
parents: 38715
diff changeset
    63
  fun z3_mk_builtin_typ (I.Sym ("Real", _)) = SOME @{typ real}
516a367eb38c preliminary support for newer versions of Z3
boehmes
parents: 38715
diff changeset
    64
    | z3_mk_builtin_typ (I.Sym ("real", _)) = SOME @{typ real} (*FIXME: delete*)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    65
    | z3_mk_builtin_typ _ = NONE
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    66
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    67
  fun z3_mk_builtin_num _ i T =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    68
    if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    69
    else NONE
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    70
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
    71
  val mk_uminus = Thm.capply (Thm.cterm_of @{theory} @{const uminus (real)})
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
    72
  val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (real)})
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
    73
  val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)})
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
    74
  val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)})
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
    75
  val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const divide (real)})
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
    76
  val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (real)})
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
    77
  val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (real)})
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    78
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    79
  fun z3_mk_builtin_fun (I.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    80
    | z3_mk_builtin_fun (I.Sym ("+", _)) [ct, cu] = SOME (mk_add ct cu)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    81
    | z3_mk_builtin_fun (I.Sym ("-", _)) [ct, cu] = SOME (mk_sub ct cu)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    82
    | z3_mk_builtin_fun (I.Sym ("*", _)) [ct, cu] = SOME (mk_mul ct cu)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    83
    | z3_mk_builtin_fun (I.Sym ("/", _)) [ct, cu] = SOME (mk_div ct cu)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    84
    | z3_mk_builtin_fun (I.Sym ("<", _)) [ct, cu] = SOME (mk_lt ct cu)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    85
    | z3_mk_builtin_fun (I.Sym ("<=", _)) [ct, cu] = SOME (mk_le ct cu)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    86
    | z3_mk_builtin_fun (I.Sym (">", _)) [ct, cu] = SOME (mk_lt cu ct)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    87
    | z3_mk_builtin_fun (I.Sym (">=", _)) [ct, cu] = SOME (mk_le cu ct)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    88
    | z3_mk_builtin_fun _ _ = NONE
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    89
in
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    90
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    91
val z3_mk_builtins = {
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    92
  mk_builtin_typ = z3_mk_builtin_typ,
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    93
  mk_builtin_num = z3_mk_builtin_num,
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    94
  mk_builtin_fun = (fn _ => fn sym => fn cts =>
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    95
    (case try (#T o Thm.rep_cterm o hd) cts of
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    96
      SOME @{typ real} => z3_mk_builtin_fun sym cts
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    97
    | _ => NONE)) }
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    98
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    99
end
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   100
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   101
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   102
(* Z3 proof reconstruction *)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   103
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   104
val real_rules = @{lemma
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   105
  "0 + (x::real) = x"
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   106
  "x + 0 = x"
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   107
  "0 * x = 0"
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   108
  "1 * x = x"
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   109
  "x + y = y + x"
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   110
  by auto}
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   111
38715
6513ea67d95d renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents: 36899
diff changeset
   112
val real_linarith_proc = Simplifier.simproc_global @{theory} "fast_real_arith" [
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   113
  "(m::real) < n", "(m::real) <= n", "(m::real) = n"] (K Lin_Arith.simproc)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   114
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   115
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   116
(* setup *)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   117
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   118
val setup =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   119
  Context.theory_map (
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40579
diff changeset
   120
    SMTLIB_Interface.add_logic (10, smtlib_logic) #>
41072
9f9bc1bdacef be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents: 41059
diff changeset
   121
    setup_builtins #>
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   122
    Z3_Interface.add_mk_builtins z3_mk_builtins #>
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   123
    fold Z3_Proof_Reconstruction.add_z3_rule real_rules #>
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   124
    Z3_Proof_Tools.add_simproc real_linarith_proc)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   125
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   126
end