Language.Hasmtlib.Type.Solver

This module provides functions for having SMT-Problems solved by external solvers.

WithSolver

class WithSolver a where

Data that can have a Solver which may be debugged.

Methods

withSolver :: Solver -> Bool -> a

Create a value with a Solver and a Bool for whether to debug the Solver.

Instances

WithSolver Pipe

Defined in Language.Hasmtlib.Type.Solver

Methods

withSolver :: Solver -> Bool -> Pipe

Stateful solving

solveWith :: (Default s, Monad m, Codec a) => Solver s m -> StateT s m a -> m (Result, Maybe (Decoded a))

solveWith solver prob solves a SMT problem prob with the given solver. It returns a pair consisting of:

1. A Result that indicates if prob is satisfiable (Sat), unsatisfiable (Unsat), or if the solver could not determine any results (Unknown).
2. A Decoded answer that was decoded using the solution to prob. Note that this answer is only meaningful if the Result is Sat or Unknown and the answer value is in a Just.

Example

import Language.Hasmtlib

main :: IO ()
main = do
  res <- solveWith @SMT (solver cvc5) $ do
    setLogic "QF_LIA"

    x <- var @IntSort

    assert $ x >? 0

    return x

  print res

The solver will probably answer with x := 1.

Interactive solving

interactiveWith :: (WithSolver s, MonadIO m) => (Solver, Handle) -> StateT s m () -> m ()

Pipes an SMT-problem interactively to the solver.

Example

import Language.Hasmtlib
import Control.Monad.IO.Class

main :: IO ()
main = do
  cvc5Living <- interactiveSolver cvc5
  interactiveWith @Pipe cvc5Living $ do
    setOption $ Incremental True
    setOption $ ProduceModels True
    setLogic "QF_LRA"

    x <- var @RealSort

    assert $ x >? 0

    (res, sol) <- solve
    liftIO $ print res
    liftIO $ print $ decode sol x

    push
    y <- var @IntSort

    assert $ y <? 0
    assert $ x === y

    res' <- checkSat
    liftIO $ print res'
    pop

    res'' <- checkSat
    liftIO $ print res''

  return ()

debugInteractiveWith :: (WithSolver s, MonadIO m) => (Solver, Handle) -> StateT s m () -> m ()

Like interactiveWith but it prints all communication with the solver to console.

Minimzation

solveMinimized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t)) => Expr t -> m (Result, Solution)

Solves the current problem with respect to a minimal solution for a given numerical expression.

Uses iterative refinement.

If you want access to intermediate results, use solveMinimizedDebug instead.

solveMinimizedDebug :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t)) => (Solution -> IO ()) -> Expr t -> m (Result, Solution)

Like solveMinimized but with access to intermediate results.

Maximization

solveMaximized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t)) => Expr t -> m (Result, Solution)

Solves the current problem with respect to a maximal solution for a given numerical expression.

Uses iterative refinement.

If you want access to intermediate results, use solveMaximizedDebug instead.

solveMaximizedDebug :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t)) => (Solution -> IO ()) -> Expr t -> m (Result, Solution)

Like solveMaximized but with access to intermediate results.