ээээ .. и в чём проблема-то ? делаете бинарные аналогично унарным 1) расширяем типы (declare-datatypes () ((TypeOp2 AND XOR и т.д.))) 2) добавляем код для функций (define-fun z3AND ((x Value)(y Value)) Value (bvand x y)) (define-fun z3XOR ((x Value)(y Value)) Value (bvxor x y)) 3) добавляем 2арную дырку (define-fun holeOp2 ((op TypeOp2)(x Value)(y Value)) Value (ite (= op AND) (z3AND x y) (z3XOR x y))) 4) генерим дерево с 0-1-2арными дырками и переменными для них, просим решить. 5) PROFIT
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
asenathwaite
(no subject)
Date: 2013-08-26 08:26 pm (UTC)1) расширяем типы
(declare-datatypes () ((TypeOp2 AND XOR и т.д.)))
2) добавляем код для функций
(define-fun z3AND ((x Value)(y Value)) Value (bvand x y))
(define-fun z3XOR ((x Value)(y Value)) Value (bvxor x y))
3) добавляем 2арную дырку
(define-fun holeOp2 ((op TypeOp2)(x Value)(y Value)) Value
(ite (= op AND) (z3AND x y)
(z3XOR x y)))
4) генерим дерево с 0-1-2арными дырками и переменными для них, просим решить.
5) PROFIT