pretty print an Integral in a given base

pretty print an Integral in hexadecimal

pretty print an Integral in binary

pretty print a whitespace separated list of Doc in parentheses

pretty print a whitespace separated list of parenthesised pairs of Docs in parentheses

pretty print the application of an operator to a list of arguments

pretty print an Integer as an SMT BitVec hexadecimal literal

pretty print an Integer as an SMT BitVec binary literal

extract the bitslice from lo to hi from the bv SMT BitVec

return a string representing the BitVec SMT sort of the given width n

pretty print the BitVec SMT sort of the given width n

cast the Int sorted SMT value n to a (BitVec w) sorted SMT value

test a (BitVec 1) sorted SMT value for "false"

test a (BitVec 1) sorted SMT value for "true"

cast a (BitVec 1) sorted SMT value to a Bool sorted SMT value

cast a Bool sorted SMT value to a (BitVec 1) sorted SMT value

wrap the SMT expression expr in the "as" qualifier with the given sort

wrap the SMT parametric expression expr in the "par" sort parameter binder with the pars list of sort parameters

wrap an SMT expression in the "forall" universal quantifier with the provided list of pairs of (variable name, sort)

wrap an SMT expression in the "exists" existential quantifier with the provided list of pairs of (variable name, sort)

wrap an SMT expression in the "match" binder, pattern matching the SMT expression against each of the patterns provided in the argument list of pairs of (pattern, expression)

wrap an SMT expression in the "let" binder with the provided list of pairs of (variable name, sort)

wrap an SMT expression in a sequence of nested "let" binders, each introducing one of the variables provided by the argument list of pairs of (variable name, sort), in the provided order

pretty print the declaration of the datatypes provided in the argument list of triples each representing a single datatype: its name, a potentially empty list of parameters, and a non empty list of constructors consisting of a name and a potentially empty list of fields

pretty print the declaration of a single datatype given its name, a potentially empty list of parameters, and a non empty list of constructors consisting of a name and a potentially empty list of fields

pretty print the definition of a function given its name, a potentially empty list of arguments, a return type and a function body

pretty print the definition of a recursive function given its name, a potentially empty list of arguments, a return type and a function body

pretty print the definition of the potentially mutually recursive functions provided in the argument list of triples each representing a single potentially recursive function: its name, a potentially empty list of arguments, a return type and a function body