projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 73a9f07) | patch
Improve pre-skolemization, move quantifiers preprocess to own file (#7153)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 8 Sep 2021 20:54:22 +0000 (15:54 -0500)
committerGitHub <noreply@github.com>
Wed, 8 Sep 2021 20:54:22 +0000 (20:54 +0000)
commit4b0650bfe0c1df81ad3236def912543510932320
tree16ca312b99881bcf36ccf840ab26079d7bafb35ctree
parent73a9f07321a854f8f9123c3645db5b7cddb827becommit | diff
Improve pre-skolemization, move quantifiers preprocess to own file (#7153)

This also heavily refactors the preskolemization method (now in QuantifiersPreprocess), in preparation for it being enabled by default. This method previously was doing a tree traversal, it now maintains a visited cache.

It makes minor cleanup to the dependencies of this method.
18 files changed:
src/CMakeLists.txt diff | blob | history
src/preprocessing/passes/quantifiers_preprocess.cpp diff | blob | history
src/preprocessing/passes/sygus_inference.cpp diff | blob | history
src/proof/proof_rule.h diff | blob | history
src/smt/env_obj.cpp diff | blob | history
src/smt/env_obj.h diff | blob | history
src/theory/quantifiers/instantiate.cpp diff | blob | history
src/theory/quantifiers/quant_util.cpp diff | blob | history
src/theory/quantifiers/quant_util.h diff | blob | history
src/theory/quantifiers/quantifiers_preprocess.cpp [new file with mode: 0644] blob
src/theory/quantifiers/quantifiers_preprocess.h [new file with mode: 0644] blob
src/theory/quantifiers/quantifiers_registry.cpp diff | blob | history
src/theory/quantifiers/quantifiers_registry.h diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.h diff | blob | history
src/theory/quantifiers/skolemize.cpp diff | blob | history
src/theory/quantifiers/skolemize.h diff | blob | history
src/theory/quantifiers/theory_quantifiers.cpp diff | blob | history