diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-15 15:19:43 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-15 15:19:43 -0600 |
commit | de79f1ad325036ca90be9144a74606310b5dab9b (patch) | |
tree | ff025f0ccc846073327b1ad823eb9d255f4a8843 /src/preprocessing | |
parent | eb6155c5f078a26b7cdddddad6e209fad0f825f8 (diff) |
Implement --no-strings-lazy-pp as a preprocessing pass (#5777)
This option eliminates extended functions in strings eagerly. This was incorrectly done at ppRewrite previously, which should not add lemmas. Instead, this makes this technique into a preprocessing pass. To do this, the interface for the strings preprocessor was cleaned to have fewer dependencies, and made to track a cache internally.
Fixes #5608, fixes #5745, fixes #5767, fixes #5771, fixes #5406.
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/rewrite.cpp | 2 | ||||
-rw-r--r-- | src/preprocessing/passes/strings_eager_pp.cpp | 59 | ||||
-rw-r--r-- | src/preprocessing/passes/strings_eager_pp.h | 45 | ||||
-rw-r--r-- | src/preprocessing/preprocessing_pass_registry.cpp | 4 |
4 files changed, 108 insertions, 2 deletions
diff --git a/src/preprocessing/passes/rewrite.cpp b/src/preprocessing/passes/rewrite.cpp index b4a353862..b8c9498e1 100644 --- a/src/preprocessing/passes/rewrite.cpp +++ b/src/preprocessing/passes/rewrite.cpp @@ -31,7 +31,7 @@ Rewrite::Rewrite(PreprocessingPassContext* preprocContext) PreprocessingPassResult Rewrite::applyInternal( AssertionPipeline* assertionsToPreprocess) -{ +{ for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) { assertionsToPreprocess->replace(i, Rewriter::rewrite((*assertionsToPreprocess)[i])); } diff --git a/src/preprocessing/passes/strings_eager_pp.cpp b/src/preprocessing/passes/strings_eager_pp.cpp new file mode 100644 index 000000000..69cb8914c --- /dev/null +++ b/src/preprocessing/passes/strings_eager_pp.cpp @@ -0,0 +1,59 @@ +/********************* */ +/*! \file strings_eager_pp.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The strings eager preprocess utility + **/ + +#include "preprocessing/passes/strings_eager_pp.h" + +#include "theory/strings/theory_strings_preprocess.h" +#include "theory/rewriter.h" + +using namespace CVC4::theory; + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +StringsEagerPp::StringsEagerPp(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "strings-eager-pp"){}; + +PreprocessingPassResult StringsEagerPp::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + NodeManager* nm = NodeManager::currentNM(); + theory::strings::SkolemCache skc(false); + theory::strings::StringsPreprocess pp(&skc); + for (size_t i = 0, nasserts = assertionsToPreprocess->size(); i < nasserts; + ++i) + { + Node prev = (*assertionsToPreprocess)[i]; + std::vector<Node> asserts; + Node rew = pp.processAssertion(prev, asserts); + if (!asserts.empty()) + { + std::vector<Node> conj; + conj.push_back(rew); + conj.insert(conj.end(), asserts.begin(), asserts.end()); + rew = nm->mkAnd(conj); + } + if (prev != rew) + { + assertionsToPreprocess->replace(i, theory::Rewriter::rewrite(rew)); + } + } + + return PreprocessingPassResult::NO_CONFLICT; +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/strings_eager_pp.h b/src/preprocessing/passes/strings_eager_pp.h new file mode 100644 index 000000000..299260c61 --- /dev/null +++ b/src/preprocessing/passes/strings_eager_pp.h @@ -0,0 +1,45 @@ +/********************* */ +/*! \file strings_eager_pp.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The strings eager preprocess utility + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H +#define CVC4__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +/** + * Eliminate all extended string functions in the input problem using + * reductions to bounded string quantifiers. + */ +class StringsEagerPp : public PreprocessingPass +{ + public: + StringsEagerPp(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* CVC4__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H */ diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp index da09f6363..f14b8b4a7 100644 --- a/src/preprocessing/preprocessing_pass_registry.cpp +++ b/src/preprocessing/preprocessing_pass_registry.cpp @@ -33,6 +33,7 @@ #include "preprocessing/passes/bv_to_bool.h" #include "preprocessing/passes/bv_to_int.h" #include "preprocessing/passes/extended_rewriter_pass.h" +#include "preprocessing/passes/foreign_theory_rewrite.h" #include "preprocessing/passes/fun_def_fmf.h" #include "preprocessing/passes/global_negate.h" #include "preprocessing/passes/ho_elim.h" @@ -50,7 +51,7 @@ #include "preprocessing/passes/sep_skolem_emp.h" #include "preprocessing/passes/sort_infer.h" #include "preprocessing/passes/static_learning.h" -#include "preprocessing/passes/foreign_theory_rewrite.h" +#include "preprocessing/passes/strings_eager_pp.h" #include "preprocessing/passes/sygus_inference.h" #include "preprocessing/passes/synth_rew_rules.h" #include "preprocessing/passes/theory_preprocess.h" @@ -153,6 +154,7 @@ PreprocessingPassRegistry::PreprocessingPassRegistry() registerPassInfo("ho-elim", callCtor<HoElim>); registerPassInfo("fun-def-fmf", callCtor<FunDefFmf>); registerPassInfo("theory-rewrite-eq", callCtor<TheoryRewriteEq>); + registerPassInfo("strings-eager-pp", callCtor<StringsEagerPp>); } } // namespace preprocessing |