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;
23 using System.Linq;
24 
25 namespace Microsoft.Z3
26 {
27     /// <summary>
28     /// Object for managing optimization context
29     /// </summary>
30     public class Optimize : Z3Object
31     {
32         /// <summary>
33         /// A string that describes all available optimize solver parameters.
34         /// </summary>
35         public string Help
36         {
37             get
38             {
39                 return Native.Z3_optimize_get_help(Context.nCtx, NativeObject);
40             }
41         }
42 
43         /// <summary>
44         /// Sets the optimize solver parameters.
45         /// </summary>
46         public Params Parameters
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 
56 	/// <summary>
57 	/// Sets parameter on the optimize solver
58 	/// </summary>
Set(string name, bool value)59 	public void Set(string name, bool value) { Parameters = Context.MkParams().Add(name, value); }
60 	/// <summary>
61 	/// Sets parameter on the optimize solver
62 	/// </summary>
Set(string name, uint value)63 	public void Set(string name, uint value) { Parameters = Context.MkParams().Add(name, value); }
64 	/// <summary>
65 	/// Sets parameter on the optimize solver
66 	/// </summary>
Set(string name, double value)67 	public void Set(string name, double value) { Parameters = Context.MkParams().Add(name, value); }
68 	/// <summary>
69 	/// Sets parameter on the optimize solver
70 	/// </summary>
Set(string name, string value)71 	public void Set(string name, string value) { Parameters = Context.MkParams().Add(name, value); }
72 	/// <summary>
73 	/// Sets parameter on the optimize solver
74 	/// </summary>
Set(string name, Symbol value)75 	public void Set(string name, Symbol value) { Parameters = Context.MkParams().Add(name, value); }
76 	/// <summary>
77 	/// Sets parameter on the optimize solver
78 	/// </summary>
Set(Symbol name, bool value)79 	public void Set(Symbol name, bool value) { Parameters = Context.MkParams().Add(name, value); }
80 	/// <summary>
81 	/// Sets parameter on the optimize solver
82 	/// </summary>
Set(Symbol name, uint value)83 	public void Set(Symbol name, uint value) { Parameters = Context.MkParams().Add(name, value); }
84 	/// <summary>
85 	/// Sets parameter on the optimize solver
86 	/// </summary>
Set(Symbol name, double value)87 	public void Set(Symbol name, double value) { Parameters = Context.MkParams().Add(name, value); }
88 	/// <summary>
89 	/// Sets parameter on the optimize solver
90 	/// </summary>
Set(Symbol name, string value)91 	public void Set(Symbol name, string value) { Parameters = Context.MkParams().Add(name, value); }
92 	/// <summary>
93 	/// Sets parameter on the optimize solver
94 	/// </summary>
Set(Symbol name, Symbol value)95 	public void Set(Symbol name, Symbol value) { Parameters = Context.MkParams().Add(name, value); }
96 
97         /// <summary>
98         /// Retrieves parameter descriptions for Optimize solver.
99         /// </summary>
100         public ParamDescrs ParameterDescriptions
101         {
102             get { return new ParamDescrs(Context, Native.Z3_optimize_get_param_descrs(Context.nCtx, NativeObject)); }
103         }
104 
105         /// <summary>
106         /// Assert a constraint (or multiple) into the optimize solver.
107         /// </summary>
Assert(params BoolExpr[] constraints)108         public void Assert(params BoolExpr[] constraints)
109         {
110             AddConstraints(constraints);
111         }
112 
113         /// <summary>
114         /// Assert a constraint (or multiple) into the optimize solver.
115         /// </summary>
Assert(IEnumerable<BoolExpr> constraints)116         public void Assert(IEnumerable<BoolExpr> constraints)
117         {
118             AddConstraints(constraints);
119         }
120 
121         /// <summary>
122         /// Alias for Assert.
123         /// </summary>
Add(params BoolExpr[] constraints)124         public void Add(params BoolExpr[] constraints)
125         {
126             AddConstraints(constraints);
127         }
128 
129         /// <summary>
130         /// Alias for Assert.
131         /// </summary>
Add(IEnumerable<BoolExpr> constraints)132         public void Add(IEnumerable<BoolExpr> constraints)
133         {
134             AddConstraints(constraints);
135         }
136 
137         /// <summary>
138         /// Assert a constraint (or multiple) into the optimize solver.
139         /// </summary>
AddConstraints(IEnumerable<BoolExpr> constraints)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         }
151         /// <summary>
152         /// Handle to objectives returned by objective functions.
153         /// </summary>
154         public class Handle
155         {
156             Optimize opt;
157             uint handle;
Handle(Optimize opt, uint h)158             internal Handle(Optimize opt, uint h)
159             {
160                 this.opt = opt;
161                 this.handle = h;
162             }
163 
164             /// <summary>
165             /// Retrieve a lower bound for the objective handle.
166             /// </summary>
167             public Expr Lower
168             {
169                 get { return opt.GetLower(handle); }
170             }
171 
172             /// <summary>
173             /// Retrieve an upper bound for the objective handle.
174             /// </summary>
175             public Expr Upper
176             {
177                 get { return opt.GetUpper(handle); }
178             }
179 
180             /// <summary>
181             /// Retrieve the value of an objective.
182             /// </summary>
183             public Expr Value
184             {
185                 get { return Lower; }
186             }
187 
188             /// <summary>
189             /// Retrieve a lower bound for the objective handle.
190             /// </summary>
191             public Expr[] LowerAsVector
192             {
193                 get { return opt.GetLowerAsVector(handle); }
194             }
195 
196             /// <summary>
197             /// Retrieve an upper bound for the objective handle.
198             /// </summary>
199             public Expr[] UpperAsVector
200             {
201                 get { return opt.GetUpperAsVector(handle); }
202             }
203 
204         }
205 
206         /// <summary>
207         /// Assert soft constraint
208         /// </summary>
209         /// <remarks>
210         /// Return an objective which associates with the group of constraints.
211         /// </remarks>
AssertSoft(BoolExpr constraint, uint weight, string group)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 
220         /// <summary>
221         /// Check satisfiability of asserted constraints.
222         /// Produce a model that (when the objectives are bounded and
223         /// don't use strict inequalities) meets the objectives.
224         /// </summary>
225         ///
Check(params Expr[] assumptions)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 
240         /// <summary>
241         /// Creates a backtracking point.
242         /// </summary>
243         /// <seealso cref="Pop"/>
Push()244         public void Push()
245         {
246             Native.Z3_optimize_push(Context.nCtx, NativeObject);
247         }
248 
249         /// <summary>
250         /// Backtrack one backtracking point.
251         /// </summary>
252         /// <remarks>Note that an exception is thrown if Pop is called without a corresponding <c>Push</c></remarks>
253         /// <seealso cref="Push"/>
Pop()254         public void Pop()
255         {
256             Native.Z3_optimize_pop(Context.nCtx, NativeObject);
257         }
258 
259 
260         /// <summary>
261         /// The model of the last <c>Check</c>.
262         /// </summary>
263         /// <remarks>
264         /// The result is <c>null</c> if <c>Check</c> was not invoked before,
265         /// if its results was not <c>SATISFIABLE</c>, or if model production is not enabled.
266         /// </remarks>
267         public Model Model
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 
279         /// <summary>
280         /// The unsat core of the last <c>Check</c>.
281         /// </summary>
282         /// <remarks>
283         /// The unsat core is a subset of <c>assumptions</c>
284         /// The result is empty if <c>Check</c> was not invoked before,
285         /// if its results was not <c>UNSATISFIABLE</c>, or if core production is disabled.
286         /// </remarks>
287         public BoolExpr[] UnsatCore
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 
297         /// <summary>
298         /// Declare an arithmetical maximization objective.
299         /// Return a handle to the objective. The handle is used as
300         /// to retrieve the values of objectives after calling Check.
301         /// The expression can be either an arithmetical expression or bit-vector.
302         /// </summary>
MkMaximize(Expr e)303         public Handle MkMaximize(Expr e)
304         {
305             return new Handle(this, Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject));
306         }
307 
308         /// <summary>
309         /// Declare an arithmetical minimization objective.
310         /// Similar to MkMaximize.
311         /// </summary>
MkMinimize(Expr e)312         public Handle MkMinimize(Expr e)
313         {
314             return new Handle(this, Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject));
315         }
316 
317 
318         /// <summary>
319         /// Retrieve a lower bound for the objective handle.
320         /// </summary>
GetLower(uint index)321         private Expr GetLower(uint index)
322         {
323             return Expr.Create(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index));
324         }
325 
326 
327         /// <summary>
328         /// Retrieve an upper bound for the objective handle.
329         /// </summary>
GetUpper(uint index)330         private Expr GetUpper(uint index)
331         {
332             return Expr.Create(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index));
333         }
334 
335         /// <summary>
336         /// Retrieve a lower bound for the objective handle.
337         /// </summary>
GetLowerAsVector(uint index)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 
345         /// <summary>
346         /// Retrieve an upper bound for the objective handle.
347         /// </summary>
GetUpperAsVector(uint index)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 
354     /// <summary>
355     /// Return a string the describes why the last to check returned unknown
356     /// </summary>
357         public String ReasonUnknown
358         {
359             get
360             {
361                 return Native.Z3_optimize_get_reason_unknown(Context.nCtx, NativeObject);
362             }
363         }
364 
365 
366         /// <summary>
367         /// Print the context to a string (SMT-LIB parseable benchmark).
368         /// </summary>
ToString()369         public override string ToString()
370         {
371             return Native.Z3_optimize_to_string(Context.nCtx, NativeObject);
372         }
373 
374         /// <summary>
375         /// Parse an SMT-LIB2 file with optimization objectives and constraints.
376         /// The parsed constraints and objectives are added to the optimization context.
377         /// </summary>
FromFile(string file)378         public void FromFile(string file)
379         {
380             Native.Z3_optimize_from_file(Context.nCtx, NativeObject, file);
381         }
382 
383         /// <summary>
384         /// Similar to FromFile. Instead it takes as argument a string.
385         /// </summary>
FromString(string s)386         public void FromString(string s)
387         {
388             Native.Z3_optimize_from_string(Context.nCtx, NativeObject, s);
389         }
390 
391         /// <summary>
392         /// The set of asserted formulas.
393         /// </summary>
394         public BoolExpr[] Assertions
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 
404         /// <summary>
405         /// The set of asserted formulas.
406         /// </summary>
407         public Expr[] Objectives
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 
418         /// <summary>
419         /// Optimize statistics.
420         /// </summary>
421         public Statistics Statistics
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
Optimize(Context ctx, IntPtr obj)432         internal Optimize(Context ctx, IntPtr obj)
433             : base(ctx, obj)
434         {
435             Debug.Assert(ctx != null);
436         }
Optimize(Context ctx)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         {
DecRefQueue()445             public DecRefQueue() : base() { }
DecRefQueue(uint move_limit)446             public DecRefQueue(uint move_limit) : base(move_limit) { }
IncRef(Context ctx, IntPtr obj)447             internal override void IncRef(Context ctx, IntPtr obj)
448             {
449                 Native.Z3_optimize_inc_ref(ctx.nCtx, obj);
450             }
451 
DecRef(Context ctx, IntPtr obj)452             internal override void DecRef(Context ctx, IntPtr obj)
453             {
454                 Native.Z3_optimize_dec_ref(ctx.nCtx, obj);
455             }
456         };
457 
IncRef(IntPtr o)458         internal override void IncRef(IntPtr o)
459         {
460             Context.Optimize_DRQ.IncAndClear(Context, o);
461             base.IncRef(o);
462         }
463 
DecRef(IntPtr o)464         internal override void DecRef(IntPtr o)
465         {
466             Context.Optimize_DRQ.Add(o);
467             base.DecRef(o);
468         }
469         #endregion
470     }
471 }
472