{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# 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

#if MIN_VERSION_base(4,20,0)
import Data.List (partition)
#else
import Data.List (foldl', partition)
#endif

import Control.DeepSeq (NFData)
import qualified Data.Binary as Binary
import Data.Bytes.Serial (Serial (deserialize, serialize))
import Data.Hashable (Hashable)
import qualified Data.Serialize as Cereal
import GHC.Generics (Generic)
import Generics.Deriving (Default (Default))
import Grisette.Internal.Core.Control.Exception
  ( VerificationConditions (AssertionViolation, AssumptionViolation),
  )
import Grisette.Internal.Core.Data.Class.EvalSym (EvalSym, evalSym)
import Grisette.Internal.Core.Data.Class.ExtractSym
  ( ExtractSym,
    extractSym,
  )
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.PPrint (PPrint (pformat), (<+>))
import Grisette.Internal.Core.Data.Class.PlainUnion
  ( PlainUnion,
    simpleMerge,
  )
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.Core.Data.Class.SymEq (SymEq)
import Grisette.Internal.SymPrim.Prim.Model (Model)
import Grisette.Internal.SymPrim.SymBool (SymBool)
import Language.Haskell.TH.Syntax (Lift)

-- $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
  | -- | True indicates that the verifier is sure that there is no
    -- counter-example, while False indicates that the verifier is not sure,
    -- but it cannot find a counter-example.
    CEGISVerifierNoCex Bool
  | CEGISVerifierException exception
  deriving (Int -> VerifierResult cex exception -> ShowS
[VerifierResult cex exception] -> ShowS
VerifierResult cex exception -> String
(Int -> VerifierResult cex exception -> ShowS)
-> (VerifierResult cex exception -> String)
-> ([VerifierResult cex exception] -> ShowS)
-> Show (VerifierResult cex exception)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall cex exception.
(Show cex, Show exception) =>
Int -> VerifierResult cex exception -> ShowS
forall cex exception.
(Show cex, Show exception) =>
[VerifierResult cex exception] -> ShowS
forall cex exception.
(Show cex, Show exception) =>
VerifierResult cex exception -> String
$cshowsPrec :: forall cex exception.
(Show cex, Show exception) =>
Int -> VerifierResult cex exception -> ShowS
showsPrec :: Int -> VerifierResult cex exception -> ShowS
$cshow :: forall cex exception.
(Show cex, Show exception) =>
VerifierResult cex exception -> String
show :: VerifierResult cex exception -> String
$cshowList :: forall cex exception.
(Show cex, Show exception) =>
[VerifierResult cex exception] -> ShowS
showList :: [VerifierResult cex exception] -> ShowS
Show, VerifierResult cex exception
-> VerifierResult cex exception -> Bool
(VerifierResult cex exception
 -> VerifierResult cex exception -> Bool)
-> (VerifierResult cex exception
    -> VerifierResult cex exception -> Bool)
-> Eq (VerifierResult cex exception)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall cex exception.
(Eq cex, Eq exception) =>
VerifierResult cex exception
-> VerifierResult cex exception -> Bool
$c== :: forall cex exception.
(Eq cex, Eq exception) =>
VerifierResult cex exception
-> VerifierResult cex exception -> Bool
== :: VerifierResult cex exception
-> VerifierResult cex exception -> Bool
$c/= :: forall cex exception.
(Eq cex, Eq exception) =>
VerifierResult cex exception
-> VerifierResult cex exception -> Bool
/= :: VerifierResult cex exception
-> VerifierResult cex exception -> Bool
Eq, (forall x.
 VerifierResult cex exception
 -> Rep (VerifierResult cex exception) x)
-> (forall x.
    Rep (VerifierResult cex exception) x
    -> VerifierResult cex exception)
-> Generic (VerifierResult cex exception)
forall x.
Rep (VerifierResult cex exception) x
-> VerifierResult cex exception
forall x.
VerifierResult cex exception
-> Rep (VerifierResult cex exception) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall cex exception x.
Rep (VerifierResult cex exception) x
-> VerifierResult cex exception
forall cex exception x.
VerifierResult cex exception
-> Rep (VerifierResult cex exception) x
$cfrom :: forall cex exception x.
VerifierResult cex exception
-> Rep (VerifierResult cex exception) x
from :: forall x.
VerifierResult cex exception
-> Rep (VerifierResult cex exception) x
$cto :: forall cex exception x.
Rep (VerifierResult cex exception) x
-> VerifierResult cex exception
to :: forall x.
Rep (VerifierResult cex exception) x
-> VerifierResult cex exception
Generic, (forall (m :: * -> *).
 Quote m =>
 VerifierResult cex exception -> m Exp)
-> (forall (m :: * -> *).
    Quote m =>
    VerifierResult cex exception
    -> Code m (VerifierResult cex exception))
-> Lift (VerifierResult cex exception)
forall cex exception (m :: * -> *).
(Lift cex, Lift exception, Quote m) =>
VerifierResult cex exception -> m Exp
forall cex exception (m :: * -> *).
(Lift cex, Lift exception, Quote m) =>
VerifierResult cex exception
-> Code m (VerifierResult cex exception)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *).
Quote m =>
VerifierResult cex exception -> m Exp
forall (m :: * -> *).
Quote m =>
VerifierResult cex exception
-> Code m (VerifierResult cex exception)
$clift :: forall cex exception (m :: * -> *).
(Lift cex, Lift exception, Quote m) =>
VerifierResult cex exception -> m Exp
lift :: forall (m :: * -> *).
Quote m =>
VerifierResult cex exception -> m Exp
$cliftTyped :: forall cex exception (m :: * -> *).
(Lift cex, Lift exception, Quote m) =>
VerifierResult cex exception
-> Code m (VerifierResult cex exception)
liftTyped :: forall (m :: * -> *).
Quote m =>
VerifierResult cex exception
-> Code m (VerifierResult cex exception)
Lift)
  deriving anyclass (Eq (VerifierResult cex exception)
Eq (VerifierResult cex exception) =>
(Int -> VerifierResult cex exception -> Int)
-> (VerifierResult cex exception -> Int)
-> Hashable (VerifierResult cex exception)
Int -> VerifierResult cex exception -> Int
VerifierResult cex exception -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall cex exception.
(Hashable cex, Hashable exception) =>
Eq (VerifierResult cex exception)
forall cex exception.
(Hashable cex, Hashable exception) =>
Int -> VerifierResult cex exception -> Int
forall cex exception.
(Hashable cex, Hashable exception) =>
VerifierResult cex exception -> Int
$chashWithSalt :: forall cex exception.
(Hashable cex, Hashable exception) =>
Int -> VerifierResult cex exception -> Int
hashWithSalt :: Int -> VerifierResult cex exception -> Int
$chash :: forall cex exception.
(Hashable cex, Hashable exception) =>
VerifierResult cex exception -> Int
hash :: VerifierResult cex exception -> Int
Hashable, VerifierResult cex exception -> ()
(VerifierResult cex exception -> ())
-> NFData (VerifierResult cex exception)
forall a. (a -> ()) -> NFData a
forall cex exception.
(NFData cex, NFData exception) =>
VerifierResult cex exception -> ()
$crnf :: forall cex exception.
(NFData cex, NFData exception) =>
VerifierResult cex exception -> ()
rnf :: VerifierResult cex exception -> ()
NFData)

instance
  (PPrint cex, PPrint exception) =>
  PPrint (VerifierResult cex exception)
  where
  pformat :: forall ann. VerifierResult cex exception -> Doc ann
pformat = \case
    CEGISVerifierFoundCex cex
cex -> Doc ann
"Found cex:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> cex -> Doc ann
forall ann. cex -> Doc ann
forall a ann. PPrint a => a -> Doc ann
pformat cex
cex
    CEGISVerifierNoCex Bool
True -> Doc ann
"No cex"
    CEGISVerifierNoCex Bool
False -> Doc ann
"Maybe no cex"
    CEGISVerifierException exception
e -> Doc ann
"Exception:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> exception -> Doc ann
forall ann. exception -> Doc ann
forall a ann. PPrint a => a -> Doc ann
pformat exception
e

-- | 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, CEGISResult exception -> CEGISResult exception -> Bool
(CEGISResult exception -> CEGISResult exception -> Bool)
-> (CEGISResult exception -> CEGISResult exception -> Bool)
-> Eq (CEGISResult exception)
forall exception.
Eq exception =>
CEGISResult exception -> CEGISResult exception -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall exception.
Eq exception =>
CEGISResult exception -> CEGISResult exception -> Bool
== :: CEGISResult exception -> CEGISResult exception -> Bool
$c/= :: forall exception.
Eq exception =>
CEGISResult exception -> CEGISResult exception -> Bool
/= :: CEGISResult exception -> CEGISResult exception -> Bool
Eq, (forall x. CEGISResult exception -> Rep (CEGISResult exception) x)
-> (forall x.
    Rep (CEGISResult exception) x -> CEGISResult exception)
-> Generic (CEGISResult exception)
forall x. Rep (CEGISResult exception) x -> CEGISResult exception
forall x. CEGISResult exception -> Rep (CEGISResult exception) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall exception x.
Rep (CEGISResult exception) x -> CEGISResult exception
forall exception x.
CEGISResult exception -> Rep (CEGISResult exception) x
$cfrom :: forall exception x.
CEGISResult exception -> Rep (CEGISResult exception) x
from :: forall x. CEGISResult exception -> Rep (CEGISResult exception) x
$cto :: forall exception x.
Rep (CEGISResult exception) x -> CEGISResult exception
to :: forall x. Rep (CEGISResult exception) x -> CEGISResult exception
Generic, (forall (m :: * -> *). Quote m => CEGISResult exception -> m Exp)
-> (forall (m :: * -> *).
    Quote m =>
    CEGISResult exception -> Code m (CEGISResult exception))
-> Lift (CEGISResult exception)
forall exception (m :: * -> *).
(Lift exception, Quote m) =>
CEGISResult exception -> m Exp
forall exception (m :: * -> *).
(Lift exception, Quote m) =>
CEGISResult exception -> Code m (CEGISResult exception)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => CEGISResult exception -> m Exp
forall (m :: * -> *).
Quote m =>
CEGISResult exception -> Code m (CEGISResult exception)
$clift :: forall exception (m :: * -> *).
(Lift exception, Quote m) =>
CEGISResult exception -> m Exp
lift :: forall (m :: * -> *). Quote m => CEGISResult exception -> m Exp
$cliftTyped :: forall exception (m :: * -> *).
(Lift exception, Quote m) =>
CEGISResult exception -> Code m (CEGISResult exception)
liftTyped :: forall (m :: * -> *).
Quote m =>
CEGISResult exception -> Code m (CEGISResult exception)
Lift)
  deriving anyclass (CEGISResult exception -> ()
(CEGISResult exception -> ()) -> NFData (CEGISResult exception)
forall exception. NFData exception => CEGISResult exception -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall exception. NFData exception => CEGISResult exception -> ()
rnf :: CEGISResult exception -> ()
NFData, Eq (CEGISResult exception)
Eq (CEGISResult exception) =>
(Int -> CEGISResult exception -> Int)
-> (CEGISResult exception -> Int)
-> Hashable (CEGISResult exception)
Int -> CEGISResult exception -> Int
CEGISResult exception -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall exception. Hashable exception => Eq (CEGISResult exception)
forall exception.
Hashable exception =>
Int -> CEGISResult exception -> Int
forall exception.
Hashable exception =>
CEGISResult exception -> Int
$chashWithSalt :: forall exception.
Hashable exception =>
Int -> CEGISResult exception -> Int
hashWithSalt :: Int -> CEGISResult exception -> Int
$chash :: forall exception.
Hashable exception =>
CEGISResult exception -> Int
hash :: CEGISResult exception -> Int
Hashable, (forall (m :: * -> *). MonadPut m => CEGISResult exception -> m ())
-> (forall (m :: * -> *). MonadGet m => m (CEGISResult exception))
-> Serial (CEGISResult exception)
forall exception (m :: * -> *).
(Serial exception, MonadGet m) =>
m (CEGISResult exception)
forall exception (m :: * -> *).
(Serial exception, MonadPut m) =>
CEGISResult exception -> m ()
forall a.
(forall (m :: * -> *). MonadPut m => a -> m ())
-> (forall (m :: * -> *). MonadGet m => m a) -> Serial a
forall (m :: * -> *). MonadGet m => m (CEGISResult exception)
forall (m :: * -> *). MonadPut m => CEGISResult exception -> m ()
$cserialize :: forall exception (m :: * -> *).
(Serial exception, MonadPut m) =>
CEGISResult exception -> m ()
serialize :: forall (m :: * -> *). MonadPut m => CEGISResult exception -> m ()
$cdeserialize :: forall exception (m :: * -> *).
(Serial exception, MonadGet m) =>
m (CEGISResult exception)
deserialize :: forall (m :: * -> *). MonadGet m => m (CEGISResult exception)
Serial)

instance (Serial exception) => Cereal.Serialize (CEGISResult exception) where
  put :: Putter (CEGISResult exception)
put = Putter (CEGISResult exception)
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => CEGISResult exception -> m ()
serialize
  get :: Get (CEGISResult exception)
get = Get (CEGISResult exception)
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m (CEGISResult exception)
deserialize

instance (Serial exception) => Binary.Binary (CEGISResult exception) where
  put :: CEGISResult exception -> Put
put = CEGISResult exception -> Put
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => CEGISResult exception -> m ()
serialize
  get :: Get (CEGISResult exception)
get = Get (CEGISResult exception)
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m (CEGISResult exception)
deserialize

-- | 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
  firstResult <- handle -> SymBool -> IO (Either SolvingFailure Model)
forall handle.
Solver handle =>
handle -> SymBool -> IO (Either SolvingFailure Model)
solverSolve handle
solver SymBool
initConstr
  case 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
-> Int
-> Int
-> [VerifierFun input exception]
-> IO ([input], CEGISResult exception)
go Model
model Bool
False Int
numAllVerifiers Int
0 [VerifierFun input exception]
verifiers
  where
    numAllVerifiers :: Int
numAllVerifiers = [VerifierFun input exception] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [VerifierFun input exception]
verifiers
    go :: Model
-> Bool
-> Int
-> Int
-> [VerifierFun input exception]
-> IO ([input], CEGISResult exception)
go Model
prevModel Bool
_ Int
0 Int
_ (VerifierFun input exception
_ : [VerifierFun input exception]
_) = ([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
needRerun Int
runBound Int
nextBound (VerifierFun input exception
verifier : [VerifierFun input exception]
remainingVerifiers) = do
      verifierResult <- VerifierFun input exception
verifier Model
prevModel
      case verifierResult of
        CEGISVerifierFoundCex input
cex -> do
          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 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 ([input
cex], SolvingFailure -> CEGISResult exception
forall exception. SolvingFailure -> CEGISResult exception
CEGISSolverFailure SolvingFailure
err)
            Right Model
model -> do
              (cexes, result) <-
                Model
-> Bool
-> Int
-> Int
-> [VerifierFun input exception]
-> IO ([input], CEGISResult exception)
go
                  Model
model
                  (Bool
needRerun Bool -> Bool -> Bool
|| Bool
rerun)
                  ([VerifierFun input exception] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [VerifierFun input exception]
remainingVerifiers Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
                  (Int
numAllVerifiers Int -> Int -> Int
forall a. Num a => a -> a -> a
- [VerifierFun input exception] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [VerifierFun input exception]
remainingVerifiers Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
                  ([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
              return (cex : cexes, result)
        CEGISVerifierNoCex {} ->
          Model
-> Bool
-> Int
-> Int
-> [VerifierFun input exception]
-> IO ([input], CEGISResult exception)
go Model
prevModel Bool
needRerun (Int
runBound Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Int
nextBound [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 Int
_ Int
_ [] = ([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 Int
_runBound Int
nextBound [] =
      Model
-> Bool
-> Int
-> Int
-> [VerifierFun input exception]
-> IO ([input], CEGISResult exception)
go Model
prevModel Bool
False Int
nextBound Int
0 [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, 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 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
          cond <- RefinementConditionFun
f Model
model
          newResult <-
            solverGenericCEGIS solver rerun cond synthConstr verifiers
          case 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)
-> EvalSym CEGISCondition
forall a. (Bool -> Model -> a -> a) -> EvalSym a
$cevalSym :: Bool -> Model -> CEGISCondition -> CEGISCondition
evalSym :: Bool -> Model -> CEGISCondition -> CEGISCondition
EvalSym) 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 ::
  ( EvalSym input,
    ExtractSym 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
  -- t'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.
(EvalSym input, ExtractSym 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
      ((SymBool -> input -> SymBool) -> SymBool -> [input] -> SymBool
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\SymBool
acc input
v -> SymBool
acc SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& input -> SymBool
cexAssertFun input
v) (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True) [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. EvalSym a => Bool -> Model -> a -> a
evalSym Bool
False (AnySymbolSet -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
symbolSet -> model -> model
exceptFor (input -> AnySymbolSet
forall a. ExtractSym a => a -> AnySymbolSet
extractSym 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
        r <- handle -> SymBool -> IO (Either SolvingFailure Model)
forall handle.
Solver handle =>
handle -> SymBool -> IO (Either SolvingFailure Model)
solverSolve handle
verifierSolver SymBool
evaluated
        case 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
 -> IO (VerifierResult input SolvingFailure))
-> VerifierResult input SolvingFailure
-> IO (VerifierResult input SolvingFailure)
forall a b. (a -> b) -> a -> b
$ Bool -> VerifierResult input SolvingFailure
forall cex exception. Bool -> VerifierResult cex exception
CEGISVerifierNoCex Bool
True
          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. EvalSym a => Bool -> Model -> a -> a
evalSym Bool
True (AnySymbolSet -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
symbolSet -> model -> model
exact (input -> AnySymbolSet
forall a. ExtractSym a => a -> AnySymbolSet
extractSym 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 (AnySymbolSet -> Bool
forall symbolSet (typedSymbol :: * -> *).
SymbolSetOps symbolSet typedSymbol =>
symbolSet -> Bool
isEmptySet (AnySymbolSet -> Bool) -> (input -> AnySymbolSet) -> input -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. input -> AnySymbolSet
forall a. ExtractSym a => a -> AnySymbolSet
extractSym) [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,
    EvalSym inputs,
    ExtractSym inputs,
    SymEq 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
  -- t'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, EvalSym inputs, ExtractSym inputs, SymEq 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.
(EvalSym input, ExtractSym 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,
    EvalSym inputs,
    ExtractSym 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, EvalSym inputs, ExtractSym 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.
(EvalSym input, ExtractSym 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,
    EvalSym inputs,
    ExtractSym 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, EvalSym inputs, ExtractSym 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.
(EvalSym input, ExtractSym 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,
    EvalSym inputs,
    ExtractSym 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, EvalSym inputs, ExtractSym 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, EvalSym inputs, ExtractSym 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,
    EvalSym inputs,
    ExtractSym inputs,
    Solver handle,
    SymEq 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, EvalSym inputs,
 ExtractSym inputs, Solver handle, SymEq 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, EvalSym inputs, ExtractSym inputs, SymEq 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,
    EvalSym inputs,
    ExtractSym inputs,
    Solver handle,
    SymEq 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, EvalSym inputs,
 ExtractSym inputs, Solver handle, SymEq 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, EvalSym inputs, ExtractSym inputs, SymEq 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,
    EvalSym inputs,
    ExtractSym inputs,
    Solver handle,
    SymEq inputs
  ) =>
  handle ->
  handle ->
  inputs ->
  (inputs -> t) ->
  IO ([inputs], CEGISResult SolvingFailure)
solverCegisExceptStdVC :: forall t (u :: * -> *) inputs handle.
(UnionWithExcept t u VerificationConditions (), PlainUnion u,
 Monad u, EvalSym inputs, ExtractSym inputs, Solver handle,
 SymEq 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, EvalSym inputs,
 ExtractSym inputs, Solver handle, SymEq 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 ::
  ( ExtractSym 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.
(ExtractSym forallInput, Solver handle) =>
handle
-> handle
-> forallInput
-> CEGISCondition
-> IO ([Model], CEGISResult SolvingFailure)
solverCegisForAll
  handle
synthesizerSolver
  handle
verifierSolver
  forallInput
input
  (CEGISCondition SymBool
pre SymBool
post) = do
    (models, 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. EvalSym a => Bool -> Model -> a -> a
evalSym Bool
False Model
md SymBool
phi)
        [VerifierFun Model SolvingFailure
verifier]
    let 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
$ AnySymbolSet -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
symbolSet -> model -> model
exceptFor AnySymbolSet
forallSymbols Model
model
          CEGISResult SolvingFailure
_ -> CEGISResult SolvingFailure
result
    return (models, 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 :: AnySymbolSet
forallSymbols = forallInput -> AnySymbolSet
forall a. ExtractSym a => a -> AnySymbolSet
extractSym forallInput
input
      verifier :: VerifierFun Model SolvingFailure
verifier Model
candidate = do
        let evaluated :: SymBool
evaluated =
              Bool -> Model -> SymBool -> SymBool
forall a. EvalSym a => Bool -> Model -> a -> a
evalSym Bool
False (AnySymbolSet -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
symbolSet -> model -> model
exceptFor AnySymbolSet
forallSymbols Model
candidate) SymBool
negphi
        handle -> IO (Either SolvingFailure ())
forall handle.
Solver handle =>
handle -> IO (Either SolvingFailure ())
solverResetAssertions handle
verifierSolver
        r <- handle -> SymBool -> IO (Either SolvingFailure Model)
forall handle.
Solver handle =>
handle -> SymBool -> IO (Either SolvingFailure Model)
solverSolve handle
verifierSolver SymBool
evaluated
        case 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
 -> IO (VerifierResult Model SolvingFailure))
-> VerifierResult Model SolvingFailure
-> IO (VerifierResult Model SolvingFailure)
forall a b. (a -> b) -> a -> b
$ Bool -> VerifierResult Model SolvingFailure
forall cex exception. Bool -> VerifierResult cex exception
CEGISVerifierNoCex Bool
True
          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 (AnySymbolSet -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
symbolSet -> model -> model
exact AnySymbolSet
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,
    EvalSym inputs,
    ExtractSym inputs,
    Solver handle,
    SymEq 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, EvalSym inputs,
 ExtractSym inputs, Solver handle, SymEq 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.
(ExtractSym 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,
    EvalSym inputs,
    ExtractSym inputs,
    Solver handle,
    SymEq 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, EvalSym inputs,
 ExtractSym inputs, Solver handle, SymEq 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.
(ExtractSym 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,
    EvalSym inputs,
    ExtractSym inputs,
    Solver handle,
    SymEq inputs
  ) =>
  handle ->
  handle ->
  inputs ->
  t ->
  IO ([Model], CEGISResult SolvingFailure)
solverCegisForAllExceptStdVC :: forall t (u :: * -> *) inputs handle.
(UnionWithExcept t u VerificationConditions (), PlainUnion u,
 Monad u, EvalSym inputs, ExtractSym inputs, Solver handle,
 SymEq 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, EvalSym inputs,
 ExtractSym inputs, Solver handle, SymEq 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 t'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 ::
  ( EvalSym input,
    ExtractSym 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
  -- t'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.
(EvalSym input, ExtractSym 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.
(EvalSym input, ExtractSym 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.
--
-- >>> let [x,c] = ["x","c"] :: [SymInteger]
-- >>> cegis z3 x (\x -> cegisPrePost (x .> 0) (x * c .< 0 .&& c .> -2))
-- (...,CEGISSuccess (Model {c -> -1 :: Integer}))
cegis ::
  ( ConfigurableSolver config handle,
    EvalSym inputs,
    ExtractSym inputs,
    SymEq 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
  -- t'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, EvalSym inputs,
 ExtractSym inputs, SymEq 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, EvalSym inputs, ExtractSym inputs, SymEq 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,
    EvalSym inputs,
    ExtractSym 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, EvalSym inputs,
 ExtractSym 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, EvalSym inputs, ExtractSym 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,
    EvalSym inputs,
    ExtractSym 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, EvalSym inputs,
 ExtractSym 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, EvalSym inputs, ExtractSym 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,
    EvalSym inputs,
    ExtractSym 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, EvalSym inputs,
 ExtractSym 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, EvalSym inputs, ExtractSym 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.
--
-- >>> let [x,c] = ["x","c"] :: [SymInteger]
-- >>> import Control.Monad.Except
-- >>> :{
--   res :: SymInteger -> ExceptT VerificationConditions Union ()
--   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 z3 x translation res
-- ([...],CEGISSuccess (Model {c -> -1 :: Integer}))
cegisExcept ::
  ( UnionWithExcept t u e v,
    PlainUnion u,
    Functor u,
    EvalSym inputs,
    ExtractSym inputs,
    ConfigurableSolver config handle,
    SymEq 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, EvalSym inputs,
 ExtractSym inputs, ConfigurableSolver config handle,
 SymEq 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, EvalSym inputs,
 ExtractSym inputs, Solver handle, SymEq 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,
    EvalSym inputs,
    ExtractSym inputs,
    ConfigurableSolver config handle,
    SymEq 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, EvalSym inputs,
 ExtractSym inputs, ConfigurableSolver config handle,
 SymEq 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, EvalSym inputs,
 ExtractSym inputs, Solver handle, SymEq 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.
--
-- >>> let [x,c] = ["x","c"] :: [SymInteger]
-- >>> import Control.Monad.Except
-- >>> :{
--   res :: SymInteger -> ExceptT VerificationConditions Union ()
--   res x = do
--     symAssume $ x .> 0
--     symAssert $ x * c .< 0
--     symAssert $ c .> -2
-- :}
--
-- >>> cegisExceptStdVC z3 x res
-- ([...],CEGISSuccess (Model {c -> -1 :: Integer}))
cegisExceptStdVC ::
  ( UnionWithExcept t u VerificationConditions (),
    PlainUnion u,
    Monad u,
    EvalSym inputs,
    ExtractSym inputs,
    ConfigurableSolver config handle,
    SymEq inputs
  ) =>
  config ->
  inputs ->
  (inputs -> t) ->
  IO ([inputs], CEGISResult SolvingFailure)
cegisExceptStdVC :: forall t (u :: * -> *) inputs config handle.
(UnionWithExcept t u VerificationConditions (), PlainUnion u,
 Monad u, EvalSym inputs, ExtractSym inputs,
 ConfigurableSolver config handle, SymEq 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, EvalSym inputs, ExtractSym inputs, Solver handle,
 SymEq 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.
--
-- >>> let [x,c] = ["x","c"] :: [SymInteger]
-- >>> cegisForAll z3 x $ cegisPrePost (x .> 0) (x * c .< 0 .&& c .> -2)
-- (...,CEGISSuccess (Model {c -> -1 :: Integer}))
cegisForAll ::
  ( ExtractSym 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.
(ExtractSym 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.
(ExtractSym 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,
    EvalSym inputs,
    ExtractSym inputs,
    ConfigurableSolver config handle,
    SymEq 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, EvalSym inputs,
 ExtractSym inputs, ConfigurableSolver config handle,
 SymEq 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, EvalSym inputs,
 ExtractSym inputs, Solver handle, SymEq 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,
    EvalSym inputs,
    ExtractSym inputs,
    ConfigurableSolver config handle,
    SymEq 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, EvalSym inputs,
 ExtractSym inputs, ConfigurableSolver config handle,
 SymEq 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, EvalSym inputs,
 ExtractSym inputs, Solver handle, SymEq 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,
    EvalSym inputs,
    ExtractSym inputs,
    ConfigurableSolver config handle,
    SymEq inputs
  ) =>
  config ->
  inputs ->
  t ->
  IO ([Model], CEGISResult SolvingFailure)
cegisForAllExceptStdVC :: forall t (u :: * -> *) inputs config handle.
(UnionWithExcept t u VerificationConditions (), PlainUnion u,
 Monad u, EvalSym inputs, ExtractSym inputs,
 ConfigurableSolver config handle, SymEq 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, EvalSym inputs, ExtractSym inputs, Solver handle,
 SymEq inputs) =>
handle
-> handle
-> inputs
-> t
-> IO ([Model], CEGISResult SolvingFailure)
solverCegisForAllExceptStdVC handle
synthesizerSolver handle
verifierSolver inputs
inputs t
u