sbv-8.7: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Data.SBV.Tools.GenTest

Contents

Description

Test generation from symbolic programs

Synopsis

# Test case generation

Generate a set of concrete test values from a symbolic program. The output can be rendered as test vectors in different languages as necessary. Use the function output call to indicate what fields should be in the test result. (Also see constrain for filtering acceptable test values.)

Type of test vectors (abstract)

getTestValues :: TestVectors -> [([CV], [CV])] Source #

Retrieve the test vectors for further processing. This function is useful in cases where renderTest is not sufficient and custom output (or further preprocessing) is needed.

Render the test as a Haskell value with the given name n.

data TestStyle Source #

Test output style

Constructors

 Haskell String As a Haskell value with given name C String As a C array of structs with given name Forte String Bool ([Int], [Int]) As a Forte/Verilog value with given name. If the boolean is True then vectors are blasted big-endian, otherwise little-endian The indices are the split points on bit-vectors for input and output values