Project

General

Profile

0.4

open

Features: support for CVC4; simple constraint solver(s); structures

80%

48 issues   (38 closed — 10 open)

Issues by
Bug

8/9
Feature

9/11
Task

21/28
Related issues
Bug #5775: BitVector.longValue returns incorrect values Actions
Bug #6352: Transformer.standardize returns 'false' on (AND (EQ a 00) (NOT(EQ a b 00))) Actions
Bug #7555: unable to create constraint-related jUnit tests including unused variables Actions
Bug #7557: ConstCastTestCase: java.lang.AssertionError: Calculator failed to substitute result Actions
Bug #8573: missing javadoc Actions
Bug #8676: BitVector's comparison operations return BitVector Actions
Bug #10177: TreeVisitor's SKIP status does not work as expected Actions
Bug #10299: Probably, a bug in BitVector.isAll{Set,Reset} Actions
Bug #10370: class ru.ispras.fortress.solver.constraint.Formulas cannot be cast to class ru.ispras.fortress.solver.constraint.Sat4jFormula Actions
Feature #5377: Не поддерживается работа с несколькими CalculatorEngine Actions
Feature #5451: Support external rules in TransformerRule interface Actions
Feature #5596: Генерация случайных значений, удовлетворяющих определённым условиям Actions
Feature #8203: bv2nat\int2bv operations Actions
Feature #8204: solver-specific header for generated SMT2 files Actions
Feature #8665: Nodes.BVEXTRACT(Node, Node, Node) convenience method Actions
Feature #8667: Nodes.EQ(Node ... nodes) convenience method Actions
Feature #8702: 'public static NodeValue.newBitVector(final boolean value)' convenience method Actions
Feature #8703: 'public static boolean isType(final Node node, final DataType ... types)' convenience method Actions
Feature #8709: 'public static boolean isOperation(final Node node, final T ... opTypes)' convenience method Actions
Feature #9123: calculate DataType for 'BVEXTRACT(i, i, x)' NodeOperation objects Actions
Task #4523: Implementing a solver for simple constraints Actions
Task #4675: Манипуляция с функциями алгебры логики Actions
Task #4713: SMT-LIB structures Actions
Task #5211: Unit-тесты для трансформеров и калькулятора Actions
Task #5421: Utility methods on expression nodes Actions
Task #5450: Support multiple rules per node in NodeTransformer Actions
Task #5478: Implement Transformer.reduce(Node expression) Actions
Task #5529: Использовать префиксы для указания основания в строковом представлении числовых данных Actions
Task #5665: Support for CVC4 Actions
Task #5819: Calculator for bit vectors Actions
Task #5877: InvariantChecks: checkTrue and checkFalse methods Actions
Task #5985: Node ExprUtils.getEquation(Node target, Node value) Actions
Task #5993: boolean ExprUtils.isKind(Node.Kind kind, Node ... nodes) Actions
Task #6124: Suggestion on InvariantChecks.check* methods Actions
Task #6364: SolverResult: implement equals\hashcode methods Actions
Task #6423: to_real, to_int, is_int operations Actions
Task #6831: ESExprParser: improve error messages Actions
Task #7378: NodeTransformer: multiple transform rules for a single enum id Actions
Task #7383: boolean isOperation(final Node expr, final T... opId) Actions
Task #7397: NodeVariable.new<type-of-variable>(final String name) Actions
Task #7402: ExprUtils: ignore repeated Node objects upon conjunction/disjunction construction Actions
Task #7527: constant casting while type conversion Actions
Task #7561: ISampleConstraint: 'getExpectedVariables' returns value that is ignored in jUnit tests Actions
Task #7772: TypeConversion.coerce: transform from MAP to BIT_VECTOR Actions
Task #7846: 'Transformer.reduce(Transformer.substitute(expression, name, term))' convenience method Actions
Task #10002: get Boolector solver from server as dependency Actions
Task #10492: use CVC4 1.8 in testing Actions
Task #10494: check Windows build of Boolector on project tests Actions