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

NativeModel: TryGetArrayValue (#5881)

Browse source 
* WiP:  Disposable, MkAdd, MkApp, MkBool, MkBoolSort, MkBound, MkBvSort, MkFalse, MkTrue, MkIntSort

* WiP: Native z3 mk_ functions

* WiP: mk_ functions for NativeContext

* WiP: add utility functions for getting values

* WiP: Adding more native utility functions

* native model pull

* WiP: NativeContext additions for array access

* WiP: use Z3_symbol in place of managed Symbol

* WiP: add solver, model, and array methods

* WiP: MkSimpleSolver, MkReal

* WiP: GetDomain GetRange

* WiP: MkExists

* Override for MkFuncDecl

* MkConstArray, MkSelect

* WiP: code cleanup

* migrate Context reference to NativeContext

* remove local signing from PR

* minor code cleanup

* Sorts to properties, fix usings,

* make IntSort property

* sort using

* IntSort, RealSort - properties

* WiP: get array value update

Co-authored-by: jfleisher <jofleish@microsoft.com>
This commit is contained in:
John Fleisher 2022-03-03 16:06:30 -05:00 committed by GitHub
parent 248a3676af
commit 35d26bc282
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 56 additions and 54 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
src/api/dotnet/NativeContext.cs
View file

@ -235,7 +235,7 @@ namespace Microsoft.Z3
public Z3_ast MkReal(string v)
{
Debug.Assert(!string.IsNullOrEmpty(v));
return Native.Z3_mk_numeral(nCtx, v, MkRealSort());
return Native.Z3_mk_numeral(nCtx, v, RealSort);
}
/// <summary>
@ -304,10 +304,14 @@ namespace Microsoft.Z3
#region Sort
public Z3_sort MkIntSort() => Native.Z3_mk_int_sort(nCtx);
public Z3_sort MkBoolSort() => Native.Z3_mk_bool_sort(nCtx);
/// <summary>
/// Sorts return same ptr for subsequent calls
/// </summary>
public Z3_sort IntSort => Native.Z3_mk_int_sort(nCtx);
public Z3_sort BoolSort => Native.Z3_mk_bool_sort(nCtx);
public Z3_sort RealSort => Native.Z3_mk_real_sort(nCtx);
public Z3_sort MkBvSort(uint size) => Native.Z3_mk_bv_sort(nCtx, size);
public Z3_sort MkRealSort() => Native.Z3_mk_real_sort(nCtx);
public Z3_sort MkListSort(string name, Z3_sort elemSort,
out Z3_func_decl inil, out Z3_func_decl iisnil,
@ -1086,17 +1090,24 @@ namespace Microsoft.Z3
/// <returns></returns>
public Z3_ast[] GetAppArgs(Z3_app app)
{
Debug.Assert(app != IntPtr.Zero);
var numArgs = Native.Z3_get_app_num_args(nCtx, app);
var numArgs = GetNumArgs(app);
var args = new Z3_ast[numArgs];
for (uint i = 0; i < numArgs; i++)
{
args[i] = Native.Z3_get_app_arg(nCtx, app, i);
args[i] = GetAppArg(app, i);
}
return args;
}
public uint GetNumArgs(Z3_app app)
{
Debug.Assert(app != IntPtr.Zero);
return Native.Z3_get_app_num_args(nCtx, app);
}
internal Z3_ast GetAppArg(Z3_app app, uint i) => Native.Z3_get_app_arg(nCtx, app, i);
/// <summary>
/// Get App Decl from IntPtr
/// </summary>

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

@ -41,7 +41,7 @@ namespace Microsoft.Z3
/// </summary>
/// <param name="a">A Constant</param>
/// <returns>An expression if the constant has an interpretation in the model, null otherwise.</returns>
public Z3_ast ConstInterp(Z3_ast a) => ConstFuncInterp(Native.Z3_get_app_decl(Context.nCtx, a));
public Z3_ast ConstInterp(Z3_ast a) => ConstFuncInterp(Native.Z3_get_app_decl(ntvContext.nCtx, a));
/// <summary>
/// Retrieves the interpretation (the assignment) of <paramref name="f"/> in the model.
@ -50,10 +50,10 @@ 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(ntvContext.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);
return Native.Z3_model_get_const_interp(ntvContext.nCtx, NativeObject, f);
}
/// <summary>
@ -63,11 +63,11 @@ namespace Microsoft.Z3
/// <returns>A FunctionInterpretation if the function has an interpretation in the model, null otherwise.</returns>
public NativeFuncInterp FuncInterp(Z3_func_decl f)
{
Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_range(Context.nCtx, f));
Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(ntvContext.nCtx, Native.Z3_get_range(ntvContext.nCtx, f));
if (Native.Z3_get_arity(Context.nCtx, f) == 0)
if (Native.Z3_get_arity(ntvContext.nCtx, f) == 0)
{
IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f);
IntPtr n = Native.Z3_model_get_const_interp(ntvContext.nCtx, NativeObject, f);
if (sk == Z3_sort_kind.Z3_ARRAY_SORT)
{
@ -75,10 +75,10 @@ namespace Microsoft.Z3
return null;
else
{
if (Native.Z3_is_as_array(Context.nCtx, n) == 0)
if (Native.Z3_is_as_array(ntvContext.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, this, f, fd);
var fd = Native.Z3_get_as_array_func_decl(ntvContext.nCtx, n);
return new NativeFuncInterp(ntvContext, this, f, fd);
}
}
else
@ -88,11 +88,11 @@ namespace Microsoft.Z3
}
else
{
IntPtr n = Native.Z3_model_get_func_interp(Context.nCtx, NativeObject, f);
IntPtr n = Native.Z3_model_get_func_interp(ntvContext.nCtx, NativeObject, f);
if (n == IntPtr.Zero)
return null;
else
return new NativeFuncInterp(Context, this, f, n);
return new NativeFuncInterp(ntvContext, this, f, n);
}
}
@ -103,7 +103,7 @@ namespace Microsoft.Z3
/// </summary>
public uint NumConsts
{
get { return Native.Z3_model_get_num_consts(Context.nCtx, NativeObject); }
get { return Native.Z3_model_get_num_consts(ntvContext.nCtx, NativeObject); }
}
@ -118,7 +118,7 @@ namespace Microsoft.Z3
uint n = NumConsts;
Z3_func_decl[] res = new Z3_func_decl[n];
for (uint i = 0; i < n; i++)
res[i] = Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i);
res[i] = Native.Z3_model_get_const_decl(ntvContext.nCtx, NativeObject, i);
return res;
}
}
@ -134,24 +134,22 @@ namespace Microsoft.Z3
uint nc = NumConsts;
for (uint i = 0; i < nc; ++i)
{
var f = Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i);
IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f);
var f = Native.Z3_model_get_const_decl(ntvContext.nCtx, NativeObject, i);
IntPtr n = Native.Z3_model_get_const_interp(ntvContext.nCtx, NativeObject, f);
if (n == IntPtr.Zero) continue;
yield return new KeyValuePair<Z3_func_decl, Z3_ast>(f, n);
}
}
}
/// <summary>
/// The number of function interpretations in the model.
/// </summary>
public uint NumFuncs
{
get { return Native.Z3_model_get_num_funcs(Context.nCtx, NativeObject); }
get { return Native.Z3_model_get_num_funcs(ntvContext.nCtx, NativeObject); }
}
/// <summary>
/// The function declarations of the function interpretations in the model.
/// </summary>
@ -163,12 +161,11 @@ namespace Microsoft.Z3
uint n = NumFuncs;
Z3_func_decl[] res = new Z3_func_decl[n];
for (uint i = 0; i < n; i++)
res[i] = Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i);
res[i] = Native.Z3_model_get_func_decl(ntvContext.nCtx, NativeObject, i);
return res;
}
}
/// <summary>
/// All symbols that have an interpretation in the model.
/// </summary>
@ -182,9 +179,9 @@ namespace Microsoft.Z3
uint n = nFuncs + nConsts;
Z3_func_decl[] res = new Z3_func_decl[n];
for (uint i = 0; i < nConsts; i++)
res[i] = Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i);
res[i] = Native.Z3_model_get_const_decl(ntvContext.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(ntvContext.nCtx, NativeObject, i);
return res;
}
}
@ -200,7 +197,6 @@ namespace Microsoft.Z3
public ModelEvaluationFailedException() : base() { }
}
/// <summary>
/// Evaluates the expression <paramref name="t"/> in the current model.
/// </summary>
@ -219,7 +215,7 @@ namespace Microsoft.Z3
{
IntPtr v = IntPtr.Zero;
if (Native.Z3_model_eval(Context.nCtx, NativeObject, t, (byte)(completion ? 1 : 0), ref v) == (byte)0)
if (Native.Z3_model_eval(ntvContext.nCtx, NativeObject, t, (byte)(completion ? 1 : 0), ref v) == (byte)0)
throw new ModelEvaluationFailedException();
else
return v;
@ -236,7 +232,7 @@ namespace Microsoft.Z3
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(ntvContext.nCtx, r);
}
/// <summary>
@ -269,33 +265,28 @@ namespace Microsoft.Z3
{
var r = Eval(t, true);
// check that r is a sequence of store over a constant default array.
var updates = new List<KeyValuePair<Z3_ast, Z3_ast>>();
var updates = new Dictionary<Z3_ast, Z3_ast>();
result = null;
while (true)
{
if (Context.GetAstKind(r) != Z3_ast_kind.Z3_APP_AST)
if (ntvContext.GetAstKind(r) != Z3_ast_kind.Z3_APP_AST)
return false;
Z3_func_decl f = Context.GetAppDecl(r);
var kind = Context.GetDeclKind(f);
Z3_func_decl f = ntvContext.GetAppDecl(r);
var kind = ntvContext.GetDeclKind(f);
if (kind == Z3_decl_kind.Z3_OP_CONST_ARRAY)
{
#if false
// TODO
result = new ArrayValue();
result.Else = r;
result.Updates = updates.ToArray();
result.Domain = updates.Select((x, y) => x).ToArray();
result.Range = updates.Select((x, y) => y).ToArray();
#endif
result.Domain = updates.Keys.ToArray();
result.Range = updates.Values.ToArray();
return true;
}
else if (kind == Z3_decl_kind.Z3_OP_STORE)
{
#if false
Debug.Assert(Context.NumArgs(r) == 3);
updates.Add(new KeyValuePair(Context.GetArg(r, 1), Context.GetArg(r, 2)));
r = Context.GetArg(r, 0);
#endif
Debug.Assert(ntvContext.GetNumArgs(r) == 3);
updates[ntvContext.GetAppArg(r, 1)] = ntvContext.GetAppArg(r, 2);
r = ntvContext.GetAppArg(r, 0);
}
else
{
@ -308,7 +299,7 @@ namespace Microsoft.Z3
/// <summary>
/// The number of uninterpreted sorts that the model has an interpretation for.
/// </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(ntvContext.nCtx, NativeObject); } }
/// <summary>
@ -328,7 +319,7 @@ namespace Microsoft.Z3
uint n = NumSorts;
Z3_sort[] res = new Z3_sort[n];
for (uint i = 0; i < n; i++)
res[i] = Native.Z3_model_get_sort(Context.nCtx, NativeObject, i);
res[i] = Native.Z3_model_get_sort(ntvContext.nCtx, NativeObject, i);
return res;
}
}
@ -340,16 +331,16 @@ namespace Microsoft.Z3
/// <returns>A string representation of the model.</returns>
public override string ToString()
{
return Native.Z3_model_to_string(Context.nCtx, NativeObject);
return Native.Z3_model_to_string(ntvContext.nCtx, NativeObject);
}
IntPtr NativeObject;
NativeContext Context;
NativeContext ntvContext;
internal NativeModel(NativeContext ctx, IntPtr obj)
{
Context = ctx;
ntvContext = ctx;
NativeObject = obj;
Debug.Assert(ctx != null);
Native.Z3_model_inc_ref(ctx.nCtx, obj);
@ -371,7 +362,7 @@ namespace Microsoft.Z3
{
if (NativeObject != IntPtr.Zero)
{
Native.Z3_model_dec_ref(Context.nCtx, NativeObject);
Native.Z3_model_dec_ref(ntvContext.nCtx, NativeObject);
NativeObject = IntPtr.Zero;
}
GC.SuppressFinalize(this);

2
src/api/dotnet/NativeSolver.cs
View file

@ -19,9 +19,9 @@ Notes:
--*/
using System;
using System.Diagnostics;
using System.Collections.Generic;
using System.Linq;
using System.Diagnostics;
namespace Microsoft.Z3
{