Hasmtlib is a library for generating SMTLib2-problems using a monad.
It takes care of encoding your problem, marshaling the data to an external solver and parsing and interpreting the result into Haskell types.
It is highly inspired by ekmett/ersatz which does the same for QSAT.
Communication with external solvers is handled by tweag/smtlib-backends.
Hasmtlib is a library for generating SMTLib2-problems using a monad.
It takes care of encoding your problem, marshaling the data to an external solver and parsing and interpreting the result into Haskell types.
It is highly inspired by ekmett/ersatz which does the same for QSAT. Communication with external solvers is handled by tweag/smtlib-backends.
Building expressions with type-level representations of the SMTLib2-Types guarantees type-safety when communicating with external solvers.
Although Hasmtlib does not yet make use of observable sharing (StableNames) like Ersatz does, sharing in the API still allows for pure formula construction.
Therefore, this allows you to use the much richer subset of Haskell than a purely monadic meta-language would, which the strong hgoes/smtlib2 is one of. This ultimately results in extremely compact code.
For instance, to define the addition of two V3 containing Real-SMT-Expressions:
instance Num a => Num (V3 a) where
(+) :: V3 a -> V3 a -> V3 a
(+) = liftA2 (+)
Hence, no extra definition is needed at all. We can use the existing instances:
{-# LANGUAGE DataKinds #-}
import Language.Hasmtlib
import Linear
-- instances with default impl
instance Codec a => Codec (V3 a)
instance Variable a => Variable (V3 a)
main :: IO ()
main = do
res <- solveWith (solver cvc5) $ do
setLogic "QF_NRA"
u :: V3 (Expr RealSort) <- variable
v <- variable
assert $ dot u v === 5
return (u,v)
print res
May print: (Sat,Just (V3 (-2.0) (-1.0) 0.0,V3 (-2.0) (-1.0) 0.0))
Features
Supported
SMTLib2-Sorts in the Haskell-Type
data SMTSort = BoolSort | IntSort | RealSort | BvSort Nat | ArraySort SMTSort SMTSort
data Expr (t :: SMTSort) where ...
ite :: Expr BoolSort -> Expr t -> Expr t -> Expr t
Full SMTLib 2.6 standard support for Sorts Int, Real, Bool, unsigned BitVec & Array
Type-level length-indexed Bitvectors for BitVec
bvConcat :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m))
Pure API with Expression-instances for Num, Floating, Bounded, ...
solveWith (solver yices) $ do
setLogic "QF_BV"
x <- var @(BvSort 16)
y <- var
assert $ x - (maxBound `mod` 8) === y * y
return (x,y)
cvc5Living <- interactiveSolver cvc5
interactiveWith cvc5Living $ do
setLogic "QF_LIA"
setOption $ ProduceModels True
x <- var @IntSort
assert $ x === 42
result <- checkSat
push
assert $ x <? 0
(result, solution) <- solve
case result of
Sat -> return solution
Unsat -> pop >> ...
Pure quantifiers for_all and exists
solveWith (solver z3) $ do
setLogic "LIA"
z <- var @IntSort
assert $ z === 0
assert $
for_all $ \x ->
exists $ \y ->
x + y === z
return z
Coming
Observable sharing & access to the expression-tree (useful for rewriting, ...)
(Maybe) signed BitVec with corresponding encoding on the type-level (unsigned, ones-complement, twos-complement)