Propagator context for .Net More...

Inheritance diagram for UserPropagator:

Public Member Functions

delegate void FixedEh (Expr term, Expr value)

Delegate type for fixed callback Note that the life-time of the term and value only applies within the scope of the callback. That means the term and value cannot be stored in an array, dictionary or similar and accessed after the callback has returned. Use the functionality Dup on expressions to create a duplicate copy that extends the lifetime. More...

delegate void EqEh (Expr term, Expr value)

Delegate type for equality or disequality callback More...

delegate void CreatedEh (Expr term)

Delegate type for when a new term using a registered function symbol is created internally More...

delegate void DecideEh (ref Expr term, ref uint idx, ref int phase)

Delegate type for callback into solver's branching

Parameters

term	A bit-vector or Boolean used for branching
idx	If the term is a bit-vector, then an index into the bit-vector being branched on
phase	Set phase to -1 (false) or 1 (true) to override solver's phase

More...

UserPropagator (Solver s)

Propagator constructor from a solver class. More...

UserPropagator (Context _ctx)

Propagator constructor from a context. It is used from inside of Fresh. More...

virtual void Dispose ()

Must be called. The object will not be garbage collected automatically even if the context is disposed More...

virtual void Push ()

Virtual method for push. It must be overwritten by inherited class. More...

virtual void Pop (uint n)

Virtual method for pop. It must be overwritten by inherited class. More...

virtual UserPropagator Fresh (Context ctx)

Virtual method for fresh. It can be overwritten by inherited class. More...

void Conflict (params Expr[] terms)

Declare combination of assigned expressions a conflict More...

void Conflict (IEnumerable< Expr > terms)

Declare combination of assigned expressions a conflict More...

void Propagate (IEnumerable< Expr > terms, Expr conseq)

Propagate consequence More...

void NextSplit (Expr e, uint idx, int phase)

Set the next decision More...

void Register (Expr term)

Track assignments to a term More...

Properties
FixedEh	Fixed `[set]`
	Set fixed callback More...

Action	Final `[set]`
	Set final callback More...

EqEh	Eq `[set]`
	Set equality event callback More...

EqEh	Diseq `[set]`
	Set disequality event callback More...

CreatedEh	Created `[set]`
	Set created callback More...

DecideEh	Decide `[set]`
	Set decision callback More...

Detailed Description

Propagator context for .Net

Definition at line 40 of file UserPropagator.cs.

Constructor & Destructor Documentation

◆ UserPropagator() [1/2]

UserPropagator ( Solver s )

inline

Propagator constructor from a solver class.

Definition at line 186 of file UserPropagator.cs.

         {
             gch = GCHandle.Alloc(this);
             solver = s;
             ctx = solver.Context;
             push_eh = _push;
             pop_eh = _pop;
             fresh_eh = _fresh;
             Native.Z3_solver_propagate_init(ctx.nCtx, solver.NativeObject, GCHandle.ToIntPtr(gch), push_eh, pop_eh, fresh_eh);
         }

Referenced by UserPropagator.Fresh().

◆ UserPropagator() [2/2]

UserPropagator ( Context _ctx )

inline

Propagator constructor from a context. It is used from inside of Fresh.

Definition at line 200 of file UserPropagator.cs.

         {
             gch = GCHandle.Alloc(this);
             solver = null;
             ctx = _ctx;
         }

Member Function Documentation

◆ Conflict() [1/2]

void Conflict ( IEnumerable< Expr > terms )

inline

Declare combination of assigned expressions a conflict

Definition at line 253 of file UserPropagator.cs.

         {
             Propagate(terms, ctx.MkFalse());
         }

◆ Conflict() [2/2]

void Conflict ( params Expr[] terms )

inline

Declare combination of assigned expressions a conflict

Definition at line 245 of file UserPropagator.cs.

         {
             Propagate(terms, ctx.MkFalse());
         }

◆ CreatedEh()

delegate void CreatedEh ( Expr term )

Delegate type for when a new term using a registered function symbol is created internally

◆ DecideEh()

delegate void DecideEh	(	ref Expr	term,
		ref uint	idx,
		ref int	phase
	)

Delegate type for callback into solver's branching

Parameters

term	A bit-vector or Boolean used for branching
idx	If the term is a bit-vector, then an index into the bit-vector being branched on
phase	Set phase to -1 (false) or 1 (true) to override solver's phase

◆ Dispose()

virtual void Dispose ( )

inlinevirtual

Must be called. The object will not be garbage collected automatically even if the context is disposed

Definition at line 218 of file UserPropagator.cs.

         {
             if (!gch.IsAllocated)
                 return;
             gch.Free();
             if (solver == null)
                 ctx.Dispose();
         }

◆ EqEh()

delegate void EqEh	(	Expr	term,
		Expr	value
	)

Delegate type for equality or disequality callback

◆ FixedEh()

delegate void FixedEh	(	Expr	term,
		Expr	value
	)

Delegate type for fixed callback Note that the life-time of the term and value only applies within the scope of the callback. That means the term and value cannot be stored in an array, dictionary or similar and accessed after the callback has returned. Use the functionality Dup on expressions to create a duplicate copy that extends the lifetime.

◆ Fresh()

virtual UserPropagator Fresh ( Context ctx )

inlinevirtual

Virtual method for fresh. It can be overwritten by inherited class.

Definition at line 240 of file UserPropagator.cs.

240 { return new UserPropagator(ctx); }

Microsoft.Z3.UserPropagator.UserPropagator

UserPropagator(Solver s)

Propagator constructor from a solver class.

Definition: UserPropagator.cs:186

◆ NextSplit()

void NextSplit	(	Expr	e,
		uint	idx,
		int	phase
	)

inline

Set the next decision

Definition at line 356 of file UserPropagator.cs.

         {
             Native.Z3_solver_next_split(ctx.nCtx, this.callback, e.NativeObject, idx, phase);
         }

◆ Pop()

virtual void Pop ( uint n )

inlinevirtual

Virtual method for pop. It must be overwritten by inherited class.

Definition at line 235 of file UserPropagator.cs.

235 { throw new Z3Exception("Pop method should be overwritten"); }

◆ Propagate()

void Propagate	(	IEnumerable< Expr >	terms,
		Expr	conseq
	)

inline

Propagate consequence

Definition at line 261 of file UserPropagator.cs.

         {
             var nTerms = Z3Object.ArrayToNative(terms.ToArray());
             Native.Z3_solver_propagate_consequence(ctx.nCtx, this.callback, (uint)nTerms.Length, nTerms, 0u, null, null, conseq.NativeObject);
         }

Referenced by UserPropagator.Conflict().

◆ Push()

virtual void Push ( )

inlinevirtual

Virtual method for push. It must be overwritten by inherited class.

Definition at line 230 of file UserPropagator.cs.

230 { throw new Z3Exception("Push method should be overwritten"); }

◆ Register()

void Register ( Expr term )

inline

Track assignments to a term

Definition at line 364 of file UserPropagator.cs.

         {
             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);
             }
         }

Property Documentation

◆ Created

CreatedEh Created

set

Set created callback

Definition at line 327 of file UserPropagator.cs.

         {
             set
             {
                 this.created_wrapper = _created;
                 this.created_eh = value;
                 if (solver != null)
                     Native.Z3_solver_propagate_created(ctx.nCtx, solver.NativeObject, created_wrapper);
             }
         }

◆ Decide

DecideEh Decide

set

Set decision callback

Definition at line 341 of file UserPropagator.cs.

         {
             set
             {
                 this.decide_wrapper = _decide;
                 this.decide_eh = value;
                 if (solver != null)
                     Native.Z3_solver_propagate_decide(ctx.nCtx, solver.NativeObject, decide_wrapper);
             }
         }

◆ Diseq

EqEh Diseq

set

Set disequality event callback

Definition at line 313 of file UserPropagator.cs.

         {
             set
             {
                 this.diseq_wrapper = _diseq;
                 this.diseq_eh = value;
                 if (solver != null)
                     Native.Z3_solver_propagate_diseq(ctx.nCtx, solver.NativeObject, diseq_wrapper);
             }
         }

◆ Eq

EqEh Eq

set

Set equality event callback

Definition at line 299 of file UserPropagator.cs.

         {
             set
             {
                 this.eq_wrapper = _eq;
                 this.eq_eh = value;
                 if (solver != null)
                     Native.Z3_solver_propagate_eq(ctx.nCtx, solver.NativeObject, eq_wrapper);
             }
         }

◆ Final

Action Final

set

Set final callback

Definition at line 285 of file UserPropagator.cs.

         {
             set
             {
                 this.final_wrapper = _final;
                 this.final_eh = value;
                 if (solver != null)
                     Native.Z3_solver_propagate_final(ctx.nCtx, solver.NativeObject, final_wrapper);
             }
         }

◆ Fixed

FixedEh Fixed

set

Set fixed callback

Definition at line 271 of file UserPropagator.cs.

         {
             set
             {
                 this.fixed_wrapper = _fixed;
                 this.fixed_eh = value;
                 if (solver != null)
                     Native.Z3_solver_propagate_fixed(ctx.nCtx, solver.NativeObject, fixed_wrapper);
             }
         }

Public Member Functions

Properties

Detailed Description

Constructor & Destructor Documentation

◆ UserPropagator() [1/2]

◆ UserPropagator() [2/2]

Member Function Documentation

◆ Conflict() [1/2]

◆ Conflict() [2/2]

◆ CreatedEh()

◆ DecideEh()

◆ Dispose()

◆ EqEh()

◆ FixedEh()

◆ Fresh()

◆ NextSplit()

◆ Pop()

◆ Propagate()

◆ Push()

◆ Register()

Property Documentation

◆ Created

◆ Decide

◆ Diseq

◆ Eq

◆ Final

◆ Fixed