Data.SBV.Program.Utils

Documentation

sampleSpec :: forall a comp spec. (SymVal a, SynthSpec spec a) => spec a -> IO (Maybe (IOs a))

Given a SynthSpec tries to generate a set of input/output values that satisfy the specification. Uses solver under the hood.

mkVarName

Arguments

:: String

Base name, which can be an empty string, in which case "UnnamedComponent" value will be used.

-> Bool

Setting isLocation to True will append "Loc" to the name.

-> Bool

If isOutput is False the value of i is also appended to the name.

-> Word

Number of an input. Can be undefined for an output.

-> String

Creates sanitized variable name suitable for SBV.

mkInputLocName :: String -> Word -> String

Shortcut for the more general mkVarName function.

mkOutputLocName :: String -> String

Shortcut for the more general mkVarName function.

mkInputVarName :: String -> Word -> String

Shortcut for the more general mkVarName function.

mkOutputVarName :: String -> String

Shortcut for the more general mkVarName function.

writePseudocode :: SynthComponent comp spec a => Program Location (comp a) -> String

Renders the solution in SSA style.