| Copyright | (c) Alexandre Joannou 2020-2021 |
|---|---|
| License | MIT |
| Stability | experimental |
| Safe Haskell | Safe-Inferred |
| Language | GHC2021 |
Blarney.Backend.SMT.NetlistUtils
Description
This module provides blarney Netlist pretty printing utilities for SMT code generation
Synopsis
- declareNLDatatype :: Netlist -> [InstId] -> String -> Doc
- mkNLDatatype :: String -> [Doc] -> Doc
- defineNLTransition :: Netlist -> Net -> (String, String) -> [InstId] -> [InstId] -> String -> Doc
- defineChainTransition :: String -> (String, String) -> String -> Doc
- assertBounded :: String -> String -> (String, String) -> [(Integer, InputWidth)] -> Int -> Bool -> Doc
- assertInduction :: String -> (String, String) -> Int -> Bool -> Doc
- wireName :: Netlist -> WireId -> String
Documentation
declareNLDatatype :: Netlist -> [InstId] -> String -> Doc Source #
Declare a datatype whose fields are specific to the provided Netlist
mkNLDatatype :: String -> [Doc] -> Doc Source #
Invoke the constructor for a datatype declared with declareNLDatatype
defineNLTransition :: Netlist -> Net -> (String, String) -> [InstId] -> [InstId] -> String -> Doc Source #
defineChainTransition :: String -> (String, String) -> String -> Doc Source #
Define the repeated application of a function
assertBounded :: String -> String -> (String, String) -> [(Integer, InputWidth)] -> Int -> Bool -> Doc Source #
Define inputs and assertion of the bounded property represented by the provided chaining function, with a given initial state, and for a given depth
assertInduction :: String -> (String, String) -> Int -> Bool -> Doc Source #
Define inputs and assertion of the induction step for proof by induction of
the provided chaining function for the checked property, for a given
induction depth and with optional state restriction.
To assert a base case, the assertBounded function can be used.