diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-09-08 15:54:22 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-08 20:54:22 +0000 |
commit | 4b0650bfe0c1df81ad3236def912543510932320 (patch) | |
tree | 16ca312b99881bcf36ccf840ab26079d7bafb35c /src/theory/quantifiers/instantiate.cpp | |
parent | 73a9f07321a854f8f9123c3645db5b7cddb827be (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.
Diffstat (limited to 'src/theory/quantifiers/instantiate.cpp')
-rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 0daf53d2d..9010d4fe1 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -28,7 +28,7 @@ #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/quantifiers_preprocess.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_registry.h" @@ -252,7 +252,7 @@ bool Instantiate::addInstantiation(Node q, q, d_qreg.d_vars[q], terms, id, pfArg, doVts, pfTmp.get()); Node orig_body = body; // now preprocess, storing the trust node for the rewrite - TrustNode tpBody = QuantifiersRewriter::preprocess(body, true); + TrustNode tpBody = d_qreg.getPreprocess().preprocess(body, true); if (!tpBody.isNull()) { Assert(tpBody.getKind() == TrustNodeKind::REWRITE); |