| author | haftmann |
| Thu, 19 Jun 2025 17:15:40 +0200 | |
| changeset 82734 | 89347c0cc6a3 |
| parent 78177 | ea7a3cc64df5 |
| permissions | -rw-r--r-- |
| 58061 | 1 |
(* Title: HOL/Tools/SMT/z3_real.ML |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
2 |
Author: Sascha Boehme, TU Muenchen |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
3 |
|
|
78177
ea7a3cc64df5
early inclusion of cvc5 proof reconstruction; slightly reorganize smt/z3_reals;
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
4 |
Z3 setup for reals based on a relaxed version of SMT-LIB (outside of LIRA). |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
5 |
*) |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
6 |
|
| 58061 | 7 |
structure Z3_Real: sig end = |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
8 |
struct |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
9 |
|
|
78177
ea7a3cc64df5
early inclusion of cvc5 proof reconstruction; slightly reorganize smt/z3_reals;
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
10 |
val setup_builtins = |
|
ea7a3cc64df5
early inclusion of cvc5 proof reconstruction; slightly reorganize smt/z3_reals;
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
11 |
SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C |
|
ea7a3cc64df5
early inclusion of cvc5 proof reconstruction; slightly reorganize smt/z3_reals;
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
12 |
(\<^Const>\<open>times \<^Type>\<open>real\<close>\<close>, "*") #> |
|
ea7a3cc64df5
early inclusion of cvc5 proof reconstruction; slightly reorganize smt/z3_reals;
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
13 |
SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C |
|
ea7a3cc64df5
early inclusion of cvc5 proof reconstruction; slightly reorganize smt/z3_reals;
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
14 |
(\<^Const>\<open>divide \<^Type>\<open>real\<close>\<close>, "/") |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
15 |
|
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
16 |
|
|
78177
ea7a3cc64df5
early inclusion of cvc5 proof reconstruction; slightly reorganize smt/z3_reals;
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
17 |
val _ = Theory.setup (Context.theory_map |
|
ea7a3cc64df5
early inclusion of cvc5 proof reconstruction; slightly reorganize smt/z3_reals;
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
18 |
setup_builtins) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
19 |
|
| 57229 | 20 |
end; |