GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-17 13:01:31 +03:00
Code Issues Projects Releases Wiki Activity
779 Commits 68 Branches 28 Tags 95 MiB
88e5965e7f
Commit Graph

779 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Brian Huffman
8ddec0a2bc Adapt to use new Data.SBV.Dynamic API in SBV-4.3 2015-04-30 13:53:24 -07:00
Adam C. Foltzer
10dcfd7243 Merge branch 'releases' into master from 2.2.2 
We accidentally forgot to merge the 2.2.2 changes back into master, but
since they were mostly temporary fixes pending SBV updates, this didn't
cause any problems. This commit is just to be tidy :)
 2015-04-30 13:51:51 -07:00
Adam C. Foltzer
0f04f0753d Merge branch 'hotfix/2.2.2' into releases 2015-04-30 13:49:20 -07:00
Brian Huffman
4eb2d6734b Fix fastTypeOf to handle selectors in the presence of type synonyms 2015-04-22 16:19:51 -07:00
Iavor S. Diatchki
aeb5ef6e6f Another way to represent simplification strucuture 2015-04-21 17:03:44 -07:00
Iavor S. Diatchki
37c3d9af06 Correct rule for LenFromThen x y w == 0. 
LenFromThen never returns an empty list
 2015-04-21 14:22:28 -07:00
Iavor S. Diatchki
05ef4d410f Merge branch 'master' of github.com:GaloisInc/cryptol 2015-04-20 17:07:36 -07:00
Iavor S. Diatchki
40b1407401 A few more special cases 2015-04-20 17:04:37 -07:00
Iavor S. Diatchki
3c12a27cb0 Fix minimization algorithm 2015-04-20 16:40:37 -07:00
Brian Huffman
7df1b1d08a Fix endian-ness bug in (^^) introduced in b6b7e18adb. 
Fixes #203.
 2015-04-20 14:45:11 -07:00
Iavor S. Diatchki
8c997d353d Handle addition and subtraction together. 2015-04-20 13:50:52 -07:00
Iavor S. Diatchki
6d22474a9f Merge branch 'master' of github.com:GaloisInc/cryptol 2015-04-20 11:53:18 -07:00
Iavor S. Diatchki
e9646b74bf Add a flag for verbose constraint solving. 2015-04-20 11:51:49 -07:00
Dylan McNamee
f12f7d82eb lg2 -> width 2015-04-20 10:00:25 -07:00
Iavor S. Diatchki
58bb7254da Remove old stuff 2015-04-17 16:19:43 -07:00
Iavor S. Diatchki
a0d669fd48 Factor out simplification of summands 2015-04-17 14:07:57 -07:00
Iavor S. Diatchki
8df51593b7 Improve simplifification of addition 2015-04-17 10:20:21 -07:00
Iavor S. Diatchki
819e71a667 Bugfix in the simplification rules 2015-04-17 09:39:50 -07:00
Iavor S. Diatchki
d5a384196b Simplify things a bit, still not quite reasonable 2015-04-16 16:01:39 -07:00
Iavor S. Diatchki
2c805ae6b4 Add a case for comparing with width above 2015-04-15 17:29:54 -07:00
Iavor S. Diatchki
74b56d8943 Remove unused stuff (some of it will may have to come back later) 2015-04-15 16:12:07 -07:00
Iavor S. Diatchki
9dde9ef1d6 Fix the one panic. Also check-point on other work. 2015-04-15 16:06:37 -07:00
Iavor S. Diatchki
0a3c306da8 Reuse some code in the defaulting mechanism. 2015-04-15 11:48:38 -07:00
Iavor S. Diatchki
aed01b03bc Reuse getVal function; work with Nat' rather than Expr in models 2015-04-15 10:29:23 -07:00
Iavor S. Diatchki
9ef11524e0 Fix documentation for check, and return a more reasonable return type. 2015-04-15 09:47:11 -07:00
Adam C. Foltzer
6ecd07da73 move Stackage config out of the way 
This was rolled into 5768dac, but I don't want to take all of those
changes for this release
 2015-04-10 11:25:58 -07:00
Adam C. Foltzer
9eaaa5b8de replace note about cvc4 on PATH 2015-04-10 11:23:00 -07:00
Adam C. Foltzer
2e44c44e2b note about CVC4 from Homebrew 2015-04-10 11:23:00 -07:00
Adam C. Foltzer
53c6283daf update readme with Homebrew info 2015-04-10 11:23:00 -07:00
Adam C. Foltzer
9660f251c2 fix #197 
Remove the autoconf hooks from Setup.hs and bump cabal version
requirement so that `license-files` is supported
 2015-04-10 11:23:00 -07:00
Adam C. Foltzer
ce36319f09 add upper bound to SBV; bump version 2015-04-10 11:22:38 -07:00
Adam C. Foltzer
52bd3fe996 replace note about cvc4 on PATH 2015-04-10 10:59:47 -07:00
Brian Huffman
711ba43e7b Bump sbv minimum version to 4.3 2015-04-10 10:49:30 -07:00
Brian Huffman
639d9fd9a6 Merge module Cryptol.Symbolic.BitVector into Cryptol.Symbolic.Value 2015-04-09 10:57:42 -07:00
Brian Huffman
24c888a7c0 Merge branch 'master' into sbv-4.3 
# Conflicts:
#	src/Cryptol/Symbolic/Prims.hs
 2015-04-09 10:51:24 -07:00
Brian Huffman
0649723ad5 Adapt to further changes in SBV 4.3 2015-04-08 17:22:35 -07:00
Trevor Elliott
69c9465cab Experiment with defaulting using the SMT solver 2015-04-03 15:12:36 -07:00
Trevor Elliott
0477ed940e Spelling bug 2015-04-02 16:23:52 -07:00
Trevor Elliott
11cfc474b8 Try to keep well-defined constraints within the language of cryptol 2015-04-02 16:11:30 -07:00
Trevor Elliott
d22d0394ab Allow improvement to return additional constraints 2015-04-02 16:10:25 -07:00
Trevor Elliott
4e5847bb16 Spelling bugs 2015-04-02 16:08:09 -07:00
Trevor Elliott
5b3e33e958 Disable logging again 2015-03-31 17:58:27 -07:00
Trevor Elliott
6ecd1b52c2 Log checkLR messages instead of putStrLn 2015-03-31 17:58:04 -07:00
Trevor Elliott
5e0c694d71 Remove unused Solver type 2015-03-31 17:57:23 -07:00
Trevor Elliott
3571768daa Spelling fixes 2015-03-31 17:38:42 -07:00
Trevor Elliott
9c464e5684 Fix a warning 2015-03-31 17:38:12 -07:00
Trevor Elliott
42c6552b54 Upgrade the simple-smt dependency 2015-03-31 17:38:04 -07:00
Adam C. Foltzer
7ceae6630a fix haddocks 2015-03-30 17:08:07 -07:00
Trevor Elliott
3ca8746eb3 Allow expected failures to be ignored 2015-03-30 16:58:33 -07:00
Trevor Elliott
2bba4a6871 Set options before logic for yices 2015-03-30 16:34:04 -07:00