Z3: str.indexof выдает неожиданный ответ, почему? - PullRequest
Новая
       10

Z3: str.indexof выдает неожиданный ответ, почему?

0 голосов
/ 01 ноября 2018

Я пытался решить следующую проблему с Z3: 

(declare-const b String)
(assert (= 3 (str.indexof "abcdef" b)))
(check-sat)
(get-model)

Я получил результат: 

sat
(model
  (define-fun b () String 
    "de")
)

Однако, когда я попытался решить следующую проблему с Z3: 

(declare-const b String)
(assert (= 4 (str.indexof "abcdef" b)))
(check-sat)
(get-model)

Но я получил результат: 

unknown
Z3(4, 10): ERROR: model is not available

Это ошибка?

1 Ответ

0 голосов
/ 01 ноября 2018

unknown не является желательным ответом здесь, но это также не ошибка. Это просто означает, что z3 не смог построить модель для удовлетворения ваших ограничений, но он также не мог решить, что они не являются неудовлетворительными. Разрешимость теории струн является открытой проблемой, поэтому это не удивительно.

Кстати, вы должны использовать старую версию z3. Когда я использую ваши сценарии, я получаю: 

$ z3 smt.string_solver=z3str3 a.smt2
sat
(model
  (define-fun b () String
    "d")
)

и 

$ z3 smt.string_solver=z3str3 a.smt2
sat
(model
  (define-fun b () String
    "e")
)

соответственно. Итак, похоже, что вещи действительно улучшились!

Обратите внимание, что z3 поставляется с несколькими решателями строк, а параметр командной строки smt.string_solver=z3str3 выбирает z3str3, самое последнее воплощение. Допустимые значения:

  • z3str3: специализированный решатель строк
  • seq: решатель последовательности
  • auto: используйте статические функции, чтобы выбрать лучший решатель

К сожалению, здесь нет четкого выбора; как правило, вам нужно попробовать все и посмотреть, какой из них работает лучше для вас. (И если они не согласны с sat / unsat, сообщите об этом как об ошибке! Различия должны быть только в производительности.)

...