Project

General

Profile

Bug #5401

error at ru/ispras/fortress/solver/constraint/ArrayTestCase.java

Added by Sergey Smolov about 6 years ago. Updated about 6 years ago.

Status:
Closed
Priority:
Normal
Assignee:
Andrei Tatarnikov
Category:
-
Target version:
Start date:
10/30/2014
Due date:
% Done:

100%

Estimated time:
Detected in build:
svn
Platform:
Published in build:
141226

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]

History

#1

Updated by Artem Kotsynyak about 6 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)

#2

Updated by Sergey Smolov about 6 years ago

Понятно. Тогда предлагаю свести исправление ошибки к замене следующей строчки в комментарии:

The constraint as described in the SMT-LIB language

Не надо вводить общественность в заблуждение:-)

#3

Updated by Artem Kotsynyak about 6 years ago

  • Status changed from New to Resolved

r644

#4

Updated by Sergey Smolov about 6 years ago

  • Status changed from Resolved to Verified
#5

Updated by Andrei Tatarnikov about 6 years ago

  • Status changed from Verified to Closed
  • % Done changed from 0 to 100
  • Published in build set to 141226

Also available in: Atom PDF