All signal/function/predicate Abstract Data Types in TSL.Logic are curried, and they need to transformed to a AST-style syntax in order to be fed into a SMT or SyGuS solver.
TSL.ModuloThoeries.AST defines the AST type, and the transformative functions thereof.
All signal/function/predicate Abstract Data Types in
TSL.Logicare curried, and they need to transformed to a AST-style syntax in order to be fed into a SMT or SyGuS solver.TSL.ModuloThoeries.ASTdefines the AST type, and the transformative functions thereof.