Grisette.Core.Data.Class.CEGISSolver

Note for the examples

The examples assumes a z3 solver available in PATH.

CEGIS solver interfaces

class CEGISSolver config failure | config -> failure where

Counter-example guided inductive synthesis (CEGIS) solver interface.

Methods

cegisMultiInputs

Arguments

:: (EvaluateSym inputs, ExtractSymbolics inputs)

=> config

The configuration of the solver

-> [inputs]

Some initial counter-examples. Providing some concrete inputs may help the solver to find a model faster. Providing symbolic inputs would cause the solver to find the program that works on all the inputs representable by it (see CEGISCondition).

-> (inputs -> CEGISCondition)

The function mapping the inputs to the conditions for the solver to solve.

-> IO ([inputs], Either failure Model)

The counter-examples generated during the CEGIS loop, and the model found by the solver.

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.

Instances

CEGISSolver (GrisetteSMTConfig n) SolvingFailure

Defined in Grisette.Backend.SBV.Data.SMT.Solving

Methods

cegisMultiInputs :: (EvaluateSym inputs, ExtractSymbolics inputs) => GrisetteSMTConfig n -> [inputs] -> (inputs -> CEGISCondition) -> IO ([inputs], Either SolvingFailure Model)

data CEGISCondition

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.

Constructors

CEGISCondition SymBool SymBool

Instances

Generic CEGISCondition

Defined in Grisette.Core.Data.Class.CEGISSolver

Associated Types

type Rep CEGISCondition :: Type -> Type

Methods

from :: CEGISCondition -> Rep CEGISCondition x

to :: Rep CEGISCondition x -> CEGISCondition

Mergeable CEGISCondition

Defined in Grisette.Core.Data.Class.CEGISSolver

Methods

rootStrategy :: MergingStrategy CEGISCondition

SimpleMergeable CEGISCondition

Defined in Grisette.Core.Data.Class.CEGISSolver

Methods

mrgIte :: SymBool -> CEGISCondition -> CEGISCondition -> CEGISCondition

type Rep CEGISCondition

Defined in Grisette.Core.Data.Class.CEGISSolver

type Rep CEGISCondition = D1 ('MetaData "CEGISCondition" "Grisette.Core.Data.Class.CEGISSolver" "grisette-0.2.0.0-CYZZ7WjRTnw1wxrPITB8ce" 'False) (C1 ('MetaCons "CEGISCondition" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SymBool) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SymBool)))

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

cegisPrePost :: SymBool -> SymBool -> CEGISCondition

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

cegis

Arguments

:: (CEGISSolver config failure, EvaluateSym inputs, ExtractSymbolics inputs)

=> config

The configuration of the solver

-> inputs

Initial symbolic inputs. The solver will try to find a program that works on all the inputs representable by it (see CEGISCondition).

-> CEGISCondition

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.

-> IO ([inputs], Either failure Model)

The counter-examples generated during the CEGIS loop, and the model found by the solver.

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 (cegisPrePost (x >~ 0) (x * c <~ 0 &&~ c >~ -2))
([],Right (Model {c -> -1 :: Integer}))

cegisExcept :: (UnionWithExcept t u e v, UnionPrjOp u, Functor u, EvaluateSym inputs, ExtractSymbolics inputs, CEGISSolver config failure) => config -> inputs -> (Either e v -> CEGISCondition) -> t -> IO ([inputs], Either failure Model)

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 :: ExceptT VerificationConditions UnionM ()
  res = 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
([],Right (Model {c -> -1 :: Integer}))

cegisExceptStdVC :: (UnionWithExcept t u VerificationConditions (), UnionPrjOp u, Monad u, EvaluateSym inputs, ExtractSymbolics inputs, CEGISSolver config failure) => config -> inputs -> t -> IO ([inputs], Either failure Model)

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 :: ExceptT VerificationConditions UnionM ()
  res = do
    symAssume $ x >~ 0
    symAssert $ x * c <~ 0
    symAssert $ c >~ -2
:}

>>> cegisExceptStdVC (precise z3) x res
([],Right (Model {c -> -1 :: Integer}))

cegisExceptVC :: (UnionWithExcept t u e v, UnionPrjOp u, Monad u, EvaluateSym inputs, ExtractSymbolics inputs, CEGISSolver config failure) => config -> inputs -> (Either e v -> u (Either VerificationConditions ())) -> t -> IO ([inputs], Either failure Model)

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.

cegisExceptMultiInputs :: (CEGISSolver config failure, EvaluateSym inputs, ExtractSymbolics inputs, UnionWithExcept t u e v, UnionPrjOp u, Monad u) => config -> [inputs] -> (Either e v -> CEGISCondition) -> (inputs -> t) -> IO ([inputs], Either failure Model)

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

cegisExceptStdVCMultiInputs :: (CEGISSolver config failure, EvaluateSym inputs, ExtractSymbolics inputs, UnionWithExcept t u VerificationConditions (), UnionPrjOp u, Monad u) => config -> [inputs] -> (inputs -> t) -> IO ([inputs], Either failure Model)

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.

cegisExceptVCMultiInputs :: (CEGISSolver config failure, EvaluateSym inputs, ExtractSymbolics inputs, UnionWithExcept t u e v, UnionPrjOp u, Monad u) => config -> [inputs] -> (Either e v -> u (Either VerificationConditions ())) -> (inputs -> t) -> IO ([inputs], Either failure Model)

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.