Z3
Optimize.cs
Go to the documentation of this file.
1/*++
2Copyright (c) 2012 Microsoft Corporation
3
4Module Name:
5
6 Optimize.cs
7
8Abstract:
9
10 Z3 Managed API: Optimizes
11
12Author:
13
14 Nikolaj Bjorner (nbjorner) 2013-12-03
15
16Notes:
17
18--*/
19
20using System;
21using System.Collections.Generic;
22using System.Diagnostics;
23using System.Linq;
24
25namespace Microsoft.Z3
26{
30 public class Optimize : Z3Object
31 {
35 public string Help
36 {
37 get
38 {
39 return Native.Z3_optimize_get_help(Context.nCtx, NativeObject);
40 }
41 }
42
47 {
48 set
49 {
50 Debug.Assert(value != null);
51 Context.CheckContextMatch(value);
52 Native.Z3_optimize_set_params(Context.nCtx, NativeObject, value.NativeObject);
53 }
54 }
55
59 public void Set(string name, bool value) { Parameters = Context.MkParams().Add(name, value); }
63 public void Set(string name, uint value) { Parameters = Context.MkParams().Add(name, value); }
67 public void Set(string name, double value) { Parameters = Context.MkParams().Add(name, value); }
71 public void Set(string name, string value) { Parameters = Context.MkParams().Add(name, value); }
75 public void Set(string name, Symbol value) { Parameters = Context.MkParams().Add(name, value); }
79 public void Set(Symbol name, bool value) { Parameters = Context.MkParams().Add(name, value); }
83 public void Set(Symbol name, uint value) { Parameters = Context.MkParams().Add(name, value); }
87 public void Set(Symbol name, double value) { Parameters = Context.MkParams().Add(name, value); }
91 public void Set(Symbol name, string value) { Parameters = Context.MkParams().Add(name, value); }
95 public void Set(Symbol name, Symbol value) { Parameters = Context.MkParams().Add(name, value); }
96
101 {
102 get { return new ParamDescrs(Context, Native.Z3_optimize_get_param_descrs(Context.nCtx, NativeObject)); }
103 }
104
108 public void Assert(params BoolExpr[] constraints)
109 {
110 AddConstraints(constraints);
111 }
112
116 public void Assert(IEnumerable<BoolExpr> constraints)
117 {
118 AddConstraints(constraints);
119 }
120
124 public void Add(params BoolExpr[] constraints)
125 {
126 AddConstraints(constraints);
127 }
128
132 public void Add(IEnumerable<BoolExpr> constraints)
133 {
134 AddConstraints(constraints);
135 }
136
140 private void AddConstraints(IEnumerable<BoolExpr> constraints)
141 {
142 Debug.Assert(constraints != null);
143 Debug.Assert(constraints.All(c => c != null));
144
145 Context.CheckContextMatch(constraints);
146 foreach (BoolExpr a in constraints)
147 {
148 Native.Z3_optimize_assert(Context.nCtx, NativeObject, a.NativeObject);
149 }
150 }
154 public class Handle
155 {
156 Optimize opt;
157 uint handle;
158 internal Handle(Optimize opt, uint h)
159 {
160 this.opt = opt;
161 this.handle = h;
162 }
163
167 public Expr Lower
168 {
169 get { return opt.GetLower(handle); }
170 }
171
175 public Expr Upper
176 {
177 get { return opt.GetUpper(handle); }
178 }
179
183 public Expr Value
184 {
185 get { return Lower; }
186 }
187
192 {
193 get { return opt.GetLowerAsVector(handle); }
194 }
195
200 {
201 get { return opt.GetUpperAsVector(handle); }
202 }
203
204 }
205
212 public Handle AssertSoft(BoolExpr constraint, uint weight, string group)
213 {
214 Context.CheckContextMatch(constraint);
215 Symbol s = Context.MkSymbol(group);
216 return new Handle(this, Native.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject));
217 }
218
219
226 public Status Check(params Expr[] assumptions)
227 {
228 Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject, (uint)assumptions.Length, AST.ArrayToNative(assumptions));
229 switch (r)
230 {
231 case Z3_lbool.Z3_L_TRUE:
232 return Status.SATISFIABLE;
233 case Z3_lbool.Z3_L_FALSE:
234 return Status.UNSATISFIABLE;
235 default:
236 return Status.UNKNOWN;
237 }
238 }
239
244 public void Push()
245 {
246 Native.Z3_optimize_push(Context.nCtx, NativeObject);
247 }
248
254 public void Pop()
255 {
256 Native.Z3_optimize_pop(Context.nCtx, NativeObject);
257 }
258
259
268 {
269 get
270 {
271 IntPtr x = Native.Z3_optimize_get_model(Context.nCtx, NativeObject);
272 if (x == IntPtr.Zero)
273 return null;
274 else
275 return new Model(Context, x);
276 }
277 }
278
288 {
289 get
290 {
291
292 ASTVector core = new ASTVector(Context, Native.Z3_optimize_get_unsat_core(Context.nCtx, NativeObject));
293 return core.ToBoolExprArray();
294 }
295 }
296
304 {
305 return new Handle(this, Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject));
306 }
307
313 {
314 return new Handle(this, Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject));
315 }
316
317
321 private Expr GetLower(uint index)
322 {
323 return Expr.Create(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index));
324 }
325
326
330 private Expr GetUpper(uint index)
331 {
332 return Expr.Create(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index));
333 }
334
338 private Expr[] GetLowerAsVector(uint index)
339 {
340 ASTVector v = new ASTVector(Context, Native.Z3_optimize_get_lower_as_vector(Context.nCtx, NativeObject, index));
341 return v.ToExprArray();
342 }
343
344
348 private Expr[] GetUpperAsVector(uint index)
349 {
350 ASTVector v = new ASTVector(Context, Native.Z3_optimize_get_upper_as_vector(Context.nCtx, NativeObject, index));
351 return v.ToExprArray();
352 }
353
358 {
359 get
360 {
361 return Native.Z3_optimize_get_reason_unknown(Context.nCtx, NativeObject);
362 }
363 }
364
365
369 public override string ToString()
370 {
371 return Native.Z3_optimize_to_string(Context.nCtx, NativeObject);
372 }
373
378 public void FromFile(string file)
379 {
380 Native.Z3_optimize_from_file(Context.nCtx, NativeObject, file);
381 }
382
386 public void FromString(string s)
387 {
388 Native.Z3_optimize_from_string(Context.nCtx, NativeObject, s);
389 }
390
395 {
396 get
397 {
398
399 ASTVector assertions = new ASTVector(Context, Native.Z3_optimize_get_assertions(Context.nCtx, NativeObject));
400 return assertions.ToBoolExprArray();
401 }
402 }
403
408 {
409 get
410 {
411
412 ASTVector objectives = new ASTVector(Context, Native.Z3_optimize_get_objectives(Context.nCtx, NativeObject));
413 return objectives.ToExprArray();
414 }
415 }
416
417
422 {
423 get
424 {
425
426 return new Statistics(Context, Native.Z3_optimize_get_statistics(Context.nCtx, NativeObject));
427 }
428 }
429
430
431 #region Internal
432 internal Optimize(Context ctx, IntPtr obj)
433 : base(ctx, obj)
434 {
435 Debug.Assert(ctx != null);
436 }
437 internal Optimize(Context ctx)
438 : base(ctx, Native.Z3_mk_optimize(ctx.nCtx))
439 {
440 Debug.Assert(ctx != null);
441 }
442
443 internal class DecRefQueue : IDecRefQueue
444 {
445 public DecRefQueue() : base() { }
446 public DecRefQueue(uint move_limit) : base(move_limit) { }
447 internal override void IncRef(Context ctx, IntPtr obj)
448 {
449 Native.Z3_optimize_inc_ref(ctx.nCtx, obj);
450 }
451
452 internal override void DecRef(Context ctx, IntPtr obj)
453 {
454 Native.Z3_optimize_dec_ref(ctx.nCtx, obj);
455 }
456 };
457
458 internal override void IncRef(IntPtr o)
459 {
460 Context.Optimize_DRQ.IncAndClear(Context, o);
461 base.IncRef(o);
462 }
463
464 internal override void DecRef(IntPtr o)
465 {
466 Context.Optimize_DRQ.Add(o);
467 base.DecRef(o);
468 }
469 #endregion
470 }
471}
The abstract syntax tree (AST) class.
Definition: AST.cs:31
Vectors of ASTs.
Definition: ASTVector.cs:29
BoolExpr[] ToBoolExprArray()
Translates an ASTVector into a BoolExpr[]
Definition: ASTVector.cs:127
Expr[] ToExprArray()
Translates an ASTVector into an Expr[]
Definition: ASTVector.cs:115
Boolean expressions
Definition: BoolExpr.cs:32
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
IDecRefQueue Optimize_DRQ
Optimize DRQ
Definition: Context.cs:4800
Params MkParams()
Creates a new ParameterSet.
Definition: Context.cs:3290
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:90
Expressions are terms.
Definition: Expr.cs:31
A Model contains interpretations (assignments) of constants and functions.
Definition: Model.cs:30
Handle to objectives returned by objective functions.
Definition: Optimize.cs:155
Expr[] UpperAsVector
Retrieve an upper bound for the objective handle.
Definition: Optimize.cs:200
Expr[] LowerAsVector
Retrieve a lower bound for the objective handle.
Definition: Optimize.cs:192
Expr Upper
Retrieve an upper bound for the objective handle.
Definition: Optimize.cs:176
Expr Value
Retrieve the value of an objective.
Definition: Optimize.cs:184
Expr Lower
Retrieve a lower bound for the objective handle.
Definition: Optimize.cs:168
Object for managing optimization context
Definition: Optimize.cs:31
void Set(string name, uint value)
Sets parameter on the optimize solver
Definition: Optimize.cs:63
BoolExpr[] Assertions
The set of asserted formulas.
Definition: Optimize.cs:395
void Set(string name, double value)
Sets parameter on the optimize solver
Definition: Optimize.cs:67
Model Model
The model of the last Check.
Definition: Optimize.cs:268
string Help
A string that describes all available optimize solver parameters.
Definition: Optimize.cs:36
void Set(string name, string value)
Sets parameter on the optimize solver
Definition: Optimize.cs:71
void Add(IEnumerable< BoolExpr > constraints)
Alias for Assert.
Definition: Optimize.cs:132
void Set(Symbol name, Symbol value)
Sets parameter on the optimize solver
Definition: Optimize.cs:95
void Push()
Creates a backtracking point.
Definition: Optimize.cs:244
Handle MkMaximize(Expr e)
Declare an arithmetical maximization objective. Return a handle to the objective. The handle is used ...
Definition: Optimize.cs:303
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the optimize solver.
Definition: Optimize.cs:108
void FromString(string s)
Similar to FromFile. Instead it takes as argument a string.
Definition: Optimize.cs:386
Params Parameters
Sets the optimize solver parameters.
Definition: Optimize.cs:47
Statistics Statistics
Optimize statistics.
Definition: Optimize.cs:422
void Pop()
Backtrack one backtracking point.
Definition: Optimize.cs:254
Handle MkMinimize(Expr e)
Declare an arithmetical minimization objective. Similar to MkMaximize.
Definition: Optimize.cs:312
void Set(Symbol name, string value)
Sets parameter on the optimize solver
Definition: Optimize.cs:91
ParamDescrs ParameterDescriptions
Retrieves parameter descriptions for Optimize solver.
Definition: Optimize.cs:101
Expr[] Objectives
The set of asserted formulas.
Definition: Optimize.cs:408
Status Check(params Expr[] assumptions)
Check satisfiability of asserted constraints. Produce a model that (when the objectives are bounded a...
Definition: Optimize.cs:226
BoolExpr[] UnsatCore
The unsat core of the last Check.
Definition: Optimize.cs:288
void Assert(IEnumerable< BoolExpr > constraints)
Assert a constraint (or multiple) into the optimize solver.
Definition: Optimize.cs:116
override string ToString()
Print the context to a string (SMT-LIB parseable benchmark).
Definition: Optimize.cs:369
void FromFile(string file)
Parse an SMT-LIB2 file with optimization objectives and constraints. The parsed constraints and objec...
Definition: Optimize.cs:378
void Set(string name, bool value)
Sets parameter on the optimize solver
Definition: Optimize.cs:59
void Set(Symbol name, double value)
Sets parameter on the optimize solver
Definition: Optimize.cs:87
void Set(Symbol name, bool value)
Sets parameter on the optimize solver
Definition: Optimize.cs:79
void Add(params BoolExpr[] constraints)
Alias for Assert.
Definition: Optimize.cs:124
Handle AssertSoft(BoolExpr constraint, uint weight, string group)
Assert soft constraint
Definition: Optimize.cs:212
void Set(string name, Symbol value)
Sets parameter on the optimize solver
Definition: Optimize.cs:75
void Set(Symbol name, uint value)
Sets parameter on the optimize solver
Definition: Optimize.cs:83
String ReasonUnknown
Return a string the describes why the last to check returned unknown
Definition: Optimize.cs:358
A ParamDescrs describes a set of parameters.
Definition: ParamDescrs.cs:29
A Params objects represents a configuration in the form of Symbol/value pairs.
Definition: Params.cs:29
Params Add(Symbol name, bool value)
Adds a parameter setting.
Definition: Params.cs:33
Objects of this class track statistical information about solvers.
Definition: Statistics.cs:30
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33
Status
Status values.
Definition: Status.cs:29
def String(name, ctx=None)
Definition: z3py.py:10693
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:102
Z3_optimize Z3_API Z3_mk_optimize(Z3_context c)
Create a new optimize context.