diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-02-01 14:37:08 +0100 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-22 17:07:59 +0100 |
| commit | ddbc3839923731686a89a401d0f9dd44f3ad339b (patch) | |
| tree | 17cc59feb26d5c19658ddf9164d367505295035f /theories/Reals | |
| parent | 9e621625618e1a0f341b87d66c1ea6027369c2e5 (diff) | |
Fix broken evaluation strategies for ring and field.
A bang indicates an argument that must be reduced, a star indicates an
argument that must be handled recursively.
PEeval: R r0 r1 add mul sub opp C phi Cpow powphi pow varmap pol
0 1 2 3 4 5 6 7 8! 9 10! 11 12* 13!
FEeval: R r0 r1 add mul sub opp div inv C phi Cpow powphi pow varmap pol
0 1 2 3 4 5 6 7 8 9 10! 11 12! 13 14* 15!
Pphi_dev: R r0 r1 add mul sub opp C c0 c1 ceq phi sign varmap pol
0 1 2 3 4 5 6 7 8! 9! 10! 11! 12! 13* 14!
Pphi_pow: R r0 r1 add mul sub opp C c0 c1 ceq phi Cpow powphi pow sign varmap pol
0 1 2 3 4 5 6 7 8! 9! 10! 11! 12 13! 14 15! 16* 17!
display_linear: R r0 r1 add mul sub opp div C c0 c1 ceq phi sign varmap num den
0 1 2 3 4 5 6 7 8 9! 10!11! 12! 13! 14* 15! 16!
display_pow_linear: R r0 r1 add mul sub opp div C c0 c1 ceq phi Cpow powphi pow sign varmap num den
0 1 2 3 4 5 6 7 8 9! 10!11! 12! 13 14! 15 16! 17* 18! 19!
PCond: R r0 r1 add mul sub opp eq C phi Cpow powphi pow varmap pol
0 1 2 3 4 5 6 7 8 9! 10 11! 12 13* 14!
Diffstat (limited to 'theories/Reals')
0 files changed, 0 insertions, 0 deletions