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

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.