Module smt_horn 

Structs

HornClause 🔒

A flattened Horn clause extracted from the constraint tree.

SmtFormatter

Functions

flatten_constraint 🔒

fmt_smt_horn

Format a task in the SMT-LIB HORN CHC format.

write_assert 🔒

write_guard_conjunction 🔒

write_kvar_decl 🔒

write_smt_horn 🔒