Rob Dockins
|
941f5a6b02
|
Revert "Remove the SignedCmp class and specialize the signed comparison operations"
This reverts commit ba99cc4924.
|
2020-05-13 09:39:29 -07:00 |
|
Rob Dockins
|
ba99cc4924
|
Remove the SignedCmp class and specialize the signed comparison operations
to bitvector types.
|
2020-05-12 17:42:52 -07:00 |
|
Rob Dockins
|
fdf52a64a5
|
Update Cryptol.cry based on discussions
|
2020-05-12 17:41:45 -07:00 |
|
Rob Dockins
|
625ee990dc
|
Update Cryptol.cry with concrete design changes to support splitting the Arith class
|
2020-05-12 12:46:09 -07:00 |
|
Kevin Quick
|
e914ceff01
|
Update what4 submodules.
|
2020-05-12 09:44:53 -07:00 |
|
Kevin Quick
|
107b709cbd
|
Merge pull request #721 from GaloisInc/ghc8.10
Updates for haskeline 0.8 and use of exceptions package.
|
2020-05-12 08:57:31 -07:00 |
|
Kevin Quick
|
e4c0f9e41f
|
Select exceptions/MonadExceptions from haskeline version, not base.
|
2020-05-11 11:30:34 -07:00 |
|
Kevin Quick
|
135df682da
|
Update what4 submodule revision.
|
2020-05-08 09:26:42 -07:00 |
|
Kevin Quick
|
4604fc54f5
|
Adjust base version compatibility check.
|
2020-05-07 14:08:56 -07:00 |
|
Kevin Quick
|
a78c1574db
|
Re-enable minimum functionality for older haskeline/GHC versions.
|
2020-05-07 10:04:12 -07:00 |
|
Kevin Quick
|
393451681b
|
Updates for haskeline 0.8 and use of exceptions package.
|
2020-05-06 14:16:53 -07:00 |
|
Iavor Diatchki
|
5c16d01e3f
|
Update CHANGES to reflect recent fixes
|
2020-05-05 15:56:01 -07:00 |
|
Iavor Diatchki
|
2219aca55c
|
Document lifted selectors.
Fixes #303
|
2020-05-05 14:59:45 -07:00 |
|
Iavor Diatchki
|
c3eca4f22a
|
Check that the declared type of prims matches the expected one.
Fixes #711
|
2020-05-05 14:30:25 -07:00 |
|
Aaron Tomb
|
6adec7f771
|
Update README with new NSA group name (#717)
Closes #679.
|
2020-05-05 11:12:04 -07:00 |
|
Rob Dockins
|
7e841e915f
|
Bump what4 submodule
|
2020-04-27 14:19:44 -07:00 |
|
Rob Dockins
|
364d586c7c
|
Bump what4 submodule
|
2020-04-27 14:19:44 -07:00 |
|
Rob Dockins
|
c04bcdf633
|
Update appveyor config
|
2020-04-27 14:19:44 -07:00 |
|
Rob Dockins
|
402ecf20dd
|
update travis and cabal.freeze files
|
2020-04-27 14:19:44 -07:00 |
|
Rob Dockins
|
ed9742be5c
|
Use panic instead of fail
|
2020-04-27 14:19:44 -07:00 |
|
Rob Dockins
|
85d727720d
|
Add sbv-any and sbv-offline to the no-warnings list
|
2020-04-27 14:19:44 -07:00 |
|
Rob Dockins
|
525ca4a6ec
|
Track what4 updates. Transition to use bvAtBE bvSetBE, etc.
|
2020-04-27 14:19:44 -07:00 |
|
Rob Dockins
|
8c9b9e9c53
|
Add "prefixed" versions of the SBV backend solvers in addition
to the default unprefixed ones (which are currently still
SBV-based).
|
2020-04-27 14:19:44 -07:00 |
|
Rob Dockins
|
d1bc32ba97
|
Update CHANGES
|
2020-04-27 14:19:44 -07:00 |
|
Rob Dockins
|
904220c806
|
Add What4 provers alongside the SBV provers with names such as w4-z3,
`w4-yices`, etc. Implement What4 based "offline" solving using
the pseudo-solver name `w4-offline`.
|
2020-04-27 14:19:44 -07:00 |
|
Rob Dockins
|
aaa0ea1744
|
Improve the what4 symbolic frontend. Individual solvers can
now be selected, and multisat queries are now supported.
|
2020-04-27 14:19:44 -07:00 |
|
Rob Dockins
|
5277c80522
|
Do explicit modular reduction for Z operations when the inputs are concrete.
|
2020-04-27 14:19:44 -07:00 |
|
Rob Dockins
|
922350ff7a
|
Put together enough of the framework required to run :sat and :prove
queries via What4. We still need to support configuring the solver to use,
multisat queries, and portfolio solving.
|
2020-04-27 14:19:44 -07:00 |
|
Rob Dockins
|
44a2b8e236
|
Very basic scaffolding for using what4 as a symbolic backend
|
2020-04-27 14:19:44 -07:00 |
|
Rob Dockins
|
1e1f7af812
|
Fix the haskeline package upper bound
|
2020-04-23 17:37:53 -07:00 |
|
robdockins
|
f29f0158ff
|
Merge pull request #703 from GaloisInc/issue702
issue702
|
2020-04-23 12:22:25 -07:00 |
|
brianhuffman
|
aa6030ba07
|
Merge pull request #708 from GaloisInc/fix-iterate
Redefine prelude function `iterate` to preserve sharing.
|
2020-04-22 11:22:17 -07:00 |
|
Brian Huffman
|
4dd77c756b
|
Update type variable numbering in test suite output.
|
2020-04-20 11:29:49 -07:00 |
|
Brian Huffman
|
0203244cd6
|
Redefine prelude function iterate to preserve sharing.
Fixes #707.
|
2020-04-18 08:12:40 -07:00 |
|
brianhuffman
|
30b41e9c45
|
Merge pull request #700 from GaloisInc/fix-warnings
Fix warnings about redundant imports.
|
2020-04-18 06:34:52 -07:00 |
|
Rob Dockins
|
ce85155dbe
|
Add unit test for issue702
|
2020-04-17 17:48:44 -07:00 |
|
Rob Dockins
|
9434236cbd
|
Enforce a canonical field ordering in the field type constructor for FinType
This solves another manifestation of issue #702.
|
2020-04-17 17:48:28 -07:00 |
|
Rob Dockins
|
194d02d06d
|
Sort the fields of a record type before comparing with the fields in
a concrete value in `toExpr`.
Fixes #702
|
2020-04-17 17:09:58 -07:00 |
|
robdockins
|
d8bf07320f
|
Merge pull request #638 from rjnw/master
Fix for freevars and adding some exports.
|
2020-04-17 16:25:01 -07:00 |
|
Brian Huffman
|
21a09179ff
|
Fix warnings about redundant imports.
|
2020-04-09 13:10:29 -07:00 |
|
Rob Dockins
|
c83f831763
|
Fix benchmark suite
|
2020-04-03 14:47:16 -07:00 |
|
robdockins
|
87ad864185
|
Merge pull request #684 from GaloisInc/eval-refactor
Evaluator refactor
|
2020-04-02 09:42:04 -07:00 |
|
Rob Dockins
|
d08046d063
|
Test case for issue #662
|
2020-04-02 09:40:44 -07:00 |
|
Rob Dockins
|
4c6424c8a7
|
Fix for #662.
This fix interprets integer division as "round down" division
in the symbolic simulator, to match the behavior of the concrete
simulator.
|
2020-03-30 22:53:10 -07:00 |
|
Rob Dockins
|
943e11478a
|
Add regression test for word updates
|
2020-03-30 15:09:53 -07:00 |
|
Rob Dockins
|
cfef882fe5
|
Minor tweaks in the concrete evaluator
|
2020-03-30 13:40:59 -07:00 |
|
Rob Dockins
|
bdfd4e6bc0
|
Add INLINE and SPECIALIZE pragmas to generate better code for the
concrete evaluator.
|
2020-03-30 13:01:06 -07:00 |
|
Rob Dockins
|
34ce8ecc00
|
Change uses of Z 0 to cause panics. The type constraints for
`Z` should make these cases impossible.
|
2020-03-30 09:54:27 -07:00 |
|
Rob Dockins
|
c94c929354
|
Comment tweaks
|
2020-03-30 09:35:00 -07:00 |
|
Iavor S. Diatchki
|
761930257d
|
Merge pull request #690 from GaloisInc/feature/689
Feature/688
|
2020-03-27 10:25:08 -07:00 |
|