ff: sub-theory #9210
ff: sub-theory #9210
Conversation
This patch adds a "sub-theory" of FF. * a sub-theory is initialized with a field size, and responsible only for the field of that size. * its interface is a restriction of the general SMT theory interface * the full FF solver essentially just multiplexes between the sub-theories
src/theory/ff/sub_theory.h
Outdated
| namespace theory { | ||
| namespace ff { | ||
|
|
||
| class SubTheory : EnvObj, context::ContextNotifyObj |
There was a problem hiding this comment.
Give some quick doc on the overall purpose of this class here (along the lines of the PR description).
| // Atoms | ||
| context::CDList<Node> d_atoms; | ||
|
|
||
| FfStatistics* d_stats; |
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
| // Facts, in notification order. | ||
| // | ||
| // Uses SAT context. | ||
| context::CDList<Node> d_facts; |
There was a problem hiding this comment.
Its a bit funny to maintain this when the Theory also can reproduce the fact queue (from this member https://github.com/cvc5/cvc5/blob/main/src/theory/theory.h#L813).
Is it critical to maintain this list? Or could this be extracted from the fact queue from TheoryFf?
If you are interested in a standard way of accessing this list, I can give some guidance, e.g. using interfaces from the TheoryState utility https://github.com/cvc5/cvc5/blob/main/src/theory/theory_state.h (I'm somewhat surprised the class introduced in this PR does not depend on this utility already).
There was a problem hiding this comment.
This list contains only the facts for this sub-theory. That is, those in the specific field that this sub-theory manages.
We could extract those from the theory-wide list as needed, but keeping them here seemed asymptotically better?
We could also keep a list here of indices into the global list, which maybe fixes the asymptotic issue, but I'm not sure the global list is meant to support random access. Also, I don't really like the idea of keeping indices into a list that is very far away codebase-wise.
Thoughts?
There was a problem hiding this comment.
If we stick with this solution, I'll leave a comment about this conversation.
There was a problem hiding this comment.
Ok, this makes sense to me, yes comment in the doc on this.
| // What is that conflict? | ||
| const std::vector<Node>& conflict() const; | ||
|
|
||
| // Get a model. |
There was a problem hiding this comment.
I assume this can only be called at a certain point? E.g. after full effort check? If so, document this.
| } | ||
| } | ||
|
|
||
| // CoCoA symbols must start with a letter and contain only letters and |
This patch adds a "sub-theory" of FF.