diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-09 20:07:33 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-09 20:07:33 -0600 |
| commit | 4f5698447f25828e2a52dad198736054e5b2dacb (patch) | |
| tree | 5614e0ae4184d042fc8b26afb58287b78f194db2 /src/theory/quantifiers/inst_match_trie.cpp | |
| parent | dcc1a5ff44ed83bdc1e2abcac3aebb299a376b08 (diff) | |
Optimize get skolems method (#5876)
This method is used to determine which skolems have definitions according to term formula removal. This optimizes the method using attributes similar to how expr::getFreeVariables works.
It will be used heavily for SAT relevancy. We should also consider updating the justification heuristic to use this method.
Diffstat (limited to 'src/theory/quantifiers/inst_match_trie.cpp')
0 files changed, 0 insertions, 0 deletions