Module Var
module Var: sig end
Abstract datatype for variables.
Author(s): Harald Ruess
The set of all variables is partitioned into
external and internal variables.
External variables consist of a name and a domain construction.
Internal variables are generated by the system, and we distinguish
between different kinds of internal variables
- rename variables for abstracting terms.
- slack variables generated by the linear arithmetic module
for expressing nonnegativity and zero constraints.
There is a name of type Name.t associated with each variable. Names for
rename and fresh variables are always of the form "x!i", where x is an
arbitrary string and i is an integer string. The name associated
with a free variable is of the form "!i" for an integer i.
module Cnstrnt: sig end
Variable constraints.
type t
Representation type for variables.
val name_of : t -> Name.t
name_of x returns the name associated with a variable x.
val cnstrnt_of : t -> Cnstrnt.t
cnstrnt_of x returns the domain constraint of variable x.
Raises Not_found is interpretation for the variable is unconstrained.
val dom_of : t -> Dom.t
dom_of x returns the domain of interpretation of variable x,
and raises Not_found if this domain is "unrestricted".
val width_of : t -> int
width_of x returns the length n of variable x
with a bitvector interpretation, and raises Not_found otherwise.
val cmp : t -> t -> int
cmp x y realizes a total ordering on variables. The result is 0
if eq x y holds, it is less than 0 we say, 'x is less than y',
and, otherwise, 'x is greater than y'. An slack variable x is always
less than a rename variable y. Otherwise, the outcome of cmp x y is
unspecified.
val (<<<) : t -> t -> bool
x <<< y holds iff cmp x y <= 0.
val mk_external : Name.t -> Cnstrnt.t -> t
mk_external n d creates an external variable with associated name n
and optional domain constraint d.
val mk_const : Th.t -> int -> Cnstrnt.t -> t
val mk_rename : Name.t -> int -> Cnstrnt.t -> t
mk_rename n d constructs a rename variable with associated
name "n!i" and optional domain constraint.
type slack =
val nonneg : Dom.t -> slack
nonneg d constructs Nonneg(d).
val mk_slack : int -> slack -> t
-
mk_slack i Zero creates a
zero slack variable with
0
as the only possible interpretation.
mk_slack i Nonneg(d) creates a nonnegative slack variable
the possible interpretations in the subset {q in D | q >= 0}
of the reals, where D the interpretation set of d according
to Dom.t.
val mk_fresh : Th.t -> int -> Cnstrnt.t -> t
mk_fresh th i d creates a fresh variable associated with
theory i and optional domain d. These variables are typically
generated by theory-specific solvers.
val is_var : t -> bool
is_var x holds iff x is an external variable, that is,
it has been returned by a call to mk_external.
val is_rename : t -> bool
is_rename x holds iff x is a rename variable.
val is_slack : slack -> t -> bool
is_cnstrnt x holds iff x is a slack variable.
val is_zero_slack : t -> bool
is_zero_slack x holds iff x is a zero slack variable.
val is_nonneg_slack : t -> bool
is_zero_slack x holds iff x is a nonnegative slack variable.
val is_const : t -> bool
val is_fresh : Th.t -> t -> bool
is_fresh i x holds iff x is a fresh variable of theory i.
val is_some_fresh : t -> bool
val is_internal : t -> bool
is_internal x holds iff either is_rename x, is_slack x, or
is_fresh x holds.
Interpretation domains
val is_real : t -> bool
is_real x holds iff x is constraint over the reals.
val is_int : t -> bool
is_int x holds iff x is constraint over the integers.
val d_external : t -> Name.t * Cnstrnt.t
val pretty : bool Pervasives.ref
val pp : t Pretty.printer
Pretty-printer for variables. If
Var.pretty is set to true, then
printing of domain restrictions is suppressed.
| Parameters: |
|
fmt |
: |
Format.formatter
|
|
x |
: |
t
|
|