Битовые векторные операции Z3

Как использовать операции битового вектора «повторить» и «повернуть_влево»?

В общем, где я могу найти подробную документацию по операциям с битовыми векторами в формате сценариев SMT2, используемом Z3?

Все, что я нахожу, похоже, просто ведет к учебникам или неработающим ссылкам:
https://github.com/Z3Prover/z3/wiki/Documentation
http://research.microsoft.com/en-us/um/redmond/projects/z3/old/documentation.html

Попытка понять «повторить», «повернуть_влево» и «повернуть_вправо» с помощью догадок не увенчалась успехом. Я не могу понять, как их использовать. Например

(display (repeat #b01))
(display (repeat #b01 3))
(display (repeat 3))
(display (rotate_left #b0001 2))

дает

"repeat expects one non-zero integer parameter"
"repeat expects one argument"
"operator is applied to arguments of the wrong sort"
"rotate left expects one argument"

Где документация? Надеясь, что они не объяснили, потому что все это стандартно, я также посмотрел на smt-lib.org, но там тоже нет этих деталей. Так разочаровывает.


z3 smt bitvector
person Thinkerton    schedule 19.05.2015    source источник

Ответы (2)


arrow_upward
3
arrow_downward

В дополнение к ответу дейвута:

Язык SMT хорошо документирован (см. smt-lib.org). теория и определение логики QF_BV. Последний содержит определение повтора:

((_ repeat i) (_ BitVec m) (_ BitVec i*m))
- ((_ repeat i) x) means concatenate i copies of x

Кроме того, Дэвид Кок написал отличное руководство по SMT2.

Имена функций в API Z3 такие же, как и в SMT2, где позволяет синтаксис, в данном случае с префиксом Z3_mk_, чтобы указать, что это функции, которые создают выражения Z3.

person Christoph Wintersteiger    schedule 20.05.2015
comment
И всего за три месяца две из трех ссылок были разорваны. - person Peter Taylor; 30.08.2015
comment
Ссылки исправлены. - person Christoph Wintersteiger; 01.09.2015

arrow_upward
3
arrow_downward

Для вашего примера вы должны написать что-то вроде этого

(declare-const a (_ BitVec 2))
(declare-const b (_ BitVec 6))
(assert (= a #b01))
(assert (= b ((_ repeat 3) a)))

(declare-const c (_ BitVec 4))
(declare-const d (_ BitVec 4))
(assert (= c #b0001))
(assert (= d ((_ rotate_left 2) c)))

(check-sat)
(get-model)

Ты получишь

sat
(model 
  (define-fun d () (_ BitVec 4)
    #x4)
  (define-fun c () (_ BitVec 4)
    #x1)
  (define-fun b () (_ BitVec 6)
    #b010101)
  (define-fun a () (_ BitVec 2)
    #b01)
)

Хорошим документом, который я обычно использую, является его API.

person dejvuth    schedule 19.05.2015
comment
Как показывает Дейвут, Repeat — это параметрическая функция, т. е. в ней есть параметр, а не аргумент, и синтаксис SMT2 для этого — (_ ... ). То же самое относится ко многим другим функциям и видам вроде (_ BitVec...). - person Christoph Wintersteiger; 19.05.2015
comment
@ChristophWintersteiger Спасибо. Я понятия не имел, почему обучающие программы сделали что-то (_ BitVec 4), потому что это не объясняется ни в одном из документов, которые я смог найти. Где ты этому научился? - person Thinkerton; 20.05.2015
comment
@dejvuth, я не понимаю. Как вы поняли это из ссылок API? При поиске повтора я вижу такие вещи, как Z3_OP_REPEAT Повторить бит-вектор n раз. которые не дают подробностей, и такие вещи, как Z3_mk_repeat (__in Z3_context c, __in unsigned i, __in Z3_ast t1), о которых я никогда бы не догадался, означают, что использование в сценариях похоже на ((_ повтор 3) a). - person Thinkerton; 20.05.2015
comment
К сожалению, API - это все, что у меня есть. (Возможно, @christoph может помочь вам больше.) В любом случае, API можно использовать косвенно для изучения синтаксиса, например. Context ctx = new Context(); BoolExpr be = ctx.mkEq(d, ctx.mkBVRotateLeft(2, c)); System.out.println(be);, где d и c равны BitVecExpr. Я знаю, что это не идеально... - person dejvuth; 20.05.2015