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.

The result of the verifier.

The verifier function.

The first argument is the state of the verifier.

The second argument is the candidate model proposed by the synthesizer.

The result of the CEGIS procedure.

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. 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.

>>> :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 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.

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

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.

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

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.

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

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.