Module smt_horn 

Structs

HornClause 🔒

A flattened Horn clause extracted from the constraint tree.

SmtFormatter

Functions

flatten_constraint 🔒

Collect all Horn clauses from a constraint tree

fmt_assert 🔒

fmt_binop_smt 🔒

fmt_binrel_smt 🔒

fmt_const_decl 🔒

fmt_constant_smt 🔒

fmt_data_ctor_smt 🔒

fmt_data_decl_smt 🔒

fmt_expr_smt 🔒

fmt_fun_def 🔒

fmt_guard 🔒

fmt_guard_conjunction 🔒

fmt_kvar_as_fun 🔒

fmt_smt_horn

Format a task in the SMT-LIB HORN CHC format

fmt_sort_ctor_smt 🔒

fmt_sort_smt 🔒

fmt_thy_func_smt 🔒