(* an universe that does nothing: i.e. no constraints are kept, no merges.. *)
val oblivion_ugraph: universe_graph
+(* one of the previous two, no set to empty_ugraph *)
+val default_ugraph: universe_graph
+
+
(*
These are the real functions to add eq/ge/gt constraints
to the passed graph, returning an updated graph or raising
UniverseInconsistency
*)
val add_eq:
- ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
+ universe -> universe -> universe_graph -> universe_graph
val add_ge:
- ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
+ universe -> universe -> universe_graph -> universe_graph
val add_gt:
- ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
+ universe -> universe -> universe_graph -> universe_graph
-val do_rank: universe_graph -> unit
+val do_rank: universe_graph -> int list * universe list
val get_rank: universe -> int
(*
returns the universe number (used to save it do xml)
*)
val univno: universe -> int
+val univuri: universe -> UriManager.uri
(** re-hash-cons URIs contained in the given universe so that phisicaly
* equality could be enforced. Mainly used by
val compare: universe -> universe -> int
val eq: universe -> universe -> bool
-(*
- Benchmarking stuff
-*)
-val get_spent_time: unit -> float
-val reset_spent_time: unit -> unit
-
val is_anon: universe -> bool