Class type Problem.problem

class type problem = object .. end

a problem clause set

Clauses

method addClauses : clause list -> unit

adds clauses (preserving their order) to front of current clauses

method addClause : clause -> unit

method addToInitialInterpretation : literal list -> unit

adds literals (preserving their order) to the initial interpretation.

method getClauses : clause list

returns the clause set.

method getInitialInterpretation : literal list

returns the initial interpretation. this should be used to initialize the context.

method getPredicateSymbols : symbol list

returns the predicate symbols contained in the clause set (except for Symbol.equality).

method getFunctionSymbols : symbol list

returns the function symbols contained in the clause set

method getConstantSymbols : symbol list

returns the constant symbols contained in the clause set

method getPredicateArities : arities

returns the predicate symbols (except for Symbol.equality) grouped by arity. ordered by increasing arity.

method getFunctionArities : arities

returns the function symbols grouped by arity. ordered by increasing arity.

method getMaxClauseLength : int

returns the length of the longest clause.

method containsEquality : bool

does the clause set contain Symbol.equality?

method isHorn : bool

is the clause set Horn?

method isBS : bool

is the clause set free of function symbols (Bernays-Schoenfinkle) ?