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

Question

Определение правил для битовых векторов в 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)) ) ) )

2

z3 smt quantifiers first-order-logic bitvector

Источник

user5116581 14 июл '15 в 19:14

1 ответ

Решение

Другие вопросы по тегам z3 smt quantifiers first-order-logic bitvector

user936310 14 июл '15 в 20:58 2015-07-14 20:58 · Accepted Answer · 2015-07-14 20:58

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

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