sig
type symbol = Symbol.symbol
type literal = Term.literal
type clause = Term.clause
type arities = (int * Problem.symbol list) list
class type problem =
object
method addClause : Problem.clause -> unit
method addClauses : Problem.clause list -> unit
method addToInitialInterpretation : Problem.literal list -> unit
method containsEquality : bool
method getClauses : Problem.clause list
method getConstantSymbols : Problem.symbol list
method getFunctionArities : Problem.arities
method getFunctionSymbols : Problem.symbol list
method getInitialInterpretation : Problem.literal list
method getMaxClauseLength : int
method getPredicateArities : Problem.arities
method getPredicateSymbols : Problem.symbol list
method isBS : bool
method isHorn : bool
end
val create :
?equality:bool ->
?horn:bool ->
Problem.clause list -> Problem.literal list -> Problem.problem
val update_arities : Problem.arities -> Problem.symbol -> Problem.arities
val get_arity : Problem.arities -> int -> Problem.symbol list
end