module P : Polynome.EXTENDED_Polynome with type r = X.rtype t = P.tType of terms of the theory
type r = X.rType of representants of terms of the theory
val timer : Timers.ty_moduleval is_mine_symb : Symbols.t -> boolReturn true if the symbol is owned by the theory.
val is_constant : t -> boolDetermines whether the semantic value is a constant value. is_constant t is equivalent to leaves t == [] (except for the special cases below), but is more efficient.
In addition, some terms (e.g. true, false, void) that have no associated theories are considered as constant by this function.
Semantic value for which is_constant returns true contains no free names and thus have the same concrete value in all contexts.
Note that for some theories (e.g. records, arrays) the constant may not be pure: it may involve nested (constant) terms of other theories.
val hash : t -> intsolve r1 r2, solve the equality r1=r2 and return the substitution
val solve : r -> r -> r Sig.solve_pb -> r Sig.solve_pbval print : Stdlib.Format.formatter -> t -> unitval fully_interpreted : Symbols.t -> boolreturn true if the symbol is fully interpreted by the theory, i.e. it is fully embedded into semantic values and does not need term-level congruence
assign_value r distincts eq selects the value to assign to r in the model as a term t, and returns Some (t, is_cs). is_cs is described below.
If no appropriate value can be chosen here, return None (only do this if either r is already a value, or there is a mechanism somewhere else in the code, such as the case_split function of a relation module, that ensures completeness of the generated model).
r is the current class representative that a value should be chosen for. No assumptions should be made on the shape of r, but do return None if it is already a value.
distincts is a list of term representatives that the returned value must be distinct from (choosing a value that is present in distincts will cause the solver to loop infinitely).
eq is a list of pairs (t, r) of terms and their initial representative (i.e., r is fst (X.make t) for each pair) that encode the equivalence class of r.
The returned bool serves a similar purpose as the is_cs flag in Th_util.case_split.
It should usually be true, which indicates that the returned term is not forced.
Use false only when the returned term contains aliens that should be assigned (e.g. records).
**When returning false, you must ensure that the equality between the first argument and the return value always hold (i.e. is a *unit* fact). In particular, the equality *must not* depend on distincts -- doing so would be unsound.**
In other words, if assign_value r distincts eq returns Some (t, false), then there must be no context in which solve r (fst X.make t) raises Unsolvable. You have been warned!
to_model_term r creates a model term if r is constant. The function cannot fail if r is a constant (that is statisfied the predicate X.is_constant).
The returned value always satisfies the predicate Expr.is_model_term. See its documentation for more details about model terms.