有一种distribute-forall
策略可用于分配全称量词而不是连词。我对通用量词和存在量词的更通用过程感兴趣,该过程将尽可能缩小量词的范围。例如,我想要公式
(exists ((x Int)) (and (= z (* 2 x)) (<= z y)))
变成
(and (exists ((x Int)) (= z (* 2 x)) (<= z y)))
.
这可以通过其他一些策略来完成吗?
有一种distribute-forall
策略可用于分配全称量词而不是连词。我对通用量词和存在量词的更通用过程感兴趣,该过程将尽可能缩小量词的范围。例如,我想要公式
(exists ((x Int)) (and (= z (* 2 x)) (<= z y)))
变成
(and (exists ((x Int)) (= z (* 2 x)) (<= z y)))
.
这可以通过其他一些策略来完成吗?
Z3 代码库中的分支mcsat
有一个名为miniscope
. 它做你想做的事。我们可以使用这些指令mcsat
构建分支。我们只需要替换为.unstable
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)
)
编辑
mcsat
分支包含最终将合并到分支中的进行中的工作master
。但是,合并可能不会在下一个正式版本(v4.3.2)中发生。当我们发布新版本时,我们合并unstable
并contrib
分支到master
分支中。
该mcsat
分支本质上是在添加新功能。unstable
它与andcontrib
分支并不矛盾。
我们鼓励高级用户(熟悉 git)使用非官方版本和替代分支。当然,在报告错误/问题时,应该使用与提交相关的 git 哈希而不是版本号。
结束编辑