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

Remove superfluouse indices to make .NET API thinner

Browse source
This commit is contained in:
Anh-Dung Phan 2013-12-10 17:15:51 -08:00
parent 34c96a8fe0
commit caba15d6b3
1 changed files with 6 additions and 39 deletions
Download patch file Download diff file Expand all files Collapse all files

45
src/api/dotnet/Optimize.cs
View file

@ -29,8 +29,6 @@ namespace Microsoft.Z3
[ContractVerification(true)] [ContractVerification(true)]
public class Optimize : Z3Object public class Optimize : Z3Object
{ {
HashSet<uint> indices;
/// <summary> /// <summary>
/// A string that describes all available optimize solver parameters. /// A string that describes all available optimize solver parameters.
/// </summary> /// </summary>
@ -64,27 +62,6 @@ namespace Microsoft.Z3
get { return new ParamDescrs(Context, Native.Z3_optimize_get_param_descrs(Context.nCtx, NativeObject)); } get { return new ParamDescrs(Context, Native.Z3_optimize_get_param_descrs(Context.nCtx, NativeObject)); }
} }
/// <summary>
/// Get the number of objectives.
/// </summary>
public uint ObjectiveCount
{
get { return (uint)indices.Count; }
}
/// <summary>
/// Get all indices of objectives.
/// </summary>
public uint[] Objectives
{
get
{
var objectives = new uint[indices.Count];
indices.CopyTo(objectives, 0);
return objectives;
}
}
/// <summary> /// <summary>
/// Assert a constraint (or multiple) into the optimize solver. /// Assert a constraint (or multiple) into the optimize solver.
/// </summary> /// </summary>
@ -118,9 +95,7 @@ namespace Microsoft.Z3
{ {
Context.CheckContextMatch(constraint); Context.CheckContextMatch(constraint);
Symbol s = Context.MkSymbol(group); Symbol s = Context.MkSymbol(group);
uint index = Native.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject); return Native.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject);
indices.Add(index);
return index;
} }
public Status Check() { public Status Check() {
@ -157,31 +132,25 @@ namespace Microsoft.Z3
public uint MkMaximize(ArithExpr e) public uint MkMaximize(ArithExpr e)
{ {
uint index = Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject); return Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject);
indices.Add(index);
return index;
} }
public uint MkMinimize(ArithExpr e) public uint MkMinimize(ArithExpr e)
{ {
uint index = Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject); return Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject);
indices.Add(index);
return index;
} }
public ArithExpr GetLower(uint index) public ArithExpr GetLower(uint index)
{ {
Contract.Requires(indices.Contains(index)); return new ArithExpr(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index));
return new ArithExpr(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index));
} }
public ArithExpr GetUpper(uint index) public ArithExpr GetUpper(uint index)
{ {
Contract.Requires(indices.Contains(index)); return new ArithExpr(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index));
return new ArithExpr(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index));
} }
public override string ToString() public override string ToString()
{ {
return Native.Z3_optimize_to_string(Context.nCtx, NativeObject); return Native.Z3_optimize_to_string(Context.nCtx, NativeObject);
} }
@ -191,13 +160,11 @@ namespace Microsoft.Z3
: base(ctx, obj) : base(ctx, obj)
{ {
Contract.Requires(ctx != null); Contract.Requires(ctx != null);
indices = new HashSet<uint>();
} }
internal Optimize(Context ctx) internal Optimize(Context ctx)
: base(ctx, Native.Z3_mk_optimize(ctx.nCtx)) : base(ctx, Native.Z3_mk_optimize(ctx.nCtx))
{ {
Contract.Requires(ctx != null); Contract.Requires(ctx != null);
indices = new HashSet<uint>();
} }
internal class DecRefQueue : IDecRefQueue internal class DecRefQueue : IDecRefQueue