java - 如何解析 Z3/Java 中的量词表达式？

Question

在下面的示例中，我想解析表达式。请让我知道这样做的 Z3 方法。（在我的应用程序中，我得到了一个由 Z3 简化的表达式。）

import com.microsoft.z3.*;

public class Z3_test {

    public static void main(String[] args) {
        Context context = new Context();
        Expr quantified;
        {
            BoolExpr b1 = context.mkBoolConst("b1");
            BoolExpr b2 = context.mkBoolConst("b2");
            BoolExpr body = context.mkIff(b1, b2);
            quantified = context.mkQuantifier(
                    true,
                    new Expr[]{b1},
                    body,
                    0,
                    null,
                    null,
                    null,
                    null);
        }
        System.out.println(quantified);
        {
            if (quantified.isQuantifier()) {
                System.out.println("quantifier");
                System.out.println("quantified.getNumArgs() = " + quantified.getNumArgs());

                // following two lines result in "com.microsoft.z3.Z3Exception: invalid argument"
                // quantified.getArgs();
                // Quantifier casted = (Quantifier) quantified;
            } else {
                System.out.println("no quantifier");
            }
        }
    }

}

z3/C++ 相关问题

另请查看集成别名方法的扩展示例，其中条件被简化。化Expr output简得到的 不能转换为 aQuantifier虽然满足.isQuantifier().

该变量ENABLE_ERROR可用于打开和关闭转换错误。

import com.microsoft.z3.*;

public class Z3_test {

    public static void main(String[] args) {
        final boolean ENABLE_ERROR = true;
        Context context = new Context();
        Expr input;
        {
            BoolExpr b1 = context.mkBoolConst("b1");
            BoolExpr b2 = context.mkBoolConst("b2");
            BoolExpr body = context.mkIff(b1, b2);
            input = context.mkQuantifier(
                    true,
                    new Expr[]{b1},
                    body,
                    0,
                    null,
                    null,
                    null,
                    null);
        }
        System.out.println("input = " + input);
        Expr output = input;
        if (ENABLE_ERROR) {
            Goal g4 = context.mkGoal(true, false, false);
            g4.add((BoolExpr) input);
            Params params = context.mkParams();
            ApplyResult ar = context.mkTactic("simplify").apply(g4, params);
            output = ar.getSubgoals()[0].AsBoolExpr();
        }
        System.out.println("output = " + output);
        {
            if (output.isQuantifier()) {
                System.out.println("quantifier");
                System.out.println("output.getNumArgs() = " + output.getNumArgs());
                Quantifier casted = (Quantifier) output;
                int i = casted.getNumBound();
                System.out.println("casted.getNumBound() = " + i);
                for (int c = 0; c < i; c++) {
                    System.out.println("casted.getBoundVariableNames(" + c + ") = " + casted.getBoundVariableNames()[c]);
                }
                System.out.println("casted.getBody() = " + casted.getBody());
            } else {
                System.out.println("no quantifier");
            }
        }
    }

}

标签： javaz3

Answer 1

这里的问题是mkQuantifier返回 a Quantifier，它本身不是一个表达式。（当然，它在正文中包含一个表达式。）

你可以这样写你的例子：

import com.microsoft.z3.*;

public class Z3_test {

    public static void main(String[] args) {
        Context context = new Context();
        Expr quantified;
        {
            BoolExpr b1 = context.mkBoolConst("b1");
            BoolExpr b2 = context.mkBoolConst("b2");
            BoolExpr body = context.mkIff(b1, b2);
            quantified = context.mkQuantifier(
                    true,
                    new Expr[]{b1},
                    body,
                    0,
                    null,
                    null,
                    null,
                    null);
        }
        System.out.println(quantified);
        {
            if (quantified.isQuantifier()) {
                System.out.println("quantifier");

                /* Cast to Quantifier first */
                Quantifier q = (Quantifier) quantified;
                int i = q.getNumBound();
                System.out.println("q.getNumBound()            = " + i);
                for (int c = 0; c < i; c++) {
                    System.out.println("q.getBoundVariableNames(" + c + ") = " + q.getBoundVariableNames()[c]);
                }
                System.out.println("q.getBody()                = " + q.getBody());
            } else {
                System.out.println("no quantifier");
            }
        }
    }

}

当我运行它时，我得到：

(forall ((b1 Bool)) (! (= b1 b2) :weight 0))
quantifier
q.getNumBound()            = 1
q.getBoundVariableNames(0) = b1
q.getBody()                = (= (:var 0) b2)

它向您展示了如何深入研究量词本身。关键是在深入研究之前将表达式转换为量词。

另请注意，绑定变量在内部已重命名，这就是您看到的原因，(:var 0)而不是b1您可能期望的原因。