Bug #5401
closederror at ru/ispras/fortress/solver/constraint/ArrayTestCase.java
100%
Description
Приведенный в тесте ru/ispras/fortress/solver/constraint/ArrayTestCase.java пример на языке SMT-LIB не выполняется решателем Z3:
[log]
Z3: ERROR: unexpected character sat ((a (_ as-array k!1))) ((v (_ as-array k!0))) (model (define-fun v () (Array Int Int) (_ as-array k!0)) (define-fun a () (Array Int Int) (_ as-array k!1)) (define-fun k!0 ((x!1 Int)) Int 0) (define-fun k!1 ((x!1 Int)) Int (ite (= x!1 37) 37 0)) )
[/log]
Код на SMT-LIB:
[code]
(define-sort ARRAY_TYPE () (Array Int Int))
(declare-fun a () ARRAY_TYPE)
(declare-fun v () ARRAY_TYPE)
(assert (= a (store v 37 37)))
(assert (= a '((37 37))))
(check-sat)
(get-value (a))
(get-value (v))
(get-model)
(exit)
[/code]
Updated by Artem Kotsynyak about 10 years ago
Приведённый пример является псевдо- SMT, потому что язык не поддерживает литералы для массивов, кроме константных (т.е. возвращающих одно значение по всем ключам, если только это не расширение Z3, уже не помню). На самом деле код транслируется в следующее:
(declare-const DefaultArrayLiteral!1 (Array Int Int))
(define-sort ARRAY_TYPE () (Array Int Int))
(declare-fun a () ARRAY_TYPE)
(declare-fun v () ARRAY_TYPE)
(assert (= a (store v 37 37)))
(assert (= a (store DefaultArrayLiteral!1 37 37))
(check-sat)
(get-value (a))
(get-value (v))
(get-model)
(exit)
Updated by Sergey Smolov about 10 years ago
Понятно. Тогда предлагаю свести исправление ошибки к замене следующей строчки в комментарии:
The constraint as described in the SMT-LIB language
Не надо вводить общественность в заблуждение:-)
Updated by Sergey Smolov about 10 years ago
- Status changed from Resolved to Verified
Updated by Andrei Tatarnikov almost 10 years ago
- Status changed from Verified to Closed
- % Done changed from 0 to 100
- Published in build set to 141226