Module Env

module Env: sig .. end

Entry point to "global" settings and datastructures.

Processing happens in the context of an env object. Usually a single env is used in a invocation of the system as standalone program. But of course also several envs could be used at the same time.

Associted with an env are

A Cfg.cfg representing configuration information.

A Term.symbol_table.

A Predicate.predicate_table. Via the predicate table, meta information about predicates, such as index declarations, as well as the extent of predicates (derived or input unit clauses) can be accessed.

A list of nonunit clauses, represented as terms.

Env provides some functions from Predicate, with a "symbolic" interface, i.e. instead of taking symbol objects as input, name and arity are used.

type env

val make_env : Cfg.cfg -> env

val get_cfg : env -> Cfg.cfg

val get_symbol_table : env -> Term.symbol_table

val get_predicate_table : env -> Predicate.predicate_table

val get_negative_units : env -> NegativeUnits.store

val get_rules : env -> Term.term list

val get_current_result : env -> Tableau.result

val set_current_result : env -> Tableau.result -> unit

val ensure_ready_to_assert : env -> Term.symbol -> Predicate.predicate

val ensure_ready_to_run : env -> Term.symbol -> Predicate.predicate

type statement_type =

`\|`	`Meta`
`\|`	`Unit`
`\|`	`Rule`
`\|`	`Disjunction`
`\|`	`False`

val classify_statement_functor : env -> Term.symbol -> statement_type

val lookup_predicate : env -> string -> int -> Predicate.predicate

Raises Not_found if the predicate does not exist.

val find_predicate : env -> string -> int -> Predicate.predicate

Ensures that the predicate exists.

val add_rule : env -> Term.term -> unit

val add_disjunction : env -> Term.term -> unit

val add_false : env -> unit

val abolish_predicate : env -> string -> int -> unit

Abolishes the specified predicate, if it exists. This means that all its unit clauses (input or derived) and declarations are removed. It has no effect on any nonunit input clauses.

val clear_rules : env -> unit

Effect that all input nonunit clauses are removed.

val begin_shared_input : env -> unit

Enable sharing of subsequent input terms. Input terms are only shared within dynamic begin_shared_input/end_shared_input contexts. The behavior for nested begin_shared_input/end_shared_input contexts is undefined.

val end_shared_input : env -> unit

Disable sharing of subsequent input terms and free resources used for sharing.

val unit_for_env : env -> Term.term -> Term.term

Returns a possibly optimized variant of the input term (a unit clause), e.g. by using subterms that are shared with other clauses.