Language.Hasmtlib.Type.Solver

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

The base type for every solver is the SolverConfig. It describes where the solver executable is located and how it should behave. You can provide a time-out using the decorator timingout. Another decorator - debugging - allows you to debug all the information you want. The actual debuggers can be found in Language.Hasmtlib.Type.Debugger.

Solver configuration

Type

data SolverConfig s

Configuration for solver processes.

Constructors

SolverConfig

Fields

• _processConfig :: Config

  The underlying config of the process

• _mTimeout :: Maybe Int

  Timeout in microseconds

• _mDebugger :: Maybe (Debugger s)

  Debugger for communication with external solver

Decoration

debugging :: Debugger s -> SolverConfig s -> SolverConfig s

Decorates a SolverConfig with a Debugger.

timingout :: Int -> SolverConfig s -> SolverConfig s

Decorates a SolverConfig with a timeout. The timeout is given as an Int which specifies after how many microseconds the entire problem including problem construction, solver interaction and solving time may time out.

When timing out, the Result will always be Unknown.

This uses timeout internally.

Lens

processConfig :: forall s. Lens' (SolverConfig s) Config

mTimeout :: forall s. Lens' (SolverConfig s) (Maybe Int)

mDebugger :: forall s s. Lens (SolverConfig s) (SolverConfig s) (Maybe (Debugger s)) (Maybe (Debugger s))

Stateful solving

type Solver s m = s -> m (Result, Solution)

Function that turns a state into a Result and a Solution.

solver :: (RenderProblem s, MonadIO m) => SolverConfig s -> Solver s m

Creates a Solver which holds an external process with a SMT-Solver.

This will:

1. Encode the SMT-problem,
2. start a new external process for the SMT-Solver,
3. send the problem to the SMT-Solver,
4. wait for an answer and parse it,
5. close the process and clean up all resources and
6. return the decoded solution.

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 :: (MonadIO m, MonadBaseControl IO m) => SolverConfig Pipe -> StateT Pipe m a -> m (Maybe a)

Pipes an SMT-problem interactively to the solver.

Example

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

main :: IO ()
main = do
  interactiveWith z3 $ do
    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 ()

Minimzation

solveMinimized

Arguments

:: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))

=> Expr t

Target to minimize

-> Maybe (Expr t -> Expr t)

Step-size: Lambda is given last result as argument, producing the next upper bound

-> Maybe (Solution -> IO ())

Accessor to intermediate results

-> m (Result, Solution)

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

This is done by incrementally refining the upper bound for a given target. Terminates, when setting the last intermediate result as new upper bound results in Unsat. Then removes that last assertion and returns the previous (now confirmed minimal) result.

You can also provide a step-size. You do not have to worry about stepping over the optimal result. This implementation takes care of it.

Access to intermediate results is also possible via an IO-Action.

Examples

x <- var @IntSort
assert $ x >? 4
solveMinimized x Nothing Nothing

The solver will return x := 5.

The first Nothing indicates that each intermediate result will be set as next upper bound. The second Nothing shows that we do not care about intermediate, but only the final (minimal) result.

x <- var @IntSort
assert $ x >? 4
solveMinimized x (Just (\r -> r-1)) (Just print)

The solver will still return x := 5.

However, here we want the next bound of each refinement to be lastResult - 1. Also, every intermediate result is printed.

Maximization

solveMaximized

Arguments

:: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))

=> Expr t

Target to maximize

-> Maybe (Expr t -> Expr t)

Step-size: Lambda is given last result as argument, producing the next lower bound

-> Maybe (Solution -> IO ())

Accessor to intermediate results

-> m (Result, Solution)

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

This is done by incrementally refining the lower bound for a given target. Terminates, when setting the last intermediate result as new lower bound results in Unsat. Then removes that last assertion and returns the previous (now confirmed maximal) result.

You can also provide a step-size. You do not have to worry about stepping over the optimal result. This implementation takes care of it.

Access to intermediate results is also possible via an IO-Action.

Examples

x <- var @IntSort
assert $ x <? 4
solveMaximized x Nothing Nothing

The solver will return x := 3.

The first Nothing indicates that each intermediate result will be set as next lower bound. The second Nothing shows that we do not care about intermediate, but only the final (maximal) result.

x <- var @IntSort
assert $ x <? 4
solveMinimized x (Just (+1)) (Just print)

The solver will still return x := 3.

However, here we want the next bound of each refinement to be lastResult + 1. Also, every intermediate result is printed.