{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE Trustworthy #-}
module Grisette.Internal.Core.Data.Class.CEGISSolver
(
SynthesisConstraintFun,
VerifierResult (..),
StatefulVerifierFun,
CEGISResult (..),
genericCEGIS,
CEGISCondition (..),
cegisPostCond,
cegisPrePost,
cegisMultiInputs,
cegis,
cegisExcept,
cegisExceptStdVC,
cegisExceptVC,
cegisExceptMultiInputs,
cegisExceptStdVCMultiInputs,
cegisExceptVCMultiInputs,
cegisForAll,
cegisForAllExcept,
cegisForAllExceptStdVC,
cegisForAllExceptVC,
)
where
import Control.Monad (foldM, unless)
import Data.List (partition)
import GHC.Generics (Generic)
import Generics.Deriving (Default (Default))
import Grisette.Internal.Core.Control.Exception
( VerificationConditions (AssertionViolation, AssumptionViolation),
)
import Grisette.Internal.Core.Data.Class.EvaluateSym (EvaluateSym, evaluateSym)
import Grisette.Internal.Core.Data.Class.ExtractSymbolics
( ExtractSymbolics,
extractSymbolics,
)
import Grisette.Internal.Core.Data.Class.LogicalOp (LogicalOp (symNot, (.&&)))
import Grisette.Internal.Core.Data.Class.Mergeable (Mergeable)
import Grisette.Internal.Core.Data.Class.ModelOps
( ModelOps (exact, exceptFor),
SymbolSetOps (isEmptySet),
)
import Grisette.Internal.Core.Data.Class.PlainUnion
( PlainUnion,
simpleMerge,
)
import Grisette.Internal.Core.Data.Class.SEq (SEq)
import Grisette.Internal.Core.Data.Class.SimpleMergeable
( SimpleMergeable,
)
import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con))
import Grisette.Internal.Core.Data.Class.Solver
( ConfigurableSolver,
Solver (solverSolve),
SolvingFailure (Unsat),
UnionWithExcept (extractUnionExcept),
solve,
withSolver,
)
import Grisette.Internal.SymPrim.Prim.Model (Model)
import Grisette.Internal.SymPrim.SymBool (SymBool)
type SynthesisConstraintFun input = Int -> input -> IO SymBool
data VerifierResult input exception
= CEGISVerifierFoundCex input
| CEGISVerifierNoCex
| CEGISVerifierException exception
type StatefulVerifierFun state input exception =
state -> Model -> IO (state, VerifierResult input exception)
data CEGISResult exception
= CEGISSuccess Model
| CEGISVerifierFailure exception
| CEGISSolverFailure SolvingFailure
deriving (Int -> CEGISResult exception -> ShowS
[CEGISResult exception] -> ShowS
CEGISResult exception -> String
(Int -> CEGISResult exception -> ShowS)
-> (CEGISResult exception -> String)
-> ([CEGISResult exception] -> ShowS)
-> Show (CEGISResult exception)
forall exception.
Show exception =>
Int -> CEGISResult exception -> ShowS
forall exception.
Show exception =>
[CEGISResult exception] -> ShowS
forall exception. Show exception => CEGISResult exception -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall exception.
Show exception =>
Int -> CEGISResult exception -> ShowS
showsPrec :: Int -> CEGISResult exception -> ShowS
$cshow :: forall exception. Show exception => CEGISResult exception -> String
show :: CEGISResult exception -> String
$cshowList :: forall exception.
Show exception =>
[CEGISResult exception] -> ShowS
showList :: [CEGISResult exception] -> ShowS
Show)
genericCEGIS ::
(ConfigurableSolver config handle) =>
config ->
SymBool ->
SynthesisConstraintFun input ->
verifierState ->
StatefulVerifierFun verifierState input exception ->
IO ([input], CEGISResult exception)
genericCEGIS :: forall config handle input verifierState exception.
ConfigurableSolver config handle =>
config
-> SymBool
-> SynthesisConstraintFun input
-> verifierState
-> StatefulVerifierFun verifierState input exception
-> IO ([input], CEGISResult exception)
genericCEGIS config
config SymBool
initConstr SynthesisConstraintFun input
synthConstr verifierState
initVerifierState StatefulVerifierFun verifierState input exception
verifier =
config
-> (handle -> IO ([input], CEGISResult exception))
-> IO ([input], CEGISResult exception)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([input], CEGISResult exception))
-> IO ([input], CEGISResult exception))
-> (handle -> IO ([input], CEGISResult exception))
-> IO ([input], CEGISResult exception)
forall a b. (a -> b) -> a -> b
$ \handle
solver -> do
Either SolvingFailure Model
firstResult <- handle -> SymBool -> IO (Either SolvingFailure Model)
forall handle.
Solver handle =>
handle -> SymBool -> IO (Either SolvingFailure Model)
solverSolve handle
solver SymBool
initConstr
case Either SolvingFailure Model
firstResult of
Left SolvingFailure
err -> ([input], CEGISResult exception)
-> IO ([input], CEGISResult exception)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], SolvingFailure -> CEGISResult exception
forall exception. SolvingFailure -> CEGISResult exception
CEGISSolverFailure SolvingFailure
err)
Right Model
model -> handle
-> Model
-> Int
-> verifierState
-> IO ([input], CEGISResult exception)
forall {t}.
Solver t =>
t
-> Model
-> Int
-> verifierState
-> IO ([input], CEGISResult exception)
go handle
solver Model
model Int
0 verifierState
initVerifierState
where
go :: t
-> Model
-> Int
-> verifierState
-> IO ([input], CEGISResult exception)
go t
solver Model
prevModel Int
iterNum verifierState
verifierState = do
(verifierState
newVerifierState, VerifierResult input exception
verifierResult) <-
StatefulVerifierFun verifierState input exception
verifier verifierState
verifierState Model
prevModel
case VerifierResult input exception
verifierResult of
CEGISVerifierFoundCex input
cex -> do
Either SolvingFailure Model
newResult <- t -> SymBool -> IO (Either SolvingFailure Model)
forall handle.
Solver handle =>
handle -> SymBool -> IO (Either SolvingFailure Model)
solverSolve t
solver (SymBool -> IO (Either SolvingFailure Model))
-> IO SymBool -> IO (Either SolvingFailure Model)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SynthesisConstraintFun input
synthConstr Int
iterNum input
cex
case Either SolvingFailure Model
newResult of
Left SolvingFailure
err -> ([input], CEGISResult exception)
-> IO ([input], CEGISResult exception)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], SolvingFailure -> CEGISResult exception
forall exception. SolvingFailure -> CEGISResult exception
CEGISSolverFailure SolvingFailure
err)
Right Model
model -> do
([input]
cexes, CEGISResult exception
result) <- t
-> Model
-> Int
-> verifierState
-> IO ([input], CEGISResult exception)
go t
solver Model
model (Int
iterNum Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) verifierState
newVerifierState
([input], CEGISResult exception)
-> IO ([input], CEGISResult exception)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (input
cex input -> [input] -> [input]
forall a. a -> [a] -> [a]
: [input]
cexes, CEGISResult exception
result)
VerifierResult input exception
CEGISVerifierNoCex -> ([input], CEGISResult exception)
-> IO ([input], CEGISResult exception)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Model -> CEGISResult exception
forall exception. Model -> CEGISResult exception
CEGISSuccess Model
prevModel)
CEGISVerifierException exception
exception ->
([input], CEGISResult exception)
-> IO ([input], CEGISResult exception)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], exception -> CEGISResult exception
forall exception. exception -> CEGISResult exception
CEGISVerifierFailure exception
exception)
data CEGISMultiInputsState input = CEGISMultiInputsState
{ forall input. CEGISMultiInputsState input -> [input]
_cegisMultiInputsRemainingSymInputs :: [input],
forall input. CEGISMultiInputsState input -> SymBool
_cegisMultiInputsPre :: SymBool,
forall input. CEGISMultiInputsState input -> SymBool
_cegisMultiInputsPost :: SymBool
}
data CEGISCondition = CEGISCondition SymBool SymBool
deriving ((forall x. CEGISCondition -> Rep CEGISCondition x)
-> (forall x. Rep CEGISCondition x -> CEGISCondition)
-> Generic CEGISCondition
forall x. Rep CEGISCondition x -> CEGISCondition
forall x. CEGISCondition -> Rep CEGISCondition x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CEGISCondition -> Rep CEGISCondition x
from :: forall x. CEGISCondition -> Rep CEGISCondition x
$cto :: forall x. Rep CEGISCondition x -> CEGISCondition
to :: forall x. Rep CEGISCondition x -> CEGISCondition
Generic)
deriving (Bool -> Model -> CEGISCondition -> CEGISCondition
(Bool -> Model -> CEGISCondition -> CEGISCondition)
-> EvaluateSym CEGISCondition
forall a. (Bool -> Model -> a -> a) -> EvaluateSym a
$cevaluateSym :: Bool -> Model -> CEGISCondition -> CEGISCondition
evaluateSym :: Bool -> Model -> CEGISCondition -> CEGISCondition
EvaluateSym) via (Default CEGISCondition)
cegisPostCond :: SymBool -> CEGISCondition
cegisPostCond :: SymBool -> CEGISCondition
cegisPostCond = SymBool -> SymBool -> CEGISCondition
CEGISCondition (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True)
cegisPrePost :: SymBool -> SymBool -> CEGISCondition
cegisPrePost :: SymBool -> SymBool -> CEGISCondition
cegisPrePost = SymBool -> SymBool -> CEGISCondition
CEGISCondition
deriving via (Default CEGISCondition) instance Mergeable CEGISCondition
deriving via (Default CEGISCondition) instance SimpleMergeable CEGISCondition
cegisMultiInputs ::
( EvaluateSym input,
ExtractSymbolics input,
ConfigurableSolver config handle
) =>
config ->
[input] ->
(input -> CEGISCondition) ->
IO ([input], CEGISResult SolvingFailure)
cegisMultiInputs :: forall input config handle.
(EvaluateSym input, ExtractSymbolics input,
ConfigurableSolver config handle) =>
config
-> [input]
-> (input -> CEGISCondition)
-> IO ([input], CEGISResult SolvingFailure)
cegisMultiInputs config
config [input]
inputs input -> CEGISCondition
toCEGISCondition = do
SymBool
initConstr <- [input] -> IO SymBool
cexesAssertFun [input]
conInputs
config
-> SymBool
-> SynthesisConstraintFun input
-> CEGISMultiInputsState input
-> StatefulVerifierFun
(CEGISMultiInputsState input) input SolvingFailure
-> IO ([input], CEGISResult SolvingFailure)
forall config handle input verifierState exception.
ConfigurableSolver config handle =>
config
-> SymBool
-> SynthesisConstraintFun input
-> verifierState
-> StatefulVerifierFun verifierState input exception
-> IO ([input], CEGISResult exception)
genericCEGIS
config
config
SymBool
initConstr
SynthesisConstraintFun input
forall {m :: * -> *} {p}. Monad m => p -> input -> m SymBool
synthConstr
([input] -> SymBool -> SymBool -> CEGISMultiInputsState input
forall input.
[input] -> SymBool -> SymBool -> CEGISMultiInputsState input
CEGISMultiInputsState [input]
symInputs (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True) (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True))
StatefulVerifierFun
(CEGISMultiInputsState input) input SolvingFailure
verifier
where
([input]
conInputs, [input]
symInputs) = (input -> Bool) -> [input] -> ([input], [input])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (SymbolSet -> Bool
forall symbolSet (typedSymbol :: * -> *).
SymbolSetOps symbolSet typedSymbol =>
symbolSet -> Bool
isEmptySet (SymbolSet -> Bool) -> (input -> SymbolSet) -> input -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. input -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics) [input]
inputs
forallSymbols :: SymbolSet
forallSymbols = [input] -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics [input]
symInputs
cexAssertFun :: input -> m SymBool
cexAssertFun input
input = do
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (SymbolSet -> Bool
forall symbolSet (typedSymbol :: * -> *).
SymbolSetOps symbolSet typedSymbol =>
symbolSet -> Bool
isEmptySet (input -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics input
input)) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall a. HasCallStack => String -> a
error String
"BUG"
CEGISCondition SymBool
pre SymBool
post <- CEGISCondition -> m CEGISCondition
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (CEGISCondition -> m CEGISCondition)
-> CEGISCondition -> m CEGISCondition
forall a b. (a -> b) -> a -> b
$ input -> CEGISCondition
toCEGISCondition input
input
SymBool -> m SymBool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBool -> m SymBool) -> SymBool -> m SymBool
forall a b. (a -> b) -> a -> b
$ SymBool
pre SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool
post
cexesAssertFun :: [input] -> IO SymBool
cexesAssertFun = (SymBool -> input -> IO SymBool)
-> SymBool -> [input] -> IO SymBool
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\SymBool
acc input
x -> (SymBool
acc SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&&) (SymBool -> SymBool) -> IO SymBool -> IO SymBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> input -> IO SymBool
forall {m :: * -> *}. Monad m => input -> m SymBool
cexAssertFun input
x) (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True)
synthConstr :: p -> input -> m SymBool
synthConstr p
_ = input -> m SymBool
forall {m :: * -> *}. Monad m => input -> m SymBool
cexAssertFun
verifier :: StatefulVerifierFun
(CEGISMultiInputsState input) input SolvingFailure
verifier state :: CEGISMultiInputsState input
state@(CEGISMultiInputsState [] SymBool
_ SymBool
_) Model
_ =
(CEGISMultiInputsState input, VerifierResult input SolvingFailure)
-> IO
(CEGISMultiInputsState input, VerifierResult input SolvingFailure)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CEGISMultiInputsState input
state, VerifierResult input SolvingFailure
forall input exception. VerifierResult input exception
CEGISVerifierNoCex)
verifier
(CEGISMultiInputsState (input
nextSymInput : [input]
symInputs) SymBool
pre SymBool
post)
Model
candidate = do
CEGISCondition SymBool
nextPre SymBool
nextPost <-
CEGISCondition -> IO CEGISCondition
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CEGISCondition -> IO CEGISCondition)
-> CEGISCondition -> IO CEGISCondition
forall a b. (a -> b) -> a -> b
$ input -> CEGISCondition
toCEGISCondition input
nextSymInput
let newPre :: SymBool
newPre = SymBool
pre SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool
nextPre
let newPost :: SymBool
newPost = SymBool
post SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool
nextPost
let evaluated :: SymBool
evaluated =
Bool -> Model -> SymBool -> SymBool
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
False (SymbolSet -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
symbolSet -> model -> model
exceptFor SymbolSet
forallSymbols Model
candidate) (SymBool -> SymBool) -> SymBool -> SymBool
forall a b. (a -> b) -> a -> b
$
SymBool
newPre SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot SymBool
newPost
Either SolvingFailure Model
r <- config -> SymBool -> IO (Either SolvingFailure Model)
forall config handle.
ConfigurableSolver config handle =>
config -> SymBool -> IO (Either SolvingFailure Model)
solve config
config SymBool
evaluated
case Either SolvingFailure Model
r of
Left SolvingFailure
Unsat ->
StatefulVerifierFun
(CEGISMultiInputsState input) input SolvingFailure
verifier ([input] -> SymBool -> SymBool -> CEGISMultiInputsState input
forall input.
[input] -> SymBool -> SymBool -> CEGISMultiInputsState input
CEGISMultiInputsState [input]
symInputs SymBool
newPre SymBool
newPost) Model
candidate
Left SolvingFailure
err ->
(CEGISMultiInputsState input, VerifierResult input SolvingFailure)
-> IO
(CEGISMultiInputsState input, VerifierResult input SolvingFailure)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return
( [input] -> SymBool -> SymBool -> CEGISMultiInputsState input
forall input.
[input] -> SymBool -> SymBool -> CEGISMultiInputsState input
CEGISMultiInputsState [] SymBool
newPre SymBool
newPost,
SolvingFailure -> VerifierResult input SolvingFailure
forall input exception. exception -> VerifierResult input exception
CEGISVerifierException SolvingFailure
err
)
Right Model
model ->
(CEGISMultiInputsState input, VerifierResult input SolvingFailure)
-> IO
(CEGISMultiInputsState input, VerifierResult input SolvingFailure)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return
( [input] -> SymBool -> SymBool -> CEGISMultiInputsState input
forall input.
[input] -> SymBool -> SymBool -> CEGISMultiInputsState input
CEGISMultiInputsState (input
nextSymInput input -> [input] -> [input]
forall a. a -> [a] -> [a]
: [input]
symInputs) SymBool
newPre SymBool
newPost,
input -> VerifierResult input SolvingFailure
forall input exception. input -> VerifierResult input exception
CEGISVerifierFoundCex (input -> VerifierResult input SolvingFailure)
-> input -> VerifierResult input SolvingFailure
forall a b. (a -> b) -> a -> b
$
Bool -> Model -> input -> input
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
False (SymbolSet -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
symbolSet -> model -> model
exact SymbolSet
forallSymbols Model
model) input
nextSymInput
)
cegis ::
( ConfigurableSolver config handle,
EvaluateSym inputs,
ExtractSymbolics inputs,
SEq inputs
) =>
config ->
inputs ->
(inputs -> CEGISCondition) ->
IO ([inputs], CEGISResult SolvingFailure)
cegis :: forall config handle inputs.
(ConfigurableSolver config handle, EvaluateSym inputs,
ExtractSymbolics inputs, SEq inputs) =>
config
-> inputs
-> (inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure)
cegis config
config inputs
inputs = config
-> [inputs]
-> (inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure)
forall input config handle.
(EvaluateSym input, ExtractSymbolics input,
ConfigurableSolver config handle) =>
config
-> [input]
-> (input -> CEGISCondition)
-> IO ([input], CEGISResult SolvingFailure)
cegisMultiInputs config
config [inputs
inputs]
cegisExceptMultiInputs ::
( ConfigurableSolver config handle,
EvaluateSym inputs,
ExtractSymbolics inputs,
UnionWithExcept t u e v,
PlainUnion u,
Monad u
) =>
config ->
[inputs] ->
(Either e v -> CEGISCondition) ->
(inputs -> t) ->
IO ([inputs], CEGISResult SolvingFailure)
cegisExceptMultiInputs :: forall config handle inputs t (u :: * -> *) e v.
(ConfigurableSolver config handle, EvaluateSym inputs,
ExtractSymbolics inputs, UnionWithExcept t u e v, PlainUnion u,
Monad u) =>
config
-> [inputs]
-> (Either e v -> CEGISCondition)
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
cegisExceptMultiInputs config
config [inputs]
cexes Either e v -> CEGISCondition
interpretFun inputs -> t
f =
config
-> [inputs]
-> (inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure)
forall input config handle.
(EvaluateSym input, ExtractSymbolics input,
ConfigurableSolver config handle) =>
config
-> [input]
-> (input -> CEGISCondition)
-> IO ([input], CEGISResult SolvingFailure)
cegisMultiInputs
config
config
[inputs]
cexes
(u CEGISCondition -> CEGISCondition
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (u CEGISCondition -> CEGISCondition)
-> (inputs -> u CEGISCondition) -> inputs -> CEGISCondition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Either e v -> CEGISCondition
interpretFun (Either e v -> CEGISCondition)
-> u (Either e v) -> u CEGISCondition
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (u (Either e v) -> u CEGISCondition)
-> (inputs -> u (Either e v)) -> inputs -> u CEGISCondition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> u (Either e v)
forall t (u :: * -> *) e v.
UnionWithExcept t u e v =>
t -> u (Either e v)
extractUnionExcept (t -> u (Either e v)) -> (inputs -> t) -> inputs -> u (Either e v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. inputs -> t
f)
cegisExceptVCMultiInputs ::
( ConfigurableSolver config handle,
EvaluateSym inputs,
ExtractSymbolics inputs,
UnionWithExcept t u e v,
PlainUnion u,
Monad u
) =>
config ->
[inputs] ->
(Either e v -> u (Either VerificationConditions ())) ->
(inputs -> t) ->
IO ([inputs], CEGISResult SolvingFailure)
cegisExceptVCMultiInputs :: forall config handle inputs t (u :: * -> *) e v.
(ConfigurableSolver config handle, EvaluateSym inputs,
ExtractSymbolics inputs, UnionWithExcept t u e v, PlainUnion u,
Monad u) =>
config
-> [inputs]
-> (Either e v -> u (Either VerificationConditions ()))
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
cegisExceptVCMultiInputs config
config [inputs]
cexes Either e v -> u (Either VerificationConditions ())
interpretFun inputs -> t
f =
config
-> [inputs]
-> (inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure)
forall input config handle.
(EvaluateSym input, ExtractSymbolics input,
ConfigurableSolver config handle) =>
config
-> [input]
-> (input -> CEGISCondition)
-> IO ([input], CEGISResult SolvingFailure)
cegisMultiInputs
config
config
[inputs]
cexes
( \inputs
v ->
u CEGISCondition -> CEGISCondition
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge
( ( \case
Left VerificationConditions
AssumptionViolation -> SymBool -> SymBool -> CEGISCondition
cegisPrePost (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False) (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True)
Left VerificationConditions
AssertionViolation -> SymBool -> CEGISCondition
cegisPostCond (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False)
Either VerificationConditions ()
_ -> SymBool -> CEGISCondition
cegisPostCond (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True)
)
(Either VerificationConditions () -> CEGISCondition)
-> u (Either VerificationConditions ()) -> u CEGISCondition
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 (inputs -> t
f inputs
v) u (Either e v)
-> (Either e v -> u (Either VerificationConditions ()))
-> u (Either VerificationConditions ())
forall a b. u a -> (a -> u b) -> u b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Either e v -> u (Either VerificationConditions ())
interpretFun)
)
)
cegisExceptStdVCMultiInputs ::
( ConfigurableSolver config handle,
EvaluateSym inputs,
ExtractSymbolics inputs,
UnionWithExcept t u VerificationConditions (),
PlainUnion u,
Monad u
) =>
config ->
[inputs] ->
(inputs -> t) ->
IO ([inputs], CEGISResult SolvingFailure)
cegisExceptStdVCMultiInputs :: forall config handle inputs t (u :: * -> *).
(ConfigurableSolver config handle, EvaluateSym inputs,
ExtractSymbolics inputs,
UnionWithExcept t u VerificationConditions (), PlainUnion u,
Monad u) =>
config
-> [inputs]
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
cegisExceptStdVCMultiInputs config
config [inputs]
cexes =
config
-> [inputs]
-> (Either VerificationConditions ()
-> u (Either VerificationConditions ()))
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
forall config handle inputs t (u :: * -> *) e v.
(ConfigurableSolver config handle, EvaluateSym inputs,
ExtractSymbolics inputs, UnionWithExcept t u e v, PlainUnion u,
Monad u) =>
config
-> [inputs]
-> (Either e v -> u (Either VerificationConditions ()))
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
cegisExceptVCMultiInputs config
config [inputs]
cexes Either VerificationConditions ()
-> u (Either VerificationConditions ())
forall a. a -> u a
forall (m :: * -> *) a. Monad m => a -> m a
return
cegisExcept ::
( UnionWithExcept t u e v,
PlainUnion u,
Functor u,
EvaluateSym inputs,
ExtractSymbolics inputs,
ConfigurableSolver config handle,
SEq inputs
) =>
config ->
inputs ->
(Either e v -> CEGISCondition) ->
(inputs -> t) ->
IO ([inputs], CEGISResult SolvingFailure)
cegisExcept :: forall t (u :: * -> *) e v inputs config handle.
(UnionWithExcept t u e v, PlainUnion u, Functor u,
EvaluateSym inputs, ExtractSymbolics inputs,
ConfigurableSolver config handle, SEq inputs) =>
config
-> inputs
-> (Either e v -> CEGISCondition)
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
cegisExcept config
config inputs
inputs Either e v -> CEGISCondition
f inputs -> t
v =
config
-> inputs
-> (inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure)
forall config handle inputs.
(ConfigurableSolver config handle, EvaluateSym inputs,
ExtractSymbolics inputs, SEq inputs) =>
config
-> inputs
-> (inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure)
cegis config
config inputs
inputs ((inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure))
-> (inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \inputs
i -> u CEGISCondition -> CEGISCondition
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (u CEGISCondition -> CEGISCondition)
-> u CEGISCondition -> CEGISCondition
forall a b. (a -> b) -> a -> b
$ Either e v -> CEGISCondition
f (Either e v -> CEGISCondition)
-> u (Either e v) -> u CEGISCondition
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 (inputs -> t
v inputs
i)
cegisExceptVC ::
( UnionWithExcept t u e v,
PlainUnion u,
Monad u,
EvaluateSym inputs,
ExtractSymbolics inputs,
ConfigurableSolver config handle,
SEq inputs
) =>
config ->
inputs ->
(Either e v -> u (Either VerificationConditions ())) ->
(inputs -> t) ->
IO ([inputs], CEGISResult SolvingFailure)
cegisExceptVC :: forall t (u :: * -> *) e v inputs config handle.
(UnionWithExcept t u e v, PlainUnion u, Monad u,
EvaluateSym inputs, ExtractSymbolics inputs,
ConfigurableSolver config handle, SEq inputs) =>
config
-> inputs
-> (Either e v -> u (Either VerificationConditions ()))
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
cegisExceptVC config
config inputs
inputs Either e v -> u (Either VerificationConditions ())
f inputs -> t
v = do
config
-> inputs
-> (inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure)
forall config handle inputs.
(ConfigurableSolver config handle, EvaluateSym inputs,
ExtractSymbolics inputs, SEq inputs) =>
config
-> inputs
-> (inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure)
cegis config
config inputs
inputs ((inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure))
-> (inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \inputs
i ->
u CEGISCondition -> CEGISCondition
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (u CEGISCondition -> CEGISCondition)
-> u CEGISCondition -> CEGISCondition
forall a b. (a -> b) -> a -> b
$
( \case
Left VerificationConditions
AssumptionViolation -> SymBool -> SymBool -> CEGISCondition
cegisPrePost (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False) (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True)
Left VerificationConditions
AssertionViolation -> SymBool -> CEGISCondition
cegisPostCond (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False)
Either VerificationConditions ()
_ -> SymBool -> CEGISCondition
cegisPostCond (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True)
)
(Either VerificationConditions () -> CEGISCondition)
-> u (Either VerificationConditions ()) -> u CEGISCondition
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 (inputs -> t
v inputs
i) u (Either e v)
-> (Either e v -> u (Either VerificationConditions ()))
-> u (Either VerificationConditions ())
forall a b. u a -> (a -> u b) -> u b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Either e v -> u (Either VerificationConditions ())
f)
cegisExceptStdVC ::
( UnionWithExcept t u VerificationConditions (),
PlainUnion u,
Monad u,
EvaluateSym inputs,
ExtractSymbolics inputs,
ConfigurableSolver config handle,
SEq inputs
) =>
config ->
inputs ->
(inputs -> t) ->
IO ([inputs], CEGISResult SolvingFailure)
cegisExceptStdVC :: forall t (u :: * -> *) inputs config handle.
(UnionWithExcept t u VerificationConditions (), PlainUnion u,
Monad u, EvaluateSym inputs, ExtractSymbolics inputs,
ConfigurableSolver config handle, SEq inputs) =>
config
-> inputs
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
cegisExceptStdVC config
config inputs
inputs = config
-> inputs
-> (Either VerificationConditions ()
-> u (Either VerificationConditions ()))
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
forall t (u :: * -> *) e v inputs config handle.
(UnionWithExcept t u e v, PlainUnion u, Monad u,
EvaluateSym inputs, ExtractSymbolics inputs,
ConfigurableSolver config handle, SEq inputs) =>
config
-> inputs
-> (Either e v -> u (Either VerificationConditions ()))
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
cegisExceptVC config
config inputs
inputs Either VerificationConditions ()
-> u (Either VerificationConditions ())
forall a. a -> u a
forall (m :: * -> *) a. Monad m => a -> m a
return
cegisForAll ::
( ExtractSymbolics forallInput,
ConfigurableSolver config handle
) =>
config ->
forallInput ->
CEGISCondition ->
IO ([Model], CEGISResult SolvingFailure)
cegisForAll :: forall forallInput config handle.
(ExtractSymbolics forallInput, ConfigurableSolver config handle) =>
config
-> forallInput
-> CEGISCondition
-> IO ([Model], CEGISResult SolvingFailure)
cegisForAll config
config forallInput
input (CEGISCondition SymBool
pre SymBool
post) = do
([Model]
models, CEGISResult SolvingFailure
result) <- config
-> SymBool
-> SynthesisConstraintFun Model
-> ()
-> StatefulVerifierFun () Model SolvingFailure
-> IO ([Model], CEGISResult SolvingFailure)
forall config handle input verifierState exception.
ConfigurableSolver config handle =>
config
-> SymBool
-> SynthesisConstraintFun input
-> verifierState
-> StatefulVerifierFun verifierState input exception
-> IO ([input], CEGISResult exception)
genericCEGIS config
config SymBool
phi SynthesisConstraintFun Model
forall {m :: * -> *} {p}. Monad m => p -> Model -> m SymBool
synthConstr () StatefulVerifierFun () Model SolvingFailure
verifier
let exactResult :: CEGISResult SolvingFailure
exactResult = case CEGISResult SolvingFailure
result of
CEGISSuccess Model
model -> Model -> CEGISResult SolvingFailure
forall exception. Model -> CEGISResult exception
CEGISSuccess (Model -> CEGISResult SolvingFailure)
-> Model -> CEGISResult SolvingFailure
forall a b. (a -> b) -> a -> b
$ SymbolSet -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
symbolSet -> model -> model
exceptFor SymbolSet
forallSymbols Model
model
CEGISResult SolvingFailure
_ -> CEGISResult SolvingFailure
result
([Model], CEGISResult SolvingFailure)
-> IO ([Model], CEGISResult SolvingFailure)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Model]
models, CEGISResult SolvingFailure
exactResult)
where
phi :: SymBool
phi = SymBool
pre SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool
post
negphi :: SymBool
negphi = SymBool
pre SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot SymBool
post
forallSymbols :: SymbolSet
forallSymbols = forallInput -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics forallInput
input
synthConstr :: p -> Model -> m SymBool
synthConstr p
_ Model
model = SymBool -> m SymBool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBool -> m SymBool) -> SymBool -> m SymBool
forall a b. (a -> b) -> a -> b
$ Bool -> Model -> SymBool -> SymBool
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
False Model
model SymBool
phi
verifier :: StatefulVerifierFun () Model SolvingFailure
verifier () Model
candidate = do
let evaluated :: SymBool
evaluated =
Bool -> Model -> SymBool -> SymBool
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
False (SymbolSet -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
symbolSet -> model -> model
exceptFor SymbolSet
forallSymbols Model
candidate) SymBool
negphi
Either SolvingFailure Model
r <- config -> SymBool -> IO (Either SolvingFailure Model)
forall config handle.
ConfigurableSolver config handle =>
config -> SymBool -> IO (Either SolvingFailure Model)
solve config
config SymBool
evaluated
case Either SolvingFailure Model
r of
Left SolvingFailure
Unsat -> ((), VerifierResult Model SolvingFailure)
-> IO ((), VerifierResult Model SolvingFailure)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((), VerifierResult Model SolvingFailure
forall input exception. VerifierResult input exception
CEGISVerifierNoCex)
Left SolvingFailure
err -> ((), VerifierResult Model SolvingFailure)
-> IO ((), VerifierResult Model SolvingFailure)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((), SolvingFailure -> VerifierResult Model SolvingFailure
forall input exception. exception -> VerifierResult input exception
CEGISVerifierException SolvingFailure
err)
Right Model
model ->
((), VerifierResult Model SolvingFailure)
-> IO ((), VerifierResult Model SolvingFailure)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((), Model -> VerifierResult Model SolvingFailure
forall input exception. input -> VerifierResult input exception
CEGISVerifierFoundCex (Model -> VerifierResult Model SolvingFailure)
-> Model -> VerifierResult Model SolvingFailure
forall a b. (a -> b) -> a -> b
$ SymbolSet -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
symbolSet -> model -> model
exact SymbolSet
forallSymbols Model
model)
cegisForAllExcept ::
( UnionWithExcept t u e v,
PlainUnion u,
Functor u,
EvaluateSym inputs,
ExtractSymbolics inputs,
ConfigurableSolver config handle,
SEq inputs
) =>
config ->
inputs ->
(Either e v -> CEGISCondition) ->
t ->
IO ([Model], CEGISResult SolvingFailure)
cegisForAllExcept :: forall t (u :: * -> *) e v inputs config handle.
(UnionWithExcept t u e v, PlainUnion u, Functor u,
EvaluateSym inputs, ExtractSymbolics inputs,
ConfigurableSolver config handle, SEq inputs) =>
config
-> inputs
-> (Either e v -> CEGISCondition)
-> t
-> IO ([Model], CEGISResult SolvingFailure)
cegisForAllExcept config
config inputs
inputs Either e v -> CEGISCondition
f t
v =
config
-> inputs
-> CEGISCondition
-> IO ([Model], CEGISResult SolvingFailure)
forall forallInput config handle.
(ExtractSymbolics forallInput, ConfigurableSolver config handle) =>
config
-> forallInput
-> CEGISCondition
-> IO ([Model], CEGISResult SolvingFailure)
cegisForAll config
config inputs
inputs (CEGISCondition -> IO ([Model], CEGISResult SolvingFailure))
-> CEGISCondition -> IO ([Model], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ u CEGISCondition -> CEGISCondition
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (u CEGISCondition -> CEGISCondition)
-> u CEGISCondition -> CEGISCondition
forall a b. (a -> b) -> a -> b
$ Either e v -> CEGISCondition
f (Either e v -> CEGISCondition)
-> u (Either e v) -> u CEGISCondition
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
cegisForAllExceptVC ::
( UnionWithExcept t u e v,
PlainUnion u,
Monad u,
EvaluateSym inputs,
ExtractSymbolics inputs,
ConfigurableSolver config handle,
SEq inputs
) =>
config ->
inputs ->
(Either e v -> u (Either VerificationConditions ())) ->
t ->
IO ([Model], CEGISResult SolvingFailure)
cegisForAllExceptVC :: forall t (u :: * -> *) e v inputs config handle.
(UnionWithExcept t u e v, PlainUnion u, Monad u,
EvaluateSym inputs, ExtractSymbolics inputs,
ConfigurableSolver config handle, SEq inputs) =>
config
-> inputs
-> (Either e v -> u (Either VerificationConditions ()))
-> t
-> IO ([Model], CEGISResult SolvingFailure)
cegisForAllExceptVC config
config inputs
inputs Either e v -> u (Either VerificationConditions ())
f t
v = do
config
-> inputs
-> CEGISCondition
-> IO ([Model], CEGISResult SolvingFailure)
forall forallInput config handle.
(ExtractSymbolics forallInput, ConfigurableSolver config handle) =>
config
-> forallInput
-> CEGISCondition
-> IO ([Model], CEGISResult SolvingFailure)
cegisForAll config
config inputs
inputs (CEGISCondition -> IO ([Model], CEGISResult SolvingFailure))
-> CEGISCondition -> IO ([Model], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$
u CEGISCondition -> CEGISCondition
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (u CEGISCondition -> CEGISCondition)
-> u CEGISCondition -> CEGISCondition
forall a b. (a -> b) -> a -> b
$
( \case
Left VerificationConditions
AssumptionViolation -> SymBool -> SymBool -> CEGISCondition
cegisPrePost (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False) (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True)
Left VerificationConditions
AssertionViolation -> SymBool -> CEGISCondition
cegisPostCond (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False)
Either VerificationConditions ()
_ -> SymBool -> CEGISCondition
cegisPostCond (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True)
)
(Either VerificationConditions () -> CEGISCondition)
-> u (Either VerificationConditions ()) -> u CEGISCondition
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 u (Either e v)
-> (Either e v -> u (Either VerificationConditions ()))
-> u (Either VerificationConditions ())
forall a b. u a -> (a -> u b) -> u b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Either e v -> u (Either VerificationConditions ())
f)
cegisForAllExceptStdVC ::
( UnionWithExcept t u VerificationConditions (),
PlainUnion u,
Monad u,
EvaluateSym inputs,
ExtractSymbolics inputs,
ConfigurableSolver config handle,
SEq inputs
) =>
config ->
inputs ->
t ->
IO ([Model], CEGISResult SolvingFailure)
cegisForAllExceptStdVC :: forall t (u :: * -> *) inputs config handle.
(UnionWithExcept t u VerificationConditions (), PlainUnion u,
Monad u, EvaluateSym inputs, ExtractSymbolics inputs,
ConfigurableSolver config handle, SEq inputs) =>
config -> inputs -> t -> IO ([Model], CEGISResult SolvingFailure)
cegisForAllExceptStdVC config
config inputs
inputs = config
-> inputs
-> (Either VerificationConditions ()
-> u (Either VerificationConditions ()))
-> t
-> IO ([Model], CEGISResult SolvingFailure)
forall t (u :: * -> *) e v inputs config handle.
(UnionWithExcept t u e v, PlainUnion u, Monad u,
EvaluateSym inputs, ExtractSymbolics inputs,
ConfigurableSolver config handle, SEq inputs) =>
config
-> inputs
-> (Either e v -> u (Either VerificationConditions ()))
-> t
-> IO ([Model], CEGISResult SolvingFailure)
cegisForAllExceptVC config
config inputs
inputs Either VerificationConditions ()
-> u (Either VerificationConditions ())
forall a. a -> u a
forall (m :: * -> *) a. Monad m => a -> m a
return