Cooper (Calculemus)

Cooper Module

Namespace: Calculemus
Assembly: Calculemus.dll

Cooper's algorithm for Presburger arithmetic.

Functions and values

Function or value	Description
`adjustcoeff x l fm` Full Usage: `adjustcoeff x l fm` Parameters: x : `term` l : `BigInteger` fm : `formula<fol>` Returns: `formula<fol>`	x : `term` l : `BigInteger` fm : `formula<fol>` Returns: `formula<fol>`
`bset x fm` Full Usage: `bset x fm` Parameters: x : `term` fm : `formula<fol>` Returns: `term list`	x : `term` fm : `formula<fol>` Returns: `term list`
`cooper vars fm` Full Usage: `cooper vars fm` Parameters: vars : `string list` fm : `formula<fol>` Returns: `formula<fol>`	vars : `string list` fm : `formula<fol>` Returns: `formula<fol>`
`dest_numeral t` Full Usage: `dest_numeral t` Parameters: t : `term` Returns: `bigint`	t : `term` Returns: `bigint`
`divlcm x fm` Full Usage: `divlcm x fm` Parameters: x : `term` fm : `formula<fol>` Returns: `bigint`	x : `term` fm : `formula<fol>` Returns: `bigint`
`evalc` Full Usage: `evalc` Returns: `formula<fol> -> formula<fol>`	Returns: `formula<fol> -> formula<fol>`
`formlcm x fm` Full Usage: `formlcm x fm` Parameters: x : `term` fm : `formula<fol>` Returns: `bigint`	x : `term` fm : `formula<fol>` Returns: `bigint`
`gcd_num n1 n2` Full Usage: `gcd_num n1 n2` Parameters: n1 : `bigint` n2 : `bigint` Returns: `bigint`	n1 : `bigint` n2 : `bigint` Returns: `bigint`
`integer_qelim` Full Usage: `integer_qelim` Returns: `formula<fol> -> formula<fol>`	Returns: `formula<fol> -> formula<fol>`
`is_numeral` Full Usage: `is_numeral` Returns: `term -> bool`	Returns: `term -> bool`
`lcm_num n1 n2` Full Usage: `lcm_num n1 n2` Parameters: n1 : `bigint` n2 : `bigint` Returns: `BigInteger`	n1 : `bigint` n2 : `bigint` Returns: `BigInteger`
`linear_add vars tm1 tm2` Full Usage: `linear_add vars tm1 tm2` Parameters: vars : `string list` tm1 : `term` tm2 : `term` Returns: `term`	vars : `string list` tm1 : `term` tm2 : `term` Returns: `term`
`linear_cmul n tm` Full Usage: `linear_cmul n tm` Parameters: n : `bigint` tm : `term` Returns: `term`	n : `bigint` tm : `term` Returns: `term`
`linear_mul tm1 tm2` Full Usage: `linear_mul tm1 tm2` Parameters: tm1 : `term` tm2 : `term` Returns: `term`	tm1 : `term` tm2 : `term` Returns: `term`
`linear_neg tm` Full Usage: `linear_neg tm` Parameters: tm : `term` Returns: `term`	tm : `term` Returns: `term`
`linear_sub vars tm1 tm2` Full Usage: `linear_sub vars tm1 tm2` Parameters: vars : `string list` tm1 : `term` tm2 : `term` Returns: `term`	vars : `string list` tm1 : `term` tm2 : `term` Returns: `term`
`linform vars fm` Full Usage: `linform vars fm` Parameters: vars : `string list` fm : `formula<fol>` Returns: `formula<fol>`	vars : `string list` fm : `formula<fol>` Returns: `formula<fol>`
`linrep vars x t fm` Full Usage: `linrep vars x t fm` Parameters: vars : `string list` x : `term` t : `term` fm : `formula<fol>` Returns: `formula<fol>`	vars : `string list` x : `term` t : `term` fm : `formula<fol>` Returns: `formula<fol>`
`lint vars tm` Full Usage: `lint vars tm` Parameters: vars : `string list` tm : `term` Returns: `term`	vars : `string list` tm : `term` Returns: `term`
`minusinf x fm` Full Usage: `minusinf x fm` Parameters: x : `term` fm : `formula<fol>` Returns: `formula<fol>`	x : `term` fm : `formula<fol>` Returns: `formula<fol>`
`mk_numeral n` Full Usage: `mk_numeral n` Parameters: n : `bigint` Returns: `term`	n : `bigint` Returns: `term`
`mkatom vars p t` Full Usage: `mkatom vars p t` Parameters: vars : `string list` p : `string` t : `term` Returns: `formula<fol>`	vars : `string list` p : `string` t : `term` Returns: `formula<fol>`
`natural_qelim` Full Usage: `natural_qelim` Returns: `formula<fol> -> formula<fol>`	Returns: `formula<fol> -> formula<fol>`
`numeral1 fn n` Full Usage: `numeral1 fn n` Parameters: fn : `bigint -> bigint` n : `term` Returns: `term`	fn : `bigint -> bigint` n : `term` Returns: `term`
`numeral2 fn m n` Full Usage: `numeral2 fn m n` Parameters: fn : `bigint -> bigint -> bigint` m : `term` n : `term` Returns: `term`	fn : `bigint -> bigint -> bigint` m : `term` n : `term` Returns: `term`
`operations` Full Usage: `operations` Returns: `(string * (bigint -> bigint -> bool)) list`	Returns: `(string * (bigint -> bigint -> bool)) list`
`posineq fm` Full Usage: `posineq fm` Parameters: fm : `formula<fol>` Returns: `formula<fol>`	fm : `formula<fol>` Returns: `formula<fol>`
`relativize r fm` Full Usage: `relativize r fm` Parameters: r : `string -> formula<'a>` fm : `formula<'a>` Returns: `formula<'a>`	r : `string -> formula<'a>` fm : `formula<'a>` Returns: `formula<'a>`
`unitycoeff x fm` Full Usage: `unitycoeff x fm` Parameters: x : `term` fm : `formula<fol>` Returns: `formula<fol>`	x : `term` fm : `formula<fol>` Returns: `formula<fol>`
`zero` Full Usage: `zero` Returns: `term`	Returns: `term`