mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

Sane indentation + removing extra spaces for Optimize.java

Browse source
This commit is contained in:
George Karpenkov 2017-02-27 18:48:44 +01:00
parent d6c79facc7
commit b3be83e7c5
1 changed files with 79 additions and 86 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

165
src/api/java/Optimize.java
View file

@ -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.
*
* <p>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.
*
* <p>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.
**/