{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Grisette.Backend.SBV.Data.SMT.Solving
( GrisetteSMTConfig (..),
sbvConfig,
TermTy,
)
where
import Control.DeepSeq
import Control.Monad.Except
import qualified Data.HashSet as S
import Data.Hashable
import Data.Kind
import Data.List (partition)
import Data.Maybe
import qualified Data.SBV as SBV
import Data.SBV.Control (Query)
import qualified Data.SBV.Control as SBVC
import GHC.TypeNats
import Grisette.Backend.SBV.Data.SMT.Lowering
import Grisette.Core.Data.Class.Bool
import Grisette.Core.Data.Class.CEGISSolver
import Grisette.Core.Data.Class.Evaluate
import Grisette.Core.Data.Class.ExtractSymbolics
import Grisette.Core.Data.Class.GenSym
import Grisette.Core.Data.Class.ModelOps
import Grisette.Core.Data.Class.Solvable
import Grisette.Core.Data.Class.Solver
import Grisette.IR.SymPrim.Data.BV
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
import Grisette.IR.SymPrim.Data.Prim.Model as PM
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
import Grisette.IR.SymPrim.Data.SymPrim
import Grisette.IR.SymPrim.Data.TabularFun
import Language.Haskell.TH.Syntax (Lift)
type Aux :: Bool -> Nat -> Type
type family Aux o n where
Aux 'True n = SBV.SInteger
Aux 'False n = SBV.SInt n
type IsZero :: Nat -> Bool
type family IsZero n where
IsZero 0 = 'True
IsZero _ = 'False
type TermTy :: Nat -> Type -> Type
type family TermTy bitWidth b where
TermTy _ Bool = SBV.SBool
TermTy n Integer = Aux (IsZero n) n
TermTy n (IntN x) = SBV.SBV (SBV.IntN x)
TermTy n (WordN x) = SBV.SBV (SBV.WordN x)
TermTy n (a =-> b) = TermTy n a -> TermTy n b
TermTy n (a --> b) = TermTy n a -> TermTy n b
TermTy _ v = v
data GrisetteSMTConfig (integerBitWidth :: Nat) where
UnboundedReasoning :: SBV.SMTConfig -> GrisetteSMTConfig 0
BoundedReasoning ::
(KnownNat integerBitWidth, IsZero integerBitWidth ~ 'False, SBV.BVIsNonZero integerBitWidth) =>
SBV.SMTConfig ->
GrisetteSMTConfig integerBitWidth
sbvConfig :: forall integerBitWidth. GrisetteSMTConfig integerBitWidth -> SBV.SMTConfig
sbvConfig :: forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth -> SMTConfig
sbvConfig (UnboundedReasoning SMTConfig
config) = SMTConfig
config
sbvConfig (BoundedReasoning SMTConfig
config) = SMTConfig
config
solveTermWith ::
forall integerBitWidth.
GrisetteSMTConfig integerBitWidth ->
Term Bool ->
IO (SymBiMap, Either SBVC.CheckSatResult PM.Model)
solveTermWith :: forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth
-> Term Bool -> IO (SymBiMap, Either CheckSatResult Model)
solveTermWith GrisetteSMTConfig integerBitWidth
config Term Bool
term = forall a. SMTConfig -> Symbolic a -> IO a
SBV.runSMTWith (forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth -> SMTConfig
sbvConfig GrisetteSMTConfig integerBitWidth
config) forall a b. (a -> b) -> a -> b
$ do
(SymBiMap
m, SBool
a) <- forall (integerBitWidth :: Nat) a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth
-> Term a -> Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrim GrisetteSMTConfig integerBitWidth
config Term Bool
term
forall a. Query a -> Symbolic a
SBVC.query forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *). SolverContext m => SBool -> m ()
SBV.constrain SBool
a
CheckSatResult
r <- Query CheckSatResult
SBVC.checkSat
case CheckSatResult
r of
CheckSatResult
SBVC.Sat -> do
SMTModel
md <- Query SMTModel
SBVC.getModel
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m, forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth -> SMTModel -> SymBiMap -> Model
parseModel GrisetteSMTConfig integerBitWidth
config SMTModel
md SymBiMap
m)
CheckSatResult
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m, forall a b. a -> Either a b
Left CheckSatResult
r)
instance Solver (GrisetteSMTConfig n) SBVC.CheckSatResult where
solve :: GrisetteSMTConfig n -> SymBool -> IO (Either CheckSatResult Model)
solve GrisetteSMTConfig n
config (Sym Term Bool
t) = forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth
-> Term Bool -> IO (SymBiMap, Either CheckSatResult Model)
solveTermWith GrisetteSMTConfig n
config Term Bool
t
solveMulti :: GrisetteSMTConfig n -> Int -> SymBool -> IO [Model]
solveMulti GrisetteSMTConfig n
config Int
n s :: SymBool
s@(Sym Term Bool
t)
| Int
n forall a. Ord a => a -> a -> Bool
> Int
0 = forall a. SMTConfig -> Symbolic a -> IO a
SBV.runSMTWith (forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth -> SMTConfig
sbvConfig GrisetteSMTConfig n
config) forall a b. (a -> b) -> a -> b
$ do
(SymBiMap
newm, SBool
a) <- forall (integerBitWidth :: Nat) a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth
-> Term a -> Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrim GrisetteSMTConfig n
config Term Bool
t
forall a. Query a -> Symbolic a
SBVC.query forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *). SolverContext m => SBool -> m ()
SBV.constrain SBool
a
CheckSatResult
r <- Query CheckSatResult
SBVC.checkSat
case CheckSatResult
r of
CheckSatResult
SBVC.Sat -> do
SMTModel
md <- Query SMTModel
SBVC.getModel
let model :: Model
model = forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth -> SMTModel -> SymBiMap -> Model
parseModel GrisetteSMTConfig n
config SMTModel
md SymBiMap
newm
Int -> Model -> SymBiMap -> Query [Model]
remainingModels Int
n Model
model SymBiMap
newm
CheckSatResult
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return []
where
allSymbols :: SymbolSet
allSymbols = forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics SymBool
s :: SymbolSet
next :: PM.Model -> SymBiMap -> Query (SymBiMap, Either SBVC.CheckSatResult PM.Model)
next :: Model -> SymBiMap -> Query (SymBiMap, Either CheckSatResult Model)
next Model
md SymBiMap
origm = do
let newtm :: Term Bool
newtm =
forall a b. (a -> b -> a) -> a -> HashSet b -> a
S.foldl'
(\Term Bool
acc (SomeTypedSymbol TypeRep t
_ TypedSymbol t
v) -> Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
acc (Term Bool -> Term Bool
pevalNotTerm (forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ forall a. TypedSymbol a -> Model -> Maybe (Term Bool)
equation TypedSymbol t
v Model
md)))
(forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm Bool
False)
(SymbolSet -> HashSet SomeTypedSymbol
unSymbolSet SymbolSet
allSymbols)
let (TermTy n Bool
lowered, SymBiMap
newm) = forall (integerBitWidth :: Nat) a.
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> (TermTy integerBitWidth a, SymBiMap)
lowerSinglePrim' GrisetteSMTConfig n
config Term Bool
newtm SymBiMap
origm
forall (m :: * -> *). SolverContext m => SBool -> m ()
SBV.constrain TermTy n Bool
lowered
CheckSatResult
r <- Query CheckSatResult
SBVC.checkSat
case CheckSatResult
r of
CheckSatResult
SBVC.Sat -> do
SMTModel
md1 <- Query SMTModel
SBVC.getModel
let model :: Model
model = forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth -> SMTModel -> SymBiMap -> Model
parseModel GrisetteSMTConfig n
config SMTModel
md1 SymBiMap
newm
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
newm, forall a b. b -> Either a b
Right Model
model)
CheckSatResult
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
newm, forall a b. a -> Either a b
Left CheckSatResult
r)
remainingModels :: Int -> PM.Model -> SymBiMap -> Query [PM.Model]
remainingModels :: Int -> Model -> SymBiMap -> Query [Model]
remainingModels Int
n1 Model
md SymBiMap
origm
| Int
n1 forall a. Ord a => a -> a -> Bool
> Int
1 = do
(SymBiMap
newm, Either CheckSatResult Model
r) <- Model -> SymBiMap -> Query (SymBiMap, Either CheckSatResult Model)
next Model
md SymBiMap
origm
case Either CheckSatResult Model
r of
Left CheckSatResult
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return [Model
md]
Right Model
mo -> do
[Model]
rmmd <- Int -> Model -> SymBiMap -> Query [Model]
remainingModels (Int
n1 forall a. Num a => a -> a -> a
- Int
1) Model
mo SymBiMap
newm
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Model
md forall a. a -> [a] -> [a]
: [Model]
rmmd
| Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return [Model
md]
solveAll :: GrisetteSMTConfig n -> SymBool -> IO [Model]
solveAll = forall a. HasCallStack => a
undefined
instance CEGISSolver (GrisetteSMTConfig n) SBVC.CheckSatResult where
cegisMultiInputs ::
forall inputs spec.
(ExtractSymbolics inputs, EvaluateSym inputs) =>
GrisetteSMTConfig n ->
[inputs] ->
(inputs -> CEGISCondition) ->
IO (Either SBVC.CheckSatResult ([inputs], PM.Model))
cegisMultiInputs :: forall inputs spec.
(ExtractSymbolics inputs, EvaluateSym inputs) =>
GrisetteSMTConfig n
-> [inputs]
-> (inputs -> CEGISCondition)
-> IO (Either CheckSatResult ([inputs], Model))
cegisMultiInputs GrisetteSMTConfig n
config [inputs]
inputs inputs -> CEGISCondition
func =
SymBool
-> [inputs]
-> Model
-> [inputs]
-> SymBool
-> SymBool
-> [inputs]
-> IO (Either CheckSatResult ([inputs], Model))
go1 ([inputs] -> SymBool
cexesAssertFun [inputs]
conInputs) [inputs]
conInputs (forall a. HasCallStack => [Char] -> a
error [Char]
"Should have at least one gen") [] (forall c t. Solvable c t => c -> t
con Bool
True) (forall c t. Solvable c t => c -> t
con Bool
True) [inputs]
symInputs
where
([inputs]
conInputs, [inputs]
symInputs) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (forall symbolSet (typedSymbol :: * -> *).
SymbolSetOps symbolSet typedSymbol =>
symbolSet -> Bool
isEmptySet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics) [inputs]
inputs
go1 :: SymBool
-> [inputs]
-> Model
-> [inputs]
-> SymBool
-> SymBool
-> [inputs]
-> IO (Either CheckSatResult ([inputs], Model))
go1 SymBool
cexFormula [inputs]
cexes Model
previousModel [inputs]
inputs SymBool
pre SymBool
post [inputs]
remainingSymInputs = do
case [inputs]
remainingSymInputs of
[] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right ([inputs]
cexes, Model
previousModel)
inputs
newInput : [inputs]
vs -> do
let CEGISCondition SymBool
nextPre SymBool
nextPost = inputs -> CEGISCondition
func inputs
newInput
let finalPre :: SymBool
finalPre = SymBool
pre forall b. LogicalOp b => b -> b -> b
&&~ SymBool
nextPre
let finalPost :: SymBool
finalPost = SymBool
post forall b. LogicalOp b => b -> b -> b
&&~ SymBool
nextPost
Either CheckSatResult ([inputs], Model)
r <- SymBool
-> inputs
-> [inputs]
-> SymBool
-> SymBool
-> IO (Either CheckSatResult ([inputs], Model))
go SymBool
cexFormula inputs
newInput (inputs
newInput forall a. a -> [a] -> [a]
: [inputs]
inputs) SymBool
finalPre SymBool
finalPost
case Either CheckSatResult ([inputs], Model)
r of
Left CheckSatResult
failure -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left CheckSatResult
failure
Right ([inputs]
newCexes, Model
mo) -> do
SymBool
-> [inputs]
-> Model
-> [inputs]
-> SymBool
-> SymBool
-> [inputs]
-> IO (Either CheckSatResult ([inputs], Model))
go1
(SymBool
cexFormula forall b. LogicalOp b => b -> b -> b
&&~ [inputs] -> SymBool
cexesAssertFun [inputs]
newCexes)
([inputs]
cexes forall a. [a] -> [a] -> [a]
++ [inputs]
newCexes)
Model
mo
(inputs
newInput forall a. a -> [a] -> [a]
: [inputs]
inputs)
SymBool
finalPre
SymBool
finalPost
[inputs]
vs
cexAssertFun :: inputs -> SymBool
cexAssertFun inputs
input =
let CEGISCondition SymBool
pre SymBool
post = inputs -> CEGISCondition
func inputs
input in SymBool
pre forall b. LogicalOp b => b -> b -> b
&&~ SymBool
post
cexesAssertFun :: [inputs] -> SymBool
cexesAssertFun :: [inputs] -> SymBool
cexesAssertFun = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\SymBool
acc inputs
x -> SymBool
acc forall b. LogicalOp b => b -> b -> b
&&~ inputs -> SymBool
cexAssertFun inputs
x) (forall c t. Solvable c t => c -> t
con Bool
True)
go ::
SymBool ->
inputs ->
[inputs] ->
SymBool ->
SymBool ->
IO (Either SBVC.CheckSatResult ([inputs], PM.Model))
go :: SymBool
-> inputs
-> [inputs]
-> SymBool
-> SymBool
-> IO (Either CheckSatResult ([inputs], Model))
go SymBool
cexFormula inputs
inputs [inputs]
allInputs SymBool
pre SymBool
post =
forall a. SMTConfig -> Symbolic a -> IO a
SBV.runSMTWith (forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth -> SMTConfig
sbvConfig GrisetteSMTConfig n
config) forall a b. (a -> b) -> a -> b
$ do
let Sym Term Bool
t = SymBool
phi forall b. LogicalOp b => b -> b -> b
&&~ SymBool
cexFormula
(SymBiMap
newm, SBool
a) <- forall (integerBitWidth :: Nat) a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth
-> Term a -> Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrim GrisetteSMTConfig n
config Term Bool
t
forall a. Query a -> Symbolic a
SBVC.query forall a b. (a -> b) -> a -> b
$
forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
forall (m :: * -> *). SolverContext m => SBool -> m ()
SBV.constrain SBool
a
CheckSatResult
r <- Query CheckSatResult
SBVC.checkSat
Either CheckSatResult Model
mr <- case CheckSatResult
r of
CheckSatResult
SBVC.Sat -> do
SMTModel
md <- Query SMTModel
SBVC.getModel
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth -> SMTModel -> SymBiMap -> Model
parseModel GrisetteSMTConfig n
config SMTModel
md SymBiMap
newm
CheckSatResult
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left CheckSatResult
r
Either CheckSatResult Model
-> [inputs]
-> SymBiMap
-> QueryT IO (SymBiMap, Either CheckSatResult ([inputs], Model))
loop ((SymbolSet
forallSymbols forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
symbolSet -> model -> model
`exceptFor`) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either CheckSatResult Model
mr) [] SymBiMap
newm
where
forallSymbols :: SymbolSet
forallSymbols :: SymbolSet
forallSymbols = forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics [inputs]
allInputs
phi :: SymBool
phi = SymBool
pre forall b. LogicalOp b => b -> b -> b
&&~ SymBool
post
negphi :: SymBool
negphi = SymBool
pre forall b. LogicalOp b => b -> b -> b
&&~ forall b. LogicalOp b => b -> b
nots SymBool
post
check :: Model -> IO (Either SBVC.CheckSatResult (inputs, PM.Model))
check :: Model -> IO (Either CheckSatResult (inputs, Model))
check Model
candidate = do
let evaluated :: SymBool
evaluated = forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
False Model
candidate SymBool
negphi
Either CheckSatResult Model
r <- forall config failure.
Solver config failure =>
config -> SymBool -> IO (Either failure Model)
solve GrisetteSMTConfig n
config SymBool
evaluated
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
Model
m <- Either CheckSatResult Model
r
let newm :: Model
newm = forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
symbolSet -> model -> model
exact SymbolSet
forallSymbols Model
m
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
False Model
newm inputs
inputs, Model
newm)
guess :: Model -> SymBiMap -> Query (SymBiMap, Either SBVC.CheckSatResult PM.Model)
guess :: Model -> SymBiMap -> Query (SymBiMap, Either CheckSatResult Model)
guess Model
candidate SymBiMap
origm = do
let Sym Term Bool
evaluated = forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
False Model
candidate SymBool
phi
let (TermTy n Bool
lowered, SymBiMap
newm) = forall (integerBitWidth :: Nat) a.
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> (TermTy integerBitWidth a, SymBiMap)
lowerSinglePrim' GrisetteSMTConfig n
config Term Bool
evaluated SymBiMap
origm
forall (m :: * -> *). SolverContext m => SBool -> m ()
SBV.constrain TermTy n Bool
lowered
CheckSatResult
r <- Query CheckSatResult
SBVC.checkSat
case CheckSatResult
r of
CheckSatResult
SBVC.Sat -> do
SMTModel
md <- Query SMTModel
SBVC.getModel
let model :: Model
model = forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth -> SMTModel -> SymBiMap -> Model
parseModel GrisetteSMTConfig n
config SMTModel
md SymBiMap
newm
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
newm, forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
symbolSet -> model -> model
exceptFor SymbolSet
forallSymbols Model
model)
CheckSatResult
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
newm, forall a b. a -> Either a b
Left CheckSatResult
r)
loop ::
Either SBVC.CheckSatResult PM.Model ->
[inputs] ->
SymBiMap ->
Query (SymBiMap, Either SBVC.CheckSatResult ([inputs], PM.Model))
loop :: Either CheckSatResult Model
-> [inputs]
-> SymBiMap
-> QueryT IO (SymBiMap, Either CheckSatResult ([inputs], Model))
loop (Right Model
mo) [inputs]
cexs SymBiMap
origm = do
Either CheckSatResult (inputs, Model)
r <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ Model -> IO (Either CheckSatResult (inputs, Model))
check Model
mo
case Either CheckSatResult (inputs, Model)
r of
Left CheckSatResult
SBVC.Unsat -> forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
origm, forall a b. b -> Either a b
Right ([inputs]
cexs, Model
mo))
Left CheckSatResult
v -> forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
origm, forall a b. a -> Either a b
Left CheckSatResult
v)
Right (inputs
cex, Model
cexm) -> do
(SymBiMap
newm, Either CheckSatResult Model
res) <- Model -> SymBiMap -> Query (SymBiMap, Either CheckSatResult Model)
guess Model
cexm SymBiMap
origm
Either CheckSatResult Model
-> [inputs]
-> SymBiMap
-> QueryT IO (SymBiMap, Either CheckSatResult ([inputs], Model))
loop Either CheckSatResult Model
res (inputs
cex forall a. a -> [a] -> [a]
: [inputs]
cexs) SymBiMap
newm
loop (Left CheckSatResult
v) [inputs]
_ SymBiMap
origm = forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
origm, forall a b. a -> Either a b
Left CheckSatResult
v)
newtype CegisInternal = CegisInternal Int
deriving (CegisInternal -> CegisInternal -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CegisInternal -> CegisInternal -> Bool
$c/= :: CegisInternal -> CegisInternal -> Bool
== :: CegisInternal -> CegisInternal -> Bool
$c== :: CegisInternal -> CegisInternal -> Bool
Eq, Int -> CegisInternal -> ShowS
[CegisInternal] -> ShowS
CegisInternal -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [CegisInternal] -> ShowS
$cshowList :: [CegisInternal] -> ShowS
show :: CegisInternal -> [Char]
$cshow :: CegisInternal -> [Char]
showsPrec :: Int -> CegisInternal -> ShowS
$cshowsPrec :: Int -> CegisInternal -> ShowS
Show, Eq CegisInternal
CegisInternal -> CegisInternal -> Bool
CegisInternal -> CegisInternal -> Ordering
CegisInternal -> CegisInternal -> CegisInternal
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
min :: CegisInternal -> CegisInternal -> CegisInternal
$cmin :: CegisInternal -> CegisInternal -> CegisInternal
max :: CegisInternal -> CegisInternal -> CegisInternal
$cmax :: CegisInternal -> CegisInternal -> CegisInternal
>= :: CegisInternal -> CegisInternal -> Bool
$c>= :: CegisInternal -> CegisInternal -> Bool
> :: CegisInternal -> CegisInternal -> Bool
$c> :: CegisInternal -> CegisInternal -> Bool
<= :: CegisInternal -> CegisInternal -> Bool
$c<= :: CegisInternal -> CegisInternal -> Bool
< :: CegisInternal -> CegisInternal -> Bool
$c< :: CegisInternal -> CegisInternal -> Bool
compare :: CegisInternal -> CegisInternal -> Ordering
$ccompare :: CegisInternal -> CegisInternal -> Ordering
Ord, forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => CegisInternal -> m Exp
forall (m :: * -> *).
Quote m =>
CegisInternal -> Code m CegisInternal
liftTyped :: forall (m :: * -> *).
Quote m =>
CegisInternal -> Code m CegisInternal
$cliftTyped :: forall (m :: * -> *).
Quote m =>
CegisInternal -> Code m CegisInternal
lift :: forall (m :: * -> *). Quote m => CegisInternal -> m Exp
$clift :: forall (m :: * -> *). Quote m => CegisInternal -> m Exp
Lift)
deriving newtype (Eq CegisInternal
Int -> CegisInternal -> Int
CegisInternal -> Int
forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: CegisInternal -> Int
$chash :: CegisInternal -> Int
hashWithSalt :: Int -> CegisInternal -> Int
$chashWithSalt :: Int -> CegisInternal -> Int
Hashable, CegisInternal -> ()
forall a. (a -> ()) -> NFData a
rnf :: CegisInternal -> ()
$crnf :: CegisInternal -> ()
NFData)