2

我想知道为什么 Z3 能够通过在某些情况下应用结合性和交换性 (AC) 公理来证明一些微不足道的等式，而在其他情况下则不行。例如，

(simplify (= (bvadd x (bvadd y z)) (bvadd z (bvadd y x))))

减少到 true，但是

(simplify (= (bvxor x (bvxor y z)) (bvxor z (bvxor y x))))

没有（Z3 只是扁平化了 bvxor 应用程序）。

我查看了源代码（src/ast/bv_decl_plugin.cpp），bvadd 和 bvxor 都被声明为 AC 符号。它与应用于每个符号的重写规则有关吗？特别是，mk_bv_add (src/ast/rewriter/bv_rewriter.cpp) 调用 mk_add_core (src/ast/simplifier/poly_simplifier_plugin.cpp) 将 bvadd 项处理为单项式的总和。

4

1 回答 1

4

是的，它与应用于符号的重写规则有关。Z3 有两个表达式简化器：src/ast/rewriter和src/ast/simplifier. 这src/ast/simplifier是遗留的，它没有在新代码中使用。simplifySMT-LIB 前端中的命令基于src/ast/rewriter. mk_bv_add实际上是使用mk_add_corein src/ast/rewriter/poly_rewriter.h。

更改代码以强制 Z3 将bvxor您问题中的表达式简化为true. 我们只需要在src/ast/rewriter/bv_rewriter.h. 新行只是对bvxor参数进行排序。这对任何 AC 操作员来说都是正确的重写。

br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & result) {
    SASSERT(num > 0);
    ...
    default:
        // NEW LINE
        std::sort(new_args.begin(), new_args.end(), ast_to_lt());
        //
        result = m_util.mk_bv_xor(new_args.size(), new_args.c_ptr());
        return BR_DONE;
    }
}

话虽如此，Z3 重写器不应该应用所有可能的简化和/或产生规范的范式。他们的主要目标是生成可能更易于求解的公式。规则基于需求增长（例如，Z3 在示例 X 中太慢，性能问题可以通过应用新的预处理规则“修复”），或基于用户请求。因此，如果您认为这是一个有用的功能，我们可以添加一个选项，对每个 AC 运算符的参数进行排序。

编辑

更正：我们还必须修改以下语句

if (!merged && !flattened && (num_coeffs == 0 || (num_coeffs == 1 && !v1.is_zero() && v1 != (rational::power_of_two(sz) - numeral(1))))
    return BR_FAILED;

mk_bv_xor当现有的重写规则都不适用时，此语句会中断 的执行。我们还必须对其进行修改。我在这里实现了这些修改。我们可以使用新选项来激活它们:bv-sort-ac。默认情况下不启用此选项。新选项在unstable(work-in-progress) 分支中可用。当设置为 true 时，它​​将对位向量 AC 运算符进行排序。请注意，该unstable分支使用了新的参数设置框架，该框架将在下一个正式版本中提供。 以下是有关如何构建unstable分支的说明。这些修改也将在本周的夜间版本中提供。

以下是一些使用新选项的示例：

(declare-const a (_ BitVec 8))
(declare-const b (_ BitVec 8))
(declare-const c (_ BitVec 8))
(declare-const d (_ BitVec 8))

(simplify (= (bvxor a b c) (bvxor b a c)))
(simplify (= (bvxor a b c) (bvxor b a c)) :bv-sort-ac true)
(simplify (= (bvxor a (bvxor b c)) (bvxor b a c)) :bv-sort-ac true)

(simplify (= (bvor a b c) (bvor b a c)))
(simplify (= (bvor a b c) (bvor b a c)) :bv-sort-ac true)
(simplify (= (bvor a (bvor b c)) (bvor b a c)) :bv-sort-ac true)


(simplify (= (bvand a b c) (bvand b a c)))
(simplify (= (bvand a b c) (bvand b a c)) :bv-sort-ac true)
(simplify (= (bvand a (bvand b c)) (bvand b a c)) :bv-sort-ac true)

; In the new parameter setting framework, each module has its own parameters.
; The bv-sort-ac is a parameter of the "rewriter" framework.
(set-option :rewriter.bv-sort-ac true)

; Now, Z3 will rewrite the following formula to true even when we do not provide
; the option :bv-sort-ac true
(simplify (= (bvand a b c) (bvand b a c)))

; It will also simplify the following assertion.
(assert (= (bvand a b c) (bvand b a c)))

(check-sat)

结束编辑

于 2013-03-24T16:30:37.030 回答