对于下面的代码，我观察到似乎是由三个不寻常的方面引起/影响的非常快的结果：
- 使用
(set-option :produce-proof true)时，最终的UNSAT非常快。如果没有这个选项，最后的 check-sat 不会终止。 - 当使用中间检查和断言（所有推送/弹出）时，最终检查的性能非常快。如果没有中间的 check-sat 命令，最终的 check-sat 不会终止。
- 重命名数据类型字段后，最终检查的性能非常糟糕（终止需要 30 倍的时间）。
有人可以解释这些情况下的行为吗？只是选项的组合导致保留正确的事实以快速回答最终的 SAT 考试吗？未使用的构造函数的字段名称如何影响求解器的性能？
与此问题相关的代码如下。嵌入在代码中的是带有额外上下文的注释和问题的重新散列。
;;;;;;;;;;;;;;;;;;;;;;;;;;;; Configuration ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; E-matching won't terminate on our queries, so turn it off
(set-option :smt.ematching false)
(set-option :smt.mbqi true)
;; In lieu of an initial test, produce-proofs true is a huge benefit to
;; the performance of the final check-sat
(set-option :produce-proofs true)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; Raw data ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Our syntactic representation of 'Bits'
;; Removing 'Raw2345', or renaming it to 'Raw2', causes ~30x more computation time.
(declare-datatypes () ((Bits zero (Xor (left Bits) (right Bits)) (Raw (raw Int)) (Raw2345 (raw2 Int)))))
;; Predicates over data
(declare-fun secret(Bits) Bool)
(declare-fun known(Bits) Bool)
;; The existence of this first test is a significant benefit to the performance
;; of the final check-sat (despite the push/pop).
(push)
(echo " There exists x and y that remain secret even when xor can cancel")
(echo " (NB rules regarding AC theories are missing)")
(assert (exists ((x Bits) (y Bits) (xA Bits) (xB Bits) (xC Bits) (yA Bits) (yB Bits) (yC Bits))
(and (= x (Xor xA (Xor xB xC)))
(= y (Xor yA (Xor yB yC)))
(secret x)
(secret y)
(known xA)
(known xB)
(known xC)
(known yA)
(known yB)
(known yC)
(not (known x))
(not (known y))
)))
(check-sat)
(pop)
;;;;;;;;;;;;;;;;;;;;;;;;;;;; Theory of xor ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Axioms for 'Xor', expressed in terms of what the attacker knows
(assert (forall ((y Bits) (x Bits)) ;nilpotence
(! (=> (known (Xor y (Xor x x)))
(known y)) :weight 0)))
(assert (forall ((x Bits)) ;identity
(! (=> (known (Xor x zero))
(known x)) :weight 0))) ;commutativity
(assert (forall ((x Bits)
(y Bits))
(! (=> (known (Xor x y))
(known (Xor y x))) :weight 1)))
(assert (forall ((x Bits) ;associativity (1)
(y Bits)
(z Bits))
(! (=> (known (Xor x (Xor y z)))
(known (Xor (Xor x y) z))) :weight 1)))
(assert (forall ((x Bits) ;associativity (2)
(y Bits)
(z Bits))
(! (=> (known (Xor (Xor x y) z))
(known (Xor x (Xor y z)))) :weight 2)))
;; Assume knowledge of xor
(assert (known zero))
(assert (forall ((x Bits)
(y Bits))
(! (=> (and (known x)
(known y))
(known (Xor x y))) :weight 4 )))
;; The below test now seems needed for decent performance - odd since
;; formulations prior to this pretty one for stackoverflow didn't include
;; this particular check-sat.
(echo " Z3 has properly discarded the pushed/popped assertion.")
(echo " Our problem remains SAT")
(check-sat)
;; Simple test
(push)
(assert
(exists ((a Bits)
(b Bits)
(c Bits)
(ra Bits)
(rb Bits)
(rc Bits))
; Our real problem:
(and (secret (Xor a (Xor b c)))
(known (Xor a (Xor ra rc)))
(known (Xor b (Xor rb ra)))
(known (Xor c (Xor rc rb)))
) ))
(echo " Can Z3 use XOR rewriting lifted within uninterpreted functions")
(echo " (should get UNSAT)")
(assert
(not (exists ((a Bits))
(and (secret a) (known a)))))
;; Skolemize must be turned off for performance reasons
;; NTS: What is Z3 doing instead about existentials?
(set-option :nnf.skolemize false)
;; NST: Presumably, performing a depth three par-then helps
;; because it aligns well with the depth of our asserts, but
;; a smarter approach will be needed later.
(check-sat-using (par-then (par-then smt smt) smt))
(pop)