Module CoordinateSystem

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.