diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index 4a579f9da..e27bab3bf 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -2254,7 +2254,30 @@ class JavaExample System.out.println("OK, model: " + s.getModel().toString()); } - + + public void optimizeExample(Context ctx) + { + System.out.println("Opt"); + + Optimize opt = ctx.mkOptimize(); + + // Set constraints. + IntExpr xExp = ctx.mkIntConst("x"); + IntExpr yExp = ctx.mkIntConst("y"); + + opt.Add(ctx.mkEq(ctx.mkAdd(xExp, yExp), ctx.mkInt(10)), + ctx.mkGe(xExp, ctx.mkInt(0)), + ctx.mkGe(yExp, ctx.mkInt(0))); + + // Set objectives. + Optimize.Handle mx = opt.MkMaximize(xExp); + Optimize.Handle my = opt.MkMaximize(yExp); + + System.out.println(opt.Check()); + System.out.println(mx); + System.out.println(my); + } + public static void main(String[] args) { JavaExample p = new JavaExample(); @@ -2274,6 +2297,8 @@ class JavaExample HashMap cfg = new HashMap(); cfg.put("model", "true"); Context ctx = new Context(cfg); + + p.optimizeExample(ctx); p.basicTests(ctx); p.castingTest(ctx); p.sudokuExample(ctx); diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java index 6c90a56c2..d80aa124d 100644 --- a/src/api/java/Optimize.java +++ b/src/api/java/Optimize.java @@ -109,6 +109,14 @@ public class Optimize extends Z3Object { return getLower(); } + + /** + * Print a string representation of the handle. + **/ + public String toString() + { + return getValue().toString(); + } } /**