Hasmtlib is a library with high-level-abstraction 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-Sorts guarantees type-safety when communicating with external solvers.
While formula construction is entirely pure, Hasmtlib - just like ersatz
- makes use of observable sharing for expressions.
This allows you to use the much richer subset of Haskell than a purely monadic meta-language would, which ultimately results in extremely compact code.
For instance, to define the addition of two V3
containing Real-SMT-Expressions:
v3Add :: V3 (Expr RealSort) -> V3 (Expr RealSort) -> V3 (Expr RealSort)
v3Add = liftA2 (+)
Even better, the Expr-GADT allows a polymorph definition:
v3Add :: Num (Expr t) => V3 (Expr t) -> V3 (Expr t) -> V3 (Expr t)
v3Add = liftA2 (+)
This looks a lot like the definition of Num for V3 a
:
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 @SMT (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))
[x] SMTLib2-Sorts in the Haskell-Type to guarantee well-typed expressions
data SMTSort =
BoolSort
| IntSort
| RealSort
| BvSort BvEnc Nat
| ArraySort SMTSort SMTSort
| StringSort
data Expr (t :: SMTSort) where ...
ite :: Expr BoolSort -> Expr t -> Expr t -> Expr t
Num
, Floating
, Bounded
, Bits
, Ixed
and many morefor_all
and exists
solveWith @SMT (solver z3) $ do
setLogic "LIA"
z <- var @IntSort
assert $ z === 0
assert $
for_all $ \x ->
exists $ \y ->
x + y === z
return z
[x] Optimization Modulo Theories (OMT) / MaxSMT
res <- solveWith @OMT (solver z3) $ do
setLogic "QF_LIA"
x <- var @IntSort
assert $ x >? -2
assertSoftWeighted (x >? -1) 5.0
minimize x
return x
SMT
what they do for SAT
.If you want highly specific implementations for different solvers, all their individual configurations and swallow the awkward typing, then use hgoes/smtlib2.
If you want to express properties about Haskell programs and automatically prove them using SMT, then use LevantErkok/sbv.
If you want to encode SMT-problems as lightweight and close to Haskell as possible, then use this library. I personally use it for scheduling/resource-allocation-problems.
There are some examples in here.
Contributions, critics and bug reports are welcome!
Please feel free to contact me through GitHub.