stub out nativesolver

Z3Prover · Mar 2, 2022 · bf14aeb · bf14aeb
1 parent bbadd17
commit bf14aeb
Show file tree

Hide file tree

Showing 3 changed files with 559 additions and 0 deletions.
diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt
@@ -88,6 +88,7 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE
     NativeContext.cs
     NativeFuncInterp.cs
     NativeModel.cs
+    NativeSolver.cs
     Optimize.cs
     ParamDescrs.cs
     Params.cs

diff --git a/src/api/dotnet/NativeContext.cs b/src/api/dotnet/NativeContext.cs
@@ -179,5 +179,23 @@ internal void InitContext()
 
         #endregion
 
+
+        /// <summary>
+        /// Utility to convert a vector object of ast to a .Net array
+        /// </summary>
+        /// <param name="vec"></param>
+        /// <returns></returns>
+        public Z3_ast[] ToArray(Z3_ast_vector vec)
+        {
+            Native.Z3_ast_vector_inc_ref(nCtx, vec);
+            var sz = Native.Z3_ast_vector_size(nCtx, vec);
+            var result = new Z3_ast[sz];
+            for (uint i = 0; i < sz; ++i)
+                result[i] = Native.Z3_ast_vector_get(nCtx, vec, i);
+            Native.Z3_ast_vector_dec_ref(nCtx, vec);
+            return result;
+
+        }
+
     }
 }