This is a major release with significant changes to the language and the runtime. Rosette 3.0 is not backward compatible with Rosette 2.x. But porting Rosette 2.x code to Rosette 3.0 should be straightforward for most applications.
The semantics of Rosette 3.0 differs from Rosette 2.x in two ways:
current-bitwidthparameter that controls the reasoning precision is set to
#fby default. As a result, symbolic constants that are declared to be integers or reals are interpreted in the theories of integers and reals, respectively. This means that the semantics of assertions over these types follows that of Racket. But reasoning about such assertions is expensive (or undecidable), so Rosette 3.0 still provides the option of approximating integer and real constants with finite-precision bitvectors. The key difference is that programs must now explicitly opt into this approximation by setting
current-bitwidthto a positive integer.
current-bitwidthis set to a positive integer k, the solutions produced by the
debugqueries are guaranteed to be correct under the k-bit semantics for integer and real constants. They are not guaranteed to be sound with respect to the infinite-precision semantics.
- Developed a new symbolic profiler for diagnosing performance issues in Rosette programs. The symbolic profiler instruments Rosette and tracks key performance metrics to identify potential issues. To use the symbolic profiler, run the command
raco symprofile program.rkt. A new performance chapter in the Rosette guide details common performance issues and how to use the symbolic profiler to identify them.
- Extended and generalized the interface to constraint solvers. The new interface allows the client code to specify a path to the solver, set the logic, provide solver-specific configuration options, and export the problem encodings sent to the solver.
- Added support for four new solvers: Boolector, CVC4, Yices, and CPLEX. These solvers are not included in the default distribution and need to be installed separately for use with Rosette.
This release includes bug fixes and the following updates:
- Added support for quantified formulas. Quantifiers can appear in assertions passed to
verifyqueries. They should not be used with
synthesizequeries. When using quantified formulas,
current-bitwidthmust be set to
- Added the
unknownsolution type. An
unknownsolution is returned if the underlying solver cannot decide if a given set of constraints is (un)satisfiable.
- Added the
distinct?predicate that returns true iff all of its arguments are pairwaise un-equal. This has a direct (efficient) translation to Z3 if the arguments are primitive solvable values (booleans, integers, reals, or bitvectors).
This release includes the following updates to Rosette 2.0:
- Added support for the
popinterface to Z3.
- Switched to log-based evaluation for Rosette documentation. Documentation generation no longer depends on Z3.
- Improved the implementation of the lifted
structconstruct. The new implementation is a minimal patch to the corresponding Racket implementation, and it enables creation and use of
structs in the REPL.
- Improved the implementation of
#%top-interactionto disallow mutation of top-level variables in the REPL. This enables definition and use of recursive procedures in the REPL, as well as definition and use of generic interfaces.
This is a major release with significant changes to the language and the symbolic evaluator. Rosette 2.0 is not backward compatible with Rosette 1.x.
This release includes the following features:
New symbolic datatypes.
real?types. These datatypes are translated to the theories of integers and reals if
current-bitwidthis set to
#f. Otherwise, they are translated to bitvectors of length
bitvector?datatype, which embeds the SMT theory of bitvectors into Rosette.
function?datatype, which embeds uninterpreted functions into Rosette.
New solver-aided queries.
Changed the behavior of solver-aided queries to no longer throw exceptions when a model is not found. Instead they return an
verifyqueries to ensure that any solution obtained with finite-precision reasoning is correct under the aribitrary-precision semantics of integers and reals.
optimizequery, which exposes Z3's optimization features.
Improved implementation for the
define-synthaxform and other high-level synthesis constructs.
Improved printing of symbolic values by James Bornholt.
Ported sample SDSLs to Rosette 2.0.
Updated The Rosette Guide to document the new language in detail.
The following features have been removed:
Support for Kodkod and CVC4 solvers.
Support for the
Support for internal logging via
This release includes a new reader for
rosette/safeimplemented by bmastenbrook.
It also includes a fix for a bug in the evaluation of symbolic boxes. Thanks to Alan Borning for reporting it.
It includes two symbolic datatypes:
number?. Assertions over numbers are translated to the theory of bitvectors.
Rosette 1.0 supports the Kodkod, Z3, and CVC4 solvers.
This release also includes the source code for three solver-aided DSLs: WebSynth (web scraping by demonstration), IFC (verification for secure stack machine semantics), and SynthCL (synthesis and verification for an Open-CL imperative language).