mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

add pb constraints to API

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-11-13 17:15:41 -08:00
parent d1937b2032
commit 2d3f6ca71d
1 changed files with 30 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -2249,6 +2249,36 @@ namespace Microsoft.Z3
}
#endregion
#region Pseudo-Boolean constraints
/// <summary>
/// Create an at-most-k constraint.
/// </summary>
public BoolExpr MkAtMost(BoolExpr[] args, uint k)
{
Contract.Requires(args != null);
Contract.Requires(Contract.Result<BoolExpr[]>() != null);
CheckContextMatch(args);
return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint) args.Length,
AST.ArrayToNative(args), k));
}
/// <summary>
/// Create a pseudo-Boolean <= constraint.
/// </summary>
public BoolExpr MkPBLe(int[] coeffs, BoolExpr[] args, int k)
{
Contract.Requires(args != null);
Contract.Requires(coeffs != null);
Contract.Requires(args.Length == coeffs.Length);
Contract.Requires(Contract.Result<BoolExpr[]>() != null);
CheckContextMatch(args);
return new BoolExpr(this, Native.Z3_mk_pble(nCtx, (uint) args.Length,
AST.ArrayToNative(args),
coeffs, k));
}
#endregion
#region Numerals
#region General Numerals