Project

General

Profile

Bug #5401

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

Added by Sergey Smolov over 5 years ago. Updated over 5 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 over 5 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 over 5 years ago

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

The constraint as described in the SMT-LIB language

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

#3

Updated by Artem Kotsynyak over 5 years ago

  • Status changed from New to Resolved

r644

#4

Updated by Sergey Smolov over 5 years ago

  • Status changed from Resolved to Verified
#5

Updated by Andrei Tatarnikov over 5 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