SBV is a Haskell framework, allowing high-level use of SMT solvers directly from Haskell. SBV is an acronym for "SMT Based Verification," and SMT is an acronym for "Satisfiability Modulo Theories."
Questions tagged [sbv]
39 questions
12
votes
2 answers
Symbolic theory proving using SBV and Haskell
I'm using SBV (with Z3 backend) in Haskell to create some theory provers. I want to check if forall x and y with given constrains (like x + y = y + x, where + is a "plus operator", not addition) some other terms are valid. I want to define axioms…
Wojciech Danilo
- 11,573
- 17
- 66
- 132
7
votes
1 answer
Are floating point SMT logics slower than real ones?
I wrote an application in Haskell that calls Z3 solver to solve constrains with some complex formulas. Thanks to Haskell I can quickly switch the data type I'm working with.
When using SBV's AlgReal type for computations, I get results in sensible…
arrowd
- 33,231
- 8
- 79
- 110
6
votes
2 answers
Asserting that typeclass holds for all results of type family application
I've got a type family defined as follows:
type family Vec a (n :: Nat) where
Vec a Z = a
Vec a (S n) = (a, Vec a n)
I'd like to assert that the result of applying this type family always fulfills the SymVal class constraint from the SBV…
jmite
- 8,171
- 6
- 40
- 81
5
votes
1 answer
Why is Int32 sort much slower than Integer sort in this SBV/Z3 code?
In an effort to learn Z3 I tried solving one of my favorite Advent of Code problems (a particularly difficult one, 2018 day 23, part 2) using the Haskell bindings sbv. Spoilers in code ahead...
module Lib
( solve
) where
import…
mjgpy3
- 8,597
- 5
- 30
- 51
4
votes
2 answers
What does "quantifier free logic" mean in SMT context?
Even for simplest arithmetic SMT problems the existential quantifier is required to declare symbolic variables. And ∀ quantifier can be turned into ∃ by inverting the constraint. So, I can use both of them in QF_* logics and it works.
I take it,…
arrowd
- 33,231
- 8
- 79
- 110
4
votes
1 answer
Turning Haskell Int values into Constants for SBV constraints
I see lots of examples of the SBV library being used like so:
f :: IO SatResult
f = sat $ do
x <- sInteger "x"
constraint $ x .< 200
For a function that takes in a Haskell Int, I would like to use that Int in my constraint formulas…
Matt Ahrens
- 129
- 7
4
votes
1 answer
Why does this SBV code stop before hitting the limit I set?
I have this theorem (not sure if that's the right word), and I want to get all the solutions.
pairCube limit = do
m <- natural exists "m"
n <- natural exists "n"
a <- natural exists "a"
constrain $ m^3 .== n^2
constrain $ m .<…
Reed Oei
- 1,427
- 2
- 13
- 19
3
votes
1 answer
Efficient way to do n-ary branch / tabulated functions?
I'm trying to get some basic information on the performance characteristics of branches in SBV.
Let's suppose I have an SInt16 and a very sparse lookup table Map Int16 a. I can implement the lookup with nested ite:
sCase :: (Mergeable a) => SInt16…
Cactus
- 27,075
- 9
- 69
- 149
3
votes
1 answer
Out-of-bounds `select` even though I `constrain` the index
I have a static-length list of values ks :: [SInt16] and an index x :: SInt16. I'd like to index into the list using x:
(.!) :: (Mergeable a) => [a] -> SInt16 -> a
xs .! i = select xs (error "(.!) : out of bounds") i
I would expect to be able to…
Cactus
- 27,075
- 9
- 69
- 149
3
votes
1 answer
Should imposing additional constraints improve solving time for SMT solvers?
I have a SMT application (built on Haskell SBV library), which solves some complex equation against single s variable in Real logic using Z3. Finding solution takes about 30 seconds in my case.
Trying to speed things up, I added additional…
arrowd
- 33,231
- 8
- 79
- 110
3
votes
1 answer
Trying to solve Constraint over Ancestor Relation with SBV
I'm trying to solve the following csp involing an ancestor relation in Haskell using the SBV Library (Version 7.12):
Give me the set of all persons who don't descend from Stephen.
My solution (see below) gets the following exception
*** Exception:…
jules
- 1,897
- 2
- 16
- 19
2
votes
1 answer
Using SBV to show satisfiability of predicates containing byte strings in Haskell
I want to use the Data.SBV library to prove satisfiability of predicates containing byte strings of arbitrary length (from Data.ByteString).
To illustrate, a predicate could be:
([0,0,1] + [255,255,255]) == [0,0,0]
In order to do so, I need to…
Nico Naus
- 21
- 1
2
votes
1 answer
Trivial Rationals problems without variables in SBV Solver in Haskell
I am working with SBV Solver in Haskell, specifically I am using the Rational type for the variables.
I want to solve linear problems for example:
solution1 = do
[x] <- sRationals ["x"]
constrain $ 5.%1 .<= x
The code works without…
Shenkok Kotoro
- 29
- 6
2
votes
1 answer
Module works with Cabal but not with Stack
I'm trying to install the sbv module https://hackage.haskell.org/package/sbv
Installation with Stack works great (no errors):
stack install sbv
but then I cannot import the corresponding module in stack ghci:
import Data.SBV
-- :…
Jivan
- 21,522
- 15
- 80
- 131
2
votes
1 answer
find a string match as many regular expressions as possible in a regular expression set
Suppose I have a regular expression set R, how can I find a string s that matches as many regular expressions as possible?
For example, if R = {a\*b, b\*, c}, then s could be "b". I am not sure, maybe z3 solver could be helpful?
GGLeod
- 43
- 5