簡化在Z3 AC符號：bvadd VS bvxor/bvor /等

Question

我不知道爲什麼Z3能夠在某些情況下，將相關性和可交換性（AC）的公理而不是在別人展示一些瑣碎的等式。例如，

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

reduces to true，但

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

does not（Z3只是變平bvxor應用程序）。

我看了看源代碼中（src/AST/bv_decl_plugin.cpp）和兩個bvadd和bvxor被宣佈爲AC符號。它是否與適用於每個這些符號的重寫規則相關？特別地，mk_bv_add（SRC/AST /重寫/ bv_rewriter.cpp）調用mk_add_core（SRC/AST /簡化器/ poly_simplifier_plugin.cpp），其處理一個bvadd術語單項式的總和。

Answer 1

是的，它關係到應用到符號的重寫規則。 Z3具有兩個簡單化者表達：src/ast/rewriter和src/ast/simplifier。 src/ast/simplifier是遺留的，它不用於新代碼。 SMT-LIB前端中的simplify命令基於src/ast/rewriter。 mk_bv_add實際上在src/ast/rewriter/poly_rewriter.h中使用mk_add_core。

將代碼更改爲強制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重寫器不應該應用所有可能的簡化和/或產生規範的標準形式。他們的主要目標是生成可能更簡單解決的公式。規則根據需求增長（例如，示例X中的Z3速度太慢，性能問題可以通過應用新的預處理規則「固定」）或基於用戶請求。所以，如果你認爲這是一個有用的功能，我們可以添加一個選項來排序每個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執行，當不存在重寫規則都適用。我們也必須修改它。我實施了這些修改here。我們可以使用新選項:bv-sort-ac激活它們。此選項默認爲啓用而不是。新的選項可在unstable（在製品）分支中找到。設置爲true時，它將對位向量AC運算符進行排序。 注意的是，unstable科採用新的參數設定的框架，將在未來正式發佈上市。 Here是關於如何構建unstable分支的說明。 這些修改也將於本週在nightly builds上提供。

下面是一些例子，使用新的選項：

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

編輯完