optimization - z3中的INST_GEN是什么

Question

上下文：我对使用z3的有限Java程序验证进行了研究。我想获得关于线性化问题的优化模型。一种标准方法是逐步搜索模型，直到找到不满意的情况为止。但是性能似乎是一个问题，并且通过引入JNI破坏了代码的可移植性，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中崩溃时将返回“ segmentation fault”。这两个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。