777 Commits

This Branch

This Branch

All Branches

Author	SHA1	Message	Date
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
Iavor S. Diatchki	75c8d4d2d6	Merge branch 'wip/cs' of github.com:GaloisInc/cryptol into wip/cs ... Conflicts: cryptol.cabal	2015-03-30 16:28:02 -07:00
Trevor Elliott	3203128b40	Merge remote-tracking branch 'origin/master' into wip/cs	2015-03-30 16:25:25 -07:00