Z3 Java API中的符号创建

Question

我是Z3的新手，请原谅我这个问题听起来太容易了。我有两个问题在Z3 Java API中重新定义常量。

1. 如何在内部创建常量？要理解我开始跟踪public BitVecExpr mkBVConst(String, int)到public StringSymbol mkSymbol(String)最终调用Native.mkStringSymbol(var1.nCtx(), var2)在var3生成变量在这行long var3 = INTERNALmkStringSymbol(var0, var2);

现在因为`INTERNALmkStringSymbol'是原生的，我无法看到它的来源。我想知道它是如何运作的。有谁知道它是如何工作的？在哪里查看其来源？

2. 我感到困惑的另一件事是使用API​​确定常量的范围。在交互式Z3中，它通过匹配推送和弹出来维护，但通过API，我不确定如何定义和管理范围。

任何见解或指导都非常感谢。

Answer 1

1. Z3是开源的，您可以从https://github.com/z3prover/z3.git查看和下载源代码。 Z3中的符号在src / util / symbol.h中定义。您将看到符号类似于LISP原子：它们在dll的生命周期中持续存在并且是唯一的。所以两个具有相同名称的符号将是指针相等的。 Java API调用C API，该API在src / api / z3_api.h中声明。目录src / api包含API函数，包括创建符号的函数。当你创建一个表达式常量，比如mkBVConst时，它是一个也是指针唯一的表达式（如果你创建两次相同的mkBVConst，非托管指针将是相同的.Java指针不一样，但是相等测试利用了所有这个的）。
2. Solver对象具有push和pop方法。您可以向求解器对象添加约束。约束的生命周期遵循推/弹嵌套：约束处于活动状态，直到有一个弹出消除添加约束的范围。