mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

update native func interp

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-03-01 14:07:20 -08:00
parent 61d2654770
commit c812d1e890
2 changed files with 64 additions and 187 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

211
src/api/dotnet/NativeFuncInterp.cs
View file

@ -22,202 +22,79 @@ using System;
namespace Microsoft.Z3
{
using Z3_context = System.IntPtr;
using Z3_ast = System.IntPtr;
using Z3_app = System.IntPtr;
using Z3_sort = System.IntPtr;
using Z3_func_decl = System.IntPtr;
using Z3_model = System.IntPtr;
using Z3_func_interp = System.IntPtr;
using Z3_func_entry = System.IntPtr;
/// <summary>
/// A function interpretation is represented as a finite map and an 'else' value.
/// Each entry in the finite map represents the value of a function given a set of arguments.
/// </summary>
public class NativeFuncInterp : IDisposable
public class NativeFuncInterp
{
#if false
/// <summary>
/// An Entry object represents an element in the finite map used to encode
/// a function interpretation.
/// Evaluation entry of a function
/// </summary>
public class Entry : Z3Object
public class Entry
{
/// <summary>
/// Return the (symbolic) value of this entry.
/// Argument values that define entry
/// </summary>
public Expr Value
{
get
{
return Expr.Create(Context, Native.Z3_func_entry_get_value(Context.nCtx, NativeObject));
}
}
public Z3_ast[] Arguments;
/// <summary>
/// The number of arguments of the entry.
/// Result of applying function to Arguments in the interpretation
/// </summary>
public uint NumArgs
{
get { return Native.Z3_func_entry_get_num_args(Context.nCtx, NativeObject); }
}
/// <summary>
/// The arguments of the function entry.
/// </summary>
public Expr[] Args
{
get
{
uint n = NumArgs;
Expr[] res = new Expr[n];
for (uint i = 0; i < n; i++)
res[i] = Expr.Create(Context, Native.Z3_func_entry_get_arg(Context.nCtx, NativeObject, i));
return res;
}
}
/// <summary>
/// A string representation of the function entry.
/// </summary>
public override string ToString()
{
uint n = NumArgs;
string res = "[";
Expr[] args = Args;
for (uint i = 0; i < n; i++)
res += args[i] + ", ";
return res + Value + "]";
}
#region Internal
internal Entry(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
internal class DecRefQueue : IDecRefQueue
{
public DecRefQueue() : base() { }
public DecRefQueue(uint move_limit) : base(move_limit) { }
internal override void IncRef(Context ctx, IntPtr obj)
{
Native.Z3_func_entry_inc_ref(ctx.nCtx, obj);
}
internal override void DecRef(Context ctx, IntPtr obj)
{
Native.Z3_func_entry_dec_ref(ctx.nCtx, obj);
}
};
internal override void IncRef(IntPtr o)
{
Context.FuncEntry_DRQ.IncAndClear(Context, o);
base.IncRef(o);
}
internal override void DecRef(IntPtr o)
{
Context.FuncEntry_DRQ.Add(o);
base.DecRef(o);
}
#endregion
};
public Z3_ast Result;
}
/// <summary>
/// The number of entries in the function interpretation.
/// Function that is interpreted
/// </summary>
public uint NumEntries
{
get { return Native.Z3_func_interp_get_num_entries(Context.nCtx, NativeObject); }
}
public Z3_func_decl Declaration;
/// <summary>
/// The entries in the function interpretation
/// Set of non-default entries defining the function graph
/// </summary>
public Entry[] Entries
{
get
{
uint n = NumEntries;
Entry[] res = new Entry[n];
for (uint i = 0; i < n; i++)
res[i] = new Entry(Context, Native.Z3_func_interp_get_entry(Context.nCtx, NativeObject, i));
return res;
}
}
public Entry[] Entries;
/// <summary>
/// The (symbolic) `else' value of the function interpretation.
/// Default cause of the function interpretation
/// </summary>
public Expr Else
public Z3_ast Else;
#region Internal
internal NativeFuncInterp(NativeContext ctx, NativeModel mdl, Z3_func_decl decl, Z3_func_interp fi)
{
get
{
return Expr.Create(Context, Native.Z3_func_interp_get_else(Context.nCtx, NativeObject));
}
}
/// <summary>
/// The arity of the function interpretation
/// </summary>
public uint Arity
{
get { return Native.Z3_func_interp_get_arity(Context.nCtx, NativeObject); }
}
/// <summary>
/// A string representation of the function interpretation.
/// </summary>
public override string ToString()
{
string res = "";
res += "[";
foreach (Entry e in Entries)
{
uint n = e.NumArgs;
if (n > 1) res += "[";
Expr[] args = e.Args;
for (uint i = 0; i < n; i++)
{
if (i != 0) res += ", ";
res += args[i];
}
if (n > 1) res += "]";
res += " -> " + e.Value + ", ";
}
res += "else -> " + Else;
res += "]";
return res;
}
#endif
#region Internal
NativeContext Context;
IntPtr NativeObject;
internal NativeFuncInterp(NativeContext ctx, IntPtr obj)
{
Context = ctx;
NativeObject = obj;
Debug.Assert(ctx != null);
// inc-ref
}
Z3_context nCtx = ctx.nCtx;
Native.Z3_func_interp_inc_ref(nCtx, fi);
/// <summary>
/// Finalizer.
/// </summary>
~NativeFuncInterp()
{
Dispose();
}
Declaration = decl;
Else = Native.Z3_func_interp_get_else(nCtx, fi);
uint numEntries = Native.Z3_func_interp_get_num_entries(nCtx, fi);
uint numArgs = Native.Z3_func_interp_get_arity(nCtx, fi);
Entries = new Entry[numEntries];
/// <summary>
/// Disposes of the underlying native Z3 object.
/// </summary>
public void Dispose()
{
if (NativeObject != IntPtr.Zero)
for (uint j = 0; j < numEntries; ++j)
{
Native.Z3_func_interp_dec_ref(Context.nCtx, NativeObject);
NativeObject = IntPtr.Zero;
var entry = Native.Z3_func_interp_get_entry(nCtx, fi, j);
Native.Z3_func_entry_inc_ref(nCtx, entry);
Entries[j].Arguments = new Z3_ast[numArgs];
for (uint i = 0; i < numArgs; ++i)
Entries[j].Arguments[i] = Native.Z3_func_entry_get_arg(nCtx, entry, i);
Entries[j].Result = Native.Z3_func_entry_get_value(nCtx, entry);
Native.Z3_func_entry_dec_ref(nCtx, entry);
}
GC.SuppressFinalize(this);
Native.Z3_func_interp_dec_ref(nCtx, fi);
}

40
src/api/dotnet/NativeModel.cs
View file

@ -53,7 +53,7 @@ namespace Microsoft.Z3
/// <returns>An expression if the function has an interpretation in the model, null otherwise.</returns>
public Z3_ast ConstFuncInterp(Z3_func_decl f)
{
if (Native.Z3_get_arity(Context.nCtx, f) != 0)
if (Native.Z3_get_arity(Context.nCtx, f) != 0)
throw new Z3Exception("Non-zero arity functions have FunctionInterpretations as a model. Use FuncInterp.");
return Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f);
@ -68,8 +68,8 @@ namespace Microsoft.Z3
{
Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_range(Context.nCtx, f));
if (Native.Z3_get_arity(Context.nCtx, f) == 0)
if (Native.Z3_get_arity(Context.nCtx, f) == 0)
{
IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f);
@ -82,7 +82,7 @@ namespace Microsoft.Z3
if (Native.Z3_is_as_array(Context.nCtx, n) == 0)
throw new Z3Exception("Argument was not an array constant");
var fd = Native.Z3_get_as_array_func_decl(Context.nCtx, n);
return new NativeFuncInterp(Context, fd);
return new NativeFuncInterp(Context, this, f, fd);
}
}
else
@ -96,7 +96,7 @@ namespace Microsoft.Z3
if (n == IntPtr.Zero)
return null;
else
return new NativeFuncInterp(Context, n);
return new NativeFuncInterp(Context, this, f, n);
}
}
@ -188,7 +188,7 @@ namespace Microsoft.Z3
for (uint i = 0; i < nConsts; i++)
res[i] = Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i);
for (uint i = 0; i < nFuncs; i++)
res[nConsts + i] = Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i);
res[nConsts + i] = Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i);
return res;
}
}
@ -238,9 +238,10 @@ namespace Microsoft.Z3
/// <summary>
/// Evaluate expression to a double, assuming it is a numeral already.
/// </summary>
public double Double(Z3_ast t) {
public double Double(Z3_ast t)
{
var r = Eval(t, true);
return Native.Z3_get_numeral_double(Context.nCtx, r);
return Native.Z3_get_numeral_double(Context.nCtx, r);
}
/// <summary>
@ -258,7 +259,6 @@ namespace Microsoft.Z3
/// the "universe" of the sort.
/// </remarks>
/// <seealso cref="NumSorts"/>
/// <seealso cref="SortUniverse"/>
public Z3_sort[] Sorts
{
get
@ -283,15 +283,15 @@ namespace Microsoft.Z3
}
IntPtr NativeObject;
NativeContext Context;
IntPtr NativeObject;
NativeContext Context;
internal NativeModel(NativeContext ctx, IntPtr obj)
{
Context = ctx;
NativeObject = obj;
Context = ctx;
NativeObject = obj;
Debug.Assert(ctx != null);
Native.Z3_model_inc_ref(ctx.nCtx, obj);
Native.Z3_model_inc_ref(ctx.nCtx, obj);
}
@ -299,9 +299,9 @@ namespace Microsoft.Z3
/// Finalizer.
/// </summary>
~NativeModel()
{
Dispose();
}
{
Dispose();
}
/// <summary>
/// Disposes of the underlying native Z3 object.
@ -310,8 +310,8 @@ namespace Microsoft.Z3
{
if (NativeObject != IntPtr.Zero)
{
Native.Z3_model_dec_ref(Context.nCtx, NativeObject);
NativeObject = IntPtr.Zero;
Native.Z3_model_dec_ref(Context.nCtx, NativeObject);
NativeObject = IntPtr.Zero;
}
GC.SuppressFinalize(this);
}