1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
(*
##
## ATS-extsolve-z3:
## Solving ATS-constraints with Z3
##
*)
(* ****** ****** *)
//
#ifdef
PATSOLVE_Z3_SOLVING
#then
#else
#include "./myheader.hats"
#endif // ifdef(PATSOLVE_Z3_SOLVING)
//
(* ****** ****** *)
//
#staload
UN = "prelude/SATS/unsafe.sats"
//
(* ****** ****** *)
extern
fun
the_Z3_context_vget
(
// argumentless
) : (
Z3_context -<prf> void | Z3_context
) = "ext#patsolve_the_Z3_context_vget"
(* ****** ****** *)
local
//
var
the_context : Z3_context
//
val config = Z3_mk_config ()
(*
val config_ = $UN.castvwtp1{ptr}(config)
*)
//
val ((*void*)) =
(
the_context :=
Z3_mk_context_rc (config)
// the_context
(*
the_context := $extfcall(Z3_context, "Z3_mk_context", config_)
*)
) (* end of [val] *)
//
val ((*void*)) = Z3_del_config (config)
//
in
//
implement
the_Z3_context_vget
((*void*)) = let
//
prval fpf = __assert() where
{
extern praxi __assert(): Z3_context -<prf> void
}
//
in
(fpf | $UN.ptr0_get<Z3_context>(addr@the_context))
end // end of [the_Z3_context_vget]
end // end of [local]
(* ****** ****** *)
(* end of [patsolve_z3_solving_ctx.dats] *)
|
