mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

add basic example of using optimizaiton context to Java as raised in issue #179

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-07-30 11:32:14 -03:00
parent 0e886cfe5e
commit a0894ac7bf
2 changed files with 34 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

27
examples/java/JavaExample.java
View file

@ -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<String, String> cfg = new HashMap<String, String>();
cfg.put("model", "true");
Context ctx = new Context(cfg);
p.optimizeExample(ctx);
p.basicTests(ctx);
p.castingTest(ctx);
p.sudokuExample(ctx);