Univariate root finding #9115
Univariate root finding #9115
Conversation
src/theory/ff/roots.cpp
Outdated
| return o.str(); | ||
| } | ||
|
|
||
| // sorting based on strings because CoCoA doesn't cmp |
There was a problem hiding this comment.
Hmm, the documentation seems to suggest that cmp exists for CoCoA::RingElem? Am I missing something?
There was a problem hiding this comment.
Yes, that's a natural question. Unfortunately, comparison only works for elements of 'ordered' rings: i.e., a ring R for which CoCoA::IsOrderedDomain(R) returns true. Most rings that CoCoA implements do not satisfy this, including prime fields.
I've expanded the comment a bit.
|
Following up on our discussion, the global manager must be created exactly once. Creating it multiple times does cause an error. |
|
|
||
| namespace cvc5::internal { | ||
|
|
||
| extern CoCoA::GlobalManager* s_cocoaGlobalManager; |
There was a problem hiding this comment.
Can you comment on the details of why this needs to be static?
Also, mention how this works if multiple solvers are created, e.g. I assume that this pointer is initialize on demand then it is not a problem to share between multiple solvers?
There was a problem hiding this comment.
Yep! Just did it. I put most of the documentation at the top of the header.
No description provided.