Complex (Calculemus)

Complex Module

Namespace: Calculemus
Assembly: Calculemus.dll

Complex quantifier elimination.

Types

Type	Description
sign

Functions and values

Function or value	Description
`assertsign sgns (p, s)` Full Usage: `assertsign sgns (p, s)` Parameters: sgns : `(term * sign) list` p : `term` s : `sign` Returns: `(term * sign) list`	sgns : `(term * sign) list` p : `term` s : `sign` Returns: `(term * sign) list`
`basic_complex_qelim vars fm` Full Usage: `basic_complex_qelim vars fm` Parameters: vars : `string list` fm : `formula<fol>` Returns: `formula<fol>`	vars : `string list` fm : `formula<fol>` Returns: `formula<fol>`
`behead vars _arg1` Full Usage: `behead vars _arg1` Parameters: vars : `string list` _arg1 : `term` Returns: `term`	vars : `string list` _arg1 : `term` Returns: `term`
`coefficients vars _arg1` Full Usage: `coefficients vars _arg1` Parameters: vars : `string list` _arg1 : `term` Returns: `term list`	vars : `string list` _arg1 : `term` Returns: `term list`
`complex_qelim` Full Usage: `complex_qelim` Returns: `formula<fol> -> formula<fol>`	Returns: `formula<fol> -> formula<fol>`
`cqelim vars (eqs, neqs) sgns` Full Usage: `cqelim vars (eqs, neqs) sgns` Parameters: vars : `string list` eqs : `term list` neqs : `term list` sgns : `(term * sign) list` Returns: `formula<fol>`	vars : `string list` eqs : `term list` neqs : `term list` sgns : `(term * sign) list` Returns: `formula<fol>`
`degree vars p` Full Usage: `degree vars p` Parameters: vars : `string list` p : `term` Returns: `int`	vars : `string list` p : `term` Returns: `int`
`findsign sgns p` Full Usage: `findsign sgns p` Parameters: sgns : `(term * sign) list` p : `term` Returns: `sign`	sgns : `(term * sign) list` p : `term` Returns: `sign`
`head vars p` Full Usage: `head vars p` Parameters: vars : `string list` p : `term` Returns: `term`	vars : `string list` p : `term` Returns: `term`
`headconst p` Full Usage: `headconst p` Parameters: p : `term` Returns: `bigint`	p : `term` Returns: `bigint`
`init_sgns` Full Usage: `init_sgns` Returns: `(term * sign) list`	Returns: `(term * sign) list`
`is_constant vars p` Full Usage: `is_constant vars p` Parameters: vars : `string list` p : `term` Returns: `bool`	vars : `string list` p : `term` Returns: `bool`
`monic p` Full Usage: `monic p` Parameters: p : `term` Returns: `term * bool`	p : `term` Returns: `term * bool`
`pdivide` Full Usage: `pdivide` Returns: `string list -> term -> term -> int * term`	Returns: `string list -> term -> term -> int * term`
`poly_add vars pol1 pol2` Full Usage: `poly_add vars pol1 pol2` Parameters: vars : `string list` pol1 : `term` pol2 : `term` Returns: `term`	vars : `string list` pol1 : `term` pol2 : `term` Returns: `term`
`poly_cmul k p` Full Usage: `poly_cmul k p` Parameters: k : `BigInteger` p : `term` Returns: `term`	k : `BigInteger` p : `term` Returns: `term`
`poly_div vars p q` Full Usage: `poly_div vars p q` Parameters: vars : `string list` p : `term` q : `term` Returns: `term`	vars : `string list` p : `term` q : `term` Returns: `term`
`poly_ladd vars pol1 tm` Full Usage: `poly_ladd vars pol1 tm` Parameters: vars : `string list` pol1 : `term` tm : `term` Returns: `term`	vars : `string list` pol1 : `term` tm : `term` Returns: `term`
`poly_lmul vars pol1 tm` Full Usage: `poly_lmul vars pol1 tm` Parameters: vars : `string list` pol1 : `term` tm : `term` Returns: `term`	vars : `string list` pol1 : `term` tm : `term` Returns: `term`
`poly_mul vars pol1 pol2` Full Usage: `poly_mul vars pol1 pol2` Parameters: vars : `string list` pol1 : `term` pol2 : `term` Returns: `term`	vars : `string list` pol1 : `term` pol2 : `term` Returns: `term`
`poly_neg _arg1` Full Usage: `poly_neg _arg1` Parameters: _arg1 : `term` Returns: `term`	_arg1 : `term` Returns: `term`
`poly_nondiv vars sgns p s` Full Usage: `poly_nondiv vars sgns p s` Parameters: vars : `string list` sgns : `(term * sign) list` p : `term` s : `term` Returns: `formula<fol>`	vars : `string list` sgns : `(term * sign) list` p : `term` s : `term` Returns: `formula<fol>`
`poly_nonzero vars sgns pol` Full Usage: `poly_nonzero vars sgns pol` Parameters: vars : `string list` sgns : `(term * sign) list` pol : `term` Returns: `formula<fol>`	vars : `string list` sgns : `(term * sign) list` pol : `term` Returns: `formula<fol>`
`poly_pow vars p n` Full Usage: `poly_pow vars p n` Parameters: vars : `string list` p : `term` n : `int` Returns: `term`	vars : `string list` p : `term` n : `int` Returns: `term`
`poly_sub vars p q` Full Usage: `poly_sub vars p q` Parameters: vars : `string list` p : `term` q : `term` Returns: `term`	vars : `string list` p : `term` q : `term` Returns: `term`
`poly_var x` Full Usage: `poly_var x` Parameters: x : `string` Returns: `term`	x : `string` Returns: `term`
`polyatom vars fm` Full Usage: `polyatom vars fm` Parameters: vars : `string list` fm : `formula<fol>` Returns: `formula<fol>`	vars : `string list` fm : `formula<fol>` Returns: `formula<fol>`
`polynate vars tm` Full Usage: `polynate vars tm` Parameters: vars : `string list` tm : `term` Returns: `term`	vars : `string list` tm : `term` Returns: `term`
`split_zero sgns pol cont_z cont_n` Full Usage: `split_zero sgns pol cont_z cont_n` Parameters: sgns : `(term * sign) list` pol : `term` cont_z : `(term * sign) list -> formula<fol>` cont_n : `(term * sign) list -> formula<fol>` Returns: `formula<fol>`	sgns : `(term * sign) list` pol : `term` cont_z : `(term * sign) list -> formula<fol>` cont_n : `(term * sign) list -> formula<fol>` Returns: `formula<fol>`
`swap swf s` Full Usage: `swap swf s` Parameters: swf : `bool` s : `sign` Returns: `sign`	swf : `bool` s : `sign` Returns: `sign`