mirror of
https://github.com/Z3Prover/z3
synced 2025-10-31 11:42:28 +00:00
use IEnumerator and format
This commit is contained in:
Nikolaj Bjorner
parent
556f0d7b5f
commit
798a4ee86e
1 changed files with 205 additions and 179 deletions
|
|
@ -37,280 +37,306 @@ namespace Microsoft.Z3
|
|||
/// <summary>
|
||||
/// Propagator context for .Net
|
||||
/// </summary>
|
||||
public class UserPropagator
|
||||
public class UserPropagator
|
||||
{
|
||||
/// <summary>
|
||||
/// Delegate type for fixed callback
|
||||
/// </summary>
|
||||
public delegate void FixedEh(Expr term, Expr value);
|
||||
public delegate void FixedEh(Expr term, Expr value);
|
||||
|
||||
/// <summary>
|
||||
/// Delegate type for equality or disequality callback
|
||||
/// </summary>
|
||||
public delegate void EqEh(Expr term, Expr value);
|
||||
public delegate void EqEh(Expr term, Expr value);
|
||||
|
||||
/// <summary>
|
||||
/// Delegate type for when a new term using a registered function symbol is created internally
|
||||
/// </summary>
|
||||
public delegate void CreatedEh(Expr term);
|
||||
public delegate void CreatedEh(Expr term);
|
||||
|
||||
/// <summary>
|
||||
/// Delegate type for callback into solver's branching
|
||||
/// <param name="term">A bit-vector or Boolean used for branching</param>
|
||||
/// <param name="idx">If the term is a bit-vector, then an index into the bit-vector being branched on</param>
|
||||
/// <param name="phase">Set phase to -1 (false) or 1 (true) to override solver's phase</param>
|
||||
/// </summary>
|
||||
public delegate void DecideEh(ref Expr term, ref uint idx, ref int phase);
|
||||
/// <param name="term">A bit-vector or Boolean used for branching</param>
|
||||
/// <param name="idx">If the term is a bit-vector, then an index into the bit-vector being branched on</param>
|
||||
/// <param name="phase">Set phase to -1 (false) or 1 (true) to override solver's phase</param>
|
||||
/// </summary>
|
||||
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<UserPropagator> propagators = new List<UserPropagator>();
|
||||
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<UserPropagator> propagators = new List<UserPropagator>();
|
||||
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;
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Propagator constructor from a solver class.
|
||||
/// </summary>
|
||||
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);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Propagator constructor from a context. It is used from inside of Fresh.
|
||||
/// </summary>
|
||||
public UserPropagator(Context _ctx)
|
||||
{
|
||||
id = propagators.Count;
|
||||
propagators.Add(this);
|
||||
{
|
||||
id = propagators.Count;
|
||||
propagators.Add(this);
|
||||
solver = null;
|
||||
ctx = _ctx;
|
||||
}
|
||||
ctx = _ctx;
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Release provate memory.
|
||||
/// </summary>
|
||||
~UserPropagator()
|
||||
{
|
||||
~UserPropagator()
|
||||
{
|
||||
propagators[id] = null;
|
||||
if (solver == null)
|
||||
ctx.Dispose();
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Virtual method for push. It must be overwritten by inherited class.
|
||||
/// </summary>
|
||||
public virtual void Push() { throw new Z3Exception("Push method should be overwritten"); }
|
||||
/// </summary>
|
||||
public virtual void Push() { throw new Z3Exception("Push method should be overwritten"); }
|
||||
|
||||
/// <summary>
|
||||
/// Virtual method for pop. It must be overwritten by inherited class.
|
||||
/// </summary>
|
||||
public virtual void Pop(uint n) { throw new Z3Exception("Pop method should be overwritten"); }
|
||||
/// </summary>
|
||||
public virtual void Pop(uint n) { throw new Z3Exception("Pop method should be overwritten"); }
|
||||
|
||||
/// <summary>
|
||||
/// Virtual method for fresh. It can be overwritten by inherited class.
|
||||
/// </summary>
|
||||
public virtual UserPropagator Fresh(Context ctx) { return new UserPropagator(ctx); }
|
||||
/// </summary>
|
||||
public virtual UserPropagator Fresh(Context ctx) { return new UserPropagator(ctx); }
|
||||
|
||||
/// <summary>
|
||||
/// Declare combination of assigned expressions a conflict
|
||||
/// </summary>
|
||||
public void Conflict(params Expr[] terms) {
|
||||
Propagate(terms, ctx.MkFalse());
|
||||
/// </summary>
|
||||
public void Conflict(params Expr[] terms)
|
||||
{
|
||||
Propagate(terms, ctx.MkFalse());
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Declare combination of assigned expressions a conflict
|
||||
/// </summary>
|
||||
public void Conflict(IEnumerable<Expr> terms)
|
||||
{
|
||||
Propagate(terms, ctx.MkFalse());
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Propagate consequence
|
||||
/// </summary>
|
||||
public void Propagate(Expr[] terms, Expr conseq) {
|
||||
var nTerms = Z3Object.ArrayToNative(terms);
|
||||
/// </summary>
|
||||
public void Propagate(IEnumerable<Expr> 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);
|
||||
}
|
||||
|
||||
|
||||
/// <summary>
|
||||
/// Set fixed callback
|
||||
/// </summary>
|
||||
/// </summary>
|
||||
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);
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Set final callback
|
||||
/// </summary>
|
||||
public Action Final
|
||||
{
|
||||
set
|
||||
{
|
||||
this.final_eh = value;
|
||||
if (solver != null)
|
||||
Native.Z3_solver_propagate_final(ctx.nCtx, solver.NativeObject, _final);
|
||||
/// </summary>
|
||||
public Action Final
|
||||
{
|
||||
set
|
||||
{
|
||||
this.final_eh = value;
|
||||
if (solver != null)
|
||||
Native.Z3_solver_propagate_final(ctx.nCtx, solver.NativeObject, _final);
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Set equality event callback
|
||||
/// </summary>
|
||||
public EqEh Eq
|
||||
{
|
||||
set
|
||||
{
|
||||
this.eq_eh = value;
|
||||
if (solver != null)
|
||||
Native.Z3_solver_propagate_eq(ctx.nCtx, solver.NativeObject, _eq);
|
||||
}
|
||||
/// </summary>
|
||||
public EqEh Eq
|
||||
{
|
||||
set
|
||||
{
|
||||
this.eq_eh = value;
|
||||
if (solver != null)
|
||||
Native.Z3_solver_propagate_eq(ctx.nCtx, solver.NativeObject, _eq);
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Set disequality event callback
|
||||
/// </summary>
|
||||
public EqEh Diseq
|
||||
{
|
||||
set
|
||||
{
|
||||
this.diseq_eh = value;
|
||||
if (solver != null)
|
||||
Native.Z3_solver_propagate_diseq(ctx.nCtx, solver.NativeObject, _diseq);
|
||||
}
|
||||
/// </summary>
|
||||
public EqEh Diseq
|
||||
{
|
||||
set
|
||||
{
|
||||
this.diseq_eh = value;
|
||||
if (solver != null)
|
||||
Native.Z3_solver_propagate_diseq(ctx.nCtx, solver.NativeObject, _diseq);
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Set created callback
|
||||
/// </summary>
|
||||
public CreatedEh Created
|
||||
{
|
||||
set
|
||||
{
|
||||
this.created_eh = value;
|
||||
if (solver != null)
|
||||
Native.Z3_solver_propagate_created(ctx.nCtx, solver.NativeObject, _created);
|
||||
}
|
||||
/// </summary>
|
||||
public CreatedEh Created
|
||||
{
|
||||
set
|
||||
{
|
||||
this.created_eh = value;
|
||||
if (solver != null)
|
||||
Native.Z3_solver_propagate_created(ctx.nCtx, solver.NativeObject, _created);
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Set decision callback
|
||||
/// </summary>
|
||||
public DecideEh Decide
|
||||
{
|
||||
set
|
||||
{
|
||||
this.decide_eh = value;
|
||||
if (solver != null)
|
||||
Native.Z3_solver_propagate_decide(ctx.nCtx, solver.NativeObject, _decide);
|
||||
}
|
||||
/// </summary>
|
||||
public DecideEh Decide
|
||||
{
|
||||
set
|
||||
{
|
||||
this.decide_eh = value;
|
||||
if (solver != null)
|
||||
Native.Z3_solver_propagate_decide(ctx.nCtx, solver.NativeObject, _decide);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
/// <summary>
|
||||
/// Set the next decision
|
||||
/// </summary>
|
||||
public void NextSplit(Expr e, uint idx, int phase)
|
||||
{
|
||||
Native.Z3_solver_next_split(ctx.nCtx, this.callback, e.NativeObject, idx, phase);
|
||||
}
|
||||
/// </summary>
|
||||
public void NextSplit(Expr e, uint idx, int phase)
|
||||
{
|
||||
Native.Z3_solver_next_split(ctx.nCtx, this.callback, e.NativeObject, idx, phase);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Track assignments to a term
|
||||
/// </summary>
|
||||
public void Register(Expr term) {
|
||||
if (this.callback != IntPtr.Zero) {
|
||||
Native.Z3_solver_propagate_register_cb(ctx.nCtx, callback, term.NativeObject);
|
||||
/// </summary>
|
||||
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);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue