From 3b0b4f554841847aa529a1d95585aedcba5b0fee Mon Sep 17 00:00:00 2001 From: yoni206 Date: Wed, 6 Jan 2021 14:41:13 -0800 Subject: [PATCH] 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. --- src/CMakeLists.txt | 2 + .../passes/foreign_theory_rewrite.cpp | 48 +++++++++++++++++ .../passes/foreign_theory_rewrite.h | 52 +++++++++++++++++++ .../preprocessing_pass_registry.cpp | 2 + 4 files changed, 104 insertions(+) create mode 100644 src/preprocessing/passes/foreign_theory_rewrite.cpp create mode 100644 src/preprocessing/passes/foreign_theory_rewrite.h 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; + +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); registerPassInfo("int-to-bv", callCtor); registerPassInfo("bv-to-int", callCtor); + registerPassInfo("foreign-theory-rewrite", callCtor); registerPassInfo("synth-rr", callCtor); registerPassInfo("real-to-int", callCtor); registerPassInfo("sygus-infer", callCtor); -- 2.30.2