问题

在下面的示例中，我想要解析这个表达式。请告诉我如何使用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());

                // 以下两行会导致 "com.microsoft.z3.Z3Exception: invalid argument" 错误
                // quantified.getArgs();
                // Quantifier casted = (Quantifier) quantified;
            } else {
                System.out.println("no quantifier");
            }
        }
    }

}

z3/C++ 相关问题

还请查看扩展示例集成 alias 方法的方法，在其中条件在简化之间被简化。从简化中获得的 Expr output 无法转换为 Quantifier，尽管它满足 .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");
            }
        }
    }

}

英文:

In the following example, I want to parse the expression.
Please make me aware of the Z3 methods for doing so.
(In my application, I get an expression simplified by 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(&quot;b1&quot;);
            BoolExpr b2 = context.mkBoolConst(&quot;b2&quot;);
            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(&quot;quantifier&quot;);
                System.out.println(&quot;quantified.getNumArgs() = &quot; + quantified.getNumArgs());

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

}

z3/C++ related question

Please also have a look at the extended example integrating the approach of alias where the condition is simplified in between. The Expr output obtained from the simplification can't be casted to a Quantifier although it satisfies .isQuantifier().

The variable ENABLE_ERROR can be used to switch the casting error on and off.

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(&quot;b1&quot;);
            BoolExpr b2 = context.mkBoolConst(&quot;b2&quot;);
            BoolExpr body = context.mkIff(b1, b2);
            input = context.mkQuantifier(
                    true,
                    new Expr[]{b1},
                    body,
                    0,
                    null,
                    null,
                    null,
                    null);
        }
        System.out.println(&quot;input = &quot; + 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(&quot;simplify&quot;).apply(g4, params);
            output = ar.getSubgoals()[0].AsBoolExpr();
        }
        System.out.println(&quot;output = &quot; + output);
        {
            if (output.isQuantifier()) {
                System.out.println(&quot;quantifier&quot;);
                System.out.println(&quot;output.getNumArgs() = &quot; + output.getNumArgs());
                Quantifier casted = (Quantifier) output;
                int i = casted.getNumBound();
                System.out.println(&quot;casted.getNumBound() = &quot; + i);
                for (int c = 0; c &lt; i; c++) {
                    System.out.println(&quot;casted.getBoundVariableNames(&quot; + c + &quot;) = &quot; + casted.getBoundVariableNames()[c]);
                }
                System.out.println(&quot;casted.getBody() = &quot; + casted.getBody());
            } else {
                System.out.println(&quot;no quantifier&quot;);
            }
        }
    }

}

答案1

得分: 0

问题在于mkQuantifier返回一个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。

英文:

The issue here is that mkQuantifier returns a Quantifier, which is not an expression by itself. (It contains an expression in the body, of course.)

You can write your example like this:

import com.microsoft.z3.*;

public class Z3_test {

    public static void main(String[] args) {
        Context context = new Context();
        Expr quantified;
        {
            BoolExpr b1 = context.mkBoolConst(&quot;b1&quot;);
            BoolExpr b2 = context.mkBoolConst(&quot;b2&quot;);
            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(&quot;quantifier&quot;);

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

}

When I run this, I get:

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

which shows you how to dive into the quantifier itself. The crucial point is to cast the expression to a quantifier before diving in.

Also note that the bound-variables are internally renamed, that's why you see (:var 0) instead of b1 which you might otherwise expect.

专注分享java语言的经验与见解，让所有开发者获益！

如何在Z3/Java中解析量化表达式？

问题

答案1

Go like channels in Java

在低资源环境下使用Apache Cassandra和Go服务器

avatica-go客户端读取Phoenix查询服务器：[驱动程序：连接错误]

向Spring端点发送POST请求，返回状态码400。

Spring Boot控制器从Golang应用程序接收到的重定向请求会被重复执行两次。

可以在不将其读入内存的情况下多次重用HTTP请求体吗？

How to register my go lang microservice in Spring Eureka Service Discovery

在应用程序-go + BDD-java中模拟第三方服务

What is value, reference vs pointer and what these three example used to pass?

Do goroutines and light-weight Java threads mean we never need use thread pools and async code again?

发表评论