Fortress v0.3.3 released

Fortress v0.3.3 has been released.
Added by Andrei Tatarnikov almost 10 years ago

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

Fortress