Project

General

Profile

News

Fortress v0.3.2 released

Added by Andrei Tatarnikov about 10 years ago

Fortress v0.3.2 has been released.

The new release includes the following changes:

  • Factory methods to simplify creating NodeValue objects
  • Support for creating deep copies of expressions
  • Utility classes for generating random values
  • Support for a variable number of operands in the expression calculator
  • Saving/loading constraints to/from an XML string
  • Aborting visiting an expression tree and skipping subtrees
  • Basic facilities to calculate the type of an expression
  • Extending the functionality of a solver with function templates
  • New standard operations: ABS, MIN, MAX, BVANDR, BVNANDR, BVORR, BVNORR, BVXORR, BVXNORR
  • Class NodeExpr was renamed to NodeOperation
  • XML format was simplified: nodes Expression and Operation were merged together (the new node is called Operation)
  • Class ExprUtils that provides a set of useful methods to work with logical expressions
  • Expression printers for Verilog and VHDL hardware description languages
  • Support for the boolean type in the calculator

The library can be downloaded from here: http://forge.ispras.ru/projects/solver-api/files

Fortress v0.3.0 released

Added by Sergey Smolov almost 11 years ago

Fortress v0.3.0 (a redesigned version of Java Constraint Solver API) has been released.

The new release includes the following changes:

  • the library was redesigned and renamed to Fortress
  • the library was decomposed into a set of reusable packages (including data, expression, calculator, transform, solver)
  • new classes for describing data were implemented (including a new bit vector implementation)
  • a lot of refactoring has been done
  • a number of bugs was fixed

The library can be downloaded from the page http://forge.ispras.ru/projects/solver-api/files

Java Constraint Solver API v0.1.1 released

Added by Sergey Smolov over 11 years ago

Java Constraint Solver API v0.1.1 has been released. The following things have been done:

  • Constraints creating (in the form of abstract syntax trees)
  • Constraints mapping to the SMT-LIB description (in this version only binary operations are supported)
  • Constraints storing in external memory (as XML files)
  • Z3 solver launching and transferring results back to Java

The library can be downloaded from the page http://forge.ispras.ru/projects/solver-api/files

(41-46/46)

Also available in: Atom