Определение правил для битовых векторов в SMT2

Я перешел с использования Int на битовые векторы в SMT. Однако логика QF_BV не позволяет использовать какие-либо квантификаторы в вашем скрипте, и мне нужно определить правила FOL. Я знаю, как исключить кванторы существования, но универсальные кванторы? Как это сделать?

Представьте себе такой код:

(set-logic QF_AUFBV)

(define-sort Index () (_ BitVec 3))

(declare-fun P (Index) Bool)

(assert (forall ((i Index)) (= (P (bvadd i #b001)) (not (P i)) ) ) )

z3 smt quantifiers first-order-logic bitvector
person Arya Pourtabatabaie    schedule 14.07.2015    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Строго говоря, вам не повезло. Согласно http://smtlib.cs.uiowa.edu/logics.shtml, существует нет логики, содержащей кванторы и битовые векторы одновременно.

При этом большинство решателей допускают нестандартные комбинации. Просто опустите команду set-logic, и вам может повезти. Например, Z3 отлично справится с вашим запросом без части set-logic; Я только что попробовал ..

person alias    schedule 14.07.2015
comment
Действительно, Z3 также распознает логику UFBV и BV (без QF_). Для них в SMTLIB также есть несколько тестов, так что я ожидаю, что они скоро станут официальной логикой. - person Christoph Wintersteiger; 15.07.2015
comment
Новый стандарт SMT-LIB 2.5 определяет (set-logic ALL) для выбора наиболее общей логики, поддерживаемой решателем. (SMT-LIB 2.5 был выпущен 28 июня 2015 г.) - person CliffordVienna; 05.08.2015