Как z3 'smt_tactic' решает формулы QF_BV?

Когда z3 использует smt_tactic (вместо тактики qfbv) для решения формулы QF_BV, будет ли он использовать битовые взрывы и использовать движок SAT? Когда я устанавливаю уровень детализации на 10, я не вижу битовых взрывов.


z3 smt
person rainoftime    schedule 09.03.2017    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Это делает бит-взрыв, но лениво. Он будет использовать решатель SMT. Обратите внимание, однако, что бит-взрыв весьма стремителен.

person Nuno Lopes    schedule 09.03.2017
comment
Спасибо. Под ленивостью вы имеете в виду, что smt_tacitc будет использовать цикл абстракции-уточнения, подобный DPLL(T), при решении экземпляра QF_BV? - person rainoftime; 10.03.2017
comment
Точно. Если вы соберете Z3 в режиме отладки и поэкспериментируете с параметрами -tr:foo, вы сможете более подробно распечатать, что происходит. (и -v:999999 также помогает). - person Nuno Lopes; 10.03.2017