Constraint package:sbv

class MonadSymbolic m => Constraint (m :: Type -> Type) a

sbv Data.SBV.Internals Data.SBV.Internals

Values that we can turn into a constraint

constraint :: (MonadIO m, Constraint (SymbolicT m) a) => State -> a -> m SV

Generate a constraint. We allow free variables here (first arg of constraintGen). This might prove to be not kosher!

type ConstraintSet = Symbolic ()

A constraint set is a symbolic program that returns no values. The idea is that the constraints/min-max goals will serve as the collection of constraints that will be used for sat/optimize calls.

constraintStr :: (MonadIO m, Constraint (SymbolicT m) a) => State -> a -> m String

sbv Data.SBV.Internals

Generate a constraint, string version We allow free variables here (first arg of constraintGen). This might prove to be not kosher!

namedConstraint :: (SolverContext m, QuantifiedBool a) => String -> a -> m ()

sbv Data.SBV Data.SBV.Internals Data.SBV.Trans

Add a named constraint. The name is used in unsat-core extraction.

optimizeValidateConstraints :: SMTConfig -> Bool

sbv Data.SBV Data.SBV.Dynamic Data.SBV.Internals Data.SBV.Trans

Validate optimization results. NB: Does NOT make sure the model is optimal, just checks they satisfy the constraints.

internalConstraint :: State -> Bool -> [(String, String)] -> SVal -> IO ()

sbv Data.SBV.Internals

Require a boolean condition to be true in the state. Only used for internal purposes.

mkConstraint :: Constraint m a => State -> a -> m ()

sbv Data.SBV.Internals Data.SBV.Internals

resConstraints :: Result -> Seq (Bool, [(String, String)], SV)

sbv Data.SBV.Internals Data.SBV.Internals

additional constraints (boolean)