Z3
Optimize.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  Optimize.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Optimizes
11 
12 Author:
13 
14  Nikolaj Bjorner (nbjorner) 2013-12-03
15 
16 Notes:
17 
18 --*/
19 
20 using System;
21 using System.Collections.Generic;
22 using System.Diagnostics.Contracts;
23 
24 namespace Microsoft.Z3
25 {
29  [ContractVerification(true)]
30  public class Optimize : Z3Object
31  {
35  public string Help
36  {
37  get
38  {
39  Contract.Ensures(Contract.Result<string>() != null);
40  return Native.Z3_optimize_get_help(Context.nCtx, NativeObject);
41  }
42  }
43 
47  public Params Parameters
48  {
49  set
50  {
51  Contract.Requires(value != null);
52  Context.CheckContextMatch(value);
53  Native.Z3_optimize_set_params(Context.nCtx, NativeObject, value.NativeObject);
54  }
55  }
56 
60  public ParamDescrs ParameterDescriptions
61  {
62  get { return new ParamDescrs(Context, Native.Z3_optimize_get_param_descrs(Context.nCtx, NativeObject)); }
63  }
64 
68  public void Assert(params BoolExpr[] constraints)
69  {
70  Contract.Requires(constraints != null);
71  Contract.Requires(Contract.ForAll(constraints, c => c != null));
72 
73  Context.CheckContextMatch(constraints);
74  foreach (BoolExpr a in constraints)
75  {
76  Native.Z3_optimize_assert(Context.nCtx, NativeObject, a.NativeObject);
77  }
78  }
79 
83  public void Add(params BoolExpr[] constraints)
84  {
85  Assert(constraints);
86  }
87 
91  public class Handle
92  {
93  Optimize opt;
94  uint handle;
95  internal Handle(Optimize opt, uint h)
96  {
97  this.opt = opt;
98  this.handle = h;
99  }
100 
104  public ArithExpr Lower
105  {
106  get { return opt.GetLower(handle); }
107  }
108 
112  public ArithExpr Upper
113  {
114  get { return opt.GetUpper(handle); }
115  }
116 
120  public ArithExpr Value
121  {
122  get { return Lower; }
123  }
124  }
125 
132  public Handle AssertSoft(BoolExpr constraint, uint weight, string group)
133  {
134  Context.CheckContextMatch(constraint);
135  Symbol s = Context.MkSymbol(group);
136  return new Handle(this, Native.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject));
137  }
138 
139 
146  public Status Check()
147  {
148  Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject);
149  switch (r)
150  {
151  case Z3_lbool.Z3_L_TRUE:
152  return Status.SATISFIABLE;
153  case Z3_lbool.Z3_L_FALSE:
154  return Status.UNSATISFIABLE;
155  default:
156  return Status.UNKNOWN;
157  }
158  }
159 
164  public void Push()
165  {
166  Native.Z3_optimize_push(Context.nCtx, NativeObject);
167  }
168 
174  public void Pop()
175  {
176  Native.Z3_optimize_pop(Context.nCtx, NativeObject);
177  }
178 
179 
187  public Model Model
188  {
189  get
190  {
191  IntPtr x = Native.Z3_optimize_get_model(Context.nCtx, NativeObject);
192  if (x == IntPtr.Zero)
193  return null;
194  else
195  return new Model(Context, x);
196  }
197  }
198 
205  {
206  return new Handle(this, Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject));
207  }
208 
214  {
215  return new Handle(this, Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject));
216  }
217 
221  private ArithExpr GetLower(uint index)
222  {
223  return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index));
224  }
225 
226 
230  private ArithExpr GetUpper(uint index)
231  {
232  return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index));
233  }
234 
238  public String getReasonUnknown()
239  {
240  Contract.Ensures(Contract.Result<string>() != null);
241  return Native.Z3_optimize_get_reason_unknown(Context.nCtx, NativeObject);
242  }
243 
244 
248  public override string ToString()
249  {
250  return Native.Z3_optimize_to_string(Context.nCtx, NativeObject);
251  }
252 
256  public Statistics Statistics
257  {
258  get
259  {
260  Contract.Ensures(Contract.Result<Statistics>() != null);
261 
262  return new Statistics(Context, Native.Z3_optimize_get_statistics(Context.nCtx, NativeObject));
263  }
264  }
265 
266 
267  #region Internal
268  internal Optimize(Context ctx, IntPtr obj)
269  : base(ctx, obj)
270  {
271  Contract.Requires(ctx != null);
272  }
273  internal Optimize(Context ctx)
274  : base(ctx, Native.Z3_mk_optimize(ctx.nCtx))
275  {
276  Contract.Requires(ctx != null);
277  }
278 
279  internal class DecRefQueue : IDecRefQueue
280  {
281  public DecRefQueue() : base() { }
282  public DecRefQueue(uint move_limit) : base(move_limit) { }
283  internal override void IncRef(Context ctx, IntPtr obj)
284  {
285  Native.Z3_optimize_inc_ref(ctx.nCtx, obj);
286  }
287 
288  internal override void DecRef(Context ctx, IntPtr obj)
289  {
290  Native.Z3_optimize_dec_ref(ctx.nCtx, obj);
291  }
292  };
293 
294  internal override void IncRef(IntPtr o)
295  {
296  Context.Optimize_DRQ.IncAndClear(Context, o);
297  base.IncRef(o);
298  }
299 
300  internal override void DecRef(IntPtr o)
301  {
302  Context.Optimize_DRQ.Add(o);
303  base.DecRef(o);
304  }
305  #endregion
306  }
307 }
override string ToString()
Print the context to a string (SMT-LIB parseable benchmark).
Definition: Optimize.cs:248
Object for managing optimizization context
Definition: Optimize.cs:30
using System
static void Z3_optimize_pop(Z3_context a0, Z3_optimize a1)
Definition: Native.cs:4595
IDecRefQueue Optimize_DRQ
Optimize DRQ
Definition: Context.cs:4539
static Z3_optimize Z3_mk_optimize(Z3_context a0)
Definition: Native.cs:4535
void Push()
Creates a backtracking point.
Definition: Optimize.cs:164
static Z3_ast Z3_optimize_get_lower(Z3_context a0, Z3_optimize a1, uint a2)
Definition: Native.cs:4641
Boolean expressions
Definition: BoolExpr.cs:31
Objects of this class track statistical information about solvers.
Definition: Statistics.cs:29
Handle MkMinimize(ArithExpr e)
Declare an arithmetical minimization objective. Similar to MkMaximize.
Definition: Optimize.cs:213
Handle MkMaximize(ArithExpr e)
Declare an arithmetical maximization objective. Return a handle to the objective. The handle is used ...
Definition: Optimize.cs:204
void Pop()
Backtrack one backtracking point.
Definition: Optimize.cs:174
String getReasonUnknown()
Return a string the describes why the last to check returned unknown
Definition: Optimize.cs:238
static void Z3_optimize_push(Z3_context a0, Z3_optimize a1)
Definition: Native.cs:4588
Handle to objectives returned by objective functions.
Definition: Optimize.cs:91
Expressions are terms.
Definition: Expr.cs:29
static string Z3_optimize_to_string(Z3_context a0, Z3_optimize a1)
Definition: Native.cs:4657
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the optimize solver.
Definition: Optimize.cs:68
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:143
static uint Z3_optimize_assert_soft(Z3_context a0, Z3_optimize a1, Z3_ast a2, string a3, IntPtr a4)
Definition: Native.cs:4564
static void Z3_optimize_inc_ref(Z3_context a0, Z3_optimize a1)
Definition: Native.cs:4543
Status
Status values.
Definition: Status.cs:27
static Z3_model Z3_optimize_get_model(Z3_context a0, Z3_optimize a1)
Definition: Native.cs:4618
Handle AssertSoft(BoolExpr constraint, uint weight, string group)
Assert soft constraint
Definition: Optimize.cs:132
A Params objects represents a configuration in the form of Symbol/value pairs.
Definition: Params.cs:29
A ParamDescrs describes a set of parameters.
Definition: ParamDescrs.cs:29
DecRefQueue interface
Definition: IDecRefQueue.cs:32
static Z3_stats Z3_optimize_get_statistics(Z3_context a0, Z3_optimize a1)
Definition: Native.cs:4673
A Model contains interpretations (assignments) of constants and functions.
Definition: Model.cs:29
static uint Z3_optimize_maximize(Z3_context a0, Z3_optimize a1, Z3_ast a2)
Definition: Native.cs:4572
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:84
static void Z3_optimize_dec_ref(Z3_context a0, Z3_optimize a1)
Definition: Native.cs:4550
static string Z3_optimize_get_reason_unknown(Z3_context a0, Z3_optimize a1)
Definition: Native.cs:4610
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
Status Check()
Check satisfiability of asserted constraints. Produce a model that (when the objectives are bounded a...
Definition: Optimize.cs:146
Z3_lbool
Z3_lbool
Definition: Enumerations.cs:10
Arithmetic expressions (int/real)
Definition: ArithExpr.cs:31
static void Z3_optimize_set_params(Z3_context a0, Z3_optimize a1, Z3_params a2)
Definition: Native.cs:4626
static Z3_param_descrs Z3_optimize_get_param_descrs(Z3_context a0, Z3_optimize a1)
Definition: Native.cs:4633
void Add(params BoolExpr[] constraints)
Alias for Assert.
Definition: Optimize.cs:83
static string Z3_optimize_get_help(Z3_context a0, Z3_optimize a1)
Definition: Native.cs:4665
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:31
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
static void Z3_optimize_assert(Z3_context a0, Z3_optimize a1, Z3_ast a2)
Definition: Native.cs:4557
static Z3_ast Z3_optimize_get_upper(Z3_context a0, Z3_optimize a1, uint a2)
Definition: Native.cs:4649
static int Z3_optimize_check(Z3_context a0, Z3_optimize a1)
Definition: Native.cs:4602
static uint Z3_optimize_minimize(Z3_context a0, Z3_optimize a1, Z3_ast a2)
Definition: Native.cs:4580