Actions
Task #5433
closed[test] write executable SMT-LIB code at testcase comments
Start date:
11/17/2014
Due date:
% Done:
100%
Estimated time:
Detected in build:
svn
Published in build:
141226
Description
Предлагается в комментариях к jUnit-тестам писать только исполняемый код на SMT-LIB. Например, в ru.ispras.fortress.solver.constraint.BitVectorExtractionTestCase вместо:
[comment]
(declare-const x (_ BitVec 32))
(declare-const y (_ BitVec 8))
(assert (= x (_ bv100 257)))
(assert (= y ((_ extract 0 7) x))
(check-sat)
(get-value (x))
(exit)
[/comment]
нужно писать:
[comment]
(declare-const x (_ BitVec 32))
(declare-const y (_ BitVec 8))
(assert (= x (_ bv257 32)))
(assert (= y ((_ extract 7 0) x)))
(check-sat)
(get-value (x y))
(exit)
[/comment]
Для проверки можно использовать http://rise4fun.com/Z3
Некорректный SMT-LIB и псевдокод на его основе из тестов необходимо изжить.
Actions