mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
using directives
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
35fb95648b
commit
8d1276fa60
|
@ -1,3 +1,29 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
NativeContext.cs
|
||||
|
||||
Abstract:
|
||||
|
||||
Z3 Managed API: Native Context
|
||||
|
||||
Author:
|
||||
|
||||
Christoph Wintersteiger (cwinter) 2012-03-22
|
||||
Nikolaj Bjorner (nbjorner) 2022-03-01
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
|
||||
using System;
|
||||
using System.Collections.Generic;
|
||||
using System.Diagnostics;
|
||||
using System.Linq;
|
||||
using System.Runtime.InteropServices;
|
||||
|
||||
namespace Microsoft.Z3
|
||||
{
|
||||
using Z3_app = System.IntPtr;
|
||||
|
|
|
@ -19,6 +19,11 @@ Notes:
|
|||
|
||||
--*/
|
||||
|
||||
using System;
|
||||
using System.Collections.Generic;
|
||||
using System.Linq;
|
||||
using System.Diagnostics;
|
||||
|
||||
namespace Microsoft.Z3
|
||||
{
|
||||
using Z3_ast = System.IntPtr;
|
||||
|
@ -36,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) => ConstInterp(Native.Z3_get_app_decl(Context.nCtx, a));
|
||||
public Z3_ast ConstInterp(Z3_ast a) => ConstFuncInterp(Native.Z3_get_app_decl(Context.nCtx, a));
|
||||
|
||||
/// <summary>
|
||||
/// Retrieves the interpretation (the assignment) of <paramref name="f"/> in the model.
|
||||
|
|
|
@ -18,6 +18,11 @@ Notes:
|
|||
|
||||
--*/
|
||||
|
||||
using System;
|
||||
using System.Collections.Generic;
|
||||
using System.Linq;
|
||||
using System.Diagnostics;
|
||||
|
||||
namespace Microsoft.Z3
|
||||
{
|
||||
|
||||
|
|
Loading…
Reference in a new issue