0.4 open Features: support for CVC4; simple constraint solver(s); structures 80% 48 issues (38 closed — 10 open) 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