Kevin Quick
33b9c7aa15
Increase indentation for config help for readability.
2021-04-28 08:09:11 -07:00
Kevin Quick
ac82d34485
Include root node in configHelp and getConfigValues
2021-04-28 08:08:53 -07:00
Kevin Quick
9660b4a27b
Fix option configHelp retrieval with blank input
2021-04-28 08:08:27 -07:00
Kevin Quick
a69c2cea9e
Update deprecation to consider more cases and nesting; add tests.
2021-04-28 08:07:47 -07:00
Kevin Quick
2e43136d0b
Adding the same Option to Config multiple times is idempotent, not a failure.
2021-04-26 11:55:59 -07:00
Kevin Quick
5d9db797ba
Add OptGetFailure and OptCreateFailure exceptions to replace config fail calls.
2021-04-26 11:55:44 -07:00
Kevin Quick
2749035ec4
Add explicit set routines for Unicode, Integer, and Bool options.
2021-04-26 11:55:15 -07:00
Kevin Quick
a957690f2e
Add deprecatedOpt wrapper to mark deprecated options
2021-04-26 11:54:39 -07:00
Kevin Quick
40bbdd1745
Fix formatting for enum and list option setting failures.
2021-04-26 11:49:54 -07:00
Kevin Quick
6c63070186
Replace option setting fail call with explicit exception.
2021-04-26 11:49:39 -07:00
Kevin Quick
206b66c1a4
Update adapter tests and online solver tests to recognize abc solver version.
2021-04-26 11:48:53 -07:00
Kevin Quick
c02d8a85a7
Add comments describing the ResponseStrictness mode values.
2021-04-26 09:14:35 -07:00
Kevin Quick
0857946b4e
Use variable bindings instead of flip.
2021-04-26 09:13:36 -07:00
Kevin Quick
cc5eab69a2
Remove duplicate step in github workflow
2021-04-20 09:59:42 -07:00
Kevin Quick
3a1e655c47
Explicitly enable tests in github workflow cabal configuration.
2021-04-20 09:59:42 -07:00
Kevin Quick
06f883ce76
STP solver can use default newDefaultWriter implementation.
2021-04-20 09:59:42 -07:00
Kevin Quick
0aacb3a1f4
Remove stdin/stdout duplicate from Solver; use values from WriterConn.
2021-04-20 09:59:42 -07:00
Kevin Quick
dc7fd65042
More SMTLib2 response parsing.
2021-04-20 09:59:42 -07:00
Kevin Quick
73b81b8431
Add solver.strict_parsing config option to control parsing strictness.
2021-04-20 09:59:41 -07:00
Kevin Quick
c5ce7c4cdb
Add Response parsing module for common response handling (with tests).
2021-04-20 09:59:41 -07:00
Kevin Quick
5e994aefbf
Parsing via smtAckResult is now total, more targeted, and shows failures.
2021-04-20 09:59:41 -07:00
Kevin Quick
1d38fa8559
Smaller scope of stderr variable for solver shutdown/cleanup
2021-04-20 09:59:41 -07:00
Kevin Quick
2b4273c818
Merge remote-tracking branch 'refs/remotes/origin/master'
2021-04-19 15:57:42 -07:00
Kevin Quick
62f338d838
Add darcs and emacs backups to .gitignore.
2021-04-19 15:57:15 -07:00
Aaron Tomb
367cdd0240
Fix bug in printing Verilog rotations for ABC ( #114 )
...
This code accidentally included Cryptol type annotations in the Verilog output (because the `bv-sized` pretty-printer includes them). Hilariously, we didn't detect this because ABC can still correctly read the result due to its very permissive parser that skips over things it doesn't understand. Attempting to load files containing rotates into Yosys, which includes a stricter Verilog parser, uncovered the error.
2021-04-15 14:02:27 -07:00
Aaron Tomb
91200aa395
Support Verilog modules with multiple outputs ( #112 )
...
Adds support for generating Verilog modules from multiple What4 expressions, rather than a single one.
2021-04-06 11:06:21 -07:00
Kevin Quick
bb38b0ccc7
Merge pull request #111 from GaloisInc/nopartialfields
...
Remove use of partial fields and add warning.
2021-03-25 14:08:13 -07:00
Kevin Quick
e09e2edffd
Use stable nix version to ensure GHC availability in CI.
2021-03-25 08:44:19 -07:00
Kevin Quick
320b966f1d
Remove use of partial fields and add warning.
...
Partial fields are the situation where an ADT is defined with record
syntax. The field accessors are of type `ADT -> field`, but the field
is only valid for one constructor of the ADT, so proper usage requires
matching on the constructor before using field accessors, and omitting
this matching can lead to invalid accesses.
This change modifies the only use of this in What4 to ensure that the
Record types are not ADT's and vice-versa.
2021-03-24 09:07:33 -07:00
Kevin Quick
652b4c8d08
Merge pull request #108 from GaloisInc/rmv_streaderwriter
...
Remove a couple of SMTReadWriter constraints.
2021-03-16 12:10:49 -07:00
Kevin Quick
65e8d78c04
Merge pull request #109 from GaloisInc/rmv_miscconstraints
...
Remove a couple of miscellaneous constraints.
2021-03-15 15:05:58 -07:00
Kevin Quick
ed9a24efbd
Remove unneeded arguments to nameResult and versionResult.
2021-03-15 11:42:23 -07:00
Kevin Quick
f03bcee989
Merge pull request #107 from GaloisInc/rmv_hashablef
...
Remove a couple of HashableF constraints not explicitly needed.
2021-03-15 11:18:32 -07:00
Kevin Quick
5e92b1afbe
Merge pull request #106 from GaloisInc/modernize
...
Update cabal version, add some warnings, fix some warnings.
2021-03-15 11:08:44 -07:00
Kevin Quick
664f39cfb1
Added cabal check to github actions.
2021-03-14 10:22:53 -07:00
Kevin Quick
8fe02d35cb
Update GHC version from 8.10.3 to 8.10.4 in Github Actions.
2021-03-14 10:22:34 -07:00
Kevin Quick
7b11cbf9c9
Update GHC and Cabal compatibility check in Github Actions.
2021-03-14 10:22:02 -07:00
Kevin Quick
287549faff
[what4-blt] Update cabal specification to version 2.2.
2021-03-14 10:21:29 -07:00
Kevin Quick
95f5b65f4d
[what4-abc] Update cabal for more recent specification version.
2021-03-14 10:19:28 -07:00
Kevin Quick
fb3e97b2e1
Update cabal version for compatibility back to GHC 8.4.
2021-03-13 14:30:07 -08:00
Kevin Quick
aac3f2bb32
Add GHC and cabal library compatibility check for .cabal file to GHC actions.
2021-03-13 14:11:39 -08:00
Kevin Quick
25e4d5f9a0
Remove other unneeded constraints.
2021-03-12 16:00:46 -08:00
Kevin Quick
c0d97ca49d
Remove a couple of miscellaneous constraints.
2021-03-12 15:46:16 -08:00
Kevin Quick
f6f66f949e
Remove a couple of SMTReadWriter constraints.
...
These don't seem to be needed, unless they should remain to indicate intent.
2021-03-12 15:43:37 -08:00
Kevin Quick
52276b16a1
Remove a couple of HashableF constraints not explicitly needed.
2021-03-12 15:40:53 -08:00
Kevin Quick
96bccffd6b
Remove use of future package specification format.
2021-03-12 15:32:56 -08:00
Kevin Quick
66b18dbfdd
Enable -Wcompat warnings.
2021-03-12 15:27:49 -08:00
Kevin Quick
51d3970f04
Remove explicit mappend instances matching canonical semigroup op.
2021-03-12 15:26:27 -08:00
Kevin Quick
a1e628aec7
[what4] qualify Data.List import for compatibility immunization.
2021-03-12 10:39:16 -08:00
Kevin Quick
8e2d41d5f0
[what4] update to Cabal version 3.0 with common stanzas.
2021-03-12 10:25:27 -08:00
