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 @SMT 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
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 @SMT 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 $ Incremental True
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 @SMT z3) $ do
setLogic "LIA"
z <- var @IntSort
assert $ z === 0
assert $
for_all $ \x ->
exists $ \y ->
x + y === z
return z
Optimization Modulo Theories (OMT) / MaxSMT
res <- solveWith (solver @OMT z3) $ do
setLogic "QF_LIA"
x <- var @IntSort
assert $ x >? -2
assertSoftWeighted (x >? -1) 5.0
minimize x
return x