newlib/z3.ajla

   1 {*
   2  * Copyright (C) 2025 Mikulas Patocka
   3  *
   4  * This file is part of Ajla.
   5  *
   6  * Ajla is free software: you can redistribute it and/or modify it under the
   7  * terms of the GNU General Public License as published by the Free Software
   8  * Foundation, either version 3 of the License, or (at your option) any later
   9  * version.
  10  *
  11  * Ajla is distributed in the hope that it will be useful, but WITHOUT ANY
  12  * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR
  13  * A PARTICULAR PURPOSE. See the GNU General Public License for more details.
  14  *
  15  * You should have received a copy of the GNU General Public License along with
  16  * Ajla. If not, see <https://www.gnu.org/licenses/>.
  17  *}
  18
  19 unit z3;
  20
  21 type z3_world;
  22 type z3_context;
  23
  24 fn z3_mk_world : z3_world;
  25 fn z3_mk_context(w : z3_world) : (z3_world, z3_context);
  26
  27 fn z3_eval_smtlib2_string(w : z3_world, ctx : z3_context, str : bytes) : (z3_world, bytes);
  28 fn z3_eval_smtlib2_string_noret(w : z3_world, ctx : z3_context, str : bytes) : z3_world;
  29
  30 implementation
  31
  32 uses exception;
  33 uses ffi;
  34
  35 type z3_world := world;
  36
  37 record z3_context [
  38         destr : ffi_destructor;
  39         ptr_z3_context : int;
  40         z3_set_error : ffi_function;
  41         z3_get_error_code : ffi_function;
  42         z3_get_error_msg : ffi_function;
  43         z3_eval_smtlib2_string : ffi_function;
  44 ]
  45
  46 fn z3_mk_world := ffi_unsafe_get_world;
  47
  48 fn z3_mk_context(implicit w : z3_world) : (z3_world, z3_context)
  49 [
  50         var ctx := z3_context.[ ];
  51         var v e : int;
  52         ctx.destr := ffi_destructor_new();
  53         ctx.z3_set_error := ffi_create_function("libz3.so.4", "Z3_set_error", ffi_error.e_none, 2, ffi_type.t_void, [ ffi_type.t_pointer, ffi_type.t_uint ]);
  54         ctx.z3_get_error_code := ffi_create_function("libz3.so.4", "Z3_get_error_code", ffi_error.e_none, 1, ffi_type.t_uint, [ ffi_type.t_pointer ]);
  55         ctx.z3_get_error_msg := ffi_create_function("libz3.so.4", "Z3_get_error_msg", ffi_error.e_none, 2, ffi_type.t_pointer, [ ffi_type.t_pointer, ffi_type.t_uint ]);
  56         ctx.z3_eval_smtlib2_string := ffi_create_function("libz3.so.4", "Z3_eval_smtlib2_string", ffi_error.e_none, 3, ffi_type.t_pointer, [ ffi_type.t_pointer, ffi_type.t_pointer ]);
  57         var z3_mk_context := ffi_create_function("libz3.so.4", "Z3_mk_context", ffi_error.e_none, 1, ffi_type.t_pointer, [ ffi_type.t_pointer ]);
  58         var z3_del_context := ffi_create_function("libz3.so.4", "Z3_del_context", ffi_error.e_none, 1, ffi_type.t_void, [ ffi_type.t_pointer ]);
  59         var z3_set_error_handler := ffi_create_function("libz3.so.4", "Z3_set_error_handler", ffi_error.e_none, 1, ffi_type.t_void, [ ffi_type.t_pointer, ffi_type.t_pointer ]);
  60
  61         atomic_enter();
  62         ctx.ptr_z3_context, e := ffi_call_function(z3_mk_context, [ 0 ]);
  63         ffi_destructor_call(ctx.destr, z3_del_context, [ ctx.ptr_z3_context ]);
  64         atomic_exit();
  65
  66         v, e := ffi_call_function(z3_set_error_handler, [ ctx.ptr_z3_context, 0 ]);
  67         return ctx;
  68 ]
  69
  70 fn z3_eval_smtlib2_string(implicit w : z3_world, ctx : z3_context, str : bytes) : (z3_world, bytes)
  71 [
  72         //if not is_exception w then eval debug("Z3: " + str);
  73         var r e ec es : int;
  74         r, e := ffi_call_function(ctx.z3_set_error, [ ctx.ptr_z3_context, 0 ]);
  75         var mem_str := ffi_poke_zstring(ctx.destr, str);
  76         r, e := ffi_call_function(ctx.z3_eval_smtlib2_string, [ ctx.ptr_z3_context, mem_str ]);
  77         ffi_destructor_free(ctx.destr, mem_str);
  78         ec, e := ffi_call_function(ctx.z3_get_error_code, [ ctx.ptr_z3_context ]);
  79         if ec <> 0 then [
  80                 es, e := ffi_call_function(ctx.z3_get_error_msg, [ ctx.ptr_z3_context, ec ]);
  81                 var b := ffi_peek_zstring(es);
  82                 b := list_join(list_break_to_lines(b), "");
  83                 xeval ffi_destructor_destroy(ctx.destr);
  84                 abort exception_make_str(z3_world, ec_library, error_invalid_operation, ec, true, b);
  85         ]
  86         var b := ffi_peek_zstring(r);
  87         xeval ffi_destructor_destroy(ctx.destr);
  88         return b;
  89 ]
  90
  91 fn z3_eval_smtlib2_string_noret(implicit w : z3_world, ctx : z3_context, str : bytes) : z3_world
  92 [
  93         var b := z3_eval_smtlib2_string(ctx, str);
  94 ]