Complex number decision package

Jump to: navigation, search

David Lester is attempting to add complex numbers to the prelude along with decision procedures for them.

In principal this is easy. The BDD algorithm works, as is, provided only that we limit the operators to "=" (and do not include order inequalities) and the bdd package is modified to handle complex coefficients.

I'm not sure how best to proceed. Do I hack a translation to the reals (via Re and Im)? This might be best.

Picking the right subtype of number_field is trickier, but do-able, and if done correctly would help eliminate the soundness bugs I tend to generate.

In practice, I'm struggling to find the right bits to tweak.

Any clues on how to persuade PVS to notice changes to prelude.pvs/prf ? Also, how do I get the variable lisp *complex* to be noticed globally? I've copied the material for *real* in globals.lisp, but (predicate *complex*) gives an error where (predicate *real*) returns real_pred .

Personal tools