grisette-0.1.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2023
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellTrustworthy
LanguageHaskell2010

Grisette.Core.Data.Class.CEGISSolver

Description

 
Synopsis

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.

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.