Fortress

The new release contains the following changes:

• Convenience methods BitVector.field and ExprUtils.isKind were implemented
• Some bug fixes and general code improvements were made

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

The new release contains the following changes:

• Support for the POWER operation in calculator (for integers)
• Some general improvements

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

The new release contains the following changes:

• Utility general-purpose class Result was implemented
• Utility method newInteger for BigInteger was added to NodeValue
• Some general code improvements were made

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

The new release contains the following changes:

• Type calculation rules for the BVZEROEXT, BVSIGNEXT, SELECT and STORE operators were implemented
• The BitVector class was improved

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

The new release contains the following changes:

• A couple of new utility methods were added
• Some general code improvements were made

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

The new release contains the following changes:

• Support for CVC4 was implemented
• Support for bit vectors, arrays and real numbers in calculator were implemented
• Additional rules for expression transformer were implemented
• Some bug fixes and general code improvements were made

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

Installation note:

In the new version, the Environment.setSolverPath method is no longer available since it causes controversy when several solvers are used. To set up the path to an external solver, you need to use the setSolverPath method of the corresponding solver object. For example:

final Solver solver = SolverId.Z3_TEXT.getSolver();
solver.setSolverPath("tools/z3/bin/z3.exe");

Another way is to set up the Z3_PATH and CVC4_PATH environment variables for the Z3 and CVC4 solvers correspondingly.

The new build contains the following changes:

• Some bug fixes and code improvements were made

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

The new build contains the following changes:

• Classes for representing and building random variates were implemented

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

The new build contains the following changes:

• Convenience methods simplifying access to expression value and type information were implemented
• The expression transformer facility was enhanced
• The possibility to control the order of visiting operands of an expression was implemented

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

The new release includes the following changes:

• Methods for converting BitVector from and to BigInteger
• Class NodeBinding that provides support SMT-LIB let-constructs
• Basic support for managing symbolic S-expressions
• Support for arbitrary size integers (LOGIC_INTEGER is based on BigInteger)
• Textual representation of a constraint is included in error log when solver fails
• Utility method ExprUtils.isSAT for checking satisfiability of expressions
• Utility method ExprUtils.getVariables for getting the list of variables contained in an expression
• Class CollectionUtils that contains utility methods for manipulating collections
• Class ConstraintUtils that provides methods to simplify creating and solving constraints
• Improvement in solver implementation that allows interpreting boolean operands of bit vector operators as bit vectors of length 1
• Debug and silent modes for SMT solvers (in the silent mode .smt files are not saved in file system after a constant has been solved)
• Support for the BVEXTRACT operator in expression type calculation logic
• Class DataMap for representing data of the MAP type
• New rules for expression transformation in the predefined rule set

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