Module Problem (.ml)


module Problem: sig .. end
a problem clause set

type symbol = Symbol.symbol 
type literal = Term.literal 
type clause = Term.clause 
type arities = (int * symbol list) list 
mapping from arity to symbols. when returned by a method of class Problem.problem sorted increasingly by arity.
class type problem = object .. end
a problem clause set
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
adds symbol to arities, that is to list of symbols with the same arity while keeping arities in increasing order.
val get_arity : arities -> int -> symbol list
returns all symbols of the given arity