module Problem:a problem clause setsig
..end
typesymbol =
Symbol.symbol
typeliteral =
Term.literal
typeclause =
Term.clause
typearities =
(int * symbol list) list
Problem.problem
sorted increasingly by arity.class type problem =object
..end
val create : ?equality:bool ->
?horn:bool -> clause list -> literal list -> problem
create equality bool clauses initial_interpretation
creates an instance of class type problem.
equality
is false and horn
is true by default,
but if set otherwise this will override clauses
.
This is for the finite model mode,
as the transformation might have removed the equality axioms,
and as non-Horn axioms are added later on.
val update_arities : arities -> symbol -> arities
val get_arity : arities -> int -> symbol list