// // An example, refering findModelExample2
import java.util.*;
import com.microsoft.z3.*;
public class Z3Application extends Object
{
	// コンストラクタ
	public Z3Application(){ test(); }
	// 目的の処理のメソッド
	public void test()
	{
		// コンテキストの生成、パラメータ設定
		HashMap<String, String> cfg = new HashMap<String, String>();
		cfg.put("model", "true");
		cfg.put("proof", "true");
		cfg.put("auto-config", "false");
		Context ctx = new Context(cfg);
		// 変数、式の表現生成
		IntExpr x = ctx.mkIntConst("x");
		IntExpr y = ctx.mkIntConst("y");
		IntExpr one = ctx.mkInt(1);
		IntExpr two = ctx.mkInt(2);
		IntExpr ten = ctx.mkInt(10);
		ArithExpr y_plus_one = ctx.mkAdd(y, one);
		BoolExpr c1 = ctx.mkLt(x, y_plus_one);
		BoolExpr c2 = ctx.mkGt(x, two);
		BoolExpr q = ctx.mkAnd(c1, c2);
		// ソルバオブジェクトの生成と論理式登録、チェックとモデル取得
		Solver s = ctx.mkSolver();
		s.add(c1,c2,q);
		System.out.println("modle for: x<y+1, x>2");
		Status st = s.check();
		if(st==Status.SATISFIABLE){
			Model model = s.getModel();
			System.out.println("x=" + model.evaluate(x,false) + ", y=" + model.evaluate(y,false));
		}else{
			System.out.println("st:" + st);
			System.exit(0);
		}
	}
	// メインメソッド
	public static void main(String... args)
	{
		Z3Application app = new Z3Application();
	}
}