Подходящая тактика Z3 для устранения тривиального экзистенциального квантификатора - PullRequest
Новая
       12

Подходящая тактика Z3 для устранения тривиального экзистенциального квантификатора

0 голосов
/ 24 марта 2019

Я экспериментирую с тактикой Z3, и мне было интересно, какая тактика может упростить тривиальные экзистенциальные квантификаторы, подобные следующим: 

(declare-datatypes () ((Value none (some (val String)))))
(declare-const foo Value)

(assert (exists ((x String)) (and (= foo (some x)) (= x "bar"))))

Я пытался сделать что-то простое: 

(apply (repeat (then (or-else split-clause skip) propagate-values simplify)))

Но это не избавляет от exists. Я могу добавить туда qe или qe2, но те чувствуют себя здесь излишне, и, как правило, берут на нетривиальные проблемы целую вечность.

Если я сделаю прямолинейное (check-sat) с максимальной детализацией, у Z3 нет проблем с решением: 

(simplifier :num-exprs 8 :num-asts 174 :time 0.00 :before-memory 2.78 :after-memory 2.78)
(smt.tactic start)
(smt.propagate-values)
(smt.nnf-cnf)
(smt.reduce-asserted)
(smt.lift-ite)
(smt.reducing)
(smt.refine-injectivity)
(smt.cheap-fourier-motzkin)
(smt.reducing)
(smt.pattern-inference)
(smt.maximizing-bv-sharing)
(smt.reduce-asserted)
(smt.simplifier-done)
(smt.searching)
sat
(model 
  (define-fun foo () Value
    (some "bar"))
)

И я надеялся, что некоторые шаги предложат тактику, которую я могу применить сам, но это не так.

Есть ли хорошая тактика для этого?

...