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