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 (Expr term, uint idx, bool phase)

Delegate type for callback into solver's branching. The values can be overridden by calling NextSplit. 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...

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

Propagate consequence

Returns: true if the propagated expression is new for the solver; false if the propagation was ignored

More...

bool Propagate (IEnumerable< Expr > terms, EqualityPairs equalities, Expr conseq)

Propagate consequence

Returns: true if the propagated expression is new for the solver; false if the propagation was ignored

More...

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

Set the next decision

Parameters

e	A bit-vector or Boolean used for branching. Use `null` to clear
idx	If the term is a bit-vector, then an index into the bit-vector being branched on
phase	The tentative truth-value (-1/false, 1/true, 0/let Z3 decide)

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 181 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 195 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 248 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 240 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	(	Expr	term,
		uint	idx,
		bool	phase
	)

Delegate type for callback into solver's branching. The values can be overridden by calling NextSplit.

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	The tentative truth-value

◆ 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 213 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 235 of file UserPropagator.cs.

235 { return new UserPropagator(ctx); }

Microsoft.Z3.UserPropagator.UserPropagator

UserPropagator(Solver s)

Propagator constructor from a solver class.

Definition: UserPropagator.cs:181

◆ NextSplit()

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

inline

Set the next decision

Parameters

e	A bit-vector or Boolean used for branching. Use `null` to clear
idx	If the term is a bit-vector, then an index into the bit-vector being branched on
phase	The tentative truth-value (-1/false, 1/true, 0/let Z3 decide)

Returns: true in case the value was successfully set; false if the next split could not be set

Definition at line 376 of file UserPropagator.cs.

         {
             return Native.Z3_solver_next_split(ctx.nCtx, this.callback, e?.NativeObject ?? IntPtr.Zero, idx, phase) != 0;
         }

◆ Pop()

virtual void Pop ( uint n )

inlinevirtual

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

Definition at line 230 of file UserPropagator.cs.

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

◆ Propagate() [1/2]

bool Propagate	(	IEnumerable< Expr >	terms,
		EqualityPairs	equalities,
		Expr	conseq
	)

inline

Propagate consequence

Returns: true if the propagated expression is new for the solver; false if the propagation was ignored

Definition at line 272 of file UserPropagator.cs.

         {
             var nTerms = Z3Object.ArrayToNative(terms.ToArray());
             var nLHS = Z3Object.ArrayToNative(equalities.LHS.ToArray());
             var nRHS = Z3Object.ArrayToNative(equalities.RHS.ToArray());
             return Native.Z3_solver_propagate_consequence(ctx.nCtx, this.callback, (uint)nTerms.Length, nTerms, (uint)equalities.Count, nLHS, nRHS, conseq.NativeObject) != 0;
         }

◆ Propagate() [2/2]

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

inline

Propagate consequence

Returns: true if the propagated expression is new for the solver; false if the propagation was ignored

Definition at line 260 of file UserPropagator.cs.

         {
             return Propagate(terms, new EqualityPairs(), conseq);
         }

Referenced by UserPropagator.Conflict().

◆ Push()

virtual void Push ( )

inlinevirtual

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

Definition at line 225 of file UserPropagator.cs.

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

◆ Register()

void Register ( Expr term )

inline

Track assignments to a term

Definition at line 384 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 340 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 354 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 326 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 312 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 298 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 284 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() [1/2]

◆ Propagate() [2/2]

◆ Push()

◆ Register()

Property Documentation

◆ Created

◆ Decide

◆ Diseq

◆ Eq

◆ Final

◆ Fixed