The response from a verifier.

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.

The verifier.

The result of the CEGIS procedure.

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.

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.

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.

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.

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.

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.

Construct a CEGIS condition with both pre- and post-conditions.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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 && 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 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 && 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}))

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 && 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}))

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.

CEGIS for symbolic programs with error handling, using multiple (possibly symbolic) inputs to represent a set of inputs.

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.

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.

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 && 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}))

CEGIS for symbolic programs with error handling, with a forall variable.

See cegisForAll and cegisExcept.

CEGIS for symbolic programs with error handling, with a forall variable.

See cegisForAll and cegisExceptStdVC.

CEGIS for symbolic programs with error handling, with a forall variable.

See cegisForAll and cegisExceptVC.