Open-Source Projects: Issueshttps://forge.ispras.ru/https://forge.ispras.ru/favicon.ico?16490126692020-09-11T11:03:19ZOpen-Source Projects
Redmine Fortress - Task #10494 (Closed): check Windows build of Boolector on project testshttps://forge.ispras.ru/issues/104942020-09-11T11:03:19ZSergey Smolovsmolov@ispras.ru
<p>Переключиться на ветку <strong>boolector-solver-integrating</strong> и в файле <strong>build.gradle</strong> для SMT-решателя boolector вместо подгрузки его извне (там сейчас подтягивается неработоспособная Windows-сборка) прописать полученную локальную сборку. Затем запустить все jUnit-тесты проекта и убедиться в том, что: а) в тестах участвует Boolector (возможно, не во всех, см. переменную <strong>isSuitableForBoolector</strong> в классе <strong>GenericSolverTestBase</strong> ); б) тесты, в которых задействуется Boolector, проходят.</p> Castle - Task #9999 (Closed): ChangeLog -> ChangeLog.mdhttps://forge.ispras.ru/issues/99992019-12-20T11:57:43ZSergey Smolovsmolov@ispras.ru
<p>Rewrite ChangeLog file to Markdown format.</p> Castle - Task #9998 (Closed): README -> README.mdhttps://forge.ispras.ru/issues/99982019-12-20T11:57:11ZSergey Smolovsmolov@ispras.ru
<p>Rewrite README to Markdown format.</p> Fortress - Task #7772 (Closed): TypeConversion.coerce: transform from MAP to BIT_VECTORhttps://forge.ispras.ru/issues/77722016-11-30T13:31:02ZSergey Smolovsmolov@ispras.ru
<p>Add support for MAP values conversion in TypeConversion.coerce method.</p>
<p>The current use case is to transform "Int -> 0|1" mapping with indices starting from 0, to bit vector value.</p> Castle - Task #6507 (Closed): build.gradle: get ANTLR jar from serverhttps://forge.ispras.ru/issues/65072016-01-14T08:53:59ZSergey Smolovsmolov@ispras.ru
<p>Предлагаю не хранить jar-файл компонента ANTLR непосредственно в репозитории проекта, а подгружать с сервера, как это сделано в Retrascope с библиотекой Antlrworks:</p>
<pre>
dependencies {
compile 'antlr:antlrworks:1.4.3'
...
compile files( "${project.projectDir}/share/jar/fortress.jar"
, ...
)
}
</pre>
<p>Для этого нужно проконсультироваться с Алексеем Демаковым, пусть положит ANTLR на forge.ispras.ru (если его ещё там нет).</p> Fortress - Task #5985 (Closed): Node ExprUtils.getEquation(Node target, Node value)https://forge.ispras.ru/issues/59852015-05-26T09:34:19ZSergey Smolovsmolov@ispras.ru
<p>return new NodeOperation(StandardOperation.EQ, target, value)</p> Fortress - Task #5802 (Closed): NodeValue newZero(DataType dataType)https://forge.ispras.ru/issues/58022015-04-06T07:41:26ZSergey Smolovsmolov@ispras.ru
<p>A convenience method with the following signature is required:</p>
<p><code>NodeValue newZero(DataType dataType)</code></p>
<p>Methods returns "zero value" of the specified data type.</p>
<p>For integer, real, boolean types it returns 0, 0.0, and <code>false</code> respectively (of course, embedded in NodeValue object).</p>
<p>For bit vector type it returns bit vector that contains only zeros.</p>
<p>For map type it returns map that contains only zeros too.</p> Fortress - Task #5600 (Closed): [transformer][ruleset] implement ITE ruleshttps://forge.ispras.ru/issues/56002015-02-05T15:24:54ZSergey Smolovsmolov@ispras.ru
<p>(ITE true x y) -> x<br />(ITE false x y) -> y</p> Fortress - Task #5466 (Closed): [solver] print the input constraint when solver returns ERROR/UNK...https://forge.ispras.ru/issues/54662014-12-04T11:39:13ZSergey Smolovsmolov@ispras.ru
<p>If solver returns an ERROR (or UNKNOWN) verdict, it would be convenient to print not only error code, but the input constraint too.</p> Fortress - Task #5464 (Closed): [solver] boolean expressions casting into bit vectorshttps://forge.ispras.ru/issues/54642014-12-04T07:07:25ZSergey Smolovsmolov@ispras.ruFortress - Task #5447 (Closed): [transformer][ruleset] стандартизация константных выражений вида ...https://forge.ispras.ru/issues/54472014-11-25T14:57:59ZSergey Smolovsmolov@ispras.ru
<p>Предлагается добавить ещё такие правила в стандартный набор:</p>
<p>x EQ y -> false<br />x EQ x -> true</p>
<p>где x и y - разные константы(NodeValue).</p> Fortress - Task #5424 (Closed): [transformer][ruleset] дополнительные правила стандартизацииhttps://forge.ispras.ru/issues/54242014-11-12T17:23:06ZSergey Smolovsmolov@ispras.ru
<p>Возникла острая необходимость в реализации следующих правил:</p>
<p>(and true e) -> e<br />(and false e) -> false<br />(or true e) -> true<br />(or false e) -> e</p>
<p>где e - булевская переменная</p> Fortress - Task #5419 (Closed): [transformer][ruleset] реализовать правило expr==false -> NOT(exp...https://forge.ispras.ru/issues/54192014-11-12T07:07:51ZSergey Smolovsmolov@ispras.ru
<p>Правила, описанные в классе ru.ispras.fortress.transformer.ruleset.Predicate, преобразуют только операции.<br />Предлагается добавить ещё одно правило "канонизации", преобразующее значения:</p>
<p>выражение expr==false преобразовывать в !(expr == true).</p>
<p>Правило нужно включить в стандартный набор.</p> Fortress - Task #5229 (Closed): [transformer] Упрощение выражений с LOGIC_BOOLEANhttps://forge.ispras.ru/issues/52292014-08-29T11:57:13ZSergey Smolovsmolov@ispras.ru
<p>Сейчас в Fortress реализовано упрощение выражений, использующих только значения типа LOGIC_INTEGER.</p>
<p>Необходимо реализовать упрощение (Transformer.reduce) выражений, использующих значения типа LOGIC_BOOLEAN.</p>
<p>Для этого можно реализовать класс StandardOperationsBoolean (по аналогии с классом StandardOperationsInt) и зарегистрировать в классе Calculator.</p> Fortress - Task #4713 (New): SMT-LIB structureshttps://forge.ispras.ru/issues/47132014-03-17T06:59:53ZSergey Smolovsmolov@ispras.ru
<p>Реализовать поддержку структур (record) как типа данных языка SMT-LIB.</p>