diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-07-12 11:55:53 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-07-12 11:55:53 -0700 |
commit | 3fe25bb26080df5e94f2cba43d463cc1082d1c29 (patch) | |
tree | 05d54305f29de1f5d152aae0e601f5779609935e | |
parent | cfa833a09da24d1a0c92932f96fbd9c301119361 (diff) | |
parent | b35641f1a4ac8d70cf868b273971ee7c5e3b35f0 (diff) |
Merge branch 'master' into fixANTLRBuildfixANTLRBuild
-rw-r--r-- | src/CMakeLists.txt | 2 | ||||
-rw-r--r-- | src/theory/arith/pp_rewrite_eq.cpp | 59 | ||||
-rw-r--r-- | src/theory/arith/pp_rewrite_eq.h | 60 |
3 files changed, 121 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 811f1c5ae..9fce77c80 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -467,6 +467,8 @@ libcvc5_add_sources( theory/arith/operator_elim.h theory/arith/partial_model.cpp theory/arith/partial_model.h + theory/arith/pp_rewrite_eq.cpp + theory/arith/pp_rewrite_eq.h theory/arith/proof_checker.cpp theory/arith/proof_checker.h theory/arith/proof_macros.h diff --git a/src/theory/arith/pp_rewrite_eq.cpp b/src/theory/arith/pp_rewrite_eq.cpp new file mode 100644 index 000000000..45f972038 --- /dev/null +++ b/src/theory/arith/pp_rewrite_eq.cpp @@ -0,0 +1,59 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Preprocess equality rewriter for arithmetic + */ + +#include "theory/arith/pp_rewrite_eq.h" + +#include "options/arith_options.h" +#include "theory/rewriter.h" + +namespace cvc5 { +namespace theory { +namespace arith { + +PreprocessRewriteEq::PreprocessRewriteEq(context::Context* c, + ProofNodeManager* pnm) + : d_ppPfGen(pnm, c, "Arith::ppRewrite"), d_pnm(pnm) +{ +} + +TrustNode PreprocessRewriteEq::ppRewriteEq(TNode atom) +{ + Assert(atom.getKind() == kind::EQUAL); + if (!options::arithRewriteEq()) + { + return TrustNode::null(); + } + Assert(atom[0].getType().isReal()); + Node leq = NodeBuilder(kind::LEQ) << atom[0] << atom[1]; + Node geq = NodeBuilder(kind::GEQ) << atom[0] << atom[1]; + Node rewritten = Rewriter::rewrite(leq.andNode(geq)); + Debug("arith::preprocess") + << "arith::preprocess() : returning " << rewritten << std::endl; + // don't need to rewrite terms since rewritten is not a non-standard op + if (proofsEnabled()) + { + return d_ppPfGen.mkTrustedRewrite( + atom, + rewritten, + d_pnm->mkNode(PfRule::INT_TRUST, {}, {atom.eqNode(rewritten)})); + } + return TrustNode::mkTrustRewrite(atom, rewritten, nullptr); +} + +bool PreprocessRewriteEq::proofsEnabled() const { return d_pnm != nullptr; } + +} // namespace arith +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/arith/pp_rewrite_eq.h b/src/theory/arith/pp_rewrite_eq.h new file mode 100644 index 000000000..fc022f1d8 --- /dev/null +++ b/src/theory/arith/pp_rewrite_eq.h @@ -0,0 +1,60 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Preprocess equality rewriter for arithmetic + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__ARITH__PP_REWRITE_EQ__H +#define CVC5__THEORY__ARITH__PP_REWRITE_EQ__H + +#include "context/context.h" +#include "expr/node.h" +#include "proof/eager_proof_generator.h" +#include "proof/proof_node_manager.h" + +namespace cvc5 { +namespace theory { +namespace arith { + +/** + * This class is responsible for rewriting arithmetic equalities based on the + * current options. + * + * In particular, we may rewrite (= x y) to (and (>= x y) (<= x y)). + */ +class PreprocessRewriteEq +{ + public: + PreprocessRewriteEq(context::Context* c, ProofNodeManager* pnm); + ~PreprocessRewriteEq() {} + /** + * Preprocess equality, applies ppRewrite for equalities. This method is + * distinct from ppRewrite since it is not allowed to construct lemmas. + */ + TrustNode ppRewriteEq(TNode eq); + + private: + /** Are proofs enabled? */ + bool proofsEnabled() const; + /** Used to prove pp-rewrites */ + EagerProofGenerator d_ppPfGen; + /** Proof node manager */ + ProofNodeManager* d_pnm; +}; + +} // namespace arith +} // namespace theory +} // namespace cvc5 + +#endif |