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

.NET API documentation fixes

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-04-09 11:24:42 +01:00
parent 2b492f04f6
commit a3b89a8af3
3 changed files with 15 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/api/dotnet/Context.cs
View file

@ -303,10 +303,10 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// Create a new finite domain sort. /// Create a new finite domain sort.
/// <param name="name">The name used to identify the sort</param>
/// <param size="size">The size of the sort</param>
/// <returns>The result is a sort</returns> /// <returns>The result is a sort</returns>
/// </summary> /// </summary>
/// <param name="name">The name used to identify the sort</param>
/// <param name="size">The size of the sort</param>
public FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size) public FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
{ {
Contract.Requires(name != null); Contract.Requires(name != null);
@ -318,12 +318,12 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// Create a new finite domain sort. /// Create a new finite domain sort.
/// <param name="name">The name used to identify the sort</param>
/// <param size="size">The size of the sort</param>
/// <returns>The result is a sort</returns> /// <returns>The result is a sort</returns>
/// Elements of the sort are created using <seealso cref="MkNumeral"/>, /// Elements of the sort are created using <seealso cref="MkNumeral(ulong, Sort)"/>,
/// and the elements range from 0 to <tt>size-1</tt>. /// and the elements range from 0 to <tt>size-1</tt>.
/// </summary> /// </summary>
/// <param name="name">The name used to identify the sort</param>
/// <param name="size">The size of the sort</param>
public FiniteDomainSort MkFiniteDomainSort(string name, ulong size) public FiniteDomainSort MkFiniteDomainSort(string name, ulong size)
{ {
Contract.Ensures(Contract.Result<FiniteDomainSort>() != null); Contract.Ensures(Contract.Result<FiniteDomainSort>() != null);

2
src/api/dotnet/Global.cs
View file

@ -43,7 +43,7 @@ namespace Microsoft.Z3
/// The parameter names are case-insensitive. The character '-' should be viewed as an "alias" for '_'. /// The parameter names are case-insensitive. The character '-' should be viewed as an "alias" for '_'.
/// Thus, the following parameter names are considered equivalent: "pp.decimal-precision" and "PP.DECIMAL_PRECISION". /// Thus, the following parameter names are considered equivalent: "pp.decimal-precision" and "PP.DECIMAL_PRECISION".
/// This function can be used to set parameters for a specific Z3 module. /// This function can be used to set parameters for a specific Z3 module.
/// This can be done by using <module-name>.<parameter-name>. /// This can be done by using [module-name].[parameter-name].
/// For example: /// For example:
/// Z3_global_param_set('pp.decimal', 'true') /// Z3_global_param_set('pp.decimal', 'true')
/// will set the parameter "decimal" in the module "pp" to true. /// will set the parameter "decimal" in the module "pp" to true.

6
src/api/dotnet/Solver.cs
View file

@ -132,7 +132,8 @@ namespace Microsoft.Z3
/// <remarks> /// <remarks>
/// This API is an alternative to <see cref="Check"/> with assumptions for extracting unsat cores. /// This API is an alternative to <see cref="Check"/> with assumptions for extracting unsat cores.
/// Both APIs can be used in the same solver. The unsat core will contain a combination /// Both APIs can be used in the same solver. The unsat core will contain a combination
/// of the Boolean variables provided using <see cref="AssertAndTrack"/> and the Boolean literals /// of the Boolean variables provided using <see cref="AssertAndTrack(BoolExpr[],BoolExpr[])"/>
/// and the Boolean literals
/// provided using <see cref="Check"/> with assumptions. /// provided using <see cref="Check"/> with assumptions.
/// </remarks> /// </remarks>
public void AssertAndTrack(BoolExpr[] constraints, BoolExpr[] ps) public void AssertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
@ -156,7 +157,8 @@ namespace Microsoft.Z3
/// <remarks> /// <remarks>
/// This API is an alternative to <see cref="Check"/> with assumptions for extracting unsat cores. /// This API is an alternative to <see cref="Check"/> with assumptions for extracting unsat cores.
/// Both APIs can be used in the same solver. The unsat core will contain a combination /// Both APIs can be used in the same solver. The unsat core will contain a combination
/// of the Boolean variables provided using <see cref="AssertAndTrack"/> and the Boolean literals /// of the Boolean variables provided using <see cref="AssertAndTrack(BoolExpr[],BoolExpr[])"/>
/// and the Boolean literals
/// provided using <see cref="Check"/> with assumptions. /// provided using <see cref="Check"/> with assumptions.
/// </remarks> /// </remarks>
public void AssertAndTrack(BoolExpr constraint, BoolExpr p) public void AssertAndTrack(BoolExpr constraint, BoolExpr p)