{-# 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
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.Core.Data.Class.CEGISSolver
  ( -- * Note for the examples

    --

    -- | The examples assumes that the [z3](https://github.com/Z3Prover/z3)
    -- solver is available in @PATH@.

    -- * Generic CEGIS interface
    VerifierResult (..),
    SynthesisConstraintFun,
    VerifierFun,
    CEGISResult (..),
    solverGenericCEGIS,
    solverGenericCEGISWithRefinement,
    genericCEGIS,
    genericCEGISWithRefinement,

    -- * CEGIS interfaces with pre/post conditions
    CEGISCondition (..),
    cegisPostCond,
    cegisPrePost,
    solverCegisMultiInputs,
    solverCegis,
    solverCegisExcept,
    solverCegisExceptStdVC,
    solverCegisExceptVC,
    solverCegisExceptMultiInputs,
    solverCegisExceptStdVCMultiInputs,
    solverCegisExceptVCMultiInputs,
    solverCegisForAll,
    solverCegisForAllExcept,
    solverCegisForAllExceptStdVC,
    solverCegisForAllExceptVC,
    cegisMultiInputs,
    cegis,
    cegisExcept,
    cegisExceptStdVC,
    cegisExceptVC,
    cegisExceptMultiInputs,
    cegisExceptStdVCMultiInputs,
    cegisExceptVCMultiInputs,
    cegisForAll,
    cegisForAllExcept,
    cegisForAllExceptStdVC,
    cegisForAllExceptVC,
  )
where

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 (solverResetAssertions),
    SolvingFailure (Unsat),
    UnionWithExcept (extractUnionExcept),
    solverSolve,
    withSolver,
  )
import Grisette.Internal.SymPrim.Prim.Model (Model)
import Grisette.Internal.SymPrim.SymBool (SymBool)
import Grisette.Lib.Data.Foldable (symAll)

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.Lib.Base
-- >>> import Grisette.SymPrim
-- >>> import Grisette.Backend

-- | The response from a verifier.
data VerifierResult cex exception
  = CEGISVerifierFoundCex cex
  | CEGISVerifierNoCex
  | CEGISVerifierException exception

-- | Build the synthesizer constraint from the verfication result. The first
-- argument will be guaranteed to be distinct during each invocation of the
-- function in the CEGIS algorithm, so it can be used to instantiate the
-- identifiers for fresh variables.
type SynthesisConstraintFun cex = cex -> IO SymBool

-- | The verifier.
type VerifierFun cex exception = Model -> IO (VerifierResult cex exception)

type RefinementConditionFun = Model -> IO SymBool

-- | The result of the CEGIS procedure.
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)

-- | Generic CEGIS procedure. See 'genericCEGIS' for more details.
--
-- The difference from 'genericCEGIS' is that this function accepts a solver
-- handle for the synthesizer, instead of a solver configuration.
solverGenericCEGIS ::
  (Solver handle) =>
  -- | Configuration of the solver.
  handle ->
  -- | Whether we should rerun the passed verifiers if any other verifier found
  -- a counter-example.
  Bool ->
  -- | The initial synthesis constraint.
  SymBool ->
  -- | Synthesis constraint from counter-examples
  SynthesisConstraintFun input ->
  -- | The verifier functions.
  [VerifierFun input exception] ->
  IO ([input], CEGISResult exception)
solverGenericCEGIS :: forall handle input exception.
Solver handle =>
handle
-> Bool
-> SymBool
-> SynthesisConstraintFun input
-> [VerifierFun input exception]
-> IO ([input], CEGISResult exception)
solverGenericCEGIS handle
solver Bool
rerun SymBool
initConstr SynthesisConstraintFun input
synthConstr [VerifierFun input exception]
verifiers = 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 -> Model
-> Bool
-> [VerifierFun input exception]
-> IO ([input], CEGISResult exception)
go Model
model Bool
False [VerifierFun input exception]
verifiers
  where
    go :: Model
-> Bool
-> [VerifierFun input exception]
-> IO ([input], CEGISResult exception)
go Model
prevModel Bool
needRerun (VerifierFun input exception
verifier : [VerifierFun input exception]
remainingVerifiers) = do
      VerifierResult input exception
verifierResult <- VerifierFun input exception
verifier Model
prevModel
      case VerifierResult input exception
verifierResult of
        CEGISVerifierFoundCex input
cex -> do
          Either SolvingFailure Model
newResult <- handle -> SymBool -> IO (Either SolvingFailure Model)
forall handle.
Solver handle =>
handle -> SymBool -> IO (Either SolvingFailure Model)
solverSolve handle
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 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) <-
                Model
-> Bool
-> [VerifierFun input exception]
-> IO ([input], CEGISResult exception)
go Model
model (Bool
needRerun Bool -> Bool -> Bool
|| Bool
rerun) ([VerifierFun input exception]
 -> IO ([input], CEGISResult exception))
-> [VerifierFun input exception]
-> IO ([input], CEGISResult exception)
forall a b. (a -> b) -> a -> b
$
                  VerifierFun input exception
verifier VerifierFun input exception
-> [VerifierFun input exception] -> [VerifierFun input exception]
forall a. a -> [a] -> [a]
: [VerifierFun input exception]
remainingVerifiers
              ([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 -> Model
-> Bool
-> [VerifierFun input exception]
-> IO ([input], CEGISResult exception)
go Model
prevModel Bool
needRerun [VerifierFun input exception]
remainingVerifiers
        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)
    go Model
prevModel Bool
False [] = ([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)
    go Model
prevModel Bool
True [] = Model
-> Bool
-> [VerifierFun input exception]
-> IO ([input], CEGISResult exception)
go Model
prevModel Bool
False [VerifierFun input exception]
verifiers

-- | Generic CEGIS procedure with refinement. See 'genericCEGISWithRefinement'
-- for more details.
--
-- The difference from 'genericCEGISWithRefinement' is that this function
-- accepts a solver handle for the synthesizer, instead of a solver
-- configuration.
solverGenericCEGISWithRefinement ::
  (Solver handle) =>
  -- | Configuration of the solver.
  handle ->
  -- | Whether we should rerun the passed verifiers if any other verifier found
  -- a counter-example.
  Bool ->
  -- | The initial synthesis constraint.
  SymBool ->
  -- | Synthesis constraint from counter-examples
  SynthesisConstraintFun input ->
  -- | Refinement condition generator.
  Maybe RefinementConditionFun ->
  -- | The verifier functions.
  [VerifierFun input exception] ->
  IO ([input], CEGISResult exception)
solverGenericCEGISWithRefinement :: forall handle input exception.
Solver handle =>
handle
-> Bool
-> SymBool
-> SynthesisConstraintFun input
-> Maybe RefinementConditionFun
-> [VerifierFun input exception]
-> IO ([input], CEGISResult exception)
solverGenericCEGISWithRefinement
  handle
solver
  Bool
rerun
  SymBool
initConstr
  SynthesisConstraintFun input
synthConstr
  Maybe RefinementConditionFun
refineCond
  [VerifierFun input exception]
verifiers = do
    ([input]
input, CEGISResult exception
r) <-
      handle
-> Bool
-> SymBool
-> SynthesisConstraintFun input
-> [VerifierFun input exception]
-> IO ([input], CEGISResult exception)
forall handle input exception.
Solver handle =>
handle
-> Bool
-> SymBool
-> SynthesisConstraintFun input
-> [VerifierFun input exception]
-> IO ([input], CEGISResult exception)
solverGenericCEGIS handle
solver Bool
rerun SymBool
initConstr SynthesisConstraintFun input
synthConstr [VerifierFun input exception]
verifiers
    case CEGISResult exception
r of
      CEGISSuccess Model
model -> handle -> [input] -> Model -> IO ([input], CEGISResult exception)
forall {t} {exception}.
Solver t =>
t -> [input] -> Model -> IO ([input], CEGISResult exception)
refine handle
solver [input]
input Model
model
      CEGISResult exception
_ -> ([input], CEGISResult exception)
-> IO ([input], CEGISResult exception)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([input]
input, CEGISResult exception
r)
    where
      refine :: t -> [input] -> Model -> IO ([input], CEGISResult exception)
refine t
solver [input]
input Model
model = case Maybe RefinementConditionFun
refineCond of
        Just RefinementConditionFun
f -> do
          SymBool
cond <- RefinementConditionFun
f Model
model
          ([input], CEGISResult exception)
newResult <-
            t
-> Bool
-> SymBool
-> SynthesisConstraintFun input
-> [VerifierFun input exception]
-> IO ([input], CEGISResult exception)
forall handle input exception.
Solver handle =>
handle
-> Bool
-> SymBool
-> SynthesisConstraintFun input
-> [VerifierFun input exception]
-> IO ([input], CEGISResult exception)
solverGenericCEGIS t
solver Bool
rerun SymBool
cond SynthesisConstraintFun input
synthConstr [VerifierFun input exception]
verifiers
          case ([input], CEGISResult exception)
newResult of
            ([input]
newInputs, CEGISSuccess Model
model) ->
              t -> [input] -> Model -> IO ([input], CEGISResult exception)
refine t
solver ([input]
input [input] -> [input] -> [input]
forall a. [a] -> [a] -> [a]
++ [input]
newInputs) Model
model
            ([input], CEGISResult exception)
_ -> ([input], CEGISResult exception)
-> IO ([input], CEGISResult exception)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([input]
input, Model -> CEGISResult exception
forall exception. Model -> CEGISResult exception
CEGISSuccess Model
model)
        Maybe RefinementConditionFun
Nothing -> ([input], CEGISResult exception)
-> IO ([input], CEGISResult exception)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([input]
input, Model -> CEGISResult exception
forall exception. Model -> CEGISResult exception
CEGISSuccess Model
model)

-- | Generic CEGIS procedure.
--
-- The CEGIS procedure will try to find a model that satisfies the initial
-- synthesis constraint, and satisfies all the inputs generated by the verifier.
genericCEGIS ::
  (ConfigurableSolver config handle) =>
  -- | Configuration of the solver.
  config ->
  -- | Whether we should rerun the passed verifiers if any other verifier found
  -- a counter-example.
  Bool ->
  -- | The initial synthesis constraint.
  SymBool ->
  -- | Synthesis constraint from counter-examples
  SynthesisConstraintFun input ->
  -- | The verifier functions.
  [VerifierFun input exception] ->
  IO ([input], CEGISResult exception)
genericCEGIS :: forall config handle input exception.
ConfigurableSolver config handle =>
config
-> Bool
-> SymBool
-> SynthesisConstraintFun input
-> [VerifierFun input exception]
-> IO ([input], CEGISResult exception)
genericCEGIS config
config Bool
rerun SymBool
initConstr SynthesisConstraintFun input
synthConstr [VerifierFun 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 ->
    handle
-> Bool
-> SymBool
-> SynthesisConstraintFun input
-> [VerifierFun input exception]
-> IO ([input], CEGISResult exception)
forall handle input exception.
Solver handle =>
handle
-> Bool
-> SymBool
-> SynthesisConstraintFun input
-> [VerifierFun input exception]
-> IO ([input], CEGISResult exception)
solverGenericCEGIS handle
solver Bool
rerun SymBool
initConstr SynthesisConstraintFun input
synthConstr [VerifierFun input exception]
verifier

-- | Generic CEGIS procedure.
--
-- The CEGIS procedure will try to find a model that satisfies the initial
-- synthesis constraint, and satisfies all the inputs generated by the verifier.
genericCEGISWithRefinement ::
  (ConfigurableSolver config handle) =>
  -- | Configuration of the solver.
  config ->
  -- | Whether we should rerun the passed verifiers if any other verifier found
  -- a counter-example.
  Bool ->
  -- | The initial synthesis constraint.
  SymBool ->
  -- | Synthesis constraint from counter-examples
  SynthesisConstraintFun input ->
  -- | Refinement condition generator.
  Maybe RefinementConditionFun ->
  -- | The verifier functions.
  [VerifierFun input exception] ->
  IO ([input], CEGISResult exception)
genericCEGISWithRefinement :: forall config handle input exception.
ConfigurableSolver config handle =>
config
-> Bool
-> SymBool
-> SynthesisConstraintFun input
-> Maybe RefinementConditionFun
-> [VerifierFun input exception]
-> IO ([input], CEGISResult exception)
genericCEGISWithRefinement
  config
config
  Bool
rerun
  SymBool
initConstr
  SynthesisConstraintFun input
synthConstr
  Maybe RefinementConditionFun
refineCond
  [VerifierFun 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
      handle
-> Bool
-> SymBool
-> SynthesisConstraintFun input
-> Maybe RefinementConditionFun
-> [VerifierFun input exception]
-> IO ([input], CEGISResult exception)
forall handle input exception.
Solver handle =>
handle
-> Bool
-> SymBool
-> SynthesisConstraintFun input
-> Maybe RefinementConditionFun
-> [VerifierFun input exception]
-> IO ([input], CEGISResult exception)
solverGenericCEGISWithRefinement
        handle
solver
        Bool
rerun
        SymBool
initConstr
        SynthesisConstraintFun input
synthConstr
        Maybe RefinementConditionFun
refineCond
        [VerifierFun input exception]
verifier

-- | The condition for CEGIS to solve.
--
-- The first argument is the pre-condition, and the second argument is the
-- post-condition.
--
-- The CEGIS procedures would try to find a model for the formula
--
-- \[
--   \forall P. (\exists I. \mathrm{pre}(P, I)) \wedge (\forall I. \mathrm{pre}(P, I)\implies \mathrm{post}(P, I))
-- \]
--
-- In program synthesis tasks, \(P\) is the symbolic constants in the symbolic
-- program, and \(I\) is the input. The pre-condition is used to restrict the
-- search space of the program. The procedure would only return programs that
-- meets the pre-conditions on every possible inputs, and there are at least
-- one possible input. The post-condition is used to specify the desired program
-- behaviors.
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)

-- | Construct a CEGIS condition with only a post-condition. The pre-condition
-- would be set to true, meaning that all programs in the program space are
-- allowed.
cegisPostCond :: SymBool -> CEGISCondition
cegisPostCond :: SymBool -> CEGISCondition
cegisPostCond = SymBool -> SymBool -> CEGISCondition
CEGISCondition (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True)

-- | Construct a CEGIS condition with both pre- and post-conditions.
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

-- | CEGIS with multiple (possibly symbolic) inputs. See 'cegisMultiInputs' for
-- more details.
--
-- The difference from 'cegisMultiInputs' is that this function accepts two
-- solver handles, one for the synthesizer and one for the verifier.
--
-- The synthesizer solver will **not** be reset, while the verifier solver will
-- be reset after each iteration.
solverCegisMultiInputs ::
  ( EvaluateSym input,
    ExtractSymbolics input,
    Solver handle
  ) =>
  -- The synthesizer solver handle
  handle ->
  -- The verifier solver handle
  handle ->
  -- | Initial symbolic inputs. The solver will try to find a
  -- program that works on all the inputs representable by these inputs (see
  -- 'CEGISCondition').
  [input] ->
  -- | The condition for the solver to solve. All the
  -- symbolic constants that are not in the inputs will
  -- be considered as part of the symbolic program.
  (input -> CEGISCondition) ->
  -- | The counter-examples generated
  -- during the CEGIS loop, and the
  -- model found by the solver.
  IO ([input], CEGISResult SolvingFailure)
solverCegisMultiInputs :: forall input handle.
(EvaluateSym input, ExtractSymbolics input, Solver handle) =>
handle
-> handle
-> [input]
-> (input -> CEGISCondition)
-> IO ([input], CEGISResult SolvingFailure)
solverCegisMultiInputs
  handle
synthesizerSolver
  handle
verifierSolver
  [input]
inputs
  input -> CEGISCondition
toCEGISCondition = do
    handle
-> Bool
-> SymBool
-> SynthesisConstraintFun input
-> [VerifierFun input SolvingFailure]
-> IO ([input], CEGISResult SolvingFailure)
forall handle input exception.
Solver handle =>
handle
-> Bool
-> SymBool
-> SynthesisConstraintFun input
-> [VerifierFun input exception]
-> IO ([input], CEGISResult exception)
solverGenericCEGIS
      handle
synthesizerSolver
      Bool
True
      ((input -> SymBool) -> [input] -> SymBool
forall (t :: * -> *) a.
Foldable t =>
(a -> SymBool) -> t a -> SymBool
symAll input -> SymBool
cexAssertFun [input]
conInputs)
      (SymBool -> IO SymBool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBool -> IO SymBool)
-> (input -> SymBool) -> SynthesisConstraintFun input
forall b c a. (b -> c) -> (a -> b) -> a -> c
. input -> SymBool
cexAssertFun)
      ([VerifierFun input SolvingFailure]
 -> IO ([input], CEGISResult SolvingFailure))
-> [VerifierFun input SolvingFailure]
-> IO ([input], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ input -> VerifierFun input SolvingFailure
getVerifier (input -> VerifierFun input SolvingFailure)
-> [input] -> [VerifierFun input SolvingFailure]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [input]
symInputs
    where
      cexAssertFun :: input -> SymBool
cexAssertFun input
input =
        case input -> CEGISCondition
toCEGISCondition input
input of
          CEGISCondition SymBool
pre SymBool
post -> SymBool
pre SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool
post
      getVerifier :: input -> VerifierFun input SolvingFailure
getVerifier input
input Model
md = do
        let CEGISCondition SymBool
pre SymBool
post = input -> CEGISCondition
toCEGISCondition input
input
        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 (input -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics input
input) Model
md) (SymBool -> SymBool) -> SymBool -> SymBool
forall a b. (a -> b) -> a -> b
$
                SymBool
pre SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot SymBool
post
        handle -> IO (Either SolvingFailure ())
forall handle.
Solver handle =>
handle -> IO (Either SolvingFailure ())
solverResetAssertions handle
verifierSolver
        Either SolvingFailure Model
r <- handle -> SymBool -> IO (Either SolvingFailure Model)
forall handle.
Solver handle =>
handle -> SymBool -> IO (Either SolvingFailure Model)
solverSolve handle
verifierSolver SymBool
evaluated
        case Either SolvingFailure Model
r of
          Left SolvingFailure
Unsat -> VerifierResult input SolvingFailure
-> IO (VerifierResult input SolvingFailure)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return VerifierResult input SolvingFailure
forall cex exception. VerifierResult cex exception
CEGISVerifierNoCex
          Left SolvingFailure
err -> VerifierResult input SolvingFailure
-> IO (VerifierResult input SolvingFailure)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (VerifierResult input SolvingFailure
 -> IO (VerifierResult input SolvingFailure))
-> VerifierResult input SolvingFailure
-> IO (VerifierResult input SolvingFailure)
forall a b. (a -> b) -> a -> b
$ SolvingFailure -> VerifierResult input SolvingFailure
forall cex exception. exception -> VerifierResult cex exception
CEGISVerifierException SolvingFailure
err
          Right Model
model -> do
            let newCexInput :: input
newCexInput =
                  Bool -> Model -> input -> input
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
True (SymbolSet -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
symbolSet -> model -> model
exact (input -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics input
input) Model
model) input
input
            VerifierResult input SolvingFailure
-> IO (VerifierResult input SolvingFailure)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (VerifierResult input SolvingFailure
 -> IO (VerifierResult input SolvingFailure))
-> VerifierResult input SolvingFailure
-> IO (VerifierResult input SolvingFailure)
forall a b. (a -> b) -> a -> b
$ input -> VerifierResult input SolvingFailure
forall cex exception. cex -> VerifierResult cex exception
CEGISVerifierFoundCex input
newCexInput
      ([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

-- | CEGIS with a single symbolic input to represent a set of inputs. See
-- 'cegis' for more details.
--
-- The difference from 'cegis' is that this function accepts two solver handles,
-- one for the synthesizer and one for the verifier.
--
-- The synthesizer solver will **not** be reset, while the verifier solver will
-- be reset after each iteration.
solverCegis ::
  ( Solver handle,
    EvaluateSym inputs,
    ExtractSymbolics inputs,
    SEq inputs
  ) =>
  -- | The synthesizer solver handle
  handle ->
  -- | The verifier solver handle
  handle ->
  -- | Initial symbolic inputs. The solver will try to find a
  -- program that works on all the inputs representable by it (see
  -- 'CEGISCondition').
  inputs ->
  -- | The condition for the solver to solve. All the
  -- symbolic constants that are not in the inputs will
  -- be considered as part of the symbolic program.
  (inputs -> CEGISCondition) ->
  -- | The counter-examples generated
  -- during the CEGIS loop, and the
  -- model found by the solver.
  IO ([inputs], CEGISResult SolvingFailure)
solverCegis :: forall handle inputs.
(Solver handle, EvaluateSym inputs, ExtractSymbolics inputs,
 SEq inputs) =>
handle
-> handle
-> inputs
-> (inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure)
solverCegis handle
synthesizerSolver handle
verifierSolver inputs
inputs =
  handle
-> handle
-> [inputs]
-> (inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure)
forall input handle.
(EvaluateSym input, ExtractSymbolics input, Solver handle) =>
handle
-> handle
-> [input]
-> (input -> CEGISCondition)
-> IO ([input], CEGISResult SolvingFailure)
solverCegisMultiInputs handle
synthesizerSolver handle
verifierSolver [inputs
inputs]

-- |
-- CEGIS for symbolic programs with error handling, using multiple (possibly
-- symbolic) inputs to represent a set of inputs.
--
-- The difference from 'cegisExceptMultiInputs' is that this function accepts
-- two solver handles, one for the synthesizer and one for the verifier.
--
-- The synthesizer solver will **not** be reset, while the verifier solver will
-- be reset after each iteration.
solverCegisExceptMultiInputs ::
  ( Solver handle,
    EvaluateSym inputs,
    ExtractSymbolics inputs,
    UnionWithExcept t u e v,
    PlainUnion u,
    Monad u
  ) =>
  handle ->
  handle ->
  [inputs] ->
  (Either e v -> CEGISCondition) ->
  (inputs -> t) ->
  IO ([inputs], CEGISResult SolvingFailure)
solverCegisExceptMultiInputs :: forall handle inputs t (u :: * -> *) e v.
(Solver handle, EvaluateSym inputs, ExtractSymbolics inputs,
 UnionWithExcept t u e v, PlainUnion u, Monad u) =>
handle
-> handle
-> [inputs]
-> (Either e v -> CEGISCondition)
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
solverCegisExceptMultiInputs
  handle
synthesizerSolver
  handle
verifierSolver
  [inputs]
cexes
  Either e v -> CEGISCondition
interpretFun
  inputs -> t
f =
    handle
-> handle
-> [inputs]
-> (inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure)
forall input handle.
(EvaluateSym input, ExtractSymbolics input, Solver handle) =>
handle
-> handle
-> [input]
-> (input -> CEGISCondition)
-> IO ([input], CEGISResult SolvingFailure)
solverCegisMultiInputs
      handle
synthesizerSolver
      handle
verifierSolver
      [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)

-- |
-- CEGIS for symbolic programs with error handling, using multiple (possibly
-- symbolic) inputs to represent a set of inputs.
--
-- The errors should be translated to assertion or assumption violations.
--
-- The difference from 'cegisExceptVCMultiInputs' is that this function accepts
-- two solver handles, one for the synthesizer and one for the verifier.
--
-- The synthesizer solver will **not** be reset, while the verifier solver will
-- be reset after each iteration.
solverCegisExceptVCMultiInputs ::
  ( Solver handle,
    EvaluateSym inputs,
    ExtractSymbolics inputs,
    UnionWithExcept t u e v,
    PlainUnion u,
    Monad u
  ) =>
  handle ->
  handle ->
  [inputs] ->
  (Either e v -> u (Either VerificationConditions ())) ->
  (inputs -> t) ->
  IO ([inputs], CEGISResult SolvingFailure)
solverCegisExceptVCMultiInputs :: forall handle inputs t (u :: * -> *) e v.
(Solver handle, EvaluateSym inputs, ExtractSymbolics inputs,
 UnionWithExcept t u e v, PlainUnion u, Monad u) =>
handle
-> handle
-> [inputs]
-> (Either e v -> u (Either VerificationConditions ()))
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
solverCegisExceptVCMultiInputs
  handle
synthesizerSolver
  handle
verifierSolver
  [inputs]
cexes
  Either e v -> u (Either VerificationConditions ())
interpretFun
  inputs -> t
f =
    handle
-> handle
-> [inputs]
-> (inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure)
forall input handle.
(EvaluateSym input, ExtractSymbolics input, Solver handle) =>
handle
-> handle
-> [input]
-> (input -> CEGISCondition)
-> IO ([input], CEGISResult SolvingFailure)
solverCegisMultiInputs
      handle
synthesizerSolver
      handle
verifierSolver
      [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)
            )
      )

-- |
-- CEGIS for symbolic programs with error handling, using multiple (possibly
-- symbolic) inputs to represent a set of inputs. See
-- 'cegisExceptStdVCMultiInputs' for more details.
--
-- The difference from 'cegisExceptStdVCMultiInputs' is that this function
-- accepts two solver handles, one for the synthesizer and one for the verifier.
--
-- The synthesizer solver will **not** be reset, while the verifier solver will
-- be reset after each iteration.
solverCegisExceptStdVCMultiInputs ::
  ( Solver handle,
    EvaluateSym inputs,
    ExtractSymbolics inputs,
    UnionWithExcept t u VerificationConditions (),
    PlainUnion u,
    Monad u
  ) =>
  handle ->
  handle ->
  [inputs] ->
  (inputs -> t) ->
  IO ([inputs], CEGISResult SolvingFailure)
solverCegisExceptStdVCMultiInputs :: forall handle inputs t (u :: * -> *).
(Solver handle, EvaluateSym inputs, ExtractSymbolics inputs,
 UnionWithExcept t u VerificationConditions (), PlainUnion u,
 Monad u) =>
handle
-> handle
-> [inputs]
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
solverCegisExceptStdVCMultiInputs handle
synthesizerSolver handle
verifierSolver [inputs]
cexes =
  handle
-> handle
-> [inputs]
-> (Either VerificationConditions ()
    -> u (Either VerificationConditions ()))
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
forall handle inputs t (u :: * -> *) e v.
(Solver handle, EvaluateSym inputs, ExtractSymbolics inputs,
 UnionWithExcept t u e v, PlainUnion u, Monad u) =>
handle
-> handle
-> [inputs]
-> (Either e v -> u (Either VerificationConditions ()))
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
solverCegisExceptVCMultiInputs handle
synthesizerSolver handle
verifierSolver [inputs]
cexes Either VerificationConditions ()
-> u (Either VerificationConditions ())
forall a. a -> u a
forall (m :: * -> *) a. Monad m => a -> m a
return

-- |
-- CEGIS for symbolic programs with error handling, using a single symbolic
-- input to represent a set of inputs. See 'cegisExcept' for more details.
--
-- The difference from 'cegisExcept' is that this function accepts two solver
-- handles, one for the synthesizer and one for the verifier.
--
-- The synthesizer solver will **not** be reset, while the verifier solver will
-- be reset after each iteration.
solverCegisExcept ::
  ( UnionWithExcept t u e v,
    PlainUnion u,
    Functor u,
    EvaluateSym inputs,
    ExtractSymbolics inputs,
    Solver handle,
    SEq inputs
  ) =>
  handle ->
  handle ->
  inputs ->
  (Either e v -> CEGISCondition) ->
  (inputs -> t) ->
  IO ([inputs], CEGISResult SolvingFailure)
solverCegisExcept :: forall t (u :: * -> *) e v inputs handle.
(UnionWithExcept t u e v, PlainUnion u, Functor u,
 EvaluateSym inputs, ExtractSymbolics inputs, Solver handle,
 SEq inputs) =>
handle
-> handle
-> inputs
-> (Either e v -> CEGISCondition)
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
solverCegisExcept handle
synthesizerSolver handle
verifierSolver inputs
inputs Either e v -> CEGISCondition
f inputs -> t
v =
  handle
-> handle
-> inputs
-> (inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure)
forall handle inputs.
(Solver handle, EvaluateSym inputs, ExtractSymbolics inputs,
 SEq inputs) =>
handle
-> handle
-> inputs
-> (inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure)
solverCegis handle
synthesizerSolver handle
verifierSolver 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)

-- |
-- CEGIS for symbolic programs with error handling, using a single symbolic
-- input to represent a set of inputs.
--
-- The errors should be translated to assertion or assumption violations.
--
-- The difference from 'cegisExceptVC' is that this function accepts two solver
-- handles, one for the synthesizer and one for the verifier.
--
-- The synthesizer solver will **not** be reset, while the verifier solver will
-- be reset after each iteration.
solverCegisExceptVC ::
  ( UnionWithExcept t u e v,
    PlainUnion u,
    Monad u,
    EvaluateSym inputs,
    ExtractSymbolics inputs,
    Solver handle,
    SEq inputs
  ) =>
  handle ->
  handle ->
  inputs ->
  (Either e v -> u (Either VerificationConditions ())) ->
  (inputs -> t) ->
  IO ([inputs], CEGISResult SolvingFailure)
solverCegisExceptVC :: forall t (u :: * -> *) e v inputs handle.
(UnionWithExcept t u e v, PlainUnion u, Monad u,
 EvaluateSym inputs, ExtractSymbolics inputs, Solver handle,
 SEq inputs) =>
handle
-> handle
-> inputs
-> (Either e v -> u (Either VerificationConditions ()))
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
solverCegisExceptVC handle
synthesizerSolver handle
verifierSolver inputs
inputs Either e v -> u (Either VerificationConditions ())
f inputs -> t
v = do
  handle
-> handle
-> inputs
-> (inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure)
forall handle inputs.
(Solver handle, EvaluateSym inputs, ExtractSymbolics inputs,
 SEq inputs) =>
handle
-> handle
-> inputs
-> (inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure)
solverCegis handle
synthesizerSolver handle
verifierSolver 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)

-- |
-- CEGIS for symbolic programs with error handling, using a single symbolic
-- input to represent a set of inputs. See 'cegisExceptStdVC' for more details.
--
-- The difference from 'cegisExceptStdVC' is that this function accepts two
-- solver handles, one for the synthesizer and one for the verifier.
--
-- The synthesizer solver will **not** be reset, while the verifier solver will
-- be reset after each iteration.
solverCegisExceptStdVC ::
  ( UnionWithExcept t u VerificationConditions (),
    PlainUnion u,
    Monad u,
    EvaluateSym inputs,
    ExtractSymbolics inputs,
    Solver handle,
    SEq inputs
  ) =>
  handle ->
  handle ->
  inputs ->
  (inputs -> t) ->
  IO ([inputs], CEGISResult SolvingFailure)
solverCegisExceptStdVC :: forall t (u :: * -> *) inputs handle.
(UnionWithExcept t u VerificationConditions (), PlainUnion u,
 Monad u, EvaluateSym inputs, ExtractSymbolics inputs,
 Solver handle, SEq inputs) =>
handle
-> handle
-> inputs
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
solverCegisExceptStdVC handle
synthesizerSolver handle
verifierSolver inputs
inputs =
  handle
-> handle
-> inputs
-> (Either VerificationConditions ()
    -> u (Either VerificationConditions ()))
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
forall t (u :: * -> *) e v inputs handle.
(UnionWithExcept t u e v, PlainUnion u, Monad u,
 EvaluateSym inputs, ExtractSymbolics inputs, Solver handle,
 SEq inputs) =>
handle
-> handle
-> inputs
-> (Either e v -> u (Either VerificationConditions ()))
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
solverCegisExceptVC handle
synthesizerSolver handle
verifierSolver inputs
inputs Either VerificationConditions ()
-> u (Either VerificationConditions ())
forall a. a -> u a
forall (m :: * -> *) a. Monad m => a -> m a
return

-- |
-- CEGIS with a single symbolic input to represent a set of inputs. See
-- 'cegisForAll' for more details.
--
-- The difference from 'cegisForAll' is that this function accepts two solver
-- handles, one for the synthesizer and one for the verifier.
--
-- The synthesizer solver will **not** be reset, while the verifier solver will
-- be reset after each iteration.
solverCegisForAll ::
  ( ExtractSymbolics forallInput,
    Solver handle
  ) =>
  handle ->
  handle ->
  -- | A symbolic value. All the symbolic constants in the value are treated as
  -- for-all variables.
  forallInput ->
  CEGISCondition ->
  -- | First output are the counter-examples for all the for-all variables, and
  -- the second output is the model for all other variables if CEGIS succeeds.
  IO ([Model], CEGISResult SolvingFailure)
solverCegisForAll :: forall forallInput handle.
(ExtractSymbolics forallInput, Solver handle) =>
handle
-> handle
-> forallInput
-> CEGISCondition
-> IO ([Model], CEGISResult SolvingFailure)
solverCegisForAll
  handle
synthesizerSolver
  handle
verifierSolver
  forallInput
input
  (CEGISCondition SymBool
pre SymBool
post) = do
    ([Model]
models, CEGISResult SolvingFailure
result) <-
      handle
-> Bool
-> SymBool
-> RefinementConditionFun
-> [VerifierFun Model SolvingFailure]
-> IO ([Model], CEGISResult SolvingFailure)
forall handle input exception.
Solver handle =>
handle
-> Bool
-> SymBool
-> SynthesisConstraintFun input
-> [VerifierFun input exception]
-> IO ([input], CEGISResult exception)
solverGenericCEGIS
        handle
synthesizerSolver
        Bool
False
        SymBool
phi
        (\Model
md -> SymBool -> IO SymBool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBool -> IO SymBool) -> SymBool -> IO SymBool
forall a b. (a -> b) -> a -> b
$ Bool -> Model -> SymBool -> SymBool
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
False Model
md SymBool
phi)
        [VerifierFun 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
      verifier :: VerifierFun 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
        handle -> IO (Either SolvingFailure ())
forall handle.
Solver handle =>
handle -> IO (Either SolvingFailure ())
solverResetAssertions handle
verifierSolver
        Either SolvingFailure Model
r <- handle -> SymBool -> IO (Either SolvingFailure Model)
forall handle.
Solver handle =>
handle -> SymBool -> IO (Either SolvingFailure Model)
solverSolve handle
verifierSolver 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 cex exception. VerifierResult cex 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 (VerifierResult Model SolvingFailure
 -> IO (VerifierResult Model SolvingFailure))
-> VerifierResult Model SolvingFailure
-> IO (VerifierResult Model SolvingFailure)
forall a b. (a -> b) -> a -> b
$ SolvingFailure -> VerifierResult Model SolvingFailure
forall cex exception. exception -> VerifierResult cex 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 (VerifierResult Model SolvingFailure
 -> IO (VerifierResult Model SolvingFailure))
-> VerifierResult Model SolvingFailure
-> IO (VerifierResult Model SolvingFailure)
forall a b. (a -> b) -> a -> b
$ Model -> VerifierResult Model SolvingFailure
forall cex exception. cex -> VerifierResult cex exception
CEGISVerifierFoundCex (SymbolSet -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
symbolSet -> model -> model
exact SymbolSet
forallSymbols Model
model)

-- |
-- CEGIS for symbolic programs with error handling, with a forall variable.
--
-- See 'cegisForAllExcept', 'cegisForAll' and 'cegisExcept'.
--
-- The difference from 'cegisForAllExcept' is that this function accepts two
-- solver handles, one for the synthesizer and one for the verifier.
--
-- The synthesizer solver will **not** be reset, while the verifier solver will
-- be reset after each iteration.
solverCegisForAllExcept ::
  ( UnionWithExcept t u e v,
    PlainUnion u,
    Functor u,
    EvaluateSym inputs,
    ExtractSymbolics inputs,
    Solver handle,
    SEq inputs
  ) =>
  handle ->
  handle ->
  inputs ->
  (Either e v -> CEGISCondition) ->
  t ->
  IO ([Model], CEGISResult SolvingFailure)
solverCegisForAllExcept :: forall t (u :: * -> *) e v inputs handle.
(UnionWithExcept t u e v, PlainUnion u, Functor u,
 EvaluateSym inputs, ExtractSymbolics inputs, Solver handle,
 SEq inputs) =>
handle
-> handle
-> inputs
-> (Either e v -> CEGISCondition)
-> t
-> IO ([Model], CEGISResult SolvingFailure)
solverCegisForAllExcept handle
synthesizerSolver handle
verifierSolver inputs
inputs Either e v -> CEGISCondition
f t
v =
  handle
-> handle
-> inputs
-> CEGISCondition
-> IO ([Model], CEGISResult SolvingFailure)
forall forallInput handle.
(ExtractSymbolics forallInput, Solver handle) =>
handle
-> handle
-> forallInput
-> CEGISCondition
-> IO ([Model], CEGISResult SolvingFailure)
solverCegisForAll handle
synthesizerSolver handle
verifierSolver 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

-- |
-- CEGIS for symbolic programs with error handling, with a forall variable.
--
-- See 'cegisForAllExceptVC' 'cegisForAll' and 'cegisExceptVC'.
--
-- The difference from 'cegisForAllExceptVC' is that this function accepts two
-- solver handles, one for the synthesizer and one for the verifier.
--
-- The synthesizer solver will **not** be reset, while the verifier solver will
-- be reset after each iteration.
solverCegisForAllExceptVC ::
  ( UnionWithExcept t u e v,
    PlainUnion u,
    Monad u,
    EvaluateSym inputs,
    ExtractSymbolics inputs,
    Solver handle,
    SEq inputs
  ) =>
  handle ->
  handle ->
  inputs ->
  (Either e v -> u (Either VerificationConditions ())) ->
  t ->
  IO ([Model], CEGISResult SolvingFailure)
solverCegisForAllExceptVC :: forall t (u :: * -> *) e v inputs handle.
(UnionWithExcept t u e v, PlainUnion u, Monad u,
 EvaluateSym inputs, ExtractSymbolics inputs, Solver handle,
 SEq inputs) =>
handle
-> handle
-> inputs
-> (Either e v -> u (Either VerificationConditions ()))
-> t
-> IO ([Model], CEGISResult SolvingFailure)
solverCegisForAllExceptVC handle
synthesizerSolver handle
verifierSolver inputs
inputs Either e v -> u (Either VerificationConditions ())
f t
v = do
  handle
-> handle
-> inputs
-> CEGISCondition
-> IO ([Model], CEGISResult SolvingFailure)
forall forallInput handle.
(ExtractSymbolics forallInput, Solver handle) =>
handle
-> handle
-> forallInput
-> CEGISCondition
-> IO ([Model], CEGISResult SolvingFailure)
solverCegisForAll handle
synthesizerSolver handle
verifierSolver 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)

-- |
-- CEGIS for symbolic programs with error handling, with a forall variable.
--
-- See 'cegisForAllExceptStdVC' 'cegisForAll' and 'cegisExceptStdVC'.
--
-- The difference from 'cegisForAllExceptStdVC' is that this function accepts
-- two solver handles, one for the synthesizer and one for the verifier.
--
-- The synthesizer solver will **not** be reset, while the verifier solver will
-- be reset after each iteration.
solverCegisForAllExceptStdVC ::
  ( UnionWithExcept t u VerificationConditions (),
    PlainUnion u,
    Monad u,
    EvaluateSym inputs,
    ExtractSymbolics inputs,
    Solver handle,
    SEq inputs
  ) =>
  handle ->
  handle ->
  inputs ->
  t ->
  IO ([Model], CEGISResult SolvingFailure)
solverCegisForAllExceptStdVC :: forall t (u :: * -> *) inputs handle.
(UnionWithExcept t u VerificationConditions (), PlainUnion u,
 Monad u, EvaluateSym inputs, ExtractSymbolics inputs,
 Solver handle, SEq inputs) =>
handle
-> handle
-> inputs
-> t
-> IO ([Model], CEGISResult SolvingFailure)
solverCegisForAllExceptStdVC handle
synthesizerSolver handle
verifierSolver inputs
inputs =
  handle
-> handle
-> inputs
-> (Either VerificationConditions ()
    -> u (Either VerificationConditions ()))
-> t
-> IO ([Model], CEGISResult SolvingFailure)
forall t (u :: * -> *) e v inputs handle.
(UnionWithExcept t u e v, PlainUnion u, Monad u,
 EvaluateSym inputs, ExtractSymbolics inputs, Solver handle,
 SEq inputs) =>
handle
-> handle
-> inputs
-> (Either e v -> u (Either VerificationConditions ()))
-> t
-> IO ([Model], CEGISResult SolvingFailure)
solverCegisForAllExceptVC handle
synthesizerSolver handle
verifierSolver inputs
inputs Either VerificationConditions ()
-> u (Either VerificationConditions ())
forall a. a -> u a
forall (m :: * -> *) a. Monad m => a -> m a
return

-- |
-- CEGIS with multiple (possibly symbolic) inputs. Solves the following formula
-- (see 'CEGISCondition' for details).
--
-- \[
--   \forall P. (\exists I\in\mathrm{inputs}. \mathrm{pre}(P, I)) \wedge (\forall I\in\mathrm{inputs}. \mathrm{pre}(P, I)\implies \mathrm{post}(P, I))
-- \]
--
-- For simpler queries, where the inputs are representable by a single
-- symbolic value, you may want to use 'cegis' or 'cegisExcept' instead.
-- We have an example for the 'cegis' call.
cegisMultiInputs ::
  ( EvaluateSym input,
    ExtractSymbolics input,
    ConfigurableSolver config handle
  ) =>
  -- | The configuration of the solver
  config ->
  -- | Initial symbolic inputs. The solver will try to find a
  -- program that works on all the inputs representable by these inputs (see
  -- 'CEGISCondition').
  [input] ->
  -- | The condition for the solver to solve. All the
  -- symbolic constants that are not in the inputs will
  -- be considered as part of the symbolic program.
  (input -> CEGISCondition) ->
  -- | The counter-examples generated
  -- during the CEGIS loop, and the
  -- model found by the solver.
  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 =
  config
-> (handle -> IO ([input], CEGISResult SolvingFailure))
-> IO ([input], CEGISResult SolvingFailure)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([input], CEGISResult SolvingFailure))
 -> IO ([input], CEGISResult SolvingFailure))
-> (handle -> IO ([input], CEGISResult SolvingFailure))
-> IO ([input], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \handle
synthesizerSolver ->
    config
-> (handle -> IO ([input], CEGISResult SolvingFailure))
-> IO ([input], CEGISResult SolvingFailure)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([input], CEGISResult SolvingFailure))
 -> IO ([input], CEGISResult SolvingFailure))
-> (handle -> IO ([input], CEGISResult SolvingFailure))
-> IO ([input], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \handle
verifierSolver ->
      handle
-> handle
-> [input]
-> (input -> CEGISCondition)
-> IO ([input], CEGISResult SolvingFailure)
forall input handle.
(EvaluateSym input, ExtractSymbolics input, Solver handle) =>
handle
-> handle
-> [input]
-> (input -> CEGISCondition)
-> IO ([input], CEGISResult SolvingFailure)
solverCegisMultiInputs
        handle
synthesizerSolver
        handle
verifierSolver
        [input]
inputs
        input -> CEGISCondition
toCEGISCondition

-- |
-- CEGIS with a single symbolic input to represent a set of inputs.
--
-- The following example tries to find the value of @c@ such that for all
-- positive @x@, @x * c < 0 && c > -2@. The @c .> -2@ clause is used to make
-- the solution unique.
--
-- >>> :set -XOverloadedStrings
-- >>> let [x,c] = ["x","c"] :: [SymInteger]
-- >>> cegis (precise z3) x (\x -> cegisPrePost (x .> 0) (x * c .< 0 .&& c .> -2))
-- (...,CEGISSuccess (Model {c -> -1 :: Integer}))
cegis ::
  ( ConfigurableSolver config handle,
    EvaluateSym inputs,
    ExtractSymbolics inputs,
    SEq inputs
  ) =>
  -- | The configuration of the solver
  config ->
  -- | Initial symbolic inputs. The solver will try to find a
  -- program that works on all the inputs representable by it (see
  -- 'CEGISCondition').
  inputs ->
  -- | The condition for the solver to solve. All the
  -- symbolic constants that are not in the inputs will
  -- be considered as part of the symbolic program.
  (inputs -> CEGISCondition) ->
  -- | The counter-examples generated
  -- during the CEGIS loop, and the
  -- model found by the solver.
  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 inputs -> CEGISCondition
condition =
  config
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([inputs], CEGISResult SolvingFailure))
 -> IO ([inputs], CEGISResult SolvingFailure))
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \handle
synthesizerSolver ->
    config
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([inputs], CEGISResult SolvingFailure))
 -> IO ([inputs], CEGISResult SolvingFailure))
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \handle
verifierSolver ->
      handle
-> handle
-> inputs
-> (inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure)
forall handle inputs.
(Solver handle, EvaluateSym inputs, ExtractSymbolics inputs,
 SEq inputs) =>
handle
-> handle
-> inputs
-> (inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure)
solverCegis handle
synthesizerSolver handle
verifierSolver inputs
inputs inputs -> CEGISCondition
condition

-- |
-- CEGIS for symbolic programs with error handling, using multiple (possibly
-- symbolic) inputs to represent a set of 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
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([inputs], CEGISResult SolvingFailure))
 -> IO ([inputs], CEGISResult SolvingFailure))
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \handle
synthesizerSolver ->
    config
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([inputs], CEGISResult SolvingFailure))
 -> IO ([inputs], CEGISResult SolvingFailure))
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \handle
verifierSolver ->
      handle
-> handle
-> [inputs]
-> (Either e v -> CEGISCondition)
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
forall handle inputs t (u :: * -> *) e v.
(Solver handle, EvaluateSym inputs, ExtractSymbolics inputs,
 UnionWithExcept t u e v, PlainUnion u, Monad u) =>
handle
-> handle
-> [inputs]
-> (Either e v -> CEGISCondition)
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
solverCegisExceptMultiInputs
        handle
synthesizerSolver
        handle
verifierSolver
        [inputs]
cexes
        Either e v -> CEGISCondition
interpretFun
        inputs -> t
f

-- |
-- CEGIS for symbolic programs with error handling, using multiple (possibly
-- symbolic) inputs to represent a set of inputs.
--
-- The errors should be translated to assertion or assumption violations.
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
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([inputs], CEGISResult SolvingFailure))
 -> IO ([inputs], CEGISResult SolvingFailure))
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \handle
synthesizerSolver ->
    config
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([inputs], CEGISResult SolvingFailure))
 -> IO ([inputs], CEGISResult SolvingFailure))
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \handle
verifierSolver ->
      handle
-> handle
-> [inputs]
-> (Either e v -> u (Either VerificationConditions ()))
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
forall handle inputs t (u :: * -> *) e v.
(Solver handle, EvaluateSym inputs, ExtractSymbolics inputs,
 UnionWithExcept t u e v, PlainUnion u, Monad u) =>
handle
-> handle
-> [inputs]
-> (Either e v -> u (Either VerificationConditions ()))
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
solverCegisExceptVCMultiInputs
        handle
synthesizerSolver
        handle
verifierSolver
        [inputs]
cexes
        Either e v -> u (Either VerificationConditions ())
interpretFun
        inputs -> t
f

-- |
-- CEGIS for symbolic programs with error handling, using multiple (possibly
-- symbolic) inputs to represent a set of inputs. This function saves the
-- efforts to implement the translation function for the standard error type
-- 'VerificationConditions', and the standard result type '()'.
--
-- This function translates assumption violations to failed pre-conditions,
-- and translates assertion violations to failed post-conditions.
-- The '()' result will not fail any conditions.
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 inputs -> t
f =
  config
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([inputs], CEGISResult SolvingFailure))
 -> IO ([inputs], CEGISResult SolvingFailure))
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \handle
synthesizerSolver ->
    config
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([inputs], CEGISResult SolvingFailure))
 -> IO ([inputs], CEGISResult SolvingFailure))
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \handle
verifierSolver ->
      handle
-> handle
-> [inputs]
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
forall handle inputs t (u :: * -> *).
(Solver handle, EvaluateSym inputs, ExtractSymbolics inputs,
 UnionWithExcept t u VerificationConditions (), PlainUnion u,
 Monad u) =>
handle
-> handle
-> [inputs]
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
solverCegisExceptStdVCMultiInputs handle
synthesizerSolver handle
verifierSolver [inputs]
cexes inputs -> t
f

-- |
-- CEGIS for symbolic programs with error handling, using a single symbolic
-- input to represent a set of inputs.
--
-- 'cegisExcept' is particularly useful when custom error types are used.
-- With 'cegisExcept', you define how the errors are interpreted to the
-- CEGIS conditions after the symbolic evaluation. This could increase the
-- readability and modularity of the code.
--
-- The following example tries to find the value of @c@ such that for all
-- positive @x@, @x * c < 0 && c > -2@. The @c .> -2@ assertion is used to make
-- the solution unique.
--
-- >>> :set -XOverloadedStrings
-- >>> let [x,c] = ["x","c"] :: [SymInteger]
-- >>> import Control.Monad.Except
-- >>> :{
--   res :: SymInteger -> ExceptT VerificationConditions UnionM ()
--   res x = do
--     symAssume $ x .> 0
--     symAssert $ x * c .< 0
--     symAssert $ c .> -2
-- :}
--
-- >>> :{
--   translation (Left AssumptionViolation) = cegisPrePost (con False) (con True)
--   translation (Left AssertionViolation) = cegisPostCond (con False)
--   translation _ = cegisPostCond (con True)
-- :}
--
-- >>> cegisExcept (precise z3) x translation res
-- ([...],CEGISSuccess (Model {c -> -1 :: Integer}))
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
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([inputs], CEGISResult SolvingFailure))
 -> IO ([inputs], CEGISResult SolvingFailure))
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \handle
synthesizerSolver ->
    config
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([inputs], CEGISResult SolvingFailure))
 -> IO ([inputs], CEGISResult SolvingFailure))
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \handle
verifierSolver ->
      handle
-> handle
-> inputs
-> (Either e v -> CEGISCondition)
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
forall t (u :: * -> *) e v inputs handle.
(UnionWithExcept t u e v, PlainUnion u, Functor u,
 EvaluateSym inputs, ExtractSymbolics inputs, Solver handle,
 SEq inputs) =>
handle
-> handle
-> inputs
-> (Either e v -> CEGISCondition)
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
solverCegisExcept handle
synthesizerSolver handle
verifierSolver inputs
inputs Either e v -> CEGISCondition
f inputs -> t
v

-- |
-- CEGIS for symbolic programs with error handling, using a single symbolic
-- input to represent a set of inputs.
--
-- The errors should be translated to assertion or assumption violations.
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 =
  config
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([inputs], CEGISResult SolvingFailure))
 -> IO ([inputs], CEGISResult SolvingFailure))
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \handle
synthesizerSolver ->
    config
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([inputs], CEGISResult SolvingFailure))
 -> IO ([inputs], CEGISResult SolvingFailure))
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \handle
verifierSolver ->
      handle
-> handle
-> inputs
-> (Either e v -> u (Either VerificationConditions ()))
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
forall t (u :: * -> *) e v inputs handle.
(UnionWithExcept t u e v, PlainUnion u, Monad u,
 EvaluateSym inputs, ExtractSymbolics inputs, Solver handle,
 SEq inputs) =>
handle
-> handle
-> inputs
-> (Either e v -> u (Either VerificationConditions ()))
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
solverCegisExceptVC handle
synthesizerSolver handle
verifierSolver inputs
inputs Either e v -> u (Either VerificationConditions ())
f inputs -> t
v

-- |
-- CEGIS for symbolic programs with error handling, using a single symbolic
-- input to represent a set of inputs. This function saves the efforts to
-- implement the translation function for the standard error type
-- 'VerificationConditions', and the standard result type '()'.
--
-- This function translates assumption violations to failed pre-conditions,
-- and translates assertion violations to failed post-conditions.
-- The '()' result will not fail any conditions.
--
-- The following example tries to find the value of @c@ such that for all
-- positive @x@, @x * c < 0 && c > -2@. The @c .> -2@ assertion is used to make
-- the solution unique.
--
-- >>> :set -XOverloadedStrings
-- >>> let [x,c] = ["x","c"] :: [SymInteger]
-- >>> import Control.Monad.Except
-- >>> :{
--   res :: SymInteger -> ExceptT VerificationConditions UnionM ()
--   res x = do
--     symAssume $ x .> 0
--     symAssert $ x * c .< 0
--     symAssert $ c .> -2
-- :}
--
-- >>> cegisExceptStdVC (precise z3) x res
-- ([...],CEGISSuccess (Model {c -> -1 :: Integer}))
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 inputs -> t
f =
  config
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([inputs], CEGISResult SolvingFailure))
 -> IO ([inputs], CEGISResult SolvingFailure))
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \handle
synthesizerSolver ->
    config
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([inputs], CEGISResult SolvingFailure))
 -> IO ([inputs], CEGISResult SolvingFailure))
-> (handle -> IO ([inputs], CEGISResult SolvingFailure))
-> IO ([inputs], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \handle
verifierSolver ->
      handle
-> handle
-> inputs
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
forall t (u :: * -> *) inputs handle.
(UnionWithExcept t u VerificationConditions (), PlainUnion u,
 Monad u, EvaluateSym inputs, ExtractSymbolics inputs,
 Solver handle, SEq inputs) =>
handle
-> handle
-> inputs
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
solverCegisExceptStdVC handle
synthesizerSolver handle
verifierSolver inputs
inputs inputs -> t
f

-- |
-- CEGIS with a single symbolic input to represent a set of inputs.
--
-- The following example tries to find the value of @c@ such that for all
-- positive @x@, @x * c < 0 && c > -2@. The @c .> -2@ clause is used to make
-- the solution unique.
--
-- >>> :set -XOverloadedStrings
-- >>> let [x,c] = ["x","c"] :: [SymInteger]
-- >>> cegisForAll (precise z3) x $ cegisPrePost (x .> 0) (x * c .< 0 .&& c .> -2)
-- (...,CEGISSuccess (Model {c -> -1 :: Integer}))
cegisForAll ::
  ( ExtractSymbolics forallInput,
    ConfigurableSolver config handle
  ) =>
  config ->
  -- | A symbolic value. All the symbolic constants in the value are treated as
  -- for-all variables.
  forallInput ->
  CEGISCondition ->
  -- | First output are the counter-examples for all the for-all variables, and
  -- the second output is the model for all other variables if CEGIS succeeds.
  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) =
  config
-> (handle -> IO ([Model], CEGISResult SolvingFailure))
-> IO ([Model], CEGISResult SolvingFailure)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([Model], CEGISResult SolvingFailure))
 -> IO ([Model], CEGISResult SolvingFailure))
-> (handle -> IO ([Model], CEGISResult SolvingFailure))
-> IO ([Model], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \handle
synthesizerSolver ->
    config
-> (handle -> IO ([Model], CEGISResult SolvingFailure))
-> IO ([Model], CEGISResult SolvingFailure)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([Model], CEGISResult SolvingFailure))
 -> IO ([Model], CEGISResult SolvingFailure))
-> (handle -> IO ([Model], CEGISResult SolvingFailure))
-> IO ([Model], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \handle
verifierSolver ->
      handle
-> handle
-> forallInput
-> CEGISCondition
-> IO ([Model], CEGISResult SolvingFailure)
forall forallInput handle.
(ExtractSymbolics forallInput, Solver handle) =>
handle
-> handle
-> forallInput
-> CEGISCondition
-> IO ([Model], CEGISResult SolvingFailure)
solverCegisForAll
        handle
synthesizerSolver
        handle
verifierSolver
        forallInput
input
        (SymBool -> SymBool -> CEGISCondition
CEGISCondition SymBool
pre SymBool
post)

-- |
-- CEGIS for symbolic programs with error handling, with a forall variable.
--
-- See 'cegisForAll' and 'cegisExcept'.
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
-> (handle -> IO ([Model], CEGISResult SolvingFailure))
-> IO ([Model], CEGISResult SolvingFailure)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([Model], CEGISResult SolvingFailure))
 -> IO ([Model], CEGISResult SolvingFailure))
-> (handle -> IO ([Model], CEGISResult SolvingFailure))
-> IO ([Model], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \handle
synthesizerSolver ->
    config
-> (handle -> IO ([Model], CEGISResult SolvingFailure))
-> IO ([Model], CEGISResult SolvingFailure)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([Model], CEGISResult SolvingFailure))
 -> IO ([Model], CEGISResult SolvingFailure))
-> (handle -> IO ([Model], CEGISResult SolvingFailure))
-> IO ([Model], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \handle
verifierSolver ->
      handle
-> handle
-> inputs
-> (Either e v -> CEGISCondition)
-> t
-> IO ([Model], CEGISResult SolvingFailure)
forall t (u :: * -> *) e v inputs handle.
(UnionWithExcept t u e v, PlainUnion u, Functor u,
 EvaluateSym inputs, ExtractSymbolics inputs, Solver handle,
 SEq inputs) =>
handle
-> handle
-> inputs
-> (Either e v -> CEGISCondition)
-> t
-> IO ([Model], CEGISResult SolvingFailure)
solverCegisForAllExcept handle
synthesizerSolver handle
verifierSolver inputs
inputs Either e v -> CEGISCondition
f t
v

-- |
-- CEGIS for symbolic programs with error handling, with a forall variable.
--
-- See 'cegisForAll' and 'cegisExceptVC'.
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 =
  config
-> (handle -> IO ([Model], CEGISResult SolvingFailure))
-> IO ([Model], CEGISResult SolvingFailure)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([Model], CEGISResult SolvingFailure))
 -> IO ([Model], CEGISResult SolvingFailure))
-> (handle -> IO ([Model], CEGISResult SolvingFailure))
-> IO ([Model], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \handle
synthesizerSolver ->
    config
-> (handle -> IO ([Model], CEGISResult SolvingFailure))
-> IO ([Model], CEGISResult SolvingFailure)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([Model], CEGISResult SolvingFailure))
 -> IO ([Model], CEGISResult SolvingFailure))
-> (handle -> IO ([Model], CEGISResult SolvingFailure))
-> IO ([Model], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \handle
verifierSolver ->
      handle
-> handle
-> inputs
-> (Either e v -> u (Either VerificationConditions ()))
-> t
-> IO ([Model], CEGISResult SolvingFailure)
forall t (u :: * -> *) e v inputs handle.
(UnionWithExcept t u e v, PlainUnion u, Monad u,
 EvaluateSym inputs, ExtractSymbolics inputs, Solver handle,
 SEq inputs) =>
handle
-> handle
-> inputs
-> (Either e v -> u (Either VerificationConditions ()))
-> t
-> IO ([Model], CEGISResult SolvingFailure)
solverCegisForAllExceptVC handle
synthesizerSolver handle
verifierSolver inputs
inputs Either e v -> u (Either VerificationConditions ())
f t
v

-- |
-- CEGIS for symbolic programs with error handling, with a forall variable.
--
-- See 'cegisForAll' and 'cegisExceptStdVC'.
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 t
u =
  config
-> (handle -> IO ([Model], CEGISResult SolvingFailure))
-> IO ([Model], CEGISResult SolvingFailure)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([Model], CEGISResult SolvingFailure))
 -> IO ([Model], CEGISResult SolvingFailure))
-> (handle -> IO ([Model], CEGISResult SolvingFailure))
-> IO ([Model], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \handle
synthesizerSolver ->
    config
-> (handle -> IO ([Model], CEGISResult SolvingFailure))
-> IO ([Model], CEGISResult SolvingFailure)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([Model], CEGISResult SolvingFailure))
 -> IO ([Model], CEGISResult SolvingFailure))
-> (handle -> IO ([Model], CEGISResult SolvingFailure))
-> IO ([Model], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \handle
verifierSolver ->
      handle
-> handle
-> inputs
-> t
-> IO ([Model], CEGISResult SolvingFailure)
forall t (u :: * -> *) inputs handle.
(UnionWithExcept t u VerificationConditions (), PlainUnion u,
 Monad u, EvaluateSym inputs, ExtractSymbolics inputs,
 Solver handle, SEq inputs) =>
handle
-> handle
-> inputs
-> t
-> IO ([Model], CEGISResult SolvingFailure)
solverCegisForAllExceptStdVC handle
synthesizerSolver handle
verifierSolver inputs
inputs t
u