From b3be83e7c59f499c6aa9ea53ed62d22f8eb3c138 Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Mon, 27 Feb 2017 18:48:44 +0100 Subject: [PATCH] Sane indentation + removing extra spaces for Optimize.java --- src/api/java/Optimize.java | 165 ++++++++++++++++++------------------- 1 file changed, 79 insertions(+), 86 deletions(-) diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java index c474a34dd..abc13b570 100644 --- a/src/api/java/Optimize.java +++ b/src/api/java/Optimize.java @@ -14,7 +14,6 @@ Author: Nikolaj Bjorner (nbjorner) 2015-07-16 Notes: - **/ package com.microsoft.z3; @@ -23,10 +22,10 @@ import com.microsoft.z3.enumerations.Z3_lbool; /** - * Object for managing optimizization context + * Object for managing optimization context **/ -public class Optimize extends Z3Object -{ +public class Optimize extends Z3Object { + /** * A string that describes all available optimize solver parameters. **/ @@ -55,7 +54,7 @@ public class Optimize extends Z3Object /** * Assert a constraint (or multiple) into the optimize solver. - **/ + **/ public void Assert(BoolExpr ... constraints) { getContext().checkContextMatch(constraints); @@ -67,103 +66,101 @@ public class Optimize extends Z3Object /** * Alias for Assert. - **/ + **/ public void Add(BoolExpr ... constraints) { - Assert(constraints); + Assert(constraints); } - + /** * Handle to objectives returned by objective functions. **/ - public class Handle - { - Optimize opt; - int handle; - Handle(Optimize opt, int h) - { - this.opt = opt; - this.handle = h; - } - - /** - * Retrieve a lower bound for the objective handle. - **/ - public ArithExpr getLower() - { - return opt.GetLower(handle); - } - - /** - * Retrieve an upper bound for the objective handle. - **/ - public ArithExpr getUpper() - { - return opt.GetUpper(handle); - } + public class Handle { - /** - * @return a triple representing the upper bound of the objective handle. - * - * The triple contains values {@code inf, value, eps}, - * where the objective value is unbounded iff {@code inf} is non-zero, - * and otherwise is represented by the expression {@code value + eps * EPSILON}, - * where {@code EPSILON} is an arbitrarily small real number. - */ - public ArithExpr[] getUpperAsVector() - { - return opt.GetUpperAsVector(handle); - } + private final Optimize opt; + private final int handle; - /** - * @return a triple representing the upper bound of the objective handle. - * - *

See {@link #getUpperAsVector()} for triple semantics. - */ - public ArithExpr[] getLowerAsVector() - { - return opt.GetLowerAsVector(handle); - } + Handle(Optimize opt, int h) + { + this.opt = opt; + this.handle = h; + } - /** - * Retrieve the value of an objective. - **/ - public ArithExpr getValue() - { - return getLower(); - } + /** + * Retrieve a lower bound for the objective handle. + **/ + public ArithExpr getLower() + { + return opt.GetLower(handle); + } - /** - * Print a string representation of the handle. - **/ - @Override - public String toString() + /** + * Retrieve an upper bound for the objective handle. + **/ + public ArithExpr getUpper() + { + return opt.GetUpper(handle); + } + + /** + * @return a triple representing the upper bound of the objective handle. + * + * The triple contains values {@code inf, value, eps}, + * where the objective value is unbounded iff {@code inf} is non-zero, + * and otherwise is represented by the expression {@code value + eps * EPSILON}, + * where {@code EPSILON} is an arbitrarily small real number. + */ + public ArithExpr[] getUpperAsVector() + { + return opt.GetUpperAsVector(handle); + } + + /** + * @return a triple representing the upper bound of the objective handle. + * + *

See {@link #getUpperAsVector()} for triple semantics. + */ + public ArithExpr[] getLowerAsVector() + { + return opt.GetLowerAsVector(handle); + } + + /** + * Retrieve the value of an objective. + **/ + public ArithExpr getValue() + { + return getLower(); + } + + /** + * Print a string representation of the handle. + **/ + @Override + public String toString() { return getValue().toString(); } } - /** + /** * Assert soft constraint * * Return an objective which associates with the group of constraints. * - **/ - + **/ public Handle AssertSoft(BoolExpr constraint, int weight, String group) { getContext().checkContextMatch(constraint); Symbol s = getContext().mkSymbol(group); return new Handle(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject())); } - - /** + /** * Check satisfiability of asserted constraints. * Produce a model that (when the objectives are bounded and * don't use strict inequalities) meets the objectives. **/ - public Status Check() { Z3_lbool r = Z3_lbool.fromInt(Native.optimizeCheck(getContext().nCtx(), getNativeObject())); @@ -176,7 +173,7 @@ public class Optimize extends Z3Object return Status.UNKNOWN; } } - + /** * Creates a backtracking point. **/ @@ -185,13 +182,11 @@ public class Optimize extends Z3Object Native.optimizePush(getContext().nCtx(), getNativeObject()); } - - /** + /** * Backtrack one backtracking point. * * Note that an exception is thrown if Pop is called without a corresponding Push. **/ - public void Pop() { Native.optimizePop(getContext().nCtx(), getNativeObject()); @@ -214,7 +209,7 @@ public class Optimize extends Z3Object } } - /** + /** * Declare an arithmetical maximization objective. * Return a handle to the objective. The handle is used as * to retrieve the values of objectives after calling Check. @@ -223,11 +218,11 @@ public class Optimize extends Z3Object { return new Handle(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject())); } - + /** * Declare an arithmetical minimization objective. * Similar to MkMaximize. - **/ + **/ public Handle MkMinimize(ArithExpr e) { return new Handle(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject())); @@ -235,16 +230,15 @@ public class Optimize extends Z3Object /** * Retrieve a lower bound for the objective handle. - **/ + **/ private ArithExpr GetLower(int index) { return (ArithExpr)Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index)); } - - + /** * Retrieve an upper bound for the objective handle. - **/ + **/ private ArithExpr GetUpper(int index) { return (ArithExpr)Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index)); @@ -294,8 +288,7 @@ public class Optimize extends Z3Object return Native.optimizeGetReasonUnknown(getContext().nCtx(), getNativeObject()); } - - + /** * Print the context to a String (SMT-LIB parseable benchmark). **/ @@ -304,7 +297,7 @@ public class Optimize extends Z3Object { return Native.optimizeToString(getContext().nCtx(), getNativeObject()); } - + /** * Optimize statistics. **/