Module Bitv.Shostak

Parameters

module X : ALIEN

Signature

type t = X.r abstract

Type of terms of the theory

type r = X.r

Type of representants of terms of the theory

val name : string

Name of the theory

val timer : Timers.ty_module
val is_mine_symb : Symbols.t -> bool

Return true if the symbol is owned by the theory.

val make : Expr.t -> r * Expr.t list

Give a representant of a term of the theory

val term_extract : r -> Expr.t option * bool
val color : r Sig.ac -> r
val type_info : t -> Ty.t
val embed : r -> t
val is_mine : t -> r
val leaves : t -> r list

Give the leaves of a term of the theory

val is_constant : t -> bool

Determines 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 subst : r -> r -> t -> r
val compare : r -> r -> int
val equal : t -> t -> bool
val hash : t -> int

solve r1 r2, solve the equality r1=r2 and return the substitution

val solve : r -> r -> r Sig.solve_pb -> r Sig.solve_pb
val print : Stdlib.Format.formatter -> t -> unit
val fully_interpreted : Symbols.t -> bool

return 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

val abstract_selectors : t -> (r * r) list -> r * (r * r) list
val assign_value : r -> r list -> (Expr.t * r) list -> (Expr.t * bool) option

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!

val to_model_term : r -> Expr.t option

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.