Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://z3prover.github.io/api/html/class_microsoft_1_1_z3_1_1_user_propagator.html below:

Z3: UserPropagator Class Reference

Propagator context for .Net More...

Returns

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

Returns

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

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)

Propagator context for .Net

Definition at line 40 of file UserPropagator.cs.

Propagator constructor from a solver class.

Definition at line 181 of file UserPropagator.cs.

gch = GCHandle.Alloc(

);

Native.Z3_solver_propagate_init(ctx.nCtx, solver.NativeObject, GCHandle.ToIntPtr(gch), push_eh, pop_eh, fresh_eh);

Context Context

Access Context object

Referenced by UserPropagator.Fresh().

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

Definition at line 195 of file UserPropagator.cs.

gch = GCHandle.Alloc(

);

Declare combination of assigned expressions a conflict

Definition at line 248 of file UserPropagator.cs.

BoolExpr MkFalse()

The false Term.

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

Propagate consequence true if the propagated expression is new for the solver; false if the propagati...

Declare combination of assigned expressions a conflict

Definition at line 240 of file UserPropagator.cs.

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

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

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.

(!gch.IsAllocated)

void Dispose()

Disposes of the context.

Delegate type for equality or disequality callback

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.

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

Definition at line 235 of file UserPropagator.cs.

UserPropagator(Solver s)

Propagator constructor from a solver class.

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.

Native.Z3_solver_next_split(ctx.nCtx,

.callback, e?.NativeObject ?? IntPtr.Zero, idx, phase) != 0;

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

Definition at line 230 of file UserPropagator.cs.

{

Z3Exception(

); }

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());

Native.Z3_solver_propagate_consequence(ctx.nCtx,

.callback, (uint)nTerms.Length, nTerms, (uint)equalities.Count, nLHS, nRHS, conseq.NativeObject) != 0;

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.

(terms,

EqualityPairs(), conseq);

Referenced by UserPropagator.Conflict().

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

Definition at line 225 of file UserPropagator.cs.

{

Z3Exception(

); }

Track assignments to a term

Definition at line 384 of file UserPropagator.cs.

(this.callback != IntPtr.Zero)

Native.Z3_solver_propagate_register_cb(ctx.nCtx, callback, term.NativeObject);

Native.Z3_solver_propagate_register(ctx.nCtx, solver.NativeObject, term.NativeObject);

Set created callback

Definition at line 340 of file UserPropagator.cs.

this.created_wrapper = _created;

this.created_eh = value;

Native.Z3_solver_propagate_created(ctx.nCtx, solver.NativeObject, created_wrapper);

Set decision callback

Definition at line 354 of file UserPropagator.cs.

this.decide_wrapper = _decide;

this.decide_eh = value;

Native.Z3_solver_propagate_decide(ctx.nCtx, solver.NativeObject, decide_wrapper);

Set disequality event callback

Definition at line 326 of file UserPropagator.cs.

this.diseq_wrapper = _diseq;

this.diseq_eh = value;

Native.Z3_solver_propagate_diseq(ctx.nCtx, solver.NativeObject, diseq_wrapper);

Set equality event callback

Definition at line 312 of file UserPropagator.cs.

this.eq_wrapper = _eq;

Native.Z3_solver_propagate_eq(ctx.nCtx, solver.NativeObject, eq_wrapper);

Set final callback

Definition at line 298 of file UserPropagator.cs.

this.final_wrapper = _final;

this.final_eh = value;

Native.Z3_solver_propagate_final(ctx.nCtx, solver.NativeObject, final_wrapper);

Set fixed callback

Definition at line 284 of file UserPropagator.cs.

this.fixed_wrapper = _fixed;

this.fixed_eh = value;

Native.Z3_solver_propagate_fixed(ctx.nCtx, solver.NativeObject, fixed_wrapper);

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4