SMT 中哪个更好的做法是:添加多个断言或单个断言? [英] Which is better practice in SMT: to add multiple assertions or single and?

问题描述

假设我有两个要在 SMT 中建模的子句，将它们作为单独的断言添加是否更好，例如

Lets say I have two clauses that I want to model in SMT, is it better to add them as separate assertions like

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

或者像这样使用和运算符添加一个断言

or to add one assertion with and operator like this

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

这对于 SMT 求解器性能方面的大规模问题是否重要.我正在使用 Z3.

Does this matter for large scale problems in terms of SMT solver performance. I am using Z3.

推荐答案

连词被拆分成多个断言，所以它并不重要.如果您引入大连词，Z3 的解析器将创建一个包含所有连词的术语，但这只是维护连词之外的恒定开销.

The conjunction gets split into multiple assertions, so it doesn't really matter too much. If you introduce a large conjunction, Z3's parser will create a term that contains all the conjuncts, but this is just a constant overhead on top of maintaining the conjuncts.

这篇关于SMT 中哪个更好的做法是:添加多个断言或单个断言?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！