Ioannis Filippidis

clear memoized attribute values when geometry changes

2

It is advantageous to restrict `ConvexPolytope` and `Polytope` to have immutable geometry (except for their annotation, i.e., the propositions), so that expensive attributes (e.g., Chebyshev radius and center, envelope, bounding...

improve polytope efficiency

2

Optimize the heavily used functions and methods in `polytope`. Possibly by pushing some things to `C` using `Cython` (optional, i.e., installation shouldn't break in case compilation fails). The profiler says:...

improve numerical accuracy of polytope.reduce (polytope.intersect)

2

`polytope.intersect` calls `polytope.reduce` to simplify the H-representation after intersection, which basically concatenates constraints. When the numbers in given matrices have different orders, `reduce` does not work well. Below is an...

Either using `threading` to avoid the cost of creating new processes with `multiprocessing`, or with a persistent pool of workers using `multiprocessing`, to which `ConvexPolytope - ConvexPolytope` jobs are passed....

monitor condition number of Polytope

1

To make the user aware of how bad ill-conditioning is in their problem, a quick search leads, e.g., to [this paper](http://www.sciencedirect.com/science/article/pii/016763779500019G).

For example, ``` a == ... b == ... a ... ``` where the defined symbols are not variables, but simply expressions to be reused throughout. Similar in purpose and...

This should be possible, by: 1. `f == EnvInit => SysInit` 2. `g == \E y: f` 3. `\A`-enumerate `g` over `x` 4. `h ==` substitute each assignment `x` in...

Cudd_SetMaxMemory

4

`Cudd_init(..., maxMemory)` does **not** place any hard limit on maximum memory occupation. Instead, an explicit call to [`Cudd_SetMaxMemory`](https://github.com/johnyf/cudd/blob/80c9396b7efcb24c33868aeffb89a557af0dc356/cudd/cudd/cuddAPI.c#L4440) is needed, in order to limit the memory occupation. A search within...

`omega.symbolic.fol.Context` arranges and uses a refinement of each variable that will be reasoned about for integer values from some finite set by a fixed finite number of variables that will...

### [Quantifier bounds](https://en.wikipedia.org/wiki/Bounded_quantifier) and dynamic type hints in `omega` As of f4aa8f8459c65d5491aadef1fef80db23944a792, the formula `\A x: P(x)` means different things, depending on whether it is given to [`omega.symbolic.fol.Context.add_expr`](https://github.com/johnyf/omega/blob/cc37e899fae3d98e356178f092046e4363160945/omega/symbolic/fol.py#L178) with `x`...