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;
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  AddConstraints(constraints);
71  }
72 
76  public void Assert(IEnumerable<BoolExpr> constraints)
77  {
78  AddConstraints(constraints);
79  }
80 
84  public void Add(params BoolExpr[] constraints)
85  {
86  AddConstraints(constraints);
87  }
88 
92  public void Add(IEnumerable<BoolExpr> constraints)
93  {
94  AddConstraints(constraints);
95  }
96 
100  private void AddConstraints(IEnumerable<BoolExpr> constraints)
101  {
102  Contract.Requires(constraints != null);
103  Contract.Requires(Contract.ForAll(constraints, c => c != null));
104 
105  Context.CheckContextMatch(constraints);
106  foreach (BoolExpr a in constraints)
107  {
108  Native.Z3_optimize_assert(Context.nCtx, NativeObject, a.NativeObject);
109  }
110  }
114  public class Handle
115  {
116  Optimize opt;
117  uint handle;
118  internal Handle(Optimize opt, uint h)
119  {
120  this.opt = opt;
121  this.handle = h;
122  }
123 
127  public ArithExpr Lower
128  {
129  get { return opt.GetLower(handle); }
130  }
131 
135  public ArithExpr Upper
136  {
137  get { return opt.GetUpper(handle); }
138  }
139 
143  public ArithExpr Value
144  {
145  get { return Lower; }
146  }
147  }
148 
155  public Handle AssertSoft(BoolExpr constraint, uint weight, string group)
156  {
157  Context.CheckContextMatch(constraint);
158  Symbol s = Context.MkSymbol(group);
159  return new Handle(this, Native.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject));
160  }
161 
162 
169  public Status Check()
170  {
171  Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject);
172  switch (r)
173  {
174  case Z3_lbool.Z3_L_TRUE:
175  return Status.SATISFIABLE;
176  case Z3_lbool.Z3_L_FALSE:
177  return Status.UNSATISFIABLE;
178  default:
179  return Status.UNKNOWN;
180  }
181  }
182 
187  public void Push()
188  {
189  Native.Z3_optimize_push(Context.nCtx, NativeObject);
190  }
191 
197  public void Pop()
198  {
199  Native.Z3_optimize_pop(Context.nCtx, NativeObject);
200  }
201 
202 
210  public Model Model
211  {
212  get
213  {
214  IntPtr x = Native.Z3_optimize_get_model(Context.nCtx, NativeObject);
215  if (x == IntPtr.Zero)
216  return null;
217  else
218  return new Model(Context, x);
219  }
220  }
221 
228  {
229  return new Handle(this, Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject));
230  }
231 
237  {
238  return new Handle(this, Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject));
239  }
240 
244  private ArithExpr GetLower(uint index)
245  {
246  return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index));
247  }
248 
249 
253  private ArithExpr GetUpper(uint index)
254  {
255  return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index));
256  }
257 
261  public String ReasonUnknown
262  {
263  get
264  {
265  Contract.Ensures(Contract.Result<string>() != null);
266  return Native.Z3_optimize_get_reason_unknown(Context.nCtx, NativeObject);
267  }
268  }
269 
270 
274  public override string ToString()
275  {
276  return Native.Z3_optimize_to_string(Context.nCtx, NativeObject);
277  }
278 
283  public void FromFile(string file)
284  {
285  Native.Z3_optimize_from_file(Context.nCtx, NativeObject, file);
286  }
287 
291  public void FromString(string s)
292  {
293  Native.Z3_optimize_from_string(Context.nCtx, NativeObject, s);
294  }
295 
299  public BoolExpr[] Assertions
300  {
301  get
302  {
303  Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
304 
305  ASTVector assertions = new ASTVector(Context, Native.Z3_optimize_get_assertions(Context.nCtx, NativeObject));
306  return assertions.ToBoolExprArray();
307  }
308  }
309 
313  public Expr[] Objectives
314  {
315  get
316  {
317  Contract.Ensures(Contract.Result<Expr[]>() != null);
318 
319  ASTVector objectives = new ASTVector(Context, Native.Z3_optimize_get_objectives(Context.nCtx, NativeObject));
320  return objectives.ToExprArray();
321  }
322  }
323 
324 
328  public Statistics Statistics
329  {
330  get
331  {
332  Contract.Ensures(Contract.Result<Statistics>() != null);
333 
334  return new Statistics(Context, Native.Z3_optimize_get_statistics(Context.nCtx, NativeObject));
335  }
336  }
337 
338 
339  #region Internal
340  internal Optimize(Context ctx, IntPtr obj)
341  : base(ctx, obj)
342  {
343  Contract.Requires(ctx != null);
344  }
345  internal Optimize(Context ctx)
346  : base(ctx, Native.Z3_mk_optimize(ctx.nCtx))
347  {
348  Contract.Requires(ctx != null);
349  }
350 
351  internal class DecRefQueue : IDecRefQueue
352  {
353  public DecRefQueue() : base() { }
354  public DecRefQueue(uint move_limit) : base(move_limit) { }
355  internal override void IncRef(Context ctx, IntPtr obj)
356  {
357  Native.Z3_optimize_inc_ref(ctx.nCtx, obj);
358  }
359 
360  internal override void DecRef(Context ctx, IntPtr obj)
361  {
362  Native.Z3_optimize_dec_ref(ctx.nCtx, obj);
363  }
364  };
365 
366  internal override void IncRef(IntPtr o)
367  {
368  Context.Optimize_DRQ.IncAndClear(Context, o);
369  base.IncRef(o);
370  }
371 
372  internal override void DecRef(IntPtr o)
373  {
374  Context.Optimize_DRQ.Add(o);
375  base.DecRef(o);
376  }
377  #endregion
378  }
379 }
override string ToString()
Print the context to a string (SMT-LIB parseable benchmark).
Definition: Optimize.cs:274
Object for managing optimizization context
Definition: Optimize.cs:30
IDecRefQueue Optimize_DRQ
Optimize DRQ
Definition: Context.cs:4958
void Push()
Creates a backtracking point.
Definition: Optimize.cs:187
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:236
Handle MkMaximize(ArithExpr e)
Declare an arithmetical maximization objective. Return a handle to the objective. The handle is used ...
Definition: Optimize.cs:227
void Pop()
Backtrack one backtracking point.
Definition: Optimize.cs:197
void Assert(IEnumerable< BoolExpr > constraints)
Assert a constraint (or multiple) into the optimize solver.
Definition: Optimize.cs:76
Vectors of ASTs.
Definition: ASTVector.cs:28
void Add(IEnumerable< BoolExpr > constraints)
Alias for Assert.
Definition: Optimize.cs:92
Handle to objectives returned by objective functions.
Definition: Optimize.cs:114
Expressions are terms.
Definition: Expr.cs:29
void FromFile(string file)
Parse an SMT-LIB2 file with optimization objectives and constraints. The parsed constraints and objec...
Definition: Optimize.cs:283
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:105
Status
Status values.
Definition: Status.cs:27
BoolExpr [] ToBoolExprArray()
Translates an ASTVector into a BoolExpr[]
Definition: ASTVector.cs:129
Handle AssertSoft(BoolExpr constraint, uint weight, string group)
Assert soft constraint
Definition: Optimize.cs:155
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
A Model contains interpretations (assignments) of constants and functions.
Definition: Model.cs:29
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:91
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Status Check()
Check satisfiability of asserted constraints. Produce a model that (when the objectives are bounded a...
Definition: Optimize.cs:169
Arithmetic expressions (int/real)
Definition: ArithExpr.cs:31
Expr [] ToExprArray()
Translates an ASTVector into an Expr[]
Definition: ASTVector.cs:117
void Add(params BoolExpr[] constraints)
Alias for Assert.
Definition: Optimize.cs:84
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
def String(name, ctx=None)
Definition: z3py.py:9443
void FromString(string s)
Similar to FromFile. Instead it takes as argument a string.
Definition: Optimize.cs:291