From 798a4ee86efcd1cd46557d98507a418bc2368bcc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 28 Jun 2022 14:24:05 -0700 Subject: [PATCH] use IEnumerator and format --- src/api/dotnet/UserPropagator.cs | 384 +++++++++++++++++-------------- 1 file changed, 205 insertions(+), 179 deletions(-) diff --git a/src/api/dotnet/UserPropagator.cs b/src/api/dotnet/UserPropagator.cs index cd8fa3ba5..eb181b272 100644 --- a/src/api/dotnet/UserPropagator.cs +++ b/src/api/dotnet/UserPropagator.cs @@ -37,280 +37,306 @@ namespace Microsoft.Z3 /// /// Propagator context for .Net /// - public class UserPropagator + public class UserPropagator { /// /// Delegate type for fixed callback /// - public delegate void FixedEh(Expr term, Expr value); + public delegate void FixedEh(Expr term, Expr value); /// /// Delegate type for equality or disequality callback /// - public delegate void EqEh(Expr term, Expr value); + public delegate void EqEh(Expr term, Expr value); /// /// Delegate type for when a new term using a registered function symbol is created internally /// - public delegate void CreatedEh(Expr term); + public delegate void CreatedEh(Expr term); /// /// Delegate type for callback into solver's branching - /// A bit-vector or Boolean used for branching - /// If the term is a bit-vector, then an index into the bit-vector being branched on - /// Set phase to -1 (false) or 1 (true) to override solver's phase - /// - public delegate void DecideEh(ref Expr term, ref uint idx, ref int phase); + /// A bit-vector or Boolean used for branching + /// If the term is a bit-vector, then an index into the bit-vector being branched on + /// Set phase to -1 (false) or 1 (true) to override solver's phase + /// + public delegate void DecideEh(ref Expr term, ref uint idx, ref int phase); // access managed objects through a static array. - // thread safety is ignored for now. - static List propagators = new List(); - int id; - Solver solver; - Context ctx; - Z3_solver_callback callback = IntPtr.Zero; - FixedEh fixed_eh; - Action final_eh; - EqEh eq_eh; - EqEh diseq_eh; - CreatedEh created_eh; - DecideEh decide_eh; + // thread safety is ignored for now. + static List propagators = new List(); + int id; + Solver solver; + Context ctx; + Z3_solver_callback callback = IntPtr.Zero; + FixedEh fixed_eh; + Action final_eh; + EqEh eq_eh; + EqEh diseq_eh; + CreatedEh created_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; - } - } + 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) { - var prop = propagators[ctx.ToInt32()]; - prop.Callback(() => prop.Push(), cb); - } - - static void _pop(voidp ctx, Z3_solver_callback cb, uint num_scopes) { - var prop = propagators[ctx.ToInt32()]; - prop.Callback(() => prop.Pop(num_scopes), cb); - } - - static voidp _fresh(voidp _ctx, Z3_context new_context) { - var prop = propagators[_ctx.ToInt32()]; - var ctx = new Context(new_context); - var prop1 = prop.Fresh(prop.ctx); - return new IntPtr(prop1.id); - } + static void _push(voidp ctx, Z3_solver_callback cb) + { + var prop = propagators[ctx.ToInt32()]; + prop.Callback(() => prop.Push(), cb); + } - static void _fixed(voidp ctx, Z3_solver_callback cb, Z3_ast _term, Z3_ast _value) { - var prop = propagators[ctx.ToInt32()]; - using var term = Expr.Create(prop.ctx, _term); - using var value = Expr.Create(prop.ctx, _value); - prop.Callback(() => prop.fixed_eh(term, value), cb); - } + static void _pop(voidp ctx, Z3_solver_callback cb, uint num_scopes) + { + var prop = propagators[ctx.ToInt32()]; + prop.Callback(() => prop.Pop(num_scopes), cb); + } - static void _final(voidp ctx, Z3_solver_callback cb) { - var prop = propagators[ctx.ToInt32()]; - prop.Callback(() => prop.final_eh(), cb); - } + static voidp _fresh(voidp _ctx, Z3_context new_context) + { + var prop = propagators[_ctx.ToInt32()]; + var ctx = new Context(new_context); + var prop1 = prop.Fresh(prop.ctx); + return new IntPtr(prop1.id); + } - static void _eq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b) { - var prop = propagators[ctx.ToInt32()]; - using var s = Expr.Create(prop.ctx, a); - using var t = Expr.Create(prop.ctx, b); - prop.Callback(() => prop.eq_eh(s, t), cb); - } + static void _fixed(voidp ctx, Z3_solver_callback cb, Z3_ast _term, Z3_ast _value) + { + var prop = propagators[ctx.ToInt32()]; + using var term = Expr.Create(prop.ctx, _term); + using var value = Expr.Create(prop.ctx, _value); + prop.Callback(() => prop.fixed_eh(term, value), cb); + } - static void _diseq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b) { - var prop = propagators[ctx.ToInt32()]; - using var s = Expr.Create(prop.ctx, a); - using var t = Expr.Create(prop.ctx, b); - prop.Callback(() => prop.diseq_eh(s, t), cb); - } + static void _final(voidp ctx, Z3_solver_callback cb) + { + var prop = propagators[ctx.ToInt32()]; + prop.Callback(() => prop.final_eh(), cb); + } - static void _created(voidp ctx, Z3_solver_callback cb, Z3_ast a) { - var prop = propagators[ctx.ToInt32()]; - using var t = Expr.Create(prop.ctx, a); - prop.Callback(() => prop.created_eh(t), cb); - } + static void _eq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b) + { + var prop = propagators[ctx.ToInt32()]; + using var s = Expr.Create(prop.ctx, a); + using var t = Expr.Create(prop.ctx, b); + prop.Callback(() => prop.eq_eh(s, t), cb); + } - static void _decide(voidp ctx, Z3_solver_callback cb, ref Z3_ast a, ref uint idx, ref int phase) { - var prop = propagators[ctx.ToInt32()]; - var t = Expr.Create(prop.ctx, a); - var u = t; - prop.callback = cb; - prop.decide_eh(ref t, ref idx, ref phase); - prop.callback = IntPtr.Zero; - if (u != t) - a = t.NativeObject; - } + static void _diseq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b) + { + var prop = propagators[ctx.ToInt32()]; + using var s = Expr.Create(prop.ctx, a); + using var t = Expr.Create(prop.ctx, b); + prop.Callback(() => prop.diseq_eh(s, t), cb); + } + + static void _created(voidp ctx, Z3_solver_callback cb, Z3_ast a) + { + var prop = propagators[ctx.ToInt32()]; + using var t = Expr.Create(prop.ctx, a); + prop.Callback(() => prop.created_eh(t), cb); + } + + static void _decide(voidp ctx, Z3_solver_callback cb, ref Z3_ast a, ref uint idx, ref int phase) + { + var prop = propagators[ctx.ToInt32()]; + var t = Expr.Create(prop.ctx, a); + var u = t; + prop.callback = cb; + prop.decide_eh(ref t, ref idx, ref phase); + prop.callback = IntPtr.Zero; + if (u != t) + a = t.NativeObject; + } /// /// Propagator constructor from a solver class. /// public UserPropagator(Solver s) - { - id = propagators.Count; - propagators.Add(this); - solver = s; - ctx = solver.Context; - Native.Z3_solver_propagate_init(ctx.nCtx, solver.NativeObject, new IntPtr(id), _push, _pop, _fresh); - } + { + id = propagators.Count; + propagators.Add(this); + solver = s; + ctx = solver.Context; + Native.Z3_solver_propagate_init(ctx.nCtx, solver.NativeObject, new IntPtr(id), _push, _pop, _fresh); + } /// /// Propagator constructor from a context. It is used from inside of Fresh. /// public UserPropagator(Context _ctx) - { - id = propagators.Count; - propagators.Add(this); + { + id = propagators.Count; + propagators.Add(this); solver = null; - ctx = _ctx; - } + ctx = _ctx; + } /// /// Release provate memory. /// - ~UserPropagator() - { + ~UserPropagator() + { propagators[id] = null; if (solver == null) ctx.Dispose(); - } + } /// /// Virtual method for push. It must be overwritten by inherited class. - /// - public virtual void Push() { throw new Z3Exception("Push method should be overwritten"); } + /// + public virtual void Push() { throw new Z3Exception("Push method should be overwritten"); } /// /// Virtual method for pop. It must be overwritten by inherited class. - /// - public virtual void Pop(uint n) { throw new Z3Exception("Pop method should be overwritten"); } + /// + public virtual void Pop(uint n) { throw new Z3Exception("Pop method should be overwritten"); } /// /// Virtual method for fresh. It can be overwritten by inherited class. - /// - public virtual UserPropagator Fresh(Context ctx) { return new UserPropagator(ctx); } + /// + public virtual UserPropagator Fresh(Context ctx) { return new UserPropagator(ctx); } /// /// Declare combination of assigned expressions a conflict - /// - public void Conflict(params Expr[] terms) { - Propagate(terms, ctx.MkFalse()); + /// + public void Conflict(params Expr[] terms) + { + Propagate(terms, ctx.MkFalse()); + } + + /// + /// Declare combination of assigned expressions a conflict + /// + public void Conflict(IEnumerable terms) + { + Propagate(terms, ctx.MkFalse()); } /// /// Propagate consequence - /// - public void Propagate(Expr[] terms, Expr conseq) { - var nTerms = Z3Object.ArrayToNative(terms); + /// + public void Propagate(IEnumerable terms, Expr conseq) + { + var nTerms = Z3Object.ArrayToNative(terms.ToArray()); Native.Z3_solver_propagate_consequence(ctx.nCtx, this.callback, (uint)nTerms.Length, nTerms, 0u, null, null, conseq.NativeObject); } /// /// Set fixed callback - /// + /// public FixedEh Fixed - { - set - { - this.fixed_eh = value; - if (solver != null) - Native.Z3_solver_propagate_fixed(ctx.nCtx, solver.NativeObject, _fixed); - } - } + { + set + { + this.fixed_eh = value; + if (solver != null) + Native.Z3_solver_propagate_fixed(ctx.nCtx, solver.NativeObject, _fixed); + } + } /// /// Set final callback - /// - public Action Final - { - set - { - this.final_eh = value; - if (solver != null) - Native.Z3_solver_propagate_final(ctx.nCtx, solver.NativeObject, _final); + /// + public Action Final + { + set + { + this.final_eh = value; + if (solver != null) + Native.Z3_solver_propagate_final(ctx.nCtx, solver.NativeObject, _final); } } /// /// Set equality event callback - /// - public EqEh Eq - { - set - { - this.eq_eh = value; - if (solver != null) - Native.Z3_solver_propagate_eq(ctx.nCtx, solver.NativeObject, _eq); - } + /// + public EqEh Eq + { + set + { + this.eq_eh = value; + if (solver != null) + Native.Z3_solver_propagate_eq(ctx.nCtx, solver.NativeObject, _eq); + } } /// /// Set disequality event callback - /// - public EqEh Diseq - { - set - { - this.diseq_eh = value; - if (solver != null) - Native.Z3_solver_propagate_diseq(ctx.nCtx, solver.NativeObject, _diseq); - } + /// + public EqEh Diseq + { + set + { + this.diseq_eh = value; + if (solver != null) + Native.Z3_solver_propagate_diseq(ctx.nCtx, solver.NativeObject, _diseq); + } } /// /// Set created callback - /// - public CreatedEh Created - { - set - { - this.created_eh = value; - if (solver != null) - Native.Z3_solver_propagate_created(ctx.nCtx, solver.NativeObject, _created); - } + /// + public CreatedEh Created + { + set + { + this.created_eh = value; + if (solver != null) + Native.Z3_solver_propagate_created(ctx.nCtx, solver.NativeObject, _created); + } } /// /// Set decision callback - /// - public DecideEh Decide - { - set - { - this.decide_eh = value; - if (solver != null) - Native.Z3_solver_propagate_decide(ctx.nCtx, solver.NativeObject, _decide); - } + /// + public DecideEh Decide + { + set + { + this.decide_eh = value; + if (solver != null) + Native.Z3_solver_propagate_decide(ctx.nCtx, solver.NativeObject, _decide); + } } - + /// /// Set the next decision - /// - public void NextSplit(Expr e, uint idx, int phase) - { - Native.Z3_solver_next_split(ctx.nCtx, this.callback, e.NativeObject, idx, phase); - } + /// + public void NextSplit(Expr e, uint idx, int phase) + { + Native.Z3_solver_next_split(ctx.nCtx, this.callback, e.NativeObject, idx, phase); + } /// /// Track assignments to a term - /// - public void Register(Expr term) { - if (this.callback != IntPtr.Zero) { - Native.Z3_solver_propagate_register_cb(ctx.nCtx, callback, term.NativeObject); + /// + public void Register(Expr term) + { + if (this.callback != IntPtr.Zero) + { + Native.Z3_solver_propagate_register_cb(ctx.nCtx, callback, term.NativeObject); } - else { - Native.Z3_solver_propagate_register(ctx.nCtx, solver.NativeObject, term.NativeObject); + else + { + Native.Z3_solver_propagate_register(ctx.nCtx, solver.NativeObject, term.NativeObject); } - } + } } }