mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

js

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-05-09 08:49:02 -07:00
parent 4549ec7331
commit fbf5e322dc
2 changed files with 23 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

43
src/api/dotnet/UserPropagator.cs
View file

@ -73,21 +73,30 @@ namespace Microsoft.Z3
CreatedEh created_eh; CreatedEh created_eh;
DecideEh decide_eh; DecideEh decide_eh;
void Callback(Action fn, Z3_solver_callback cb) {
this.callback = cb;
try {
fn();
}
catch {
// TBD: add debug log or exception handler
}
finally {
this.callback = IntPtr.Zero;
}
}
static void _push(voidp ctx, Z3_solver_callback cb) { static void _push(voidp ctx, Z3_solver_callback cb) {
var gch = GCHandle.FromIntPtr(ctx); var gch = GCHandle.FromIntPtr(ctx);
var prop = (UserPropagator)gch.Target; var prop = (UserPropagator)gch.Target;
prop.callback = cb; prop.Callback(() => prop.Push(), cb);
prop.Push();
prop.callback = IntPtr.Zero;
} }
static void _pop(voidp ctx, Z3_solver_callback cb, uint num_scopes) { static void _pop(voidp ctx, Z3_solver_callback cb, uint num_scopes) {
var gch = GCHandle.FromIntPtr(ctx); var gch = GCHandle.FromIntPtr(ctx);
var prop = (UserPropagator)gch.Target; var prop = (UserPropagator)gch.Target;
prop.callback = cb; prop.Callback(() => prop.Pop(num_scopes), cb);
prop.Pop(num_scopes);
prop.callback = IntPtr.Zero;
} }
static voidp _fresh(voidp _ctx, Z3_context new_context) { static voidp _fresh(voidp _ctx, Z3_context new_context) {
@ -103,17 +112,13 @@ namespace Microsoft.Z3
var prop = (UserPropagator)gch.Target; var prop = (UserPropagator)gch.Target;
using var term = Expr.Create(prop.ctx, _term); using var term = Expr.Create(prop.ctx, _term);
using var value = Expr.Create(prop.ctx, _value); using var value = Expr.Create(prop.ctx, _value);
prop.callback = cb; prop.Callback(() => prop.fixed_eh(term, value), cb);
prop.fixed_eh(term, value);
prop.callback = IntPtr.Zero;
} }
static void _final(voidp ctx, Z3_solver_callback cb) { static void _final(voidp ctx, Z3_solver_callback cb) {
var gch = GCHandle.FromIntPtr(ctx); var gch = GCHandle.FromIntPtr(ctx);
var prop = (UserPropagator)gch.Target; var prop = (UserPropagator)gch.Target;
prop.callback = cb; prop.Callback(() => prop.final_eh(), cb);
prop.final_eh();
prop.callback = IntPtr.Zero;
} }
static void _eq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b) { static void _eq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b) {
@ -121,9 +126,7 @@ namespace Microsoft.Z3
var prop = (UserPropagator)gch.Target; var prop = (UserPropagator)gch.Target;
using var s = Expr.Create(prop.ctx, a); using var s = Expr.Create(prop.ctx, a);
using var t = Expr.Create(prop.ctx, b); using var t = Expr.Create(prop.ctx, b);
prop.callback = cb; prop.Callback(() => prop.eq_eh(s, t), cb);
prop.eq_eh(s, t);
prop.callback = IntPtr.Zero;
} }
static void _diseq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b) { static void _diseq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b) {
@ -131,18 +134,14 @@ namespace Microsoft.Z3
var prop = (UserPropagator)gch.Target; var prop = (UserPropagator)gch.Target;
using var s = Expr.Create(prop.ctx, a); using var s = Expr.Create(prop.ctx, a);
using var t = Expr.Create(prop.ctx, b); using var t = Expr.Create(prop.ctx, b);
prop.callback = cb; prop.Callback(() => prop.diseq_eh(s, t), cb);
prop.diseq_eh(s, t);
prop.callback = IntPtr.Zero;
} }
static void _created(voidp ctx, Z3_solver_callback cb, Z3_ast a) { static void _created(voidp ctx, Z3_solver_callback cb, Z3_ast a) {
var gch = GCHandle.FromIntPtr(ctx); var gch = GCHandle.FromIntPtr(ctx);
var prop = (UserPropagator)gch.Target; var prop = (UserPropagator)gch.Target;
using var t = Expr.Create(prop.ctx, a); using var t = Expr.Create(prop.ctx, a);
prop.callback = cb; prop.Callback(() => prop.created_eh(t), cb);
prop.created_eh(t);
prop.callback = IntPtr.Zero;
} }
static void _decide(voidp ctx, Z3_solver_callback cb, ref Z3_ast a, ref uint idx, ref int phase) { static void _decide(voidp ctx, Z3_solver_callback cb, ref Z3_ast a, ref uint idx, ref int phase) {
@ -152,7 +151,7 @@ namespace Microsoft.Z3
var u = t; var u = t;
prop.callback = cb; prop.callback = cb;
prop.decide_eh(ref t, ref idx, ref phase); prop.decide_eh(ref t, ref idx, ref phase);
prop.callback = IntPtr.Zero; prop.callback = IntPtr.Zero;
if (u != t) if (u != t)
a = t.NativeObject; a = t.NativeObject;
} }

3
src/api/js/scripts/parse-api.js
View file

@ -54,7 +54,8 @@ let types = {
Z3_fixed_eh: 'Z3_fixed_eh', Z3_fixed_eh: 'Z3_fixed_eh',
Z3_eq_eh: 'Z3_eq_eh', Z3_eq_eh: 'Z3_eq_eh',
Z3_final_eh: 'Z3_final_eh', Z3_final_eh: 'Z3_final_eh',
Z3_created_eh: 'Z3_created_eh', Z3_created_eh: 'Z3_created_eh',
Z3_decide_eh: 'Z3_decide_eh'
}; };
let defApis = Object.create(null); let defApis = Object.create(null);