Что эквивалентно check-sat-using в z3py? - PullRequest
Новая
       8

Что эквивалентно check-sat-using в z3py?

1 голос
/ 03 февраля 2020

Я пытался достичь той же цели, что и этот пост. Z3 случайность сгенерированных значений модели

Кроме того, ответ в smt, как мне использовать check-sat-using в z3py в python? Может кто-нибудь помочь мне перевести этот код в python код? 

(set-option :smt.arith.random_initial_value true)
(declare-const x Int)
(declare-const y Int)
(assert (> (+ x y) 0))
(check-sat-using (using-params qflra :random_seed 1))
(get-model)
(check-sat-using (using-params qflra :random_seed 2))
(get-model)
(check-sat-using (using-params qflra :random_seed 3))
(get-model)

1 Ответ

1 голос
/ 03 февраля 2020

В интерфейсе SMTLib check-sat-using - это способ указать z3, какую тактику использовать. Когда вы используете z3py, вы напрямую используете язык tacti c и явно создаете решатели. Таким образом, в некотором смысле в z3py нет соответствующего вызова check-sat-using. Вместо этого вы получаете целый язык tacti c, который является гораздо более гибким и мощным.

Для примеров см .: http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/strategies-examples.htm

Обратите внимание, что check-sat-using объединяет тактику и настройки в некотором смысле, в z3py вы используете set_param для достижения настроек параметров и язык tacti c для express, какую стратегию вы хотите использовать.

Как общее правило большой палец, не пытайтесь «переводить» между интерфейсами SMTLib и Z3 Python. Хотя оба могут express выполнять одни и те же запросы, модель программирования различна, и попытка перевести «команда за командой» приведет к неидиоматическому c и сложному в обслуживании коду. Вместо этого, если вы хотите использовать Z3py, просто узнайте, как там все делается, помня, что они могут сильно отличаться от земли SMTLib. Это отличный ресурс для прочтения, чтобы вы могли начать: http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/

...