From 07157d18e197627eeabb02f5a4176a79c8b40c90 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sat, 22 Feb 2025 07:29:45 -0600 Subject: [PATCH] Setup --- src/CMakeLists.txt | 2 + src/rewriter/basic_rewrite_rcons.cpp | 16 ++++++- src/rewriter/basic_rewrite_rcons.h | 3 ++ src/theory/bv/macro_rewrite_elaborator.cpp | 50 ++++++++++++++++++++ src/theory/bv/macro_rewrite_elaborator.h | 55 ++++++++++++++++++++++ 5 files changed, 125 insertions(+), 1 deletion(-) create mode 100644 src/theory/bv/macro_rewrite_elaborator.cpp create mode 100644 src/theory/bv/macro_rewrite_elaborator.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0664ff14232..b5685185e3a 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -656,6 +656,8 @@ libcvc5_add_sources( theory/bv/bv_solver_bitblast_internal.h theory/bv/int_blaster.cpp theory/bv/int_blaster.h + theory/bv/macro_rewrite_elaborator.cpp + theory/bv/macro_rewrite_elaborator.h theory/bv/proof_checker.cpp theory/bv/proof_checker.h theory/bv/theory_bv.cpp diff --git a/src/rewriter/basic_rewrite_rcons.cpp b/src/rewriter/basic_rewrite_rcons.cpp index 83c68090941..31e0f8819db 100644 --- a/src/rewriter/basic_rewrite_rcons.cpp +++ b/src/rewriter/basic_rewrite_rcons.cpp @@ -68,7 +68,8 @@ BasicRewriteRCons::BasicRewriteRCons(Env& env) : EnvObj(env), d_theoryRewriteMacroExpand( statisticsRegistry().registerHistogram( - "BasicRewriteRCons::macroExpandCount")) + "BasicRewriteRCons::macroExpandCount")), + d_bvRewElab(env) { } @@ -354,6 +355,19 @@ void BasicRewriteRCons::ensureProofForTheoryRewrite(CDProof* cdp, handledMacro = true; } break; + case ProofRewriteRule::MACRO_BV_EXTRACT_CONCAT: + case ProofRewriteRule::MACRO_BV_EXTRACT_SIGN_EXTEND: + case ProofRewriteRule::MACRO_BV_ASHR_BY_CONST: + case ProofRewriteRule::MACRO_BV_OR_SIMPLIFY: + case ProofRewriteRule::MACRO_BV_AND_SIMPLIFY: + case ProofRewriteRule::MACRO_BV_XOR_SIMPLIFY: + case ProofRewriteRule::MACRO_BV_AND_OR_XOR_CONCAT_PULLUP: + case ProofRewriteRule::MACRO_BV_MULT_SLT_MULT: + case ProofRewriteRule::MACRO_BV_CONCAT_EXTRACT_MERGE: + case ProofRewriteRule::MACRO_BV_CONCAT_CONSTANT_MERGE: + case ProofRewriteRule::MACRO_BV_FLATTEN_ASSOC_COMMUT: + handledMacro = d_bvRewElab.ensureProofFor(cdp, id, eq); + break; default: break; } if (handledMacro) diff --git a/src/rewriter/basic_rewrite_rcons.h b/src/rewriter/basic_rewrite_rcons.h index 94066de9a69..aaa0b4a82c5 100644 --- a/src/rewriter/basic_rewrite_rcons.h +++ b/src/rewriter/basic_rewrite_rcons.h @@ -27,6 +27,7 @@ #include "smt/env_obj.h" #include "theory/builtin/proof_checker.h" #include "theory/rewriter.h" +#include "theory/bv/macro_rewrite_elaborator.h" namespace cvc5::internal { namespace rewriter { @@ -451,6 +452,8 @@ class BasicRewriteRCons : protected EnvObj * expanded in macro elimination by this class. */ HistogramStat d_theoryRewriteMacroExpand; + /** The BV rewrite elaborator */ + theory::bv::MacroRewriteElaborator d_bvRewElab; }; } // namespace rewriter diff --git a/src/theory/bv/macro_rewrite_elaborator.cpp b/src/theory/bv/macro_rewrite_elaborator.cpp new file mode 100644 index 00000000000..846086f018d --- /dev/null +++ b/src/theory/bv/macro_rewrite_elaborator.cpp @@ -0,0 +1,50 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2024 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. + * **************************************************************************** + * + * Methods for elaborating MACRO_BV_* proof rewrites. + */ + +#include "theory/bv/macro_rewrite_elaborator.h" + +namespace cvc5::internal { +namespace theory { +namespace bv { + +MacroRewriteElaborator::MacroRewriteElaborator(Env& env) : EnvObj(env){} +MacroRewriteElaborator::~MacroRewriteElaborator() {} +bool MacroRewriteElaborator::ensureProofFor(CDProof* cdp, + ProofRewriteRule id, + const Node& eq) +{ + switch (id) + { + case ProofRewriteRule::MACRO_BV_EXTRACT_CONCAT: + case ProofRewriteRule::MACRO_BV_EXTRACT_SIGN_EXTEND: + case ProofRewriteRule::MACRO_BV_ASHR_BY_CONST: + case ProofRewriteRule::MACRO_BV_OR_SIMPLIFY: + case ProofRewriteRule::MACRO_BV_AND_SIMPLIFY: + case ProofRewriteRule::MACRO_BV_XOR_SIMPLIFY: + case ProofRewriteRule::MACRO_BV_AND_OR_XOR_CONCAT_PULLUP: + case ProofRewriteRule::MACRO_BV_MULT_SLT_MULT: + case ProofRewriteRule::MACRO_BV_CONCAT_EXTRACT_MERGE: + case ProofRewriteRule::MACRO_BV_CONCAT_CONSTANT_MERGE: + case ProofRewriteRule::MACRO_BV_FLATTEN_ASSOC_COMMUT: + break; + default: + break; + } + return false; +} + +} // namespace bv +} // namespace theory +} // namespace cvc5::internal diff --git a/src/theory/bv/macro_rewrite_elaborator.h b/src/theory/bv/macro_rewrite_elaborator.h new file mode 100644 index 00000000000..518b1c654f4 --- /dev/null +++ b/src/theory/bv/macro_rewrite_elaborator.h @@ -0,0 +1,55 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2024 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. + * **************************************************************************** + * + * Methods for elaborating MACRO_BV_* proof rewrites. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__BV__MACRO_REWRITE_ELABORATOR_H +#define CVC5__THEORY__BV__MACRO_REWRITE_ELABORATOR_H + +#include "proof/proof.h" +#include "smt/env_obj.h" + +namespace cvc5::internal { +namespace theory { +namespace bv { + +/** + * Methods for elaborating MACRO_BV_* proof rewrites. This class is called during + * RARE proof reconstruction. + */ +class MacroRewriteElaborator : protected EnvObj +{ + public: + /** Constructor */ + MacroRewriteElaborator(Env& env); + ~MacroRewriteElaborator(); + /** + * Elaborate a rewrite eq that was proven by a macro rewrite rule. + * + * @param cdp The proof to add to. + * @param id The (macro) rewrite id that proved the rewrite. + * @param eq The rewrite proven. + * @return true if added a closed proof of eq to cdp. + */ + bool ensureProofFor(CDProof* cdp, + ProofRewriteRule id, + const Node& eq); +}; + +} // namespace bv +} // namespace theory +} // namespace cvc5::internal + +#endif /* CVC5__THEORY__BV__MACRO_REWRITE_ELABORATOR_H */