{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE Trustworthy #-}

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

    --

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

    -- * Generic CEGIS interface
    SynthesisConstraintFun,
    VerifierResult (..),
    StatefulVerifierFun,
    CEGISResult (..),
    genericCEGIS,

    -- * CEGIS interfaces with pre/post conditions
    CEGISCondition (..),
    cegisPostCond,
    cegisPrePost,
    cegisMultiInputs,
    cegis,
    cegisExcept,
    cegisExceptStdVC,
    cegisExceptVC,
    cegisExceptMultiInputs,
    cegisExceptStdVCMultiInputs,
    cegisExceptVCMultiInputs,
    cegisForAll,
    cegisForAllExcept,
    cegisForAllExceptStdVC,
    cegisForAllExceptVC,
  )
where

import Control.Monad (foldM, unless)
import Data.List (partition)
import GHC.Generics (Generic)
import Generics.Deriving (Default (Default))
import Grisette.Internal.Core.Control.Exception
  ( VerificationConditions (AssertionViolation, AssumptionViolation),
  )
import Grisette.Internal.Core.Data.Class.EvaluateSym (EvaluateSym, evaluateSym)
import Grisette.Internal.Core.Data.Class.ExtractSymbolics
  ( ExtractSymbolics,
    extractSymbolics,
  )
import Grisette.Internal.Core.Data.Class.LogicalOp (LogicalOp (symNot, (.&&)))
import Grisette.Internal.Core.Data.Class.Mergeable (Mergeable)
import Grisette.Internal.Core.Data.Class.ModelOps
  ( ModelOps (exact, exceptFor),
    SymbolSetOps (isEmptySet),
  )
import Grisette.Internal.Core.Data.Class.PlainUnion
  ( PlainUnion,
    simpleMerge,
  )
import Grisette.Internal.Core.Data.Class.SEq (SEq)
import Grisette.Internal.Core.Data.Class.SimpleMergeable
  ( SimpleMergeable,
  )
import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con))
import Grisette.Internal.Core.Data.Class.Solver
  ( ConfigurableSolver,
    Solver (solverSolve),
    SolvingFailure (Unsat),
    UnionWithExcept (extractUnionExcept),
    solve,
    withSolver,
  )
import Grisette.Internal.SymPrim.Prim.Model (Model)
import Grisette.Internal.SymPrim.SymBool (SymBool)

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

-- | Synthesis constraint function.
--
-- The first argument is the iteration number, for angelic programs, you can use
-- it to instantiate the angelic variables in the program.
--
-- The second argument is the counter-example generated by the verifier.
--
-- The synthesizer will try to find a program that is true for all the synthesis
-- constraints.
type SynthesisConstraintFun input = Int -> input -> IO SymBool

-- | The result of the verifier.
data VerifierResult input exception
  = CEGISVerifierFoundCex input
  | CEGISVerifierNoCex
  | CEGISVerifierException exception

-- | The verifier function.
--
-- The first argument is the state of the verifier.
--
-- The second argument is the candidate model proposed by the synthesizer.
type StatefulVerifierFun state input exception =
  state -> Model -> IO (state, VerifierResult input exception)

-- | The result of the CEGIS procedure.
data CEGISResult exception
  = CEGISSuccess Model
  | CEGISVerifierFailure exception
  | CEGISSolverFailure SolvingFailure
  deriving (Int -> CEGISResult exception -> ShowS
[CEGISResult exception] -> ShowS
CEGISResult exception -> String
(Int -> CEGISResult exception -> ShowS)
-> (CEGISResult exception -> String)
-> ([CEGISResult exception] -> ShowS)
-> Show (CEGISResult exception)
forall exception.
Show exception =>
Int -> CEGISResult exception -> ShowS
forall exception.
Show exception =>
[CEGISResult exception] -> ShowS
forall exception. Show exception => CEGISResult exception -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall exception.
Show exception =>
Int -> CEGISResult exception -> ShowS
showsPrec :: Int -> CEGISResult exception -> ShowS
$cshow :: forall exception. Show exception => CEGISResult exception -> String
show :: CEGISResult exception -> String
$cshowList :: forall exception.
Show exception =>
[CEGISResult exception] -> ShowS
showList :: [CEGISResult exception] -> ShowS
Show)

-- | Generic CEGIS procedure.
--
-- 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 ->
  -- | The initial synthesis constraint.
  SymBool ->
  -- | The synthesis constraint function.
  SynthesisConstraintFun input ->
  -- | The initial state of the verifier.
  verifierState ->
  -- | The verifier function.
  StatefulVerifierFun verifierState input exception ->
  IO ([input], CEGISResult exception)
genericCEGIS :: forall config handle input verifierState exception.
ConfigurableSolver config handle =>
config
-> SymBool
-> SynthesisConstraintFun input
-> verifierState
-> StatefulVerifierFun verifierState input exception
-> IO ([input], CEGISResult exception)
genericCEGIS config
config SymBool
initConstr SynthesisConstraintFun input
synthConstr verifierState
initVerifierState StatefulVerifierFun verifierState input exception
verifier =
  config
-> (handle -> IO ([input], CEGISResult exception))
-> IO ([input], CEGISResult exception)
forall config handle a.
ConfigurableSolver config handle =>
config -> (handle -> IO a) -> IO a
withSolver config
config ((handle -> IO ([input], CEGISResult exception))
 -> IO ([input], CEGISResult exception))
-> (handle -> IO ([input], CEGISResult exception))
-> IO ([input], CEGISResult exception)
forall a b. (a -> b) -> a -> b
$ \handle
solver -> do
    Either SolvingFailure Model
firstResult <- handle -> SymBool -> IO (Either SolvingFailure Model)
forall handle.
Solver handle =>
handle -> SymBool -> IO (Either SolvingFailure Model)
solverSolve handle
solver SymBool
initConstr
    case Either SolvingFailure Model
firstResult of
      Left SolvingFailure
err -> ([input], CEGISResult exception)
-> IO ([input], CEGISResult exception)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], SolvingFailure -> CEGISResult exception
forall exception. SolvingFailure -> CEGISResult exception
CEGISSolverFailure SolvingFailure
err)
      Right Model
model -> handle
-> Model
-> Int
-> verifierState
-> IO ([input], CEGISResult exception)
forall {t}.
Solver t =>
t
-> Model
-> Int
-> verifierState
-> IO ([input], CEGISResult exception)
go handle
solver Model
model Int
0 verifierState
initVerifierState
  where
    go :: t
-> Model
-> Int
-> verifierState
-> IO ([input], CEGISResult exception)
go t
solver Model
prevModel Int
iterNum verifierState
verifierState = do
      (verifierState
newVerifierState, VerifierResult input exception
verifierResult) <-
        StatefulVerifierFun verifierState input exception
verifier verifierState
verifierState Model
prevModel
      case VerifierResult input exception
verifierResult of
        CEGISVerifierFoundCex input
cex -> do
          Either SolvingFailure Model
newResult <- t -> SymBool -> IO (Either SolvingFailure Model)
forall handle.
Solver handle =>
handle -> SymBool -> IO (Either SolvingFailure Model)
solverSolve t
solver (SymBool -> IO (Either SolvingFailure Model))
-> IO SymBool -> IO (Either SolvingFailure Model)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SynthesisConstraintFun input
synthConstr Int
iterNum input
cex
          case Either SolvingFailure Model
newResult of
            Left SolvingFailure
err -> ([input], CEGISResult exception)
-> IO ([input], CEGISResult exception)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], SolvingFailure -> CEGISResult exception
forall exception. SolvingFailure -> CEGISResult exception
CEGISSolverFailure SolvingFailure
err)
            Right Model
model -> do
              ([input]
cexes, CEGISResult exception
result) <- t
-> Model
-> Int
-> verifierState
-> IO ([input], CEGISResult exception)
go t
solver Model
model (Int
iterNum Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) verifierState
newVerifierState
              ([input], CEGISResult exception)
-> IO ([input], CEGISResult exception)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (input
cex input -> [input] -> [input]
forall a. a -> [a] -> [a]
: [input]
cexes, CEGISResult exception
result)
        VerifierResult input exception
CEGISVerifierNoCex -> ([input], CEGISResult exception)
-> IO ([input], CEGISResult exception)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Model -> CEGISResult exception
forall exception. Model -> CEGISResult exception
CEGISSuccess Model
prevModel)
        CEGISVerifierException exception
exception ->
          ([input], CEGISResult exception)
-> IO ([input], CEGISResult exception)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], exception -> CEGISResult exception
forall exception. exception -> CEGISResult exception
CEGISVerifierFailure exception
exception)

data CEGISMultiInputsState input = CEGISMultiInputsState
  { forall input. CEGISMultiInputsState input -> [input]
_cegisMultiInputsRemainingSymInputs :: [input],
    forall input. CEGISMultiInputsState input -> SymBool
_cegisMultiInputsPre :: SymBool,
    forall input. CEGISMultiInputsState input -> SymBool
_cegisMultiInputsPost :: SymBool
  }

-- | The condition for CEGIS to solve.
--
-- The first argument is the pre-condition, and the second argument is the
-- post-condition.
--
-- The CEGIS procedures would try to find a model for the formula
--
-- \[
--   \forall P. (\exists I. \mathrm{pre}(P, I)) \wedge (\forall I. \mathrm{pre}(P, I)\implies \mathrm{post}(P, I))
-- \]
--
-- In program synthesis tasks, \(P\) is the symbolic constants in the symbolic
-- program, and \(I\) is the input. The pre-condition is used to restrict the
-- search space of the program. The procedure would only return programs that
-- meets the pre-conditions on every possible inputs, and there are at least
-- one possible input. The post-condition is used to specify the desired program
-- behaviors.
data CEGISCondition = CEGISCondition SymBool SymBool
  deriving ((forall x. CEGISCondition -> Rep CEGISCondition x)
-> (forall x. Rep CEGISCondition x -> CEGISCondition)
-> Generic CEGISCondition
forall x. Rep CEGISCondition x -> CEGISCondition
forall x. CEGISCondition -> Rep CEGISCondition x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CEGISCondition -> Rep CEGISCondition x
from :: forall x. CEGISCondition -> Rep CEGISCondition x
$cto :: forall x. Rep CEGISCondition x -> CEGISCondition
to :: forall x. Rep CEGISCondition x -> CEGISCondition
Generic)
  deriving (Bool -> Model -> CEGISCondition -> CEGISCondition
(Bool -> Model -> CEGISCondition -> CEGISCondition)
-> EvaluateSym CEGISCondition
forall a. (Bool -> Model -> a -> a) -> EvaluateSym a
$cevaluateSym :: Bool -> Model -> CEGISCondition -> CEGISCondition
evaluateSym :: Bool -> Model -> CEGISCondition -> CEGISCondition
EvaluateSym) via (Default CEGISCondition)

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

-- | Construct a CEGIS condition with both pre- and post-conditions.
cegisPrePost :: SymBool -> SymBool -> CEGISCondition
cegisPrePost :: SymBool -> SymBool -> CEGISCondition
cegisPrePost = SymBool -> SymBool -> CEGISCondition
CEGISCondition

deriving via (Default CEGISCondition) instance Mergeable CEGISCondition

deriving via (Default CEGISCondition) instance SimpleMergeable CEGISCondition

-- |
-- CEGIS with multiple (possibly symbolic) inputs. Solves the following formula
-- (see 'CEGISCondition' for details).
--
-- \[
--   \forall P. (\exists I\in\mathrm{inputs}. \mathrm{pre}(P, I)) \wedge (\forall I\in\mathrm{inputs}. \mathrm{pre}(P, I)\implies \mathrm{post}(P, I))
-- \]
--
-- For simpler queries, where the inputs are representable by a single
-- symbolic value, you may want to use 'cegis' or 'cegisExcept' instead.
-- We have an example for the 'cegis' call.
cegisMultiInputs ::
  ( EvaluateSym input,
    ExtractSymbolics input,
    ConfigurableSolver config handle
  ) =>
  config ->
  [input] ->
  (input -> CEGISCondition) ->
  IO ([input], CEGISResult SolvingFailure)
cegisMultiInputs :: forall input config handle.
(EvaluateSym input, ExtractSymbolics input,
 ConfigurableSolver config handle) =>
config
-> [input]
-> (input -> CEGISCondition)
-> IO ([input], CEGISResult SolvingFailure)
cegisMultiInputs config
config [input]
inputs input -> CEGISCondition
toCEGISCondition = do
  SymBool
initConstr <- [input] -> IO SymBool
cexesAssertFun [input]
conInputs
  config
-> SymBool
-> SynthesisConstraintFun input
-> CEGISMultiInputsState input
-> StatefulVerifierFun
     (CEGISMultiInputsState input) input SolvingFailure
-> IO ([input], CEGISResult SolvingFailure)
forall config handle input verifierState exception.
ConfigurableSolver config handle =>
config
-> SymBool
-> SynthesisConstraintFun input
-> verifierState
-> StatefulVerifierFun verifierState input exception
-> IO ([input], CEGISResult exception)
genericCEGIS
    config
config
    SymBool
initConstr
    SynthesisConstraintFun input
forall {m :: * -> *} {p}. Monad m => p -> input -> m SymBool
synthConstr
    ([input] -> SymBool -> SymBool -> CEGISMultiInputsState input
forall input.
[input] -> SymBool -> SymBool -> CEGISMultiInputsState input
CEGISMultiInputsState [input]
symInputs (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True) (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True))
    StatefulVerifierFun
  (CEGISMultiInputsState input) input SolvingFailure
verifier
  where
    ([input]
conInputs, [input]
symInputs) = (input -> Bool) -> [input] -> ([input], [input])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (SymbolSet -> Bool
forall symbolSet (typedSymbol :: * -> *).
SymbolSetOps symbolSet typedSymbol =>
symbolSet -> Bool
isEmptySet (SymbolSet -> Bool) -> (input -> SymbolSet) -> input -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. input -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics) [input]
inputs
    forallSymbols :: SymbolSet
forallSymbols = [input] -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics [input]
symInputs
    cexAssertFun :: input -> m SymBool
cexAssertFun input
input = do
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (SymbolSet -> Bool
forall symbolSet (typedSymbol :: * -> *).
SymbolSetOps symbolSet typedSymbol =>
symbolSet -> Bool
isEmptySet (input -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics input
input)) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall a. HasCallStack => String -> a
error String
"BUG"
      CEGISCondition SymBool
pre SymBool
post <- CEGISCondition -> m CEGISCondition
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (CEGISCondition -> m CEGISCondition)
-> CEGISCondition -> m CEGISCondition
forall a b. (a -> b) -> a -> b
$ input -> CEGISCondition
toCEGISCondition input
input
      SymBool -> m SymBool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBool -> m SymBool) -> SymBool -> m SymBool
forall a b. (a -> b) -> a -> b
$ SymBool
pre SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool
post
    cexesAssertFun :: [input] -> IO SymBool
cexesAssertFun = (SymBool -> input -> IO SymBool)
-> SymBool -> [input] -> IO SymBool
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\SymBool
acc input
x -> (SymBool
acc SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&&) (SymBool -> SymBool) -> IO SymBool -> IO SymBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> input -> IO SymBool
forall {m :: * -> *}. Monad m => input -> m SymBool
cexAssertFun input
x) (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True)
    synthConstr :: p -> input -> m SymBool
synthConstr p
_ = input -> m SymBool
forall {m :: * -> *}. Monad m => input -> m SymBool
cexAssertFun
    verifier :: StatefulVerifierFun
  (CEGISMultiInputsState input) input SolvingFailure
verifier state :: CEGISMultiInputsState input
state@(CEGISMultiInputsState [] SymBool
_ SymBool
_) Model
_ =
      (CEGISMultiInputsState input, VerifierResult input SolvingFailure)
-> IO
     (CEGISMultiInputsState input, VerifierResult input SolvingFailure)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CEGISMultiInputsState input
state, VerifierResult input SolvingFailure
forall input exception. VerifierResult input exception
CEGISVerifierNoCex)
    verifier
      (CEGISMultiInputsState (input
nextSymInput : [input]
symInputs) SymBool
pre SymBool
post)
      Model
candidate = do
        CEGISCondition SymBool
nextPre SymBool
nextPost <-
          CEGISCondition -> IO CEGISCondition
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CEGISCondition -> IO CEGISCondition)
-> CEGISCondition -> IO CEGISCondition
forall a b. (a -> b) -> a -> b
$ input -> CEGISCondition
toCEGISCondition input
nextSymInput
        let newPre :: SymBool
newPre = SymBool
pre SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool
nextPre
        let newPost :: SymBool
newPost = SymBool
post SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool
nextPost
        let evaluated :: SymBool
evaluated =
              Bool -> Model -> SymBool -> SymBool
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
False (SymbolSet -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
symbolSet -> model -> model
exceptFor SymbolSet
forallSymbols Model
candidate) (SymBool -> SymBool) -> SymBool -> SymBool
forall a b. (a -> b) -> a -> b
$
                SymBool
newPre SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot SymBool
newPost
        Either SolvingFailure Model
r <- config -> SymBool -> IO (Either SolvingFailure Model)
forall config handle.
ConfigurableSolver config handle =>
config -> SymBool -> IO (Either SolvingFailure Model)
solve config
config SymBool
evaluated
        case Either SolvingFailure Model
r of
          Left SolvingFailure
Unsat ->
            StatefulVerifierFun
  (CEGISMultiInputsState input) input SolvingFailure
verifier ([input] -> SymBool -> SymBool -> CEGISMultiInputsState input
forall input.
[input] -> SymBool -> SymBool -> CEGISMultiInputsState input
CEGISMultiInputsState [input]
symInputs SymBool
newPre SymBool
newPost) Model
candidate
          Left SolvingFailure
err ->
            (CEGISMultiInputsState input, VerifierResult input SolvingFailure)
-> IO
     (CEGISMultiInputsState input, VerifierResult input SolvingFailure)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return
              ( [input] -> SymBool -> SymBool -> CEGISMultiInputsState input
forall input.
[input] -> SymBool -> SymBool -> CEGISMultiInputsState input
CEGISMultiInputsState [] SymBool
newPre SymBool
newPost,
                SolvingFailure -> VerifierResult input SolvingFailure
forall input exception. exception -> VerifierResult input exception
CEGISVerifierException SolvingFailure
err
              )
          Right Model
model ->
            (CEGISMultiInputsState input, VerifierResult input SolvingFailure)
-> IO
     (CEGISMultiInputsState input, VerifierResult input SolvingFailure)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return
              ( [input] -> SymBool -> SymBool -> CEGISMultiInputsState input
forall input.
[input] -> SymBool -> SymBool -> CEGISMultiInputsState input
CEGISMultiInputsState (input
nextSymInput input -> [input] -> [input]
forall a. a -> [a] -> [a]
: [input]
symInputs) SymBool
newPre SymBool
newPost,
                input -> VerifierResult input SolvingFailure
forall input exception. input -> VerifierResult input exception
CEGISVerifierFoundCex (input -> VerifierResult input SolvingFailure)
-> input -> VerifierResult input SolvingFailure
forall a b. (a -> b) -> a -> b
$
                  Bool -> Model -> input -> input
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
False (SymbolSet -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
symbolSet -> model -> model
exact SymbolSet
forallSymbols Model
model) input
nextSymInput
              )

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

-- |
-- CEGIS for symbolic programs with error handling, using multiple (possibly
-- symbolic) inputs to represent a set of inputs.
cegisExceptMultiInputs ::
  ( ConfigurableSolver config handle,
    EvaluateSym inputs,
    ExtractSymbolics inputs,
    UnionWithExcept t u e v,
    PlainUnion u,
    Monad u
  ) =>
  config ->
  [inputs] ->
  (Either e v -> CEGISCondition) ->
  (inputs -> t) ->
  IO ([inputs], CEGISResult SolvingFailure)
cegisExceptMultiInputs :: forall config handle inputs t (u :: * -> *) e v.
(ConfigurableSolver config handle, EvaluateSym inputs,
 ExtractSymbolics inputs, UnionWithExcept t u e v, PlainUnion u,
 Monad u) =>
config
-> [inputs]
-> (Either e v -> CEGISCondition)
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
cegisExceptMultiInputs config
config [inputs]
cexes Either e v -> CEGISCondition
interpretFun inputs -> t
f =
  config
-> [inputs]
-> (inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure)
forall input config handle.
(EvaluateSym input, ExtractSymbolics input,
 ConfigurableSolver config handle) =>
config
-> [input]
-> (input -> CEGISCondition)
-> IO ([input], CEGISResult SolvingFailure)
cegisMultiInputs
    config
config
    [inputs]
cexes
    (u CEGISCondition -> CEGISCondition
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (u CEGISCondition -> CEGISCondition)
-> (inputs -> u CEGISCondition) -> inputs -> CEGISCondition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Either e v -> CEGISCondition
interpretFun (Either e v -> CEGISCondition)
-> u (Either e v) -> u CEGISCondition
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (u (Either e v) -> u CEGISCondition)
-> (inputs -> u (Either e v)) -> inputs -> u CEGISCondition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> u (Either e v)
forall t (u :: * -> *) e v.
UnionWithExcept t u e v =>
t -> u (Either e v)
extractUnionExcept (t -> u (Either e v)) -> (inputs -> t) -> inputs -> u (Either e v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. inputs -> t
f)

-- |
-- CEGIS for symbolic programs with error handling, using multiple (possibly
-- symbolic) inputs to represent a set of inputs.
--
-- The errors should be translated to assertion or assumption violations.
cegisExceptVCMultiInputs ::
  ( ConfigurableSolver config handle,
    EvaluateSym inputs,
    ExtractSymbolics inputs,
    UnionWithExcept t u e v,
    PlainUnion u,
    Monad u
  ) =>
  config ->
  [inputs] ->
  (Either e v -> u (Either VerificationConditions ())) ->
  (inputs -> t) ->
  IO ([inputs], CEGISResult SolvingFailure)
cegisExceptVCMultiInputs :: forall config handle inputs t (u :: * -> *) e v.
(ConfigurableSolver config handle, EvaluateSym inputs,
 ExtractSymbolics inputs, UnionWithExcept t u e v, PlainUnion u,
 Monad u) =>
config
-> [inputs]
-> (Either e v -> u (Either VerificationConditions ()))
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
cegisExceptVCMultiInputs config
config [inputs]
cexes Either e v -> u (Either VerificationConditions ())
interpretFun inputs -> t
f =
  config
-> [inputs]
-> (inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure)
forall input config handle.
(EvaluateSym input, ExtractSymbolics input,
 ConfigurableSolver config handle) =>
config
-> [input]
-> (input -> CEGISCondition)
-> IO ([input], CEGISResult SolvingFailure)
cegisMultiInputs
    config
config
    [inputs]
cexes
    ( \inputs
v ->
        u CEGISCondition -> CEGISCondition
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge
          ( ( \case
                Left VerificationConditions
AssumptionViolation -> SymBool -> SymBool -> CEGISCondition
cegisPrePost (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False) (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True)
                Left VerificationConditions
AssertionViolation -> SymBool -> CEGISCondition
cegisPostCond (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False)
                Either VerificationConditions ()
_ -> SymBool -> CEGISCondition
cegisPostCond (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True)
            )
              (Either VerificationConditions () -> CEGISCondition)
-> u (Either VerificationConditions ()) -> u CEGISCondition
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (t -> u (Either e v)
forall t (u :: * -> *) e v.
UnionWithExcept t u e v =>
t -> u (Either e v)
extractUnionExcept (inputs -> t
f inputs
v) u (Either e v)
-> (Either e v -> u (Either VerificationConditions ()))
-> u (Either VerificationConditions ())
forall a b. u a -> (a -> u b) -> u b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Either e v -> u (Either VerificationConditions ())
interpretFun)
          )
    )

-- |
-- CEGIS for symbolic programs with error handling, using multiple (possibly
-- symbolic) inputs to represent a set of inputs. This function saves the
-- efforts to implement the translation function for the standard error type
-- 'VerificationConditions', and the standard result type '()'.
--
-- This function translates assumption violations to failed pre-conditions,
-- and translates assertion violations to failed post-conditions.
-- The '()' result will not fail any conditions.
cegisExceptStdVCMultiInputs ::
  ( ConfigurableSolver config handle,
    EvaluateSym inputs,
    ExtractSymbolics inputs,
    UnionWithExcept t u VerificationConditions (),
    PlainUnion u,
    Monad u
  ) =>
  config ->
  [inputs] ->
  (inputs -> t) ->
  IO ([inputs], CEGISResult SolvingFailure)
cegisExceptStdVCMultiInputs :: forall config handle inputs t (u :: * -> *).
(ConfigurableSolver config handle, EvaluateSym inputs,
 ExtractSymbolics inputs,
 UnionWithExcept t u VerificationConditions (), PlainUnion u,
 Monad u) =>
config
-> [inputs]
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
cegisExceptStdVCMultiInputs config
config [inputs]
cexes =
  config
-> [inputs]
-> (Either VerificationConditions ()
    -> u (Either VerificationConditions ()))
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
forall config handle inputs t (u :: * -> *) e v.
(ConfigurableSolver config handle, EvaluateSym inputs,
 ExtractSymbolics inputs, UnionWithExcept t u e v, PlainUnion u,
 Monad u) =>
config
-> [inputs]
-> (Either e v -> u (Either VerificationConditions ()))
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
cegisExceptVCMultiInputs config
config [inputs]
cexes Either VerificationConditions ()
-> u (Either VerificationConditions ())
forall a. a -> u a
forall (m :: * -> *) a. Monad m => a -> m a
return

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

-- |
-- CEGIS for symbolic programs with error handling, using a single symbolic
-- input to represent a set of inputs.
--
-- The errors should be translated to assertion or assumption violations.
cegisExceptVC ::
  ( UnionWithExcept t u e v,
    PlainUnion u,
    Monad u,
    EvaluateSym inputs,
    ExtractSymbolics inputs,
    ConfigurableSolver config handle,
    SEq inputs
  ) =>
  config ->
  inputs ->
  (Either e v -> u (Either VerificationConditions ())) ->
  (inputs -> t) ->
  IO ([inputs], CEGISResult SolvingFailure)
cegisExceptVC :: forall t (u :: * -> *) e v inputs config handle.
(UnionWithExcept t u e v, PlainUnion u, Monad u,
 EvaluateSym inputs, ExtractSymbolics inputs,
 ConfigurableSolver config handle, SEq inputs) =>
config
-> inputs
-> (Either e v -> u (Either VerificationConditions ()))
-> (inputs -> t)
-> IO ([inputs], CEGISResult SolvingFailure)
cegisExceptVC config
config inputs
inputs Either e v -> u (Either VerificationConditions ())
f inputs -> t
v = do
  config
-> inputs
-> (inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure)
forall config handle inputs.
(ConfigurableSolver config handle, EvaluateSym inputs,
 ExtractSymbolics inputs, SEq inputs) =>
config
-> inputs
-> (inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure)
cegis config
config inputs
inputs ((inputs -> CEGISCondition)
 -> IO ([inputs], CEGISResult SolvingFailure))
-> (inputs -> CEGISCondition)
-> IO ([inputs], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ \inputs
i ->
    u CEGISCondition -> CEGISCondition
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (u CEGISCondition -> CEGISCondition)
-> u CEGISCondition -> CEGISCondition
forall a b. (a -> b) -> a -> b
$
      ( \case
          Left VerificationConditions
AssumptionViolation -> SymBool -> SymBool -> CEGISCondition
cegisPrePost (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False) (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True)
          Left VerificationConditions
AssertionViolation -> SymBool -> CEGISCondition
cegisPostCond (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False)
          Either VerificationConditions ()
_ -> SymBool -> CEGISCondition
cegisPostCond (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True)
      )
        (Either VerificationConditions () -> CEGISCondition)
-> u (Either VerificationConditions ()) -> u CEGISCondition
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (t -> u (Either e v)
forall t (u :: * -> *) e v.
UnionWithExcept t u e v =>
t -> u (Either e v)
extractUnionExcept (inputs -> t
v inputs
i) u (Either e v)
-> (Either e v -> u (Either VerificationConditions ()))
-> u (Either VerificationConditions ())
forall a b. u a -> (a -> u b) -> u b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Either e v -> u (Either VerificationConditions ())
f)

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

-- |
-- CEGIS with a single symbolic input to represent a set of inputs.
--
-- The following example tries to find the value of @c@ such that for all
-- positive @x@, @x * c < 0 && c > -2@. The @c .> -2@ clause is used to make
-- the solution unique.
--
-- >>> :set -XOverloadedStrings
-- >>> let [x,c] = ["x","c"] :: [SymInteger]
-- >>> cegisForAll (precise z3) x $ cegisPrePost (x .> 0) (x * c .< 0 .&& c .> -2)
-- (...,CEGISSuccess (Model {c -> -1 :: Integer}))
cegisForAll ::
  ( ExtractSymbolics forallInput,
    ConfigurableSolver config handle
  ) =>
  config ->
  -- | A symbolic value. All the symbolic constants in the value are treated as
  -- for-all variables.
  forallInput ->
  CEGISCondition ->
  -- | First output are the counter-examples for all the for-all variables, and
  -- the second output is the model for all other variables if CEGIS succeeds.
  IO ([Model], CEGISResult SolvingFailure)
cegisForAll :: forall forallInput config handle.
(ExtractSymbolics forallInput, ConfigurableSolver config handle) =>
config
-> forallInput
-> CEGISCondition
-> IO ([Model], CEGISResult SolvingFailure)
cegisForAll config
config forallInput
input (CEGISCondition SymBool
pre SymBool
post) = do
  ([Model]
models, CEGISResult SolvingFailure
result) <- config
-> SymBool
-> SynthesisConstraintFun Model
-> ()
-> StatefulVerifierFun () Model SolvingFailure
-> IO ([Model], CEGISResult SolvingFailure)
forall config handle input verifierState exception.
ConfigurableSolver config handle =>
config
-> SymBool
-> SynthesisConstraintFun input
-> verifierState
-> StatefulVerifierFun verifierState input exception
-> IO ([input], CEGISResult exception)
genericCEGIS config
config SymBool
phi SynthesisConstraintFun Model
forall {m :: * -> *} {p}. Monad m => p -> Model -> m SymBool
synthConstr () StatefulVerifierFun () Model SolvingFailure
verifier
  let exactResult :: CEGISResult SolvingFailure
exactResult = case CEGISResult SolvingFailure
result of
        CEGISSuccess Model
model -> Model -> CEGISResult SolvingFailure
forall exception. Model -> CEGISResult exception
CEGISSuccess (Model -> CEGISResult SolvingFailure)
-> Model -> CEGISResult SolvingFailure
forall a b. (a -> b) -> a -> b
$ SymbolSet -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
symbolSet -> model -> model
exceptFor SymbolSet
forallSymbols Model
model
        CEGISResult SolvingFailure
_ -> CEGISResult SolvingFailure
result
  ([Model], CEGISResult SolvingFailure)
-> IO ([Model], CEGISResult SolvingFailure)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Model]
models, CEGISResult SolvingFailure
exactResult)
  where
    phi :: SymBool
phi = SymBool
pre SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool
post
    negphi :: SymBool
negphi = SymBool
pre SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot SymBool
post
    forallSymbols :: SymbolSet
forallSymbols = forallInput -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics forallInput
input
    synthConstr :: p -> Model -> m SymBool
synthConstr p
_ Model
model = SymBool -> m SymBool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBool -> m SymBool) -> SymBool -> m SymBool
forall a b. (a -> b) -> a -> b
$ Bool -> Model -> SymBool -> SymBool
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
False Model
model SymBool
phi
    verifier :: StatefulVerifierFun () Model SolvingFailure
verifier () Model
candidate = do
      let evaluated :: SymBool
evaluated =
            Bool -> Model -> SymBool -> SymBool
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
False (SymbolSet -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
symbolSet -> model -> model
exceptFor SymbolSet
forallSymbols Model
candidate) SymBool
negphi
      Either SolvingFailure Model
r <- config -> SymBool -> IO (Either SolvingFailure Model)
forall config handle.
ConfigurableSolver config handle =>
config -> SymBool -> IO (Either SolvingFailure Model)
solve config
config SymBool
evaluated
      case Either SolvingFailure Model
r of
        Left SolvingFailure
Unsat -> ((), VerifierResult Model SolvingFailure)
-> IO ((), VerifierResult Model SolvingFailure)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((), VerifierResult Model SolvingFailure
forall input exception. VerifierResult input exception
CEGISVerifierNoCex)
        Left SolvingFailure
err -> ((), VerifierResult Model SolvingFailure)
-> IO ((), VerifierResult Model SolvingFailure)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((), SolvingFailure -> VerifierResult Model SolvingFailure
forall input exception. exception -> VerifierResult input exception
CEGISVerifierException SolvingFailure
err)
        Right Model
model ->
          ((), VerifierResult Model SolvingFailure)
-> IO ((), VerifierResult Model SolvingFailure)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((), Model -> VerifierResult Model SolvingFailure
forall input exception. input -> VerifierResult input exception
CEGISVerifierFoundCex (Model -> VerifierResult Model SolvingFailure)
-> Model -> VerifierResult Model SolvingFailure
forall a b. (a -> b) -> a -> b
$ SymbolSet -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
symbolSet -> model -> model
exact SymbolSet
forallSymbols Model
model)

-- |
-- CEGIS for symbolic programs with error handling, with a forall variable.
--
-- See 'cegisForAll' and 'cegisExcept'.
cegisForAllExcept ::
  ( UnionWithExcept t u e v,
    PlainUnion u,
    Functor u,
    EvaluateSym inputs,
    ExtractSymbolics inputs,
    ConfigurableSolver config handle,
    SEq inputs
  ) =>
  config ->
  inputs ->
  (Either e v -> CEGISCondition) ->
  t ->
  IO ([Model], CEGISResult SolvingFailure)
cegisForAllExcept :: forall t (u :: * -> *) e v inputs config handle.
(UnionWithExcept t u e v, PlainUnion u, Functor u,
 EvaluateSym inputs, ExtractSymbolics inputs,
 ConfigurableSolver config handle, SEq inputs) =>
config
-> inputs
-> (Either e v -> CEGISCondition)
-> t
-> IO ([Model], CEGISResult SolvingFailure)
cegisForAllExcept config
config inputs
inputs Either e v -> CEGISCondition
f t
v =
  config
-> inputs
-> CEGISCondition
-> IO ([Model], CEGISResult SolvingFailure)
forall forallInput config handle.
(ExtractSymbolics forallInput, ConfigurableSolver config handle) =>
config
-> forallInput
-> CEGISCondition
-> IO ([Model], CEGISResult SolvingFailure)
cegisForAll config
config inputs
inputs (CEGISCondition -> IO ([Model], CEGISResult SolvingFailure))
-> CEGISCondition -> IO ([Model], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$ u CEGISCondition -> CEGISCondition
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (u CEGISCondition -> CEGISCondition)
-> u CEGISCondition -> CEGISCondition
forall a b. (a -> b) -> a -> b
$ Either e v -> CEGISCondition
f (Either e v -> CEGISCondition)
-> u (Either e v) -> u CEGISCondition
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> u (Either e v)
forall t (u :: * -> *) e v.
UnionWithExcept t u e v =>
t -> u (Either e v)
extractUnionExcept t
v

-- |
-- CEGIS for symbolic programs with error handling, with a forall variable.
--
-- See 'cegisForAll' and 'cegisExceptVC'.
cegisForAllExceptVC ::
  ( UnionWithExcept t u e v,
    PlainUnion u,
    Monad u,
    EvaluateSym inputs,
    ExtractSymbolics inputs,
    ConfigurableSolver config handle,
    SEq inputs
  ) =>
  config ->
  inputs ->
  (Either e v -> u (Either VerificationConditions ())) ->
  t ->
  IO ([Model], CEGISResult SolvingFailure)
cegisForAllExceptVC :: forall t (u :: * -> *) e v inputs config handle.
(UnionWithExcept t u e v, PlainUnion u, Monad u,
 EvaluateSym inputs, ExtractSymbolics inputs,
 ConfigurableSolver config handle, SEq inputs) =>
config
-> inputs
-> (Either e v -> u (Either VerificationConditions ()))
-> t
-> IO ([Model], CEGISResult SolvingFailure)
cegisForAllExceptVC config
config inputs
inputs Either e v -> u (Either VerificationConditions ())
f t
v = do
  config
-> inputs
-> CEGISCondition
-> IO ([Model], CEGISResult SolvingFailure)
forall forallInput config handle.
(ExtractSymbolics forallInput, ConfigurableSolver config handle) =>
config
-> forallInput
-> CEGISCondition
-> IO ([Model], CEGISResult SolvingFailure)
cegisForAll config
config inputs
inputs (CEGISCondition -> IO ([Model], CEGISResult SolvingFailure))
-> CEGISCondition -> IO ([Model], CEGISResult SolvingFailure)
forall a b. (a -> b) -> a -> b
$
    u CEGISCondition -> CEGISCondition
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (u CEGISCondition -> CEGISCondition)
-> u CEGISCondition -> CEGISCondition
forall a b. (a -> b) -> a -> b
$
      ( \case
          Left VerificationConditions
AssumptionViolation -> SymBool -> SymBool -> CEGISCondition
cegisPrePost (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False) (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True)
          Left VerificationConditions
AssertionViolation -> SymBool -> CEGISCondition
cegisPostCond (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False)
          Either VerificationConditions ()
_ -> SymBool -> CEGISCondition
cegisPostCond (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True)
      )
        (Either VerificationConditions () -> CEGISCondition)
-> u (Either VerificationConditions ()) -> u CEGISCondition
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (t -> u (Either e v)
forall t (u :: * -> *) e v.
UnionWithExcept t u e v =>
t -> u (Either e v)
extractUnionExcept t
v u (Either e v)
-> (Either e v -> u (Either VerificationConditions ()))
-> u (Either VerificationConditions ())
forall a b. u a -> (a -> u b) -> u b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Either e v -> u (Either VerificationConditions ())
f)

-- |
-- CEGIS for symbolic programs with error handling, with a forall variable.
--
-- See 'cegisForAll' and 'cegisExceptStdVC'.
cegisForAllExceptStdVC ::
  ( UnionWithExcept t u VerificationConditions (),
    PlainUnion u,
    Monad u,
    EvaluateSym inputs,
    ExtractSymbolics inputs,
    ConfigurableSolver config handle,
    SEq inputs
  ) =>
  config ->
  inputs ->
  t ->
  IO ([Model], CEGISResult SolvingFailure)
cegisForAllExceptStdVC :: forall t (u :: * -> *) inputs config handle.
(UnionWithExcept t u VerificationConditions (), PlainUnion u,
 Monad u, EvaluateSym inputs, ExtractSymbolics inputs,
 ConfigurableSolver config handle, SEq inputs) =>
config -> inputs -> t -> IO ([Model], CEGISResult SolvingFailure)
cegisForAllExceptStdVC config
config inputs
inputs = config
-> inputs
-> (Either VerificationConditions ()
    -> u (Either VerificationConditions ()))
-> t
-> IO ([Model], CEGISResult SolvingFailure)
forall t (u :: * -> *) e v inputs config handle.
(UnionWithExcept t u e v, PlainUnion u, Monad u,
 EvaluateSym inputs, ExtractSymbolics inputs,
 ConfigurableSolver config handle, SEq inputs) =>
config
-> inputs
-> (Either e v -> u (Either VerificationConditions ()))
-> t
-> IO ([Model], CEGISResult SolvingFailure)
cegisForAllExceptVC config
config inputs
inputs Either VerificationConditions ()
-> u (Either VerificationConditions ())
forall a. a -> u a
forall (m :: * -> *) a. Monad m => a -> m a
return