Hasmtlib

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 (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 = IntSort | RealSort | BoolSort | BvSort Nat
    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 and unsigned BitVec
• 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)
  

• Add your own solvers via the Solver type

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

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

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

• Incremental solving

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

Examples

There are some examples in here.

Contact information

Contributions, critics and bug reports are welcome!

Please feel free to contact me through GitHub.