mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 04:13:38 +00:00
Code Activity

finish NativeModel

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-03-01 12:40:03 -08:00
parent c0826d58bf
commit deeb5e9921
1 changed files with 17 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -37,7 +37,7 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// A Model contains interpretations (assignments) of constants and functions. /// A Model contains interpretations (assignments) of constants and functions.
/// </summary> /// </summary>
public class NativeModel public class NativeModel : IDisposable
{ {
/// <summary> /// <summary>
/// Retrieves the interpretation (the assignment) of <paramref name="a"/> in the model. /// Retrieves the interpretation (the assignment) of <paramref name="a"/> in the model.
@ -155,28 +155,28 @@ namespace Microsoft.Z3
get { return Native.Z3_model_get_num_funcs(Context.nCtx, NativeObject); } get { return Native.Z3_model_get_num_funcs(Context.nCtx, NativeObject); }
} }
#if false
/// <summary> /// <summary>
/// The function declarations of the function interpretations in the model. /// The function declarations of the function interpretations in the model.
/// </summary> /// </summary>
public FuncDecl[] FuncDecls public Z3_func_decl[] FuncDecls
{ {
get get
{ {
uint n = NumFuncs; uint n = NumFuncs;
FuncDecl[] res = new FuncDecl[n]; Z3_func_decl[] res = new Z3_func_decl[n];
for (uint i = 0; i < n; i++) for (uint i = 0; i < n; i++)
res[i] = new FuncDecl(Context, Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i)); res[i] = Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i);
return res; return res;
} }
} }
/// <summary> /// <summary>
/// All symbols that have an interpretation in the model. /// All symbols that have an interpretation in the model.
/// </summary> /// </summary>
public FuncDecl[] Decls public Z3_func_decl[] Decls
{ {
get get
{ {
@ -184,11 +184,11 @@ namespace Microsoft.Z3
uint nFuncs = NumFuncs; uint nFuncs = NumFuncs;
uint nConsts = NumConsts; uint nConsts = NumConsts;
uint n = nFuncs + nConsts; uint n = nFuncs + nConsts;
FuncDecl[] res = new FuncDecl[n]; Z3_func_decl[] res = new Z3_func_decl[n];
for (uint i = 0; i < nConsts; i++) for (uint i = 0; i < nConsts; i++)
res[i] = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i)); res[i] = Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i);
for (uint i = 0; i < nFuncs; i++) for (uint i = 0; i < nFuncs; i++)
res[nConsts + i] = new FuncDecl(Context, 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; return res;
} }
} }
@ -204,6 +204,7 @@ namespace Microsoft.Z3
public ModelEvaluationFailedException() : base() { } public ModelEvaluationFailedException() : base() { }
} }
/// <summary> /// <summary>
/// Evaluates the expression <paramref name="t"/> in the current model. /// Evaluates the expression <paramref name="t"/> in the current model.
/// </summary> /// </summary>
@ -220,24 +221,19 @@ namespace Microsoft.Z3
/// <returns>The evaluation of <paramref name="t"/> in the model.</returns> /// <returns>The evaluation of <paramref name="t"/> in the model.</returns>
public Z3_ast Eval(Z3_ast t, bool completion = false) public Z3_ast Eval(Z3_ast t, bool completion = false)
{ {
Debug.Assert(t != null);
IntPtr v = IntPtr.Zero; IntPtr v = IntPtr.Zero;
if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (byte)(completion ? 1 : 0), ref v) == (byte)0) if (Native.Z3_model_eval(Context.nCtx, NativeObject, t, (byte)(completion ? 1 : 0), ref v) == (byte)0)
throw new ModelEvaluationFailedException(); throw new ModelEvaluationFailedException();
else else
return Z3_ast.Create(Context, v); return v;
} }
/// <summary> /// <summary>
/// Alias for <c>Eval</c>. /// Alias for <c>Eval</c>.
/// </summary> /// </summary>
public Z3_ast Evaluate(Z3_ast t, bool completion = false) public Z3_ast Evaluate(Z3_ast t, bool completion = false) => Eval(t, completion);
{
Debug.Assert(t != null);
return Eval(t, completion);
}
/// <summary> /// <summary>
/// Evaluate expression to a double, assuming it is a numeral already. /// Evaluate expression to a double, assuming it is a numeral already.
@ -252,6 +248,7 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public uint NumSorts { get { return Native.Z3_model_get_num_sorts(Context.nCtx, NativeObject); } } public uint NumSorts { get { return Native.Z3_model_get_num_sorts(Context.nCtx, NativeObject); } }
/// <summary> /// <summary>
/// The uninterpreted sorts that the model has an interpretation for. /// The uninterpreted sorts that the model has an interpretation for.
/// </summary> /// </summary>
@ -262,20 +259,19 @@ namespace Microsoft.Z3
/// </remarks> /// </remarks>
/// <seealso cref="NumSorts"/> /// <seealso cref="NumSorts"/>
/// <seealso cref="SortUniverse"/> /// <seealso cref="SortUniverse"/>
public Sort[] Sorts public Z3_sort[] Sorts
{ {
get get
{ {
uint n = NumSorts; uint n = NumSorts;
Sort[] res = new Sort[n]; Z3_sort[] res = new Z3_sort[n];
for (uint i = 0; i < n; i++) for (uint i = 0; i < n; i++)
res[i] = Sort.Create(Context, Native.Z3_model_get_sort(Context.nCtx, NativeObject, i)); res[i] = Native.Z3_model_get_sort(Context.nCtx, NativeObject, i);
return res; return res;
} }
} }
#endif
/// <summary> /// <summary>
/// Conversion of models to strings. /// Conversion of models to strings.
@ -287,7 +283,6 @@ namespace Microsoft.Z3
} }
IntPtr NativeObject; IntPtr NativeObject;
NativeContext Context; NativeContext Context;