This was removed from the `flakes` repo in GaloisInc/flakes#7. The rationale is
that odd Yices version numbers are development versions, and we only want to
test release versions. `what4`'s CI was testing 2.6.1 (a development version),
so let's just remove it.
Bitwuzla is a relatively new SMT solver with support for the bitvector,
floating point, array, and uninterpreted function theories. This patch adds the
necessary plumbing to invoke Bitwuzla using What4.
Co-authored-by: Ryan Scott <rscott@galois.com>
`versions-6.0.2` introduces a `Lift Version` instance, which finally allows us
to delete the ugly, CPP'd mess of orphan instances that we define in
`What4.Utils.Versions`.
Related to #240.
`versions-6.0.*` removes the `VChunk` data type, which `what4` defines an
orphan `Lift` instance for. This requires some CPP to fix up. This is somewhat
messy, and in an ideal world, we'd move these orphan instances directly to the
`versions` library. (See also https://github.com/fosskers/versions/issues/68.)
Fixes#240.
This patch contains a variety of fixes needed to build the libraries in the
`what4` repo with GHC 9.6:
* GHC 9.6 bundles `mtl-2.3.*`, which no longer re-exports `Control.Monad`,
`Control.Monad.IO.Class`, and similar modules from `mtl`-related modules.
To accommodate this, various imports have been made more explicit.
* `MonadTrans t` now has a quantified `forall m. Monad m => Monad (t m)`
superclass in `mtl-2.3.*`. As a result, the `MonadTrans (PartialT sym)`
instance must now have an `IsExpr (SymExpr sym)` instance context in order
for it to typecheck, as this is the same instance context that `PartialT`'s
`Monad` instance has.
This is technically a breaking change, so I have noted it in the `what4`
changelog. That being said, this change is unlikely to affect many people
in practice, considering that the `MonadTrans` instance for `PartialT` is
usually used in tandem with the `Monad` instance.
* Various upper version bounds on `base` have been lifted to allow building
with `base-4.18`.
* The `aig` submodule has been bumped to bring in the changes from
GaloisInc/aig#15, which allows it to build with GHC 9.6.
This change incorporates the serialization/deserialization capabilities from the what4-serialize package into what4. The new functionality enables serializing what4 terms as s-expressions that are intended to match SMTLib2. It also supports deserializing them from the text form into what4 terms in memory.
Note that this is just an import of the code from the what4-serialize library (with a few modest fixes), so if you previously relied on what4-serialize, you will need to delete your dependency on that library when updating. Post-merge, the code in what4 should be a drop-in replacement for the what4-serialize library.
Fixes#104
Co-authored-by: Ryan Scott <ryan.gl.scott@gmail.com>
* Added offline get-abduct feature with an example file of how to use it
* Unstable: trying to add get-abduct to the online solver
* Stable: added a way to get single abduct
* Working online version of get-abduct
* Refactored abduct commands so that variable name bound to abducts is taken from the front-end
* Changed name from getAbduct to getAbducts
* Added ability for user to specify grammar
* Turning off unsat-cores in cvc5 since unsat cores and abduction are not compatible. We need a better solution at some point
* Enabling unsat cores in cvc5
* Adding a way to push and pop frame 2
* Adding a way to push and pop frame 2
* Partially finished formula to CFG function implemented
* Removing all the grammar related stuff, readying for merge
* Addressing most of the PR feedback
* Update what4/src/What4/Protocol/SMTWriter.hs
Co-authored-by: Ryan Scott <ryan.gl.scott@gmail.com>
* Stable abduction tests
* Update what4/test/Abduct.hs
Co-authored-by: Ryan Scott <ryan.gl.scott@gmail.com>
* Update what4/test/Abduct.hs
Co-authored-by: Ryan Scott <ryan.gl.scott@gmail.com>
* Fixing imports in abduct test
* cvc5-1.0.2
Co-authored-by: Ryan Scott <ryan.gl.scott@gmail.com>
For intMax/Min x y, checks if either x <= y or y <= x
can be statically determined.
Explicitly sets the abstract domain of the result
to be rangeMax/Min of the arguments.
Fixes#215.
Running `hedgehog`'s `checkSequential` function alone isn't enough to cause a
test suite to fail if one or more of the test cases to fail. Per a comment in
the `hedgehog` source code
[here](3d4dde46e1/hedgehog-example/test/test.hs (L34-L42)),
the idiomatic way to do make a `checkSequential` failure imply test suite
failure is to check the result of running `checkSequential` and, if that is
`False`, throw `exitFailure`. This patch incorporates that advice into the
`test_templates` test suite.
Fixes#206.
* Draft: Support CVC5
TODO RGS: Fix the test suite
TODO RGS: CI support
[ci skip]
* Deprecated ALL_SUPPORTED and added ALL
* Integrated cvc5 with tests
* Changed expected timeouts in OnlineSolverTest
* In response to Ryan's comments
* Dropping GHC 8.6.5 from CI
* Correcting cvc5 feature list and undoing a previous unintentional change
* Adding cvc5 tests in ExprBuilderSMTLib2
Co-authored-by: Ryan Scott <rscott@galois.com>
Co-authored-by: arjunvish <arjun.viswanathan23@gmail.com>
