RetroSearch Browse

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

OnClause - clause inference callback More...

OnClause - clause inference callback

Definition at line 41 of file OnClause.cs.

◆ OnClause()

OnClause constructor

Definition at line 75 of file OnClause.cs.

77

gch = GCHandle.Alloc(

this

);

81

on_clause_eh = _on_clause;

82

Native.Z3_solver_register_on_clause(ctx.nCtx, solver.NativeObject, GCHandle.ToIntPtr(gch), on_clause_eh);

Context Context

Access Context object

◆ Dispose()

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

Definition at line 96 of file OnClause.cs.

◆ OnClauseEh()

Delegate type for when clauses are inferred. An inference is a pair comprising of

a proof (hint). A partial (or comprehensive) derivation justifying the inference.
a clause (vector of literals) The life-time of the proof hint and clause vector is limited to the scope of the callback. should the callback want to store hints or clauses it will need to call Dup on the hints and/or extract literals from the clause, respectively.

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