Copyright	(c) Sirui Lu 2021-2023
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	Trustworthy
Language	Haskell2010

Grisette.Core.Data.Class.CEGISSolver

Contents

Note for the examples
CEGIS solver interfaces

Description

Synopsis

class CEGISSolver config failure | config -> failure where
- cegisMultiInputs :: (EvaluateSym inputs, ExtractSymbolics inputs) => config -> [inputs] -> (inputs -> CEGISCondition) -> IO (Either failure ([inputs], Model))
data CEGISCondition = CEGISCondition SymBool SymBool
cegisPostCond :: SymBool -> CEGISCondition
cegisPrePost :: SymBool -> SymBool -> CEGISCondition
cegis :: (CEGISSolver config failure, EvaluateSym inputs, ExtractSymbolics inputs) => config -> inputs -> CEGISCondition -> IO (Either failure ([inputs], Model))
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 (Either failure ([inputs], Model))
cegisExceptStdVC :: (UnionWithExcept t u VerificationConditions (), UnionPrjOp u, Monad u, EvaluateSym inputs, ExtractSymbolics inputs, CEGISSolver config failure) => config -> inputs -> t -> IO (Either failure ([inputs], Model))
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 (Either failure ([inputs], Model))
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 (Either failure ([inputs], Model))
cegisExceptStdVCMultiInputs :: (CEGISSolver config failure, EvaluateSym inputs, ExtractSymbolics inputs, UnionWithExcept t u VerificationConditions (), UnionPrjOp u, Monad u) => config -> [inputs] -> (inputs -> t) -> IO (Either failure ([inputs], Model))
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 (Either failure ([inputs], Model))

Note for the examples

The examples assumes a z3 solver available in PATH.

CEGIS solver interfaces

class CEGISSolver config failure | config -> failure where Source #

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

Methods

cegisMultiInputs Source #

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 (Either failure ([inputs], 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

Instances details

CEGISSolver (GrisetteSMTConfig n) CheckSatResult Source #
Instance details Defined in Grisette.Backend.SBV.Data.SMT.Solving Methods cegisMultiInputs :: (EvaluateSym inputs, ExtractSymbolics inputs) => GrisetteSMTConfig n -> [inputs] -> (inputs -> CEGISCondition) -> IO (Either CheckSatResult ([inputs], Model)) Source #

data CEGISCondition Source #

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

Instances details

Generic CEGISCondition Source #
Instance details 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 Source #
Instance details Defined in Grisette.Core.Data.Class.CEGISSolver Methods rootStrategy :: MergingStrategy CEGISCondition Source #
SimpleMergeable CEGISCondition Source #
Instance details Defined in Grisette.Core.Data.Class.CEGISSolver Methods mrgIte :: SymBool -> CEGISCondition -> CEGISCondition -> CEGISCondition Source #
type Rep CEGISCondition Source #
Instance details Defined in Grisette.Core.Data.Class.CEGISSolver type Rep CEGISCondition = D1 ('MetaData "CEGISCondition" "Grisette.Core.Data.Class.CEGISSolver" "grisette-0.1.0.0-7JmpZvRpjzaDDLSSjCfe9O" '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 Source #

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 Source #

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

cegis Source #

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 (Either failure ([inputs], 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 (UnboundedReasoning 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 (Either failure ([inputs], Model)) Source #

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 (UnboundedReasoning 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 (Either failure ([inputs], Model)) Source #

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 (UnboundedReasoning 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 (Either failure ([inputs], Model)) Source #

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 (Either failure ([inputs], Model)) Source #

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 (Either failure ([inputs], Model)) Source #

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 (Either failure ([inputs], Model)) Source #

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.