mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-12 09:03:26 +00:00
Code Activity

make .NET and Java bindings for optimization use Expr instead of ArithExpr to accomodate bit-vector optimization

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-13 08:51:16 -08:00
parent 7c63a5cc1d
commit dbb35b951c
2 changed files with 33 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/api/dotnet/Optimize.cs
View file

@ -124,7 +124,7 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// Retrieve a lower bound for the objective handle. /// Retrieve a lower bound for the objective handle.
/// </summary> /// </summary>
public ArithExpr Lower public Expr Lower
{ {
get { return opt.GetLower(handle); } get { return opt.GetLower(handle); }
} }
@ -132,7 +132,7 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// Retrieve an upper bound for the objective handle. /// Retrieve an upper bound for the objective handle.
/// </summary> /// </summary>
public ArithExpr Upper public Expr Upper
{ {
get { return opt.GetUpper(handle); } get { return opt.GetUpper(handle); }
} }
@ -140,7 +140,7 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// Retrieve the value of an objective. /// Retrieve the value of an objective.
/// </summary> /// </summary>
public ArithExpr Value public Expr Value
{ {
get { return Lower; } get { return Lower; }
} }
@ -148,7 +148,7 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// Retrieve a lower bound for the objective handle. /// Retrieve a lower bound for the objective handle.
/// </summary> /// </summary>
public ArithExpr[] LowerAsVector public Expr[] LowerAsVector
{ {
get { return opt.GetLowerAsVector(handle); } get { return opt.GetLowerAsVector(handle); }
} }
@ -156,7 +156,7 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// Retrieve an upper bound for the objective handle. /// Retrieve an upper bound for the objective handle.
/// </summary> /// </summary>
public ArithExpr[] UpperAsVector public Expr[] UpperAsVector
{ {
get { return opt.GetUpperAsVector(handle); } get { return opt.GetUpperAsVector(handle); }
} }
@ -240,8 +240,9 @@ namespace Microsoft.Z3
/// Declare an arithmetical maximization objective. /// Declare an arithmetical maximization objective.
/// Return a handle to the objective. The handle is used as /// Return a handle to the objective. The handle is used as
/// to retrieve the values of objectives after calling Check. /// to retrieve the values of objectives after calling Check.
/// The expression can be either an arithmetical expression or bit-vector.
/// </summary> /// </summary>
public Handle MkMaximize(ArithExpr e) public Handle MkMaximize(Expr e)
{ {
return new Handle(this, Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject)); return new Handle(this, Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject));
} }
@ -250,45 +251,46 @@ namespace Microsoft.Z3
/// Declare an arithmetical minimization objective. /// Declare an arithmetical minimization objective.
/// Similar to MkMaximize. /// Similar to MkMaximize.
/// </summary> /// </summary>
public Handle MkMinimize(ArithExpr e) public Handle MkMinimize(Expr e)
{ {
return new Handle(this, Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject)); return new Handle(this, Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject));
} }
/// <summary> /// <summary>
/// Retrieve a lower bound for the objective handle. /// Retrieve a lower bound for the objective handle.
/// </summary> /// </summary>
private ArithExpr GetLower(uint index) private Expr GetLower(uint index)
{ {
return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index)); return Expr.Create(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index));
} }
/// <summary> /// <summary>
/// Retrieve an upper bound for the objective handle. /// Retrieve an upper bound for the objective handle.
/// </summary> /// </summary>
private ArithExpr GetUpper(uint index) private Expr GetUpper(uint index)
{ {
return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index)); return Expr.Create(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index));
} }
/// <summary> /// <summary>
/// Retrieve a lower bound for the objective handle. /// Retrieve a lower bound for the objective handle.
/// </summary> /// </summary>
private ArithExpr[] GetLowerAsVector(uint index) private Expr[] GetLowerAsVector(uint index)
{ {
ASTVector v = new ASTVector(Context, Native.Z3_optimize_get_lower_as_vector(Context.nCtx, NativeObject, index)); ASTVector v = new ASTVector(Context, Native.Z3_optimize_get_lower_as_vector(Context.nCtx, NativeObject, index));
return v.ToArithExprArray(); return v.ToExprArray();
} }
/// <summary> /// <summary>
/// Retrieve an upper bound for the objective handle. /// Retrieve an upper bound for the objective handle.
/// </summary> /// </summary>
private ArithExpr[] GetUpperAsVector(uint index) private Expr[] GetUpperAsVector(uint index)
{ {
ASTVector v = new ASTVector(Context, Native.Z3_optimize_get_upper_as_vector(Context.nCtx, NativeObject, index)); ASTVector v = new ASTVector(Context, Native.Z3_optimize_get_upper_as_vector(Context.nCtx, NativeObject, index));
return v.ToArithExprArray(); return v.ToExprArray();
} }
/// <summary> /// <summary>

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

@ -89,7 +89,7 @@ public class Optimize extends Z3Object {
/** /**
* Retrieve a lower bound for the objective handle. * Retrieve a lower bound for the objective handle.
**/ **/
public ArithExpr getLower() public Expr getLower()
{ {
return opt.GetLower(handle); return opt.GetLower(handle);
} }
@ -97,7 +97,7 @@ public class Optimize extends Z3Object {
/** /**
* Retrieve an upper bound for the objective handle. * Retrieve an upper bound for the objective handle.
**/ **/
public ArithExpr getUpper() public Expr getUpper()
{ {
return opt.GetUpper(handle); return opt.GetUpper(handle);
} }
@ -110,7 +110,7 @@ public class Optimize extends Z3Object {
* and otherwise is represented by the expression {@code value + eps * EPSILON}, * and otherwise is represented by the expression {@code value + eps * EPSILON},
* where {@code EPSILON} is an arbitrarily small real number. * where {@code EPSILON} is an arbitrarily small real number.
*/ */
public ArithExpr[] getUpperAsVector() public Expr[] getUpperAsVector()
{ {
return opt.GetUpperAsVector(handle); return opt.GetUpperAsVector(handle);
} }
@ -120,7 +120,7 @@ public class Optimize extends Z3Object {
* *
* <p>See {@link #getUpperAsVector()} for triple semantics. * <p>See {@link #getUpperAsVector()} for triple semantics.
*/ */
public ArithExpr[] getLowerAsVector() public Expr[] getLowerAsVector()
{ {
return opt.GetLowerAsVector(handle); return opt.GetLowerAsVector(handle);
} }
@ -128,7 +128,7 @@ public class Optimize extends Z3Object {
/** /**
* Retrieve the value of an objective. * Retrieve the value of an objective.
**/ **/
public ArithExpr getValue() public Expr getValue()
{ {
return getLower(); return getLower();
} }
@ -214,7 +214,7 @@ public class Optimize extends Z3Object {
* Return a handle to the objective. The handle is used as * Return a handle to the objective. The handle is used as
* to retrieve the values of objectives after calling Check. * to retrieve the values of objectives after calling Check.
**/ **/
public Handle MkMaximize(ArithExpr e) public Handle MkMaximize(Expr e)
{ {
return new Handle(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject())); return new Handle(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
} }
@ -223,7 +223,7 @@ public class Optimize extends Z3Object {
* Declare an arithmetical minimization objective. * Declare an arithmetical minimization objective.
* Similar to MkMaximize. * Similar to MkMaximize.
**/ **/
public Handle MkMinimize(ArithExpr e) public Handle MkMinimize(Expr e)
{ {
return new Handle(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject())); return new Handle(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
} }
@ -231,17 +231,17 @@ public class Optimize extends Z3Object {
/** /**
* Retrieve a lower bound for the objective handle. * Retrieve a lower bound for the objective handle.
**/ **/
private ArithExpr GetLower(int index) private Expr GetLower(int index)
{ {
return (ArithExpr)Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index)); return Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
} }
/** /**
* Retrieve an upper bound for the objective handle. * Retrieve an upper bound for the objective handle.
**/ **/
private ArithExpr GetUpper(int index) private Expr GetUpper(int index)
{ {
return (ArithExpr)Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index)); return Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
} }
/** /**
@ -249,7 +249,7 @@ public class Optimize extends Z3Object {
* *
* <p>See {@link Handle#getUpperAsVector}. * <p>See {@link Handle#getUpperAsVector}.
*/ */
private ArithExpr[] GetUpperAsVector(int index) { private Expr[] GetUpperAsVector(int index) {
return unpackObjectiveValueVector( return unpackObjectiveValueVector(
Native.optimizeGetUpperAsVector( Native.optimizeGetUpperAsVector(
getContext().nCtx(), getNativeObject(), index getContext().nCtx(), getNativeObject(), index
@ -262,7 +262,7 @@ public class Optimize extends Z3Object {
* *
* <p>See {@link Handle#getLowerAsVector}. * <p>See {@link Handle#getLowerAsVector}.
*/ */
private ArithExpr[] GetLowerAsVector(int index) { private Expr[] GetLowerAsVector(int index) {
return unpackObjectiveValueVector( return unpackObjectiveValueVector(
Native.optimizeGetLowerAsVector( Native.optimizeGetLowerAsVector(
getContext().nCtx(), getNativeObject(), index getContext().nCtx(), getNativeObject(), index
@ -270,12 +270,12 @@ public class Optimize extends Z3Object {
); );
} }
private ArithExpr[] unpackObjectiveValueVector(long nativeVec) { private Expr[] unpackObjectiveValueVector(long nativeVec) {
ASTVector vec = new ASTVector( ASTVector vec = new ASTVector(
getContext(), nativeVec getContext(), nativeVec
); );
return new ArithExpr[] { return new Expr[] {
(ArithExpr) vec.get(0), (ArithExpr) vec.get(1), (ArithExpr) vec.get(2) (Expr) vec.get(0), (Expr) vec.get(1), (Expr) vec.get(2)
}; };
} }