Jared Weakly
ebca4d7329
Merge pull request #741 from GaloisInc/serialize-windows-builds
...
Serialize nightly windows builds
2020-05-27 10:37:58 -07:00
Jared Weakly
221e411b68
Serialize nightly windows builds
2020-05-27 10:26:44 -07:00
Rob Dockins
da83c813b2
Additional code comments
2020-05-26 17:08:20 -07:00
Rob Dockins
c1b641c420
Add a test case for issue725
2020-05-26 17:08:20 -07:00
Rob Dockins
06584f4d10
Refactor and comment the Cryptol.Symbolic.SBV module
2020-05-26 17:08:20 -07:00
Rob Dockins
aaf78e23ec
Add a bit more output for the Satisfiable/Counterexample cases
2020-05-26 17:08:20 -07:00
Rob Dockins
1b584d9567
typo
2020-05-26 17:08:20 -07:00
Rob Dockins
60dcbd1d40
Make SBV backends behave the same as What4 backends WRT safety predicates.
...
For now, we always include the safety predicate as part of `:sat` and `:prove`
queries. Eventually, we will make this more configurable and have the
UI indicate if the property or the safety condition failed on proof counterexamples,
etc.
2020-05-26 17:08:20 -07:00
Rob Dockins
dbbd8607a0
Invoke a more severe exception throwing mechanism when we cannot
...
symbolicly translate an operation in the SBV backend.
This matches the behavior of the What4 backends.
2020-05-26 17:08:20 -07:00
brianhuffman
780b1bcecc
Merge pull request #733 from GaloisInc/issue731
...
Issue731
2020-05-22 14:38:15 -07:00
Brian Huffman
37f1fd8b4b
Add regression test for #731 .
2020-05-18 17:17:58 -07:00
Brian Huffman
e1fb6e940d
Pretty-print Prop constructor PAnd using tuple-style syntax.
...
This matches the syntax used for parsing type constraint synonyms.
Fixes #731 .
2020-05-18 17:15:13 -07:00
Brian Huffman
5c44ac6221
Properly parenthesize type applications in pretty printer for type Prop.
...
Special cases for PArith, PCmp, PSignedCmp, and PLiteral are removed,
as they are covered correctly by the fallback case.
2020-05-18 17:14:13 -07:00
brianhuffman
5cc3e11e78
Merge pull request #726 from GaloisInc/singleSubst
...
Enforce datatype invariants when creating `Subst` values
2020-05-18 15:51:15 -07:00
Brian Huffman
0cf21ace93
Check for kind mismatch in singleSubst.
...
If there is a kind mismatch, it returns the new `SubstKindMismatch`
constructor of the `SubstError` type.
Also change `bindVar` to rely on `singleSubst` for kind checking.
2020-05-18 12:34:01 -07:00
Brian Huffman
2c72419b1a
Document kind-correctness invariant for Subst datatype.
2020-05-18 12:31:19 -07:00
Brian Huffman
700b31803c
Add regression test for #723 .
2020-05-15 07:36:11 -07:00
Brian Huffman
df4af1af3b
Make singleSubst perform checks and return Either type.
...
The old `singleSubst` has been renamed to `uncheckedSingleSubst`.
Fixes #723 .
2020-05-15 07:30:48 -07:00
Brian Huffman
08db8868e5
Make extendSubst re-use freeParams function.
2020-05-15 07:28:13 -07:00
Brian Huffman
6ea73cdf39
Move function freeParams into a different module.
2020-05-15 07:20:38 -07:00
Brian Huffman
c0ebf1132c
Introduce convenience function singleTParamSubst.
2020-05-15 07:10:15 -07:00
Brian Huffman
2f21e65d0e
Document additional invariant on 'Subst' type.
2020-05-15 07:06:15 -07:00
Jared Weakly
1c38465ca8
Implement GitHub actions ( #722 )
...
* Builds nightly binary tarballs on Linux, macOS, and Windows
* Runs tests on every PR and merge to master
* Includes GitHub Actions status in README instead of Travis
* Makes the GitRev recompile hack less fragile
* Makes the Makefile Cabal v3 compatible
* Builds the manual as part of the CI process
2020-05-14 10:50:22 -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
