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

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

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

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

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

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


smtp smtplib z3 smt sat-solvers
person Mohammed    schedule 12.07.2014    source источник

Ответы (1)


arrow_upward
4
arrow_downward

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

person Nikolaj Bjorner    schedule 12.07.2014