Module Problem (.ml)

module Problem: sig .. end

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