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/smt/term_formula_removal.h | |
| 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/smt/term_formula_removal.h')
| -rw-r--r-- | src/smt/term_formula_removal.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index 0c026a5fe..54dc488bf 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -135,6 +135,10 @@ class RemoveTermFormulas { */ void getSkolems(TNode n, std::unordered_set<Node, NodeHashFunction>& skolems) const; + /** + * Does n have skolems introduced by this class? + */ + bool hasSkolems(TNode n) const; /** * Get the lemma for the skolem, or the null node if k is not a skolem this |