hasmtlib: A monad for interfacing with external SMT solvers

[ gpl, library, logic, smt ] [ Propose Tags ] [ Report a vulnerability ]

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, 2.0.0, 2.0.1, 2.1.0, 2.2.0, 2.3.0, 2.3.1, 2.3.2, 2.4.0, 2.5.0, 2.5.1, 2.6.0, 2.6.1, 2.6.2, 2.6.3, 2.7.0, 2.7.1, 2.7.2, 2.8.0, 2.8.1
Change log CHANGELOG.md
Dependencies array (>=0.5 && <1), attoparsec (>=0.14.4 && <1), base (>=4.17.2 && <5), bitvec (>=1.1.5 && <2), bytestring (>=0.11.5 && <1), constrained-some (>=0.1 && <0.2), 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), lifted-base (>=0.2 && <0.5), monad-control (>=1.0 && <1.2), mtl (>=2.2.2 && <3), smtlib-backends (>=0.4 && <0.5), smtlib-backends-process (>=0.3 && <0.4), some (>=1.0.6 && <1.1), text (>=2.0.2 && <3), unordered-containers (>=0.2.20 && <0.3), utf8-string (>=1.0.2 && <2), vector-sized (>=1 && <2) [details]
Tested with ghc ==9.4.8, ghc ==9.6.4, ghc ==9.8.2
License GPL-3.0-only
Copyright © 2024 Julian Bruder
Author Julian Bruder
Maintainer julian.bruder@outlook.com
Category SMT, Logic
Home page https://github.com/bruderj15/Hasmtlib
Bug tracker https://github.com/bruderj15/Hasmtlib/issues
Uploaded by bruderj15 at 2024-11-28T22:01:26Z
Distributions
Downloads 566 total (82 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-2.8.0

[back to package description]

Hackage Static Badge Haskell-CI License: GPL v3

Hasmtlib - Haskell SMTLib MTL Library

Hasmtlib is a library with high-level-abstraction 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 to guarantee well-typed expressions
      data SMTSort =
          BoolSort
        | IntSort
        | RealSort
        | BvSort BvEnc 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 Bool, Int, Real, BitVec, Array & String
  • Type-level length-indexed Bitvectors with type-level encoding (Signed/Unsigned) for BitVec
  • Pure API with plenty common instances: Num, Floating, Bounded, Bits, Ixed and many more
  • Add your own solvers via the Solver type
  • Solvers via external processes: CVC5, Z3, Yices2-SMT, MathSAT, OptiMathSAT, OpenSMT & Bitwuzla
  • Support for incremental solving
  • 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
    
  • ekmett/ersatz: Huge inspiration for this library (some code stolen). We do for SMT what they do for SAT.
  • hgoes/smtlib2: Their eDSL is highly expressive and focuses on well-typed SMT-expressions. But their approach is a little verbose and makes usage feel quite heavy. Their eDSL is also entirely monadic and therefore formula construction is painful.
  • yav/simple-smt: They are lightweight but their types are weak and their API is barely embedded into Haskell.
  • LevantErkok/sbv: While they "express properties about Haskell programs and automatically prove them using SMT", we instead use Haskell to simplify the encoding of SMT-Problems. They can do a whole lot (C-Code-Gen, Crypto-Stuff,...), which is cool, but adds weight.

If you want highly specific implementations for different solvers, all their individual configurations and swallow the awkward typing, then use hgoes/smtlib2.

If you want to express properties about Haskell programs and automatically prove them using SMT, then use LevantErkok/sbv.

If you want to encode SMT-problems as lightweight and close to Haskell as possible, then use this library. I personally use it for scheduling/resource-allocation-problems.

Examples

There are some examples in here.

Contact information

Contributions, critics and bug reports are welcome!

Please feel free to contact me through GitHub.