public static void solve1()

in src/main/java/workspace/HelloZ3.java [12:38]

• 20 lines of code
• 2 McCabe index (conditional complexity)

    public static void solve1() {
        //application example of z3
        //reference https://qiita.com/quentin-maisonneuve/items/4f32cf52293dc44ffc3d

        System.out.println("(a || b) && c");
        Context context = new Context(new HashMap<>());
        BoolExpr a = context.mkBoolConst("a");
        BoolExpr b = context.mkBoolConst("b");
        BoolExpr c = context.mkBoolConst("c");
        BoolExpr formula = context.mkAnd(context.mkOr(a, b), c); // (a || b) && c

        Solver solver = context.mkSolver();
        solver.add(formula);

        if(solver.check() == Status.SATISFIABLE) {
            Model model = solver.getModel();
            Expr resultVa = model.eval(a, false);
            Expr resultVb = model.eval(b, false);
            Expr resultVc = model.eval(c, false);

            System.out.println("a:"+resultVa);   // Result is true
            System.out.println("b:"+resultVb);   // Result is false
            System.out.println("c:"+resultVc);   // Result is true
        }

        context.close();
    }