#
18b62363 |
|
11-Apr-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Get src/n-bit to build given tight-equality
|
#
77404ec9 |
|
29-Oct-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add MOD_ss to srw_ss() If it breaks proofs, this is easy to reverse in a script by doing val _ = diminish_srw_ss ["MOD_ss"] before the old behaviour is being relied upon
|
#
778bb566 |
|
29-Jan-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Clean up some code.
|
#
e6364b62 |
|
01-Apr-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Remove the constant bit$LSB, which was simply arithmetic$ODD. This may break some user proofs. Also tidy-up bitScript and numeral_bitScript.
|
#
994d4858 |
|
27-Aug-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Overhaul to rich_listTheory (it had become a bit of a disaster area). Some points: 1. rich_listTheory now uses the same constant names that are used in listTheory, e.g. TAKE instead of FIRSTN. 2. listTheory theorems are no longer replicated (saved again) in rich_listTheory. This avoids DB.match returning multiple instances of the same theorem. It also avoids saving around 100 theorems twice — in some cases after re-proving them. 3. Compatibility is now maintained though a bunch of SML "val" assignments added using adjoin_to_theory, e.g. val ZIP_FIRSTN_LEQ = ZIP_TAKE_LEQ val ALL_DISTINCT_SNOC = listTheory.ALL_DISTINCT_SNOC 4. Some incompatibilities are introduced: * FRONT___LENGTH is deleted, since it is the same as rich_listTheory.LENGTH_FRONT. * COUNT_LIST___ADD -> COUNT_LIST_ADD * COUNT_LIST___COUNT -> COUNT_LIST_COUNT * The compute theorems for COUNT_LIST and SPLITP have been renamed. * Some other theorems are no longer saved, e.g. rich_listTheory.list_INDUCT 5. Some theorems in listTheory have gained quantifiers.
|
#
a2328149 |
|
23-Sep-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Adopt ML-style syntax for case expressions and use freed up "||" for bitwise-or. See issue #24.
|
#
08369277 |
|
04-Apr-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
A few extra theorems.
|
#
2e079a71 |
|
29-Mar-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added new operations for shifting by a bit-vector value, namely: LSL: <<~ LSR: >>>~ ASR: >>~ ROR: #>>~ ROL: #<<~ These are supported by the procedures in blastLib. For example, one can prove w <+ 10w /\ s <+ 3w ==> w <<~ (s + 1w) <+ 73w : word16 The time-complexity is a pretty shocking but "simple" 32-bit problems seem to be okay. NB. ROR and ROL only bit-blast with word sizes that are a power of two. Added a new conversion WORD_MOD_BITS_CONV for mapping applications of ``word_mod w (n2w n)`` into ``(h -- 0) w`` where n is a power of two. Also added support for bit-blasting arbitrary multiplication, but the word-size limit is set to 8 bits by default. Things seem to be just about feasible with that limit (and become horrendously slow after that). To improve performance, the conversion BBLAST_CONV does not have exactly the same coverage as before. For backward compatibility, a conversion EBLAST_CONV (which calls SAT at every bit position) is now available.
|
#
5650aab7 |
|
16-Aug-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Remove Unicode that has crept in to some source scripts.
|
#
cf46facb |
|
25-Jun-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix handling of quantifiers in BBLAST_CONV. For example, was previously converting ``!a. P a`` to ``!a. P a = T`` instead of ``(!a. P a) = T``. Few other minor tweaks.
|
#
4d386328 |
|
26-May-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added a bit-blasting conversion: BBLAST_CONV. This goes beyond the capabilities of WORD_BIT_EQ_CONV by expanding out additions / subtractions. This allows the new conversion to automatically handle small but tricky bit vector goals. For example: ``(x && 3w = 0w:word32) ==> ((x + 4w * y) && 3w = 0w)`` and ``!a:word8. a <+ 4w /\ b <+ a /\ c <=+ 5w ==> (b + c) <=+ 7w`` (These aren't provable with wordsLib.WORD_DECIDE.) Obviously bit-blasting is a brute force approach, so the new conversion should be used with care. It will only work well for smallish word sizes and when there is only and handful of additions around. It is also "eager" -- additions are expanded out even when not strictly necessary. For example, in ``(a + b) <+ c /\ c <+ d ==> (a + b) <+ d:word32`` the sum ``a + b`` is expanded. Users may be able to achieve speed-ups by first introducing abbreviations and then proving general forms, e.g. ``x <+ c /\ c <+ d ==> x <+ d:word32`` The conversion handles most operators, however, the following are not covered / interpreted: -- Type variables for word lengths, i.e. terms of type ``:'a word``. -- General multiplication, i.e. ``w1 * w2``. Multiplication by a literal is okay, although this may introduce many additions. -- Bit field selections with non-literal bounds, e.g. ``(exp1 -- exp2) w``. -- Shifting by non-literal amounts, e.g. ``w << exp``. -- ``n2w exp`` and ``w2n w``. Also w2s, s2w, w2l and l2w. -- word_div, word_sdiv, word_mod and word_log2.
|