[Context IuWFNg]
HashMap<String, String> cfg ݒ
Context ctx = new Context(cfg);

[̋Lq(BoolExpr ̐)]
IntExpr,RealExpr,ArrayExpr, ̐
BoolExpr ̌`ɐĖ萶

[\oAo^A[/]
Solver s = ctx.mkSolver();
s.add(BoolExpr...);
œKȂctx.mkOptimize(), Add(BoolExpr...), mkMaximize/mkMinimize(Expr)

Status st = s.check();
st == Status.SATISFIABLE ̏ꍇɃf擾\
Model m = s.getModel();
擾Integer/Double = m.evaluate(Expr,false)

[\oAo^A[Aؖ擾]
Solver s = ctx.mkSolver();
s.add(BoolExpr...);
unsat core ̐ǐՂ邽߂ɂs.assertAndTrack(BoolExpr, BoolExpr)
Status st = s.check();
st == Status.UNSATISFIABLE ̏ꍇɏؖ擾\
ؖ擾s.getProof()
UnsatCore 擾Expr[] s.getUnsatCore()