z3 中的 INST_GEN 是什么

Question

上下文：我研究使用 z3 进行有界 Java 程序验证。我想得到一个关于线性化问题的优化模型。一种标准方法可以是逐步搜索模型，直到找到未满足的情况。但是性能似乎是个问题，它通过引入 JNI 破坏了代码的可移植性，它将 z3 c/c++ api 集成到我的工具中。

现在我想对 java 方法的所有输入添加约束。我使用数量数组（我使用数组理论来模拟堆）。但是，z3 总是在可满足的问题上立即返回“未知”。似乎不可能生成模型。我注意到z3有一个选项，INST_GEN，然后我试图理解它。我将以下公式提供给 z3。

(set-option :INST_GEN true)
(define-sort S () (_ BitVec 2))
(declare-fun s () S)
(assert (= s (_ bv0 2)))

(define-sort A () (Array S S))
(push) ;; 1st case    
(assert (forall ((a A)) (= (select a s) s)))
(check-sat)
(get-model)
(pop)

(push) ;; 2nd case
(declare-fun a () A)
(assert (forall ((t S)) (= (select a t) t)))
(check-sat)
(get-model)
(pop)

(push) ;; 3rd case
(check-sat)
(get-model)
(pop)

在第一种和第二种情况下，z3 在 Linux 中返回“分段错误”，而在 Windows 7 中崩溃。z3 都是版本 4.0，x64。

第3种情况，免量化，Z3成功生成模型

sat 
(model (define-fun s () (_ BitVec 2) #b00) )

我的第一个问题是这个选项是如何工作的？它是否枚举数组？

第二个问题是，我注意到 z3 可以在量化数组的不满意问题上成功返回“unsat”。 z3 是否支持某些选项或方法来在量化数组、有界索引和元素的满意问题中生成模型？例如使用 if-then-else 子句。

感谢您的阅读和考虑！任何建议都非常感谢！

Answer 1

首先，选项INST_GEN 是实验的一部分。它不应该暴露给外部用户。这个选项没有经过认真测试。它将在以后的版本中隐藏。对此感到抱歉。

其次，一般来说，Z3 在量化数组的可满足问题上会失败。以下tutorial（量词部分）描述了 Z3 完整的许多片段。

最后，Z3 有许多不同的引擎/求解器。但是，其中只有一个支持增量求解。每当使用push/pop 命令时，Z3 都会自动切换到这个增量求解器。 如果我们删除push 和pop 命令，那么Z3 可以证明第二个问题是可以满足的。 这是修改后示例的链接：http://rise4fun.com/Z3/apcQ。