Загадочный (и хрупкий) результат запроса SMT, связанного с электронным соответствием - PullRequest
Новая
       7

Загадочный (и хрупкий) результат запроса SMT, связанного с электронным соответствием

0 голосов
/ 19 сентября 2018

Для следующего файла smt (который был сведен к минимуму из примера, созданного Viper / Boogie), Z3 возвращает unknown (очень быстро). 

(set-option :print-success false)
(set-info :smt-lib-version 2.0)
(set-option :AUTO_CONFIG false)
(set-option :pp.bv_literals false)
(set-option :MODEL.V2 true)
(set-option :smt.PHASE_SELECTION 0)
(set-option :smt.RESTART_STRATEGY 0)
(set-option :smt.RESTART_FACTOR |1.5|)
(set-option :smt.ARITH.RANDOM_INITIAL_VALUE true)
(set-option :smt.CASE_SPLIT 3)
(set-option :smt.DELAY_UNITS true)
(set-option :NNF.SK_HACK true)
(set-option :smt.MBQI false)
(set-option :smt.QI.EAGER_THRESHOLD 100)
(set-option :TYPE_CHECK true)
(set-option :smt.BV.REFLECT true)
; (options as set by Boogie)

(declare-sort T@Seq 0)
(declare-fun Append (T@Seq T@Seq) T@Seq)
(declare-fun Empty () T@Seq)
(declare-fun Singleton (Int) T@Seq)
(declare-fun dummy () Bool)
(declare-fun Contains (T@Seq Int) Bool)
; Empty ++ s == s
(assert (forall ((s T@Seq) ) (! (= (Append Empty s) s)
 :qid |_0314cbp.11:15|
 :skolemid |0|
 :pattern ( (Append Empty s))
)))
; (strange axiom)
; forall s0,s1 :: {s0++s1} s0 != Empty ==> dummy
(assert (forall ((s0 T@Seq) (s1 T@Seq) ) (!  (=> (not (= s0 Empty)) dummy)
 :qid |_0314cbp.17:15|
 :skolemid |3|
 :pattern ( (Append s0 s1))
)))
; forall s0,s1,x :: {(Contains s0++s1 x)} Contains s0++s1 x <==> (Contains s0 x || Contains s1 x)
(assert (forall ((s0@@0 T@Seq) (s1@@0 T@Seq) (x Int) ) (!  (and (=>     (Contains (Append s0@@0 s1@@0) x) (or (Contains s0@@0 x) (Contains s1@@0 x))) (=> (or (Contains s0@@0 x) (Contains s1@@0 x)) (Contains (Append s0@@0 s1@@0) x)))
 :qid |_0314cbp.22:15|
 :skolemid |4|
 :pattern ( (Contains (Append s0@@0 s1@@0) x))
)))
(declare-fun s () T@Seq)
(declare-fun s1 () T@Seq) ; spurious term, used for assumption
(declare-fun i () Int)
(declare-fun f (Int) Bool)
(push 1)
(assert (not
; forall x_1 :: {(Contains s x_1)} f x_1
(=> (and (forall ((x_1 Int) ) (! (f x_1)
 :qid |_0314cbp.34:20|
 :skolemid |5|
 :pattern ( (Contains s x_1))
)) (= s1 (Append s (Singleton 1)))) (=> (Contains (Append s (Singleton 1)) i ) ( f i ))))
)
(check-sat)
(pop 1)
; Invalid

Насколько я понимаю, этот результатожидается;единственный способ получить unsat, о котором я знаю, - создать экземпляр последнего квантификатора (внутри последней формулы assert ed), чей шаблон равен (Contains s x_1).Этот термин не известен в контексте;для известного (Contains (Append s (Singleton 1)) i ) возможно создание экземпляра квантификатора с :qid |_0314cbp.22:15|, что приводит к дизъюнкции (or (Contains s i ) (Contains (Singleton 1) i)).Если / когда Z3 разветвляется на этой дизъюнкции, в первом случае будет термин для получения unsat из последней аксиомы с, но во втором - нет.Как объяснено в другом месте , Z3 будет возвращать экземпляры, сделанные между такими разбиениями.

Что удивляет меня в этом примере, так это то, что в него можно внести много модификаций, чтобы получить unsat результат, и они либо ослабляют сделанные логические предположения, либо оставляют их без изменений;в каждом случае я не понимаю, почему те же рассуждения, что и выше, не применимы для объяснения того, что unknown следует ожидать.Например:

  1. Предположение (= s1 (Append s (Singleton 1))) является ложным;термин s1 больше нигде в проблеме не используется, а (Append s (Singleton 1)) является известным термином в следующем аспекте (поэтому его наличие не должно влиять на потенциальное электронное сопоставление).Однако удаление или замена на true (т.е. ослабление сделанных допущений) приведет к unsat.

  2. Удаление любого из первых двух квантификаторов (второй из которыхне имеет никакого логического значения) приведет к unsat.

  3. Переписывание третьей аксиомы для выражения импликации (Contains s0++s1 x ==> (Contains s0 x || Contains s1 x)), а не if-and-only-if приведет кunsat.

  4. Удаление (push 1) и (pop 1) приведет к unsat.

Мой главный вопрос:эти (изменения) поведения, ожидаемые, и как я могу их объяснить?Кроме того, если есть хороший способ узнать, что Z3 делает с проблемой, и попытаться раскрыть для себя больше информации, я был бы рад сделать это.

Я попробовал пример (и еговарианты) с использованием инструмента Axiom Profiler;там я смог увидеть, что делается такое же количество определений квантификаторов (3), но в случае аксиомы о распределении Contains по Append иногда упрощенный термин, кажется, изучается Z3, а неполный квантификатор тела.Я могу предоставить более подробную информацию об этом, если они будут полезны.

...