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

stub out array serialization

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-03-03 11:38:23 -08:00
parent cd324a4734
commit e1e8d15827
2 changed files with 38 additions and 33 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -232,11 +232,10 @@ namespace Microsoft.Z3
/// </summary>
/// <param name="v">A string representing the Term value in decimal notation.</param>
/// <returns>A Term with value <paramref name="v"/> and sort Real</returns>
public Z3_ast MkReal(string v, Z3_sort realSort)
public Z3_ast MkReal(string v)
{
Debug.Assert(!string.IsNullOrEmpty(v));
return Native.Z3_mk_numeral(nCtx, v, realSort);
return Native.Z3_mk_numeral(nCtx, v, MkRealSort());
}
/// <summary>
@ -378,11 +377,7 @@ namespace Microsoft.Z3
/// <summary>
/// Creates a Boolean value.
/// </summary>
public Z3_ast MkBool(bool value)
{
return value ? MkTrue() : MkFalse();
}
public Z3_ast MkBool(bool value) => value ? MkTrue() : MkFalse();
/// <summary>
/// Create an expression representing <c>t1 iff t2</c>.
@ -1166,7 +1161,7 @@ namespace Microsoft.Z3
Debug.Assert(v != IntPtr.Zero);
int result = i = 0;
if (Native.Z3_get_numeral_int(nCtx, v, ref result) == 0) ;
if (Native.Z3_get_numeral_int(nCtx, v, ref result) == 0)
{
return false;
}
@ -1197,8 +1192,7 @@ namespace Microsoft.Z3
/// Try to get long from AST
/// </summary>
/// <param name="v"></param>
/// <param name=""></param>
/// <param name=""></param>
/// <param name="i"></param>
/// <returns></returns>
public bool TryGetNumeralInt64(Z3_ast v, out long i)
{

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

@ -263,35 +263,46 @@ namespace Microsoft.Z3
/// Convert the interpretation of t into a sequence of array updates
/// </summary>
/// <param name="t"></param>
/// <param name="result"></param>
/// <returns>null if the argument does evaluate to a sequence of stores to an array</returns>
public bool TryGetArrayValue(Z3_ast t, out ArrayValue result)
{
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>>();
//while (true)
//{
// // check that r is an app, and the decl-kind is Z3_OP_ARRAY_CONST or Z3_OP_ARRAY_STORE
// // if it is Z3_OP_ARRAY_CONST then set result.Else and break;
// // if it is ARRAY_STORE, then append to 'updates' and continue
// // in other cases return null
// return false;
//}
if (updates.Any())
{
result = new ArrayValue()
{
Updates = updates.ToArray()
};
return true;
}
result = null;
return false;
while (true)
{
if (Context.GetAstKind(r) != Z3_ast_kind.Z3_APP_AST)
return false;
Z3_func_decl f = Context.GetAppDecl(r);
var kind = Context.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
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
}
else
{
return false;
}
}
return true;
}
/// <summary>