mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 12:23:38 +00:00
Code Activity

Clean up build warnings (#5884)

Browse source 
* Clean up warnings in compile for documentation notes

* remove snk from local build

Co-authored-by: jfleisher <jofleish@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
John Fleisher 2022-03-07 15:55:30 -05:00 • committed by GitHub
parent e3568d5b47
commit 97c7ce63b5
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 13 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -308,25 +308,25 @@ namespace Microsoft.Z3
/// Integer Sort /// Integer Sort
/// </summary> /// </summary>
public Z3_sort IntSort => Native.Z3_mk_int_sort(nCtx); public Z3_sort IntSort => Native.Z3_mk_int_sort(nCtx);
/// <summary> /// <summary>
/// Boolean Sort /// Returns the "singleton" BoolSort for this NativeContext
/// </summary> /// </summary>
public Z3_sort BoolSort => Native.Z3_mk_bool_sort(nCtx); public Z3_sort BoolSort => Native.Z3_mk_bool_sort(nCtx);
/// <summary> /// <summary>
/// Real Sort /// Returns the "singleton" RealSort for this NativeContext
/// </summary> /// </summary>
public Z3_sort RealSort => Native.Z3_mk_real_sort(nCtx); public Z3_sort RealSort => Native.Z3_mk_real_sort(nCtx);
/// <summary> /// <summary>
/// Bit-vector sort /// Returns the BvSort for size in this NativeContext
/// </summary> /// </summary>
/// <param name="size"></param>
/// <returns></returns>
public Z3_sort MkBvSort(uint size) => Native.Z3_mk_bv_sort(nCtx, size); public Z3_sort MkBvSort(uint size) => Native.Z3_mk_bv_sort(nCtx, size);
/// <summary> /// <summary>
/// Given an elemSort create a List of elemSort /// returns ListSort
/// The function returns the list sort, constructors, accessors and recognizers
/// </summary> /// </summary>
/// <param name="name"></param> /// <param name="name"></param>
/// <param name="elemSort"></param> /// <param name="elemSort"></param>
@ -436,7 +436,7 @@ namespace Microsoft.Z3
#region Symbol #region Symbol
/// <summary> /// <summary>
/// Create a symbol from a string /// Return a ptr to symbol for string
/// </summary> /// </summary>
/// <param name="name"></param> /// <param name="name"></param>
/// <returns></returns> /// <returns></returns>
@ -809,6 +809,7 @@ namespace Microsoft.Z3
} }
/// <summary> /// <summary>
/// Same as MkForAll but defaults to "forall" = false
/// Create an existential Quantifier. /// Create an existential Quantifier.
/// </summary> /// </summary>
/// <param name="sorts"></param> /// <param name="sorts"></param>
@ -1142,7 +1143,7 @@ namespace Microsoft.Z3
} }
/// <summary> /// <summary>
/// Retrieve number of arguments to a function application /// Return number of arguments for app
/// </summary> /// </summary>
/// <param name="app"></param> /// <param name="app"></param>
/// <returns></returns> /// <returns></returns>

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

@ -251,12 +251,14 @@ namespace Microsoft.Z3
public Z3_ast Else; public Z3_ast Else;
/// <summary> /// <summary>
/// Domain for array
/// Updates.Keys /// Updates.Keys
/// </summary> /// </summary>
public Z3_ast[] Domain; public Z3_ast[] Domain;
/// <summary> /// <summary>
/// Updates.Range /// Range for array
/// Updates.Values
/// </summary> /// </summary>
public Z3_ast[] Range; public Z3_ast[] Range;
} }