diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2021-01-06 14:41:13 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-06 16:41:13 -0600 |
commit | 3b0b4f554841847aa529a1d95585aedcba5b0fee (patch) | |
tree | 8e870a8dc0398f85d0c6799e3c9a26cf96bd4d40 | |
parent | c32c2c5f5203fff6d4982755e3784f6f2f315b3b (diff) |
strings arith checks preprocessing pass: step 1 (#5747)
We are adding a preprocessing pass that simplifies arithmetic constraints related to strings.
For example, len(s) >= 0 would be replaced by true.
This will make use of CVC4::theory::strings::ArithEntail::check.
This PR is the first step. It only includes the preprocessing pass infrastructure, with an empty implementation of the main function StrLenSimplify::simplify. It also adds the pass to the registry.
The implementation of this function is not complicated, but is left for a future PR in order to keep the PR short.
Future PRs will include an implementation of the main function, tests, and a command line option to turn on the pass.
-rw-r--r-- | src/CMakeLists.txt | 2 | ||||
-rw-r--r-- | src/preprocessing/passes/foreign_theory_rewrite.cpp | 48 | ||||
-rw-r--r-- | src/preprocessing/passes/foreign_theory_rewrite.h | 52 | ||||
-rw-r--r-- | src/preprocessing/preprocessing_pass_registry.cpp | 2 |
4 files changed, 104 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 08404ce73..f01c948db 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -102,6 +102,8 @@ libcvc4_add_sources( preprocessing/passes/sort_infer.h preprocessing/passes/static_learning.cpp preprocessing/passes/static_learning.h + preprocessing/passes/foreign_theory_rewrite.cpp + preprocessing/passes/foreign_theory_rewrite.h preprocessing/passes/sygus_inference.cpp preprocessing/passes/sygus_inference.h preprocessing/passes/synth_rew_rules.cpp diff --git a/src/preprocessing/passes/foreign_theory_rewrite.cpp b/src/preprocessing/passes/foreign_theory_rewrite.cpp new file mode 100644 index 000000000..74183d518 --- /dev/null +++ b/src/preprocessing/passes/foreign_theory_rewrite.cpp @@ -0,0 +1,48 @@ +/********************* */ +/*! \file foreign_theory_rewrite.cpp + ** \verbatim + ** Top contributors (to current version): + ** Yoni Zohar + ** 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 foreign_theory_rewrite preprocessing pass + ** + ** Simplifies nodes of one theory using rewrites from another. + **/ + +#include "preprocessing/passes/foreign_theory_rewrite.h" + +#include "expr/node_traversal.h" +#include "theory/strings/arith_entail.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +using namespace CVC4::theory; + +ForeignTheoryRewrite::ForeignTheoryRewrite(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "foreign-theory-rewrite"), + d_cache(preprocContext->getUserContext()){}; + +Node ForeignTheoryRewrite::simplify(Node n) { assert(false); } + +PreprocessingPassResult ForeignTheoryRewrite::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) + { + assertionsToPreprocess->replace( + i, Rewriter::rewrite(simplify((*assertionsToPreprocess)[i]))); + } + + return PreprocessingPassResult::NO_CONFLICT; +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/foreign_theory_rewrite.h b/src/preprocessing/passes/foreign_theory_rewrite.h new file mode 100644 index 000000000..9b7f71b50 --- /dev/null +++ b/src/preprocessing/passes/foreign_theory_rewrite.h @@ -0,0 +1,52 @@ +/********************* */ +/*! \file foreign_theory_rewrite.h + ** \verbatim + ** Top contributors (to current version): + ** Yoni Zohar + ** 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 foreign_theory_rewrite preprocessing pass + ** + ** Simplifies nodes of one theory using rewrites from another. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H +#define CVC4__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H + +#include "context/cdhashmap.h" +#include "context/cdo.h" +#include "context/context.h" +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +using CDNodeMap = context::CDHashMap<Node, Node, NodeHashFunction>; + +class ForeignTheoryRewrite : public PreprocessingPass +{ + public: + ForeignTheoryRewrite(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + // the main function that simplifies n + Node simplify(Node n); + // A cache to store the simplified nodes + CDNodeMap d_cache; +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* CVC4__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H */ diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp index b21d4e30c..da09f6363 100644 --- a/src/preprocessing/preprocessing_pass_registry.cpp +++ b/src/preprocessing/preprocessing_pass_registry.cpp @@ -50,6 +50,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/sygus_inference.h" #include "preprocessing/passes/synth_rew_rules.h" #include "preprocessing/passes/theory_preprocess.h" @@ -124,6 +125,7 @@ PreprocessingPassRegistry::PreprocessingPassRegistry() registerPassInfo("global-negate", callCtor<GlobalNegate>); registerPassInfo("int-to-bv", callCtor<IntToBV>); registerPassInfo("bv-to-int", callCtor<BVToInt>); + registerPassInfo("foreign-theory-rewrite", callCtor<ForeignTheoryRewrite>); registerPassInfo("synth-rr", callCtor<SynthRewRulesPass>); registerPassInfo("real-to-int", callCtor<RealToInt>); registerPassInfo("sygus-infer", callCtor<SygusInference>); |