Previous  Up  Next

Module Structure

module Structure: sig .. end
Representing relational structures with real-valued functions.

Modules used in structure representation.


module IntMap: Map.S  with type key = int
Maps from int to 'alpha 
module StringMap: Map.S  with type key = string
Maps from string to 'alpha 
module Elems: Set.S  with type elt = int
Sets of integers 
val add_elems : int list -> Elems.t -> Elems.t
val elems_of_list : int list -> Elems.t
module Tuples: Set.S  with type elt = int array
Sets of tuples of ints 
val add_tuples : int array list -> Tuples.t -> Tuples.t
val tuples_of_list : int array list -> Tuples.t

Structure type and basic getters.


type structure
Elements are internally represented by integers, bu the structure also stores a naming of elements. No element is named by a decimal numeral other than its number to prevent misunderstandings. Elements not appearing in names are assumed to be named by their decimal numeral.
val compare_elems : int -> int -> int
Comparison function for elements.

Comparison function for structures.

val compare : structure -> structure -> int
Equality check on structures.
val equal : structure -> structure -> bool
val elements : structure -> int list
Return the list of elements in a structure.
val elems : structure -> Elems.t
Return the set of elements in a structure.
val constants : structure -> (string * int) list
Return the assignment of constants in the structure.
val nbr_elems : structure -> int
Number of elements in a structure.
val relations : structure -> Tuples.t StringMap.t
Relations in the structure.
val functions : structure -> float IntMap.t StringMap.t
Functions in the structure.

Elements and their names.


val elem_nbr : structure -> string -> int
The integer corresponding to a given element name.
val elem_name : structure -> int -> string
The element name of an element (given by integers)
val names : structure -> int StringMap.t
The map containing element names.
val inv_names : structure -> string IntMap.t
The inverse map of element names.
val replace_names : structure ->
       int StringMap.t -> string IntMap.t -> structure
Replace the names of elements by new maps.

Basic helper functions


val rel_size : structure -> string -> int
Size of a relation, i.e. number of tuples in it.
val rev_string_to_int_map : int StringMap.t -> string IntMap.t
Reverse a map: make a string IntMap from an int StringMap.
val rev_int_to_string_map : string IntMap.t -> int StringMap.t
Reverse a map: make an int StringMap from a string IntMap.
val empty_structure : unit -> structure
Return the empty structure (with empty signature).
val default_circle_structure : unit -> structure
Return the default structure for the circle shape.
val empty_with_signat : (string * int) list -> structure
Return the empty structure with given relational signature.
val incident : structure -> int -> (string * int array list) list
Return the list of relation tuples incident to an element e in struc.
val check_rel : structure -> string -> int array -> bool
Check if a relation holds for a tuple.
val rel_graph : string -> structure -> Tuples.t
Graph of a relation in a model, returns an empty set if the relation is not in the signature.
val rel_incidence : string -> structure -> Tuples.t array
Incidences of a relation in a model, returns an empty set if the relation is not in the signature.
val fun_val : structure -> string -> int -> float
Return the value of function f on e in struc.
val elems_with_val : structure -> string -> float -> int list
Return the elements on which function f has value x in struc.
val model_val : structure -> string -> int -> structure
Return the model assigned by f to e in struc.
val add_models : structure ->
       string -> (int * structure) list -> structure
Assign models to elements by f in struc, replacing previous.
val f_signature : structure -> string list
Return the list of functions.
val rel_signature : structure -> (string * int) list
Return the list of relations with their arities.
val rel_sizes : structure -> (string * int) list
Cardinality of graphs of all relations in the structure.

Printing structures


val elem_str : structure -> int -> string
Print the elements e as string.
val rel_str : ?print_arity:bool ->
       structure -> string -> Tuples.t -> string
Print the relation named rel_name with tuples ts as string. Unless print_arity is false, print the arity if ts is empty.
val ext_str : ?show_empty:bool -> structure -> string
Print the structure struc as string, in extensive form (not using condensed representations like boards). If show_empty is false, do not print the signatures of empty relations.
val str : ?show_empty:bool -> ?show_models:bool -> structure -> string
Print the structure struc as string.
val fprint_rel : ?print_arity:bool ->
       structure ->
       Format.formatter -> string * Tuples.t -> unit
Print the relation with tuples ts. Unless print_arity is false, print the arity if ts is empty.
val fprint_fun : structure ->
       Format.formatter -> string * float IntMap.t -> unit
val fprint_ext_structure : show_empty:bool -> Format.formatter -> structure -> unit
val fprint : show_empty:bool -> Format.formatter -> structure -> unit
val print : ?show_empty:bool -> structure -> unit
val sprint : ?show_empty:bool -> structure -> string
val board_elem_coords : string -> int * int
Coordinates, column first, of a board element name. Raises Not_found if the name is not of proper format.
val board_coords_name : int * int -> string
Board element name under given coordinates, column first. Raises Not_found if the coordinates are out of bounds.
val compare_diff : ?cmp_funs:(float -> float -> bool) ->
       structure -> structure -> bool * string
Compare two structures and explain the first difference met.
val diff_elems : structure -> structure -> (int * string list) list
Elements from s1 which differ in s2, with differing relation names.

Adding elements possibly with string names


val add_constant : structure -> string -> int -> structure
Add a new constant. Does not check for doubles.
exception Structure_mismatch of string
Nonexisting elements or relations, signature mismatch, etc.
val add_elem : structure -> ?name:string -> int -> structure
Add element e to struc if it is not yet there. Return new structure.
val add_new_elem : structure -> ?name:string -> unit -> structure * int
Add new element to struc, return the updated structure and the element.
val find_elem : structure -> string -> int
val find_or_new_elem : structure -> string -> structure * int
Find an element in the structure, and if not present, add new one.

Adding relation tuples possibly with named elements


val add_rel_name : string -> int -> structure -> structure
Ensure relation named rn exists in struc, add if needed.
val add_rel : structure -> string -> int array -> structure
Add tuple tp to relation rn in structure struc.
val add_rel_named_elems : structure -> string -> string array -> structure
Add tuple tp to relation rn in structure struc.
val unsafe_add_rel : structure -> string -> int array -> structure
Add tuple tp to relation rn in structure struc without checking whether it and its elements already exist in the structure and without checking arity.
val add_rels : structure -> string -> int array list -> structure
Add tuples tps to relation rn in structure struc.
val unsafe_add_rels : structure -> string -> int array list -> structure
Add tuples tps to relation rn in structure struc without checking for elements existence and arity matching.
val free_for_rel : string -> int -> structure
Return a structure with a single relation of given arity, over a single tuple, of different elements.

Adding function assignments possibly to named elements


val add_fun : structure -> string -> int * float -> structure
Add function assignment e -> x to function fn in structure struc.
val add_funs : structure -> string -> (int * float) list -> structure
Add function assignments assgns to fn in structure struc.
val change_fun : structure -> string -> string -> float -> structure
Change function fn assignment for element e to x in struc.
val change_fun_int : structure -> string -> int -> float -> structure

Global function to create structures from lists


val create_from_lists : ?struc:structure ->
       string list ->
       (string * int option * string array list, string * string) Aux.choice list ->
       (string * (string * float) list) list -> structure
val create_from_lists_position : ?struc:structure ->
       string list ->
       (string * int option * string array list, string * string) Aux.choice list ->
       structure
val create_from_lists_range : float ->
       ?struc:structure ->
       string list ->
       (string * int option * string array list, string * string) Aux.choice list ->
       structure

Removing relation tuples and elements from a structure


val del_rel : structure -> string -> int array -> structure
Remove the tuple tp from relation rn in structure struc.
val del_rels : structure -> string -> int array list -> structure
Remove the tuples tps from relation rn in structure struc.
val clear_rels : ?remove_from_sig:bool ->
       structure -> (string -> bool) -> structure
Remove all relations matching the predicate. By default, also remove them from the signature.
val clear_fun : structure -> string -> structure
Remove the given function from struc.
val clear_names : structure -> structure
Remove element names from structure.
val del_elem : structure -> int -> structure
Remove the element e and all incident relation tuples from struc.
val del_elems : structure ->
       int list -> structure * (string * int array list) list
Remove elements es and all incident relation tuples from struc. Return the resulting structure and deleted relation tuples.
val gc_elems : ?ignore_funs:bool -> structure -> structure
Remove the elements that are not incident to any relation (and have no defined properties, unless ignore_funs is given).
val diffrels_struc : structure -> structure -> string list option
Differing relations (used in solver cache)

Creating a structure from a TRS string


val trs_set_struc : structure -> string * Term.term * Term.term -> structure
Apply TRS values to a structure.
val struc_from_trs : string -> string * structure
Parse the TRS string, output messages and the resulting structure.

Parser Helpers


exception Board_parse_error of string
val parse_board : ?row_col_rels:string * string ->
       ?pos_initial:float * float ->
       ?pos_increment:float * float ->
       ?struc:structure -> string -> structure
Parse a rectangular board as a model, using "R" for rows, "C" for columns, and the letter at a position for a unary predicate. Line breaks '\n' are used for separating rows, spaces ' ' can be used for formatting, dot '.' is used for blank fields.