缩小量词的范围在Z3

Question

有是可用于通过结合分配通用量词一个distribute-forall战术。我对通用量词和存在量词都有一个更一般化的程序感兴趣，它们尽可能地缩小了量词的范围。 例如，我想式

(exists ((x Int)) (and (= z (* 2 x)) (<= z y)))被转化成

(and (exists ((x Int)) (= z (* 2 x)) (<= z y)))。

这可以通过一些其他的战术（S）来完成？

Answer 1

在Z3代码库的分支mcsat有一个名为miniscope新战术。它做你想要的。我们可以使用these instructions建立mcsat分支。我们只需要将替换为mcsat。

下面是使用这种战术的一些例子。

(declare-const z Int) 
(declare-const x Int) 
(declare-const y Int) 

(assert (exists ((x Int)) (and (= z (* 2 x)) (<= z y)))) 

(apply miniscope) 

和所产生的输出

(goals 
(goal 
    (<= z y) 
    (exists ((x!1 Int)) (= z (* 2 x!1))) 
    :precision precise :depth 3) 
) 

下面是一个更复杂的例子：

(set-option :pp.max-depth 100) 
(declare-fun p (Int) Bool) 
(declare-fun q1 (Int Real) Bool) 
(declare-fun q2 (Real Real) Bool) 
(declare-fun q3 (Int Int) Bool) 

(assert (forall ((x1 Int) (x2 Real)) 
       (or (q2 x2 x2) (exists ((y Real)) (and (q1 y x2) (q1 x1 x2)))))) 

(apply miniscope) 

和所产生的输出

(goals 
(goal 
    (forall ((x2 Real)) 
    (or (q2 x2 x2) 
     (and (forall ((x1 Int)) (q1 x1 x2)) 
      (exists ((y Real)) (q1 (to_int y) x2))))) 
    :precision precise :depth 3) 
) 

EDIT

mcsat分支包含正在进行的工作，最终将合并到master分支中。但是，下一次正式发布（v4.3.2）可能不会发生合并。当我们发布新版本时，我们将unstable和contrib分支合并到master分支中。

的mcsat分支基本上是增加新的功能。它与unstable和contrib分支不兼容。

我们鼓励高级用户（熟悉的git）使用非官方发布和选择分支。当然，在报告错误/问题时，应该使用与提交相关联的git散列，而不是版本号。

编辑完