A monad for interfacing with external SMT solvers.

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

v3Add :: V3 (Expr RealSort) -> V3 (Expr RealSort) -> V3 (Expr RealSort)
v3Add = liftA2 (+)

Even better, the Expr-GADT allows for 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

• [x] 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
  

• [x] Full SMTLib 2.6 standard support for Sorts Int, Real, Bool, unsigned BitVec, Array & String
• [x] Type-level length-indexed Bitvectors for BitVec

    bvConcat :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m))
  

• [x] 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)
  

• [x] 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)
  

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

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

• [x] 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 >> ...
  

• [x] 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
  

• [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
  

Examples

There are some examples in here.

Contact information

Contributions, critics and bug reports are welcome!

Please feel free to contact me through GitHub.