Что является лучшей практикой в ​​SMT: добавить несколько утверждений или одно и?

Question

Допустим, у меня есть два предложения, которые я хочу смоделировать в SMT, лучше добавить их как отдельные утверждения типа

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

или добавить одно утверждение с помощью оператора и, как это

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

Имеет ли это значение для крупномасштабных проблем с точки зрения производительности решателя SMT. Я использую Z3.

Answer 1

Соединение разбивается на несколько утверждений, поэтому оно не имеет большого значения. Если вы введете большую конъюнкцию, парсер Z3 создаст термин, который содержит все конъюнкты, но это просто постоянные издержки поверх поддержки конъюнктов.