在SMT中更好的做法是：添加多個斷言或單個和？

Question

可以說我有，我想在SMT模型兩個分句，是能夠更好地將其添加爲單獨的斷言像

(assert (> x y)) 
(assert (< y 2)) 

或與和運營商添加一個斷言這樣

(assert (and 
(> x y) 
(< y 2) 
)) 

這對SMT解算器性能方面的大規模問題是否有影響？我正在使用Z3。

Answer 1

連接被分成多個斷言，所以它並不重要。 如果引入一個大連詞，Z3的解析器將創建一個包含所有連詞的詞語，但這只是維持連詞的一個常量。