Previous  Up  Next

Module Context (.ml)


module Context: sig .. end
context with operations

Internally applies the Compact rule of the model evolution calculus.

As only order preserving (chronological, backjumping) backtracking is used, the context can be seen as a stack of literals, backtracking always removes the last elements that were added.

Each context literal has its unique non-negative id, which is strictly increasing within the literal stack, i.e. the oldest context literal has the lowest id, and the most recent added context literal has the highest id.


Types

type config = Config.config 
type statistic = Statistic.statistic 
type counter = Counter.counter 
type var = Var.var 
type symbol = Symbol.symbol 
type term = Term.term 
type literal = Term.literal 
type clause = Term.clause 
type choice_point = State.choice_point 
type state = State.state 
type problem = Problem.problem 
type bound = Bound.bound 
type finite_domain = Finite_domain.finite_domain

type element = private {
   el_id : int; (*unique id per context literal.*)
   el_literal : literal; (*the context literal.*)
   el_choice_point : choice_point; (*the choice point in which the context literal was added.*)
   el_pars : var list; (*the parameters of the context literal.*)
   el_generation : int; (*depth of the tree of context literals needed to compute this context literal.*)
   el_is_fd_incomplete : bool; (*Config.finite_domain mode is active, and iff true then this context literal depends on the totality axioms. That is, a refutation depends on the domain size, and is not a refutation of the original problem.*)
   mutable el_compacted : int; (*compacted by the context literal with the given id, or none if id = -1*)
}
a context literal with some information
type context

Functions


Initialization


val create : config -> statistic -> state -> context
creates the context and fixes the indexing method based.
val from_file : string ->
       config -> statistic -> state -> context
from_file file_name creates a context from a file. The file should contain one literal per line, readable by Read_tme.
Raises

Constants


val null_element : element
for initialization usage, invalid choice point.
val assert_element : element
pseudo assert literal for use as the assert gap in a context unifier, contains Term.assert_literal, always valid choice point.
val plus_v_element : element
pseudo plus_v literal for use in a context unifier, contains Term.plus_v, always valid choice point.
val minus_v_element : element
pseudo minus_v literal for use in a context unifier, contains Term.minus_v, always valid choice point.

Access


val add : context -> literal -> int -> bool -> element
add context literal generation is_fd_incomplete adds a new literal to the context, for generation see Context.element.
val is_universal : context -> bool
does the context contain only universal (i.e. no parametric) literals?
val element_equal : element -> element -> bool
the same element?
val element_for_literal : context -> literal -> element option
returns the element for a literal, if the literal is in the context.
val most_recent_element : context -> element
returns the most recently added context literal.
Raises Not_found if the context is empty.
val is_more_recent : element -> element -> bool
returns true if the first element has been added later to the context.

Iteration


val iter : (element -> unit) -> context -> unit
val fold : ('a -> element -> 'a) -> 'a -> context -> 'a

Checks


val check_contradictory : context -> literal -> element option
check_contradictory context literal checks if literal is contradictory with the context. Returns a contradictory context element, if one exists.
val check_subsumed : context -> literal -> element option
check_subsumed context literal checks if literal is (p-preservingly) subsumed by the context. Returns a subsuming context element, if one exists.
val check_productive : context ->
       literal -> literal -> element option
check_productive context producer produced checks if producer is producing the negation of produced in the context (that is producer is the context literal and produced the remainder literal of the context unifier to check). Returns a shielding context element, if one exists.
val is_true : context -> literal -> bool
is the literal true in the current context?
val find_all_unifiable : context -> literal -> element list
find_all_unifiable context literal returns all (also compacted) context elements that unify with literal
val find_all_subsuming : context -> literal -> element list
find_all_subsuming context literal returns all (also compacted) context elements that (p-preservingly) subsume literal

Representation


val element_to_string : element -> string
val print_context : context -> Pervasives.out_channel -> unit
prints the (not compacted) context literals, one literal per line.
val print_DIG : context -> Pervasives.out_channel -> problem -> unit
print_DIG context out problem prints the context in the DIG model representation, i.e. as a disjunction of implicit generalizations. an implicit generalization is an atom paired with a set of exception atoms, A \ {B_0, ..., B_n} , with the semantics that all ground instances of A except for all ground instances of any B_i are true in the described model.

problem must contain the input problem.

does only print non-compacted literals defined over the input signature, like Context.print_context show_model.

val print_tptp_model : context ->
       Pervasives.out_channel ->
       problem -> finite_domain option -> bound -> unit
print the model represented by the context.

in finite domain mode the finite domain must be given, and the bound is needed to get the current domain size.

val print_multiplication_tables : context ->
       Pervasives.out_channel -> problem -> bound -> unit
print the multiplication tables of a finite domain model.

if tptp is true, then the TPTP format is used, otherwise a more concise and easier human-readable notation.

val print_max_size : context -> unit
string representation of the maximimal context size during the derivation (ala Print.print_label).

Backtracking


val backtrack : context -> unit
removes context elements added in invalid choice points, and undoes the corresponding compacting of the context.

DEPENDENCY: State_backtrack must have been executed before.