module CoordinateSystem: sig
.. end
A coordinate system is a bijection between a set of coordinates and a set
of terms.
type 'a
t
Coordinate system
type
cs_term = [ `App of Syntax.symbol * Linear.QQVector.t list
| `Floor of Linear.QQVector.t
| `Inv of Linear.QQVector.t
| `Mod of Linear.QQVector.t * Linear.QQVector.t
| `Mul of Linear.QQVector.t * Linear.QQVector.t ]
A cs_term is a term associated with a coordinate, which is defined in
terms of lower coordinates.
val pp : Format.formatter -> 'a t -> unit
val pp_vector : 'a t -> Format.formatter -> Linear.QQVector.t -> unit
val pp_cs_term : 'a t -> Format.formatter -> cs_term -> unit
val mk_empty : 'a Syntax.context -> 'a t
val get_context : 'a t -> 'a Syntax.context
val copy : 'a t -> 'a t
val admit_term : 'a t -> 'a Syntax.term -> unit
Extend a coordinate system to admit a term
val admit_cs_term : 'a t -> cs_term -> unit
Extend a coordinate system with one additional coordinate term, if that
coordinate does not already belong to the system.
val const_id : int
Virtual coordinate associated with 1
val dim : 'a t -> int
Number of dimensions in the coordinate system
val int_dim : 'a t -> int
Number of integer dimensions in the coordinate system
val real_dim : 'a t -> int
Number of real dimensions in the coordinate system
val destruct_coordinate : 'a t -> int -> cs_term
val term_of_coordinate : 'a t -> int -> 'a Syntax.term
Find the term associated with a coordinate
val term_of_vec : 'a t -> Linear.QQVector.t -> 'a Syntax.term
val cs_term_id : ?admit:bool -> 'a t -> cs_term -> int
Find the coordinate associated with an coordinate term. If the coordinate
term is does not belong to the coorindate system and admit
is set then
extend the coordinate system; otherwise, raise Not_found
.
val vec_of_term : ?admit:bool -> 'a t -> 'a Syntax.term -> Linear.QQVector.t
Find the vector associated with an admissible term. If the term is
inadmissible and admit
is set then extend the coordinate system; otherwise,
raise Not_found
.
val type_of_id : 'a t -> int -> [ `TyInt | `TyReal ]
val polynomial_of_term : 'a t -> 'a Syntax.term -> Polynomial.Mvp.t
Find a polynomial associated with an admissible term over
*non-multiplicative* cooridnate.
val polynomial_of_vec : 'a t -> Linear.QQVector.t -> Polynomial.Mvp.t
Convert a vector to a polynomial *without multiplicative coordinates*.
Multiplicative coordinates are expanded into higher-degree polynomials
over non-multiplicative coordinates.
val polynomial_of_coordinate : 'a t -> int -> Polynomial.Mvp.t
val term_of_polynomial : 'a t -> Polynomial.Mvp.t -> 'a Syntax.term
val admits : 'a t -> 'a Syntax.term -> bool
Does a coordinate system admit the given term?
val project_ideal : 'a t ->
Polynomial.Mvp.t list ->
?subterm:(Syntax.symbol -> bool) ->
(Syntax.symbol -> bool) -> (int * 'a Syntax.term * 'a Syntax.formula) list
val subcoordinates : 'a t -> int -> SrkUtil.Int.Set.t
Find the set of all coordinates that are associated with subterms of the
term associated with a given coordinate.
val direct_subcoordinates : 'a t -> int -> SrkUtil.Int.Set.t
Find the set of all coordinates that are associated with *direct* subterms
of the term associated with a given coordinate.