1

有一种distribute-forall策略可用于分配全称量词而不是连词。我对通用量词和存在量词的更通用过程感兴趣,该过程将尽可能缩小量词的范围。例如,我想要公式

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

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

这可以通过其他一些策略来完成吗?

4

1 回答 1

2

Z3 代码库中的分支mcsat有一个名为miniscope. 它做你想做的事。我们可以使用这些指令mcsat构建分支。我们只需要替换为.unstablemcsat

下面是一些使用这种策略的例子。

(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)
)

编辑

mcsat分支包含最终将合并到分支中的进行中的工作master。但是,合并可能不会在下一个正式版本(v4.3.2)中发生。当我们发布新版本时,我们合并unstablecontrib分支到master分支中。

mcsat分支本质上是在添加新功能。unstable它与andcontrib分支并不矛盾。

我们鼓励高级用户(熟悉 git)使用非官方版本和替代分支。当然,在报告错误/问题时,应该使用与提交相关的 git 哈希而不是版本号。

结束编辑

于 2013-04-08T16:38:44.800 回答