Previous  Up  Next

Module Arith


module Arith: sig  end

Symbols



Symbols 


val num : Mpa.Q.t -> Sym.t
Parameters:
q : Mpa.Q.t
 
val multq : Mpa.Q.t -> Sym.t
Parameters:
q : Mpa.Q.t
 
val add : Sym.t


Theory-specific recognizers 


val is_interp : Term.t -> bool
Parameters:
a : Term.t


Destructors 


val d_num : Term.t -> Mpa.Q.t option
Parameters:
?? : Term.t
 
val d_multq : Term.t -> (Mpa.Q.t * Term.t) option
Parameters:
?? : Term.t
 
val d_add : Term.t -> Term.t list option
Parameters:
?? : Term.t
 
val monomials : Term.t -> Term.t list
Parameters:
?? : Term.t


Recognizers 


val is_num : Term.t -> bool
Parameters:
?? : Term.t
 
val is_zero : Term.t -> bool
Parameters:
?? : Term.t
 
val is_one : Term.t -> bool
Parameters:
?? : Term.t
 
val is_q : Mpa.Q.t -> Term.t -> bool
Parameters:
q : Mpa.Q.t
?? : Term.t
 
val is_multq : Term.t -> bool
Parameters:
?? : Term.t
 
val is_diophantine : Term.t -> bool
Parameters:
?? : Term.t


Constants 


val mk_num : Mpa.Q.t -> Term.t
val mk_zero : Term.Map.key
val mk_one : Term.t
val mk_two : Term.t


Normalizations 


val poly_of : Term.t -> Mpa.Q.t * Term.t list
val of_poly : Mpa.Q.t -> Term.Map.key list -> Term.Map.key
Parameters:
q : Mpa.Q.t
l : Term.Map.key list
 
val mono_of : Term.t -> Mpa.Q.t * Term.t
Parameters:
?? : Term.t
 
val of_mono : Mpa.Q.t -> Term.Map.key -> Term.Map.key
Parameters:
q : Mpa.Q.t
x : Term.Map.key
 
val fold : (Mpa.Q.t -> Term.t -> 'a -> 'a) -> Term.t -> 'a -> 'a
Parameters:
f : Mpa.Q.t -> Term.t -> 'a -> 'a
a : Term.t
e : 'a


Constructors 


val mk_multq : Mpa.Q.t -> Term.Map.key -> Term.Map.key
Parameters:
q : Mpa.Q.t
a : Term.Map.key
 
val mk_addq : Mpa.Q.t -> Term.t -> Term.t
Parameters:
q : Mpa.Q.t
a : Term.t
 
val mk_add : Term.Map.key -> Term.Map.key -> Term.Map.key
Parameters:
a : Term.Map.key
b : Term.Map.key
 
val mk_addl : Term.Map.key list -> Term.Map.key
Parameters:
l : Term.Map.key list
 
val mk_incr : Term.t -> Term.Map.key
Parameters:
a : Term.t
 
val mk_neg : Term.Map.key -> Term.Map.key
Parameters:
a : Term.Map.key
 
val mk_sub : Term.Map.key -> Term.Map.key -> Term.Map.key
Parameters:
a : Term.Map.key
b : Term.Map.key
 
val map : (Term.Map.key -> Term.Map.key) -> Term.Map.key -> Term.Map.key
Mapping a term transformer f over a.
Parameters:
f : Term.Map.key -> Term.Map.key
a : Term.Map.key
 
val replace : Term.Map.key -> Term.t -> Term.Map.key -> Term.Map.key
Replacing a variable with a term.
Parameters:
a : Term.Map.key
x : Term.t
e : Term.Map.key
 
val apply : Term.Map.key -> Term.Map.key Term.Map.t -> Term.Map.key
Application of a substitution.
Parameters:
a : Term.Map.key
m : Term.Map.key Term.Map.t
 
val sigma : Sym.arith -> Term.Map.key list -> Term.Map.key
Interface for sigmatizing arithmetic terms.
Parameters:
op : Sym.arith
l : Term.Map.key list
 
val tau : Term.t -> Dom.t
Domain interpretation.
Parameters:
?? : Term.t
 
val qsolve : Term.Map.key * Term.Map.key -> (Term.Map.key * Term.Map.key) option
Parameters:
(a,b) : Term.Map.key * Term.Map.key


Integer solver 


val mk_fresh : unit -> Term.Map.key
module Euclid: sig  end
val zsolve : Term.Map.key * Term.Map.key -> (Term.t * Term.Map.key) list
Parameters:
(a,b) : Term.Map.key * Term.Map.key
 
val vectorize : Term.t list -> Euclid.t list * Term.t list
Parameters:
ml : Term.t list
 
val general : Euclid.t list ->
       Euclid.t * Euclid.t list -> Term.Map.key list * Term.Map.key list
Compute the general solution of a linear Diophantine equation with coefficients al, the gcd d of al and a particular solution pl. In the case of four coeffients, compute, for example, (p0 p1 p2 p3) + k0/d * (a1 -a0 0 0) + k1/d * (0 a2 -a1 0) + k2/d * (0 0 a3 -a2) Here, k0, k1, and k2 are fresh variables. Note that any basis of the vector space of solutions xl of the equation al * xl = 0 would be appropriate.
Parameters:
al : Euclid.t list
(d,pl) : Euclid.t * Euclid.t list
 
val integer_solve : bool Pervasives.ref
val solve : Fact.equal -> Fact.equal list
Parameters:
e : Fact.equal
 
val isolate : Term.t -> Term.Map.key * Term.Map.key -> Term.Map.key
Isolate y in a solved equality x = a.
Parameters:
y : Term.t
(x,a) : Term.Map.key * Term.Map.key