Hasmtlib - Haskell SMTLib MTL Library

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-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))

Features

• SMTLib2-Sorts in the Haskell-Type

    data SMTSort =
        BoolSort
      | IntSort
      | RealSort
      | BvSort Nat
      | ArraySort SMTSort SMTSort
      | StringSort
    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 & String
• 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 @SMT (solver yices) $ do
      setLogic "QF_BV"
      x <- var @(BvSort 16)
      y <- var
      assert $ x - (maxBound `mod` 8) === y * y
      return (x,y)
  

• Add your own solvers via the Solver type

    -- | Function that turns a state (usually SMT or OMT) into a result and a solution
    type Solver s m = s -> m (Result, Solution)
  

• Solvers via external processes: CVC5, Z3, Yices2-SMT, MathSAT, OptiMathSAT, OpenSMT & Bitwuzla

    (result, solution) <- solveWith @SMT (solver mathsat) $ do
      setLogic "QF_LIA"
      assert $ ...
  

• Incremental solving

      cvc5Living <- interactiveSolver cvc5
      interactiveWith @Pipe 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 @SMT (solver 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 @OMT (solver z3) $ do
      setLogic "QF_LIA"
      x <- var @IntSort
  
      assert $ x >? -2
      assertSoftWeighted (x >? -1) 5.0
      minimize x
  
      return x
  

Examples

There are some examples in here.

Contact information

Contributions, critics and bug reports are welcome!

Please feel free to contact me through GitHub.