diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-12 13:55:13 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-07-12 18:55:13 +0000 |
commit | b35641f1a4ac8d70cf868b273971ee7c5e3b35f0 (patch) | |
tree | e05ba328b28ed05a11756712a9303ac05cefdd1d /src/theory/arith | |
parent | e01ae3a87f4e1dc4b4511e8bd028d5c0838ccedc (diff) |
Add arithmetic preprocess rewrite equality module (#6860)
This is the first part of a refactoring which will ensure that the linear arithmetic solver does not violate integer type constraints in its model.
This PR moves the method https://github.com/ajreynol/CVC4/blob/master/src/theory/arith/theory_arith.cpp#L129 to its own module / file.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/pp_rewrite_eq.cpp | 59 | ||||
-rw-r--r-- | src/theory/arith/pp_rewrite_eq.h | 60 |
2 files changed, 119 insertions, 0 deletions
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 |