projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: dcc1a5f) | patch
Optimize get skolems method (#5876)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 10 Feb 2021 02:07:33 +0000 (20:07 -0600)
committerGitHub <noreply@github.com>
Wed, 10 Feb 2021 02:07:33 +0000 (20:07 -0600)
commit4f5698447f25828e2a52dad198736054e5b2dacb
tree5614e0ae4184d042fc8b26afb58287b78f194db2tree
parentdcc1a5ff44ed83bdc1e2abcac3aebb299a376b08commit | 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.
src/smt/term_formula_removal.cpp diff | blob | history
src/smt/term_formula_removal.h diff | blob | history