The main user visible effect of this might be that sometime things on
the Cryptol command line are instantiated in a slightly different way:
we get `inf` sometimes when we got a finite example before.
We could work around this if it is an issue, but I am not sure which
behavior is more reasonable.
The syntax is just as described in ticket #373: We have a new
declaration form consisting of the keyword 'constraint' followed
by a identifier and optionally a list of type parameters; the
right-hand side is either a single constraint or a parenthesized,
comma-separated list of type constraints. For example:
constraint NonZero n = (fin n, 1 <= n)
last : {n, a} NonZero n => [n]a -> a
last xs = xs!0
Regression test check31 was failing somewhat unpredictably due to the
use of lazy I/O when loading the Z3 prelude for the type checker. Using
the `strict` package seems to fix it.
This commit reorganizes how lexicographic comparisons are done in
the concrete simulator to reuse the same combinator from the symbolic
simulator. This makes it more straightforward to implement the new
signed comparison.
This class will represent types that can be meaningfully compared for
signed bitvector equality. It lifts the comparison operations on
nonempty bitvectors through tuples, records and finite sequences via
lexicographic order.
However, see the following SBV issue that currently affects
Cryptol behavior when computing signed right shifts with
symbolic index amounts:
https://github.com/LeventErkok/sbv/issues/323
It appears to have negligable or negative performance advantages over
the representation on sequence maps. Deleting the additional representation
removes a lot of code paths, and makes things somewhat simpler.
When bitsequences cannot be packed as words, they have been
represented using an explicit sequence datastructure containing
thunks for the individual bits. However, for finite, but very large,
bitsequences this was consuming unacceptable amounts of memory.
When bitvector lengths cross an arbitrarily-designated threshold
(currently 2^16 bits) we instead use a sparse representation based
on SeqMap, similar to the representation used for other finite and
infinite sequence types.
This patch does not add a warning when using 'random' in symbolic expressions.
We currently don't have any organized mechanism for generating warnings during
evaluation, and the value of emitting such a warning is debatable.
Fixes#364
This prevents a loss of desirable sharing in the interpreter, and turns
recursive algorithms with potential sharing from exponential-time to linear
time. It appears to have little impact on other algorithms.
Fixes#432
This fails on Windows and we don't really know how to fix it. The fact
that it always fails masks more interesting failures, so I think it's
better to just skip it for now.
