{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Grisette.Internal.Core.Data.Class.Solver
(
SolvingFailure (..),
MonadicSolver (..),
SolverCommand (..),
ConfigurableSolver (..),
Solver (..),
withSolver,
solve,
solveMulti,
UnionWithExcept (..),
solveExcept,
solveMultiExcept,
)
where
import Control.DeepSeq (NFData)
import Control.Exception (SomeException, bracket)
import Control.Monad.Except (ExceptT, runExceptT)
import qualified Data.HashSet as S
import Data.Hashable (Hashable)
import Data.Maybe (fromJust)
import GHC.Generics (Generic)
import Grisette.Internal.Core.Data.Class.ExtractSymbolics
( ExtractSymbolics (extractSymbolics),
)
import Grisette.Internal.Core.Data.Class.LogicalOp (LogicalOp (symNot, (.||)))
import Grisette.Internal.Core.Data.Class.PlainUnion
( PlainUnion,
simpleMerge,
)
import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con))
import Grisette.Internal.SymPrim.Prim.Model
( Model,
SymbolSet (unSymbolSet),
equation,
)
import Grisette.Internal.SymPrim.Prim.Term
( SomeTypedSymbol (SomeTypedSymbol),
)
import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))
import Language.Haskell.TH.Syntax (Lift)
data SolveInternal = SolveInternal
deriving (SolveInternal -> SolveInternal -> Bool
(SolveInternal -> SolveInternal -> Bool)
-> (SolveInternal -> SolveInternal -> Bool) -> Eq SolveInternal
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SolveInternal -> SolveInternal -> Bool
== :: SolveInternal -> SolveInternal -> Bool
$c/= :: SolveInternal -> SolveInternal -> Bool
/= :: SolveInternal -> SolveInternal -> Bool
Eq, Int -> SolveInternal -> ShowS
[SolveInternal] -> ShowS
SolveInternal -> String
(Int -> SolveInternal -> ShowS)
-> (SolveInternal -> String)
-> ([SolveInternal] -> ShowS)
-> Show SolveInternal
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SolveInternal -> ShowS
showsPrec :: Int -> SolveInternal -> ShowS
$cshow :: SolveInternal -> String
show :: SolveInternal -> String
$cshowList :: [SolveInternal] -> ShowS
showList :: [SolveInternal] -> ShowS
Show, Eq SolveInternal
Eq SolveInternal =>
(SolveInternal -> SolveInternal -> Ordering)
-> (SolveInternal -> SolveInternal -> Bool)
-> (SolveInternal -> SolveInternal -> Bool)
-> (SolveInternal -> SolveInternal -> Bool)
-> (SolveInternal -> SolveInternal -> Bool)
-> (SolveInternal -> SolveInternal -> SolveInternal)
-> (SolveInternal -> SolveInternal -> SolveInternal)
-> Ord SolveInternal
SolveInternal -> SolveInternal -> Bool
SolveInternal -> SolveInternal -> Ordering
SolveInternal -> SolveInternal -> SolveInternal
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: SolveInternal -> SolveInternal -> Ordering
compare :: SolveInternal -> SolveInternal -> Ordering
$c< :: SolveInternal -> SolveInternal -> Bool
< :: SolveInternal -> SolveInternal -> Bool
$c<= :: SolveInternal -> SolveInternal -> Bool
<= :: SolveInternal -> SolveInternal -> Bool
$c> :: SolveInternal -> SolveInternal -> Bool
> :: SolveInternal -> SolveInternal -> Bool
$c>= :: SolveInternal -> SolveInternal -> Bool
>= :: SolveInternal -> SolveInternal -> Bool
$cmax :: SolveInternal -> SolveInternal -> SolveInternal
max :: SolveInternal -> SolveInternal -> SolveInternal
$cmin :: SolveInternal -> SolveInternal -> SolveInternal
min :: SolveInternal -> SolveInternal -> SolveInternal
Ord, (forall x. SolveInternal -> Rep SolveInternal x)
-> (forall x. Rep SolveInternal x -> SolveInternal)
-> Generic SolveInternal
forall x. Rep SolveInternal x -> SolveInternal
forall x. SolveInternal -> Rep SolveInternal x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SolveInternal -> Rep SolveInternal x
from :: forall x. SolveInternal -> Rep SolveInternal x
$cto :: forall x. Rep SolveInternal x -> SolveInternal
to :: forall x. Rep SolveInternal x -> SolveInternal
Generic, Eq SolveInternal
Eq SolveInternal =>
(Int -> SolveInternal -> Int)
-> (SolveInternal -> Int) -> Hashable SolveInternal
Int -> SolveInternal -> Int
SolveInternal -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> SolveInternal -> Int
hashWithSalt :: Int -> SolveInternal -> Int
$chash :: SolveInternal -> Int
hash :: SolveInternal -> Int
Hashable, (forall (m :: * -> *). Quote m => SolveInternal -> m Exp)
-> (forall (m :: * -> *).
Quote m =>
SolveInternal -> Code m SolveInternal)
-> Lift SolveInternal
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => SolveInternal -> m Exp
forall (m :: * -> *).
Quote m =>
SolveInternal -> Code m SolveInternal
$clift :: forall (m :: * -> *). Quote m => SolveInternal -> m Exp
lift :: forall (m :: * -> *). Quote m => SolveInternal -> m Exp
$cliftTyped :: forall (m :: * -> *).
Quote m =>
SolveInternal -> Code m SolveInternal
liftTyped :: forall (m :: * -> *).
Quote m =>
SolveInternal -> Code m SolveInternal
Lift, SolveInternal -> ()
(SolveInternal -> ()) -> NFData SolveInternal
forall a. (a -> ()) -> NFData a
$crnf :: SolveInternal -> ()
rnf :: SolveInternal -> ()
NFData)
data SolvingFailure
=
Unsat
|
Unk
|
ResultNumLimitReached
|
SolvingError SomeException
|
Terminated
deriving (Int -> SolvingFailure -> ShowS
[SolvingFailure] -> ShowS
SolvingFailure -> String
(Int -> SolvingFailure -> ShowS)
-> (SolvingFailure -> String)
-> ([SolvingFailure] -> ShowS)
-> Show SolvingFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SolvingFailure -> ShowS
showsPrec :: Int -> SolvingFailure -> ShowS
$cshow :: SolvingFailure -> String
show :: SolvingFailure -> String
$cshowList :: [SolvingFailure] -> ShowS
showList :: [SolvingFailure] -> ShowS
Show)
class MonadicSolver m where
monadicSolverPush :: Int -> m ()
monadicSolverPop :: Int -> m ()
monadicSolverSolve :: SymBool -> m (Either SolvingFailure Model)
data SolverCommand
= SolverSolve SymBool
| SolverPush Int
| SolverPop Int
| SolverTerminate
class Solver handle where
solverRunCommand ::
(handle -> IO (Either SolvingFailure a)) ->
handle ->
SolverCommand ->
IO (Either SolvingFailure a)
solverSolve :: handle -> SymBool -> IO (Either SolvingFailure Model)
solverPush :: handle -> Int -> IO (Either SolvingFailure ())
solverPush handle
handle Int
n =
(handle -> IO (Either SolvingFailure ()))
-> handle -> SolverCommand -> IO (Either SolvingFailure ())
forall handle a.
Solver handle =>
(handle -> IO (Either SolvingFailure a))
-> handle -> SolverCommand -> IO (Either SolvingFailure a)
forall a.
(handle -> IO (Either SolvingFailure a))
-> handle -> SolverCommand -> IO (Either SolvingFailure a)
solverRunCommand (IO (Either SolvingFailure ())
-> handle -> IO (Either SolvingFailure ())
forall a b. a -> b -> a
const (IO (Either SolvingFailure ())
-> handle -> IO (Either SolvingFailure ()))
-> IO (Either SolvingFailure ())
-> handle
-> IO (Either SolvingFailure ())
forall a b. (a -> b) -> a -> b
$ Either SolvingFailure () -> IO (Either SolvingFailure ())
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either SolvingFailure () -> IO (Either SolvingFailure ()))
-> Either SolvingFailure () -> IO (Either SolvingFailure ())
forall a b. (a -> b) -> a -> b
$ () -> Either SolvingFailure ()
forall a b. b -> Either a b
Right ()) handle
handle (SolverCommand -> IO (Either SolvingFailure ()))
-> SolverCommand -> IO (Either SolvingFailure ())
forall a b. (a -> b) -> a -> b
$ Int -> SolverCommand
SolverPush Int
n
solverPop :: handle -> Int -> IO (Either SolvingFailure ())
solverPop handle
handle Int
n =
(handle -> IO (Either SolvingFailure ()))
-> handle -> SolverCommand -> IO (Either SolvingFailure ())
forall handle a.
Solver handle =>
(handle -> IO (Either SolvingFailure a))
-> handle -> SolverCommand -> IO (Either SolvingFailure a)
forall a.
(handle -> IO (Either SolvingFailure a))
-> handle -> SolverCommand -> IO (Either SolvingFailure a)
solverRunCommand (IO (Either SolvingFailure ())
-> handle -> IO (Either SolvingFailure ())
forall a b. a -> b -> a
const (IO (Either SolvingFailure ())
-> handle -> IO (Either SolvingFailure ()))
-> IO (Either SolvingFailure ())
-> handle
-> IO (Either SolvingFailure ())
forall a b. (a -> b) -> a -> b
$ Either SolvingFailure () -> IO (Either SolvingFailure ())
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either SolvingFailure () -> IO (Either SolvingFailure ()))
-> Either SolvingFailure () -> IO (Either SolvingFailure ())
forall a b. (a -> b) -> a -> b
$ () -> Either SolvingFailure ()
forall a b. b -> Either a b
Right ()) handle
handle (SolverCommand -> IO (Either SolvingFailure ()))
-> SolverCommand -> IO (Either SolvingFailure ())
forall a b. (a -> b) -> a -> b
$ Int -> SolverCommand
SolverPop Int
n
solverTerminate :: handle -> IO ()
solverForceTerminate :: handle -> IO ()
class
(Solver handle) =>
ConfigurableSolver config handle
| config -> handle
where
newSolver :: config -> IO handle
withSolver ::
(ConfigurableSolver config handle) =>
config ->
(handle -> IO a) ->
IO a
withSolver :: forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config = IO handle -> (handle -> IO ()) -> (handle -> IO a) -> IO a
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
bracket (config -> IO handle
forall config handle.
ConfigurableSolver config handle =>
config -> IO handle
newSolver config
config) handle -> IO ()
forall handle. Solver handle => handle -> IO ()
solverTerminate
solve ::
(ConfigurableSolver config handle) =>
config ->
SymBool ->
IO (Either SolvingFailure Model)
solve :: forall config handle.
ConfigurableSolver config handle =>
config -> SymBool -> IO (Either SolvingFailure Model)
solve config
config SymBool
formula = config
-> (handle -> IO (Either SolvingFailure Model))
-> IO (Either SolvingFailure Model)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config (handle -> SymBool -> IO (Either SolvingFailure Model)
forall handle.
Solver handle =>
handle -> SymBool -> IO (Either SolvingFailure Model)
`solverSolve` SymBool
formula)
solveMulti ::
(ConfigurableSolver config handle) =>
config ->
Int ->
SymBool ->
IO ([Model], SolvingFailure)
solveMulti :: forall config handle.
ConfigurableSolver config handle =>
config -> Int -> SymBool -> IO ([Model], SolvingFailure)
solveMulti config
config Int
numOfModelRequested SymBool
formula =
config
-> (handle -> IO ([Model], SolvingFailure))
-> IO ([Model], SolvingFailure)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([Model], SolvingFailure))
-> IO ([Model], SolvingFailure))
-> (handle -> IO ([Model], SolvingFailure))
-> IO ([Model], SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \handle
solver -> do
Either SolvingFailure Model
firstModel <- handle -> SymBool -> IO (Either SolvingFailure Model)
forall handle.
Solver handle =>
handle -> SymBool -> IO (Either SolvingFailure Model)
solverSolve handle
solver SymBool
formula
case Either SolvingFailure Model
firstModel of
Left SolvingFailure
err -> ([Model], SolvingFailure) -> IO ([Model], SolvingFailure)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], SolvingFailure
err)
Right Model
model -> do
([Model]
models, SolvingFailure
err) <- handle -> Model -> Int -> IO ([Model], SolvingFailure)
go handle
solver Model
model Int
numOfModelRequested
([Model], SolvingFailure) -> IO ([Model], SolvingFailure)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Model
model Model -> [Model] -> [Model]
forall a. a -> [a] -> [a]
: [Model]
models, SolvingFailure
err)
where
allSymbols :: SymbolSet
allSymbols = SymBool -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics SymBool
formula :: SymbolSet
go :: handle -> Model -> Int -> IO ([Model], SolvingFailure)
go handle
solver Model
prevModel Int
n
| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1 = ([Model], SolvingFailure) -> IO ([Model], SolvingFailure)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], SolvingFailure
ResultNumLimitReached)
| Bool
otherwise = do
let newFormula :: SymBool
newFormula =
(SymBool -> SomeTypedSymbol -> SymBool)
-> SymBool -> HashSet SomeTypedSymbol -> SymBool
forall a b. (a -> b -> a) -> a -> HashSet b -> a
S.foldl'
( \SymBool
acc (SomeTypedSymbol TypeRep t
_ TypedSymbol t
v) ->
SymBool
acc
SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| (SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot (Term Bool -> SymBool
SymBool (Term Bool -> SymBool) -> Term Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ Maybe (Term Bool) -> Term Bool
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Term Bool) -> Term Bool) -> Maybe (Term Bool) -> Term Bool
forall a b. (a -> b) -> a -> b
$ TypedSymbol t -> Model -> Maybe (Term Bool)
forall a. TypedSymbol a -> Model -> Maybe (Term Bool)
equation TypedSymbol t
v Model
prevModel))
)
(Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False)
(SymbolSet -> HashSet SomeTypedSymbol
unSymbolSet SymbolSet
allSymbols)
Either SolvingFailure Model
res <- handle -> SymBool -> IO (Either SolvingFailure Model)
forall handle.
Solver handle =>
handle -> SymBool -> IO (Either SolvingFailure Model)
solverSolve handle
solver SymBool
newFormula
case Either SolvingFailure Model
res of
Left SolvingFailure
err -> ([Model], SolvingFailure) -> IO ([Model], SolvingFailure)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], SolvingFailure
err)
Right Model
model -> do
([Model]
models, SolvingFailure
err) <- handle -> Model -> Int -> IO ([Model], SolvingFailure)
go handle
solver Model
model (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
([Model], SolvingFailure) -> IO ([Model], SolvingFailure)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Model
model Model -> [Model] -> [Model]
forall a. a -> [a] -> [a]
: [Model]
models, SolvingFailure
err)
class UnionWithExcept t u e v | t -> u e v where
:: t -> u (Either e v)
instance UnionWithExcept (ExceptT e u v) u e v where
extractUnionExcept :: ExceptT e u v -> u (Either e v)
extractUnionExcept = ExceptT e u v -> u (Either e v)
forall e (u :: * -> *) v. ExceptT e u v -> u (Either e v)
runExceptT
solveExcept ::
( UnionWithExcept t u e v,
PlainUnion u,
Functor u,
ConfigurableSolver config handle
) =>
config ->
(Either e v -> SymBool) ->
t ->
IO (Either SolvingFailure Model)
solveExcept :: forall t (u :: * -> *) e v config handle.
(UnionWithExcept t u e v, PlainUnion u, Functor u,
ConfigurableSolver config handle) =>
config
-> (Either e v -> SymBool) -> t -> IO (Either SolvingFailure Model)
solveExcept config
config Either e v -> SymBool
f t
v = config -> SymBool -> IO (Either SolvingFailure Model)
forall config handle.
ConfigurableSolver config handle =>
config -> SymBool -> IO (Either SolvingFailure Model)
solve config
config (u SymBool -> SymBool
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (u SymBool -> SymBool) -> u SymBool -> SymBool
forall a b. (a -> b) -> a -> b
$ Either e v -> SymBool
f (Either e v -> SymBool) -> u (Either e v) -> u SymBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> u (Either e v)
forall t (u :: * -> *) e v.
UnionWithExcept t u e v =>
t -> u (Either e v)
extractUnionExcept t
v)
solveMultiExcept ::
( UnionWithExcept t u e v,
PlainUnion u,
Functor u,
ConfigurableSolver config handle
) =>
config ->
Int ->
(Either e v -> SymBool) ->
t ->
IO ([Model], SolvingFailure)
solveMultiExcept :: forall t (u :: * -> *) e v config handle.
(UnionWithExcept t u e v, PlainUnion u, Functor u,
ConfigurableSolver config handle) =>
config
-> Int
-> (Either e v -> SymBool)
-> t
-> IO ([Model], SolvingFailure)
solveMultiExcept config
config Int
n Either e v -> SymBool
f t
v =
config -> Int -> SymBool -> IO ([Model], SolvingFailure)
forall config handle.
ConfigurableSolver config handle =>
config -> Int -> SymBool -> IO ([Model], SolvingFailure)
solveMulti config
config Int
n (u SymBool -> SymBool
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (u SymBool -> SymBool) -> u SymBool -> SymBool
forall a b. (a -> b) -> a -> b
$ Either e v -> SymBool
f (Either e v -> SymBool) -> u (Either e v) -> u SymBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> u (Either e v)
forall t (u :: * -> *) e v.
UnionWithExcept t u e v =>
t -> u (Either e v)
extractUnionExcept t
v)