module CHC: sig .. end
Constrained Horn Clauses
type 'a solver
CHC solver
val mk_solver : ?context:SrkZ3.z3_context -> 'a Syntax.context -> 'a solver
val register_relation : 'a solver -> Syntax.symbol -> unit
Register a symbol as a relation in a system of constrained Horn clauses.
Each relation should be registered before calling check.
val add_rule : 'a solver -> 'a Syntax.formula -> 'a Syntax.formula -> unit
add_rule solver hypothesis conclusion adds the rule hypothesis =>
conclusion to solver.
val add : 'a solver -> 'a Syntax.formula list -> unit
add solver formulas asserts that each formula in formulas holds.
These formulas should not be CHCs.
val check : 'a solver -> 'a Syntax.formula list -> [ `Sat | `Unknown | `Unsat ]
val get_solution : 'a solver -> Syntax.symbol -> 'a Syntax.formula
val to_string : 'a solver -> string
val push : 'a solver -> unit
val pop : 'a solver -> unit