mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

add decide callback

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-05-08 15:30:03 -07:00
parent c8d12975c9
commit 8218f25222
3 changed files with 40 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
scripts/update_api.py
View file

@ -414,6 +414,7 @@ def mk_dotnet(dotnet):
for name, ret, sig in Closures:
sig = sig.replace("void*","voidp").replace("unsigned","uint")
sig = sig.replace("Z3_ast*","ref IntPtr").replace("uint*","ref uint").replace("Z3_lbool*","ref int")
ret = ret.replace("void*","voidp").replace("unsigned","uint")
if "*" in sig or "*" in ret:
continue
@ -1349,7 +1350,8 @@ z3_ml_callbacks = frozenset([
'Z3_solver_propagate_final',
'Z3_solver_propagate_eq',
'Z3_solver_propagate_diseq',
'Z3_solver_propagate_created'
'Z3_solver_propagate_created',
'Z3_solver_propagate_decide'
])
def mk_ml(ml_src_dir, ml_output_dir):

36
src/api/dotnet/UserPropagator.cs
View file

@ -55,6 +55,14 @@ namespace Microsoft.Z3
/// </summary>
public delegate void CreatedEh(Expr term);
/// <summary>
/// Delegate type for callback into solver's branching
/// <param name="term">A bit-vector or Boolean used for branching</param>
/// <param name="idx">If the term is a bit-vector, then an index into the bit-vector being branched on</param>
/// <param name="phase">Set phase to -1 (false) or 1 (true) to override solver's phase</param>
/// </summary>
public delegate void DecideEh(ref Expr term, ref uint idx, ref int phase);
Solver solver;
Context ctx;
GCHandle gch;
@ -64,6 +72,7 @@ namespace Microsoft.Z3
EqEh eq_eh;
EqEh diseq_eh;
CreatedEh created_eh;
DecideEh decide_eh;
static void _push(voidp ctx, Z3_solver_callback cb) {
@ -137,6 +146,20 @@ namespace Microsoft.Z3
prop.callback = IntPtr.Zero;
}
static void _decide(voidp ctx, Z3_solver_callback cb, ref Z3_ast a, ref uint idx, ref int phase) {
var gch = GCHandle.FromIntPtr(ctx);
var prop = (UserPropagator)gch.Target;
var t = Expr.Create(prop.ctx, a);
var u = t;
prop.callback = cb;
prop.decide_eh(ref t, ref idx, ref phase);
prop.callback = IntPtr.Zero;
if (u != t) {
a = t.NativeObject;
}
t.Dispose();
}
/// <summary>
/// Propagator constructor from a solver class.
/// </summary>
@ -266,6 +289,19 @@ namespace Microsoft.Z3
}
}
/// <summary>
/// Set decision callback
/// </summary>
public DecideEh Decide
{
set
{
this.decide_eh = value;
if (solver != null)
Native.Z3_solver_propagate_decide(ctx.nCtx, solver.NativeObject, _decide);
}
}
/// <summary>
/// Track assignments to a term
/// </summary>

1
src/api/z3_api.h
View file

@ -6801,6 +6801,7 @@ extern "C" {
In case the expression is a bitvector the bit to split on is determined by the bit argument and the
truth-value to try first is given by is_pos. In case the truth value is undefined the solver will decide.
def_API('Z3_solver_propagate_decide', VOID, (_in(CONTEXT), _in(SOLVER), _fnptr(Z3_decide_eh)))
*/
void Z3_API Z3_solver_propagate_decide(Z3_context c, Z3_solver s, Z3_decide_eh decide_eh);