From e1e8d15827ecb727e38776d57b20ce7e7afd37ae Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 3 Mar 2022 11:38:23 -0800
Subject: [PATCH] stub out array serialization

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/dotnet/NativeContext.cs | 16 +++-------
 src/api/dotnet/NativeModel.cs   | 55 ++++++++++++++++++++-------------
 2 files changed, 38 insertions(+), 33 deletions(-)

diff --git a/src/api/dotnet/NativeContext.cs b/src/api/dotnet/NativeContext.cs
index 604d752b2..6961b39dd 100644
--- a/src/api/dotnet/NativeContext.cs
+++ b/src/api/dotnet/NativeContext.cs
@@ -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)
         {
diff --git a/src/api/dotnet/NativeModel.cs b/src/api/dotnet/NativeModel.cs
index a4a7f11be..6a8ff21cf 100644
--- a/src/api/dotnet/NativeModel.cs
+++ b/src/api/dotnet/NativeModel.cs
@@ -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>