hasmtlib: A monad for interfacing with external SMT solvers

[ gpl, library, smt ] [ Propose Tags ]

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.


[Skip to Readme]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 1.0.0, 1.0.1, 1.0.2, 1.1.0, 1.1.1, 1.1.2, 1.2.0, 1.3.0, 1.3.1
Dependencies attoparsec (>=0.14.4 && <1), base (>=4.17.2 && <5), bitvec (>=1.1.5 && <2), bytestring (>=0.11.5 && <1), containers (>=0.6.7 && <1), data-default (>=0.7.1 && <1), dependent-map (>=0.4 && <1), finite-typelits (>=0.1.0 && <1), lens (>=5 && <6), mtl (>=2.2.2 && <3), smtlib-backends (>=0.4 && <1), smtlib-backends-process (>=0.3 && <1), some (>=1.0.6 && <1.1), text (>=2.0.2 && <3), utf8-string (>=1.0.2 && <2), vector-sized (>=1 && <2) [details]
License GPL-3.0-only
Copyright 2024 Julian Bruder
Author Julian Bruder
Maintainer julian.bruder@outlook.com
Category SMT
Home page https://github.com/bruderj15/Hasmtlib
Uploaded by bruderj15 at 2024-06-21T13:50:04Z
Distributions
Downloads 116 total (116 in the last 30 days)
Rating 2.0 (votes: 1) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs uploaded by user
Build status unknown [no reports yet]

Readme for hasmtlib-1.1.0

[back to package description]

Hackage Static Badge Haskell-CI License: GPL v3

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.