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.

delegate void EqEh (Expr term, Expr value)

Delegate type for equality or disequality callback.

delegate void CreatedEh (Expr term)

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

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.

delegate bool OnBindingEh (Expr q, Expr inst)

Delegate type for callback when a quantifier is bound to an instance.

UserPropagator (Solver s)

Propagator constructor from a solver class.

UserPropagator (Context _ctx)

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

virtual void Dispose ()

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

virtual void Push ()

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

virtual void Pop (uint n)

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

virtual UserPropagator Fresh (Context ctx)

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

void Conflict (params Expr[] terms)

Declare combination of assigned expressions a conflict.

void Conflict (IEnumerable< Expr > terms)

Declare combination of assigned expressions a conflict.

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

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

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)

void Register (Expr term)

Track assignments to a term.

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

Action	Final `[set]`
	Set final callback.

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

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

CreatedEh	Created `[set]`
	Set created callback.

DecideEh	Decide `[set]`
	Set decision callback.

OnBindingEh	OnBinding `[set]`
	Set binding callback.

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

◆ UserPropagator() [2/2]

UserPropagator ( Context _ctx )

inline

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

Definition at line 218 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 271 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 263 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.

Referenced by UserPropagator.OnBindingEh().

◆ 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

Referenced by UserPropagator.OnBindingEh().

◆ 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 236 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.

Referenced by UserPropagator.OnBindingEh().

◆ 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.

Referenced by UserPropagator.OnBindingEh().

◆ Fresh()

virtual UserPropagator Fresh ( Context ctx )

inlinevirtual

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

Definition at line 258 of file UserPropagator.cs.

258{ return new UserPropagator(ctx); }

Microsoft.Z3.UserPropagator.UserPropagator

UserPropagator(Solver s)

Propagator constructor from a solver class.

Definition UserPropagator.cs:204

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

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

◆ OnBindingEh()

delegate bool OnBindingEh	(	Expr	q,
		Expr	inst
	)

Delegate type for callback when a quantifier is bound to an instance.

Parameters

q	Quantifier
inst	Instance

Returns: true if binding is allowed to take effect in the solver, false if blocked by callback

Referenced by UserPropagator.OnBindingEh().

◆ Pop()

virtual void Pop ( uint n )

inlinevirtual

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

Definition at line 253 of file UserPropagator.cs.

253{ 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 295 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 283 of file UserPropagator.cs.

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

Referenced by UserPropagator.Conflict(), UserPropagator.Conflict(), and UserPropagator.Propagate().

◆ Push()

virtual void Push ( )

inlinevirtual

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

Definition at line 248 of file UserPropagator.cs.

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

◆ Register()

void Register ( Expr term )

inline

Track assignments to a term.

Definition at line 423 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 363 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 377 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 349 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 335 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 321 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 307 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);
            }
        }

◆ OnBinding

OnBindingEh OnBinding

set

Set binding callback.

Definition at line 391 of file UserPropagator.cs.

        {
            set
            {
                this.on_binding_wrapper = _on_binding;
                this.on_binding_eh = value;
                if (solver != null)
                    Native.Z3_solver_propagate_on_binding(ctx.nCtx, solver.NativeObject, on_binding_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()

◆ OnBindingEh()

◆ Pop()

◆ Propagate() [1/2]

◆ Propagate() [2/2]

◆ Push()

◆ Register()

Property Documentation

◆ Created

◆ Decide

◆ Diseq

◆ Eq

◆ Final

◆ Fixed

◆ OnBinding