Module Read_darwin (.ml)

module Read_darwin: sig .. end

This input format was mainly implemented for quick testing and debugging. Every formula is seen as a clause. White space between tokens is ignored.

All functions
Raises Const.PARSE_ERROR on incorrect input.

• Variable: starts with an upper case letter, e.g. X
• Universal Variable: may be prefixed with a _, e.g. _X if prefixed a number is also a valid name, e.g. _0
• Parametric Variable: must be prefixed with a =, e.g. =U if prefixed a number is also a valid name, e.g. =0
• Symbols: starts with a lower case letter or a number, e.g. a, barrel, 0
• Term: uses (, ) to enclose its arguments, e.g. p(X, a)
• Literal: like a term, prefix - for a negative literal, prefix + or nothing for a positive literal, e.g. -p(X, a)
• Clause: e.g. { p(X), -p(a) }
• Clauses: e.g. { p(X) } { -p(a) }

type var = Var.var 

type term = Term.term 

type literal = Term.literal 

type clause = Term.clause 

val to_var : string -> var

val to_term : string -> term

val to_literal : string -> literal

val to_clause : string -> clause

val to_clauses : string -> clause list

val to_clauses_from_string : string -> clause list

val to_clauses_from_file : string -> clause list