Rob Dockins
|
442d9eec4b
|
Generalize >>$ to accept Integral shift amounts.
|
2020-05-14 14:59:54 -07:00 |
|
Rob Dockins
|
8da51d3eb0
|
Rearrange evaluation backends to follow new typeclass structures
|
2020-05-14 14:58:12 -07:00 |
|
Rob Dockins
|
07865237cf
|
Enumerate the bits of a bounded integer in a different way
|
2020-05-14 09:34:37 -07:00 |
|
Rob Dockins
|
3b910b9d70
|
Fixup/clean some of the what4 primitives
|
2020-05-14 09:33:51 -07:00 |
|
Rob Dockins
|
dc4efc4482
|
specialize the type of the lg2 primitive
|
2020-05-14 09:32:05 -07:00 |
|
Rob Dockins
|
f6b929ace4
|
Implement (^^) via square-and-multiply rather than making it a primitive.
|
2020-05-14 09:23:58 -07:00 |
|
Rob Dockins
|
97d99072a0
|
Fix the solver code for Integral. It was previously failing too
early if sequence element type is a variable.
|
2020-05-14 09:18:30 -07:00 |
|
Brian Huffman
|
9424752b45
|
Specialize types of signed div/mod operators (/$) and (%$) to bitvectors.
|
2020-05-13 17:19:18 -07:00 |
|
Brian Huffman
|
dbd1543548
|
Generalize shift/rotate operations to class 'Index'.
|
2020-05-13 17:17:28 -07:00 |
|
Brian Huffman
|
09cf32060f
|
Generalize indexing operations to class 'Integral'.
|
2020-05-13 14:01:29 -07:00 |
|
Rob Dockins
|
202ddba695
|
Remove the Arith class from the typechecker, and replace it with
the new numeric clasess `Ring`, `Integral`, `Field`, and `Round`.
|
2020-05-13 13:28:03 -07:00 |
|
Rob Dockins
|
ada7f8ee9c
|
Fix errors in prelude modifications
|
2020-05-13 13:25:37 -07:00 |
|
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 |
|