From cb54d547b2a0e99258cb4c754bc4d979abee93f8 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 6 Oct 2020 07:00:22 -0500 Subject: [PATCH] Add arithmetic preprocess module (#5188) This class serves a similar purpose to the strings preprocess module (https://github.com/CVC4/CVC4/blob/master/src/theory/strings/theory_strings_preprocess.h). It can potentially be used for reducing extended arithmetic operators on demand via lemmas. This PR does not change the current behavior, but generalizes the use of operator elimination in TheoryArith to make this possible. --- src/CMakeLists.txt | 2 + src/theory/arith/arith_preprocess.cpp | 68 +++++++++++++++++++++++ src/theory/arith/arith_preprocess.h | 80 +++++++++++++++++++++++++++ src/theory/arith/theory_arith.cpp | 6 +- src/theory/arith/theory_arith.h | 5 +- 5 files changed, 156 insertions(+), 5 deletions(-) create mode 100644 src/theory/arith/arith_preprocess.cpp create mode 100644 src/theory/arith/arith_preprocess.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 65223f3c5..4ca57effd 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -285,6 +285,8 @@ libcvc4_add_sources( theory/arith/arith_lemma.h theory/arith/arith_msum.cpp theory/arith/arith_msum.h + theory/arith/arith_preprocess.cpp + theory/arith/arith_preprocess.h theory/arith/arith_rewriter.cpp theory/arith/arith_rewriter.h theory/arith/arith_state.cpp diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp new file mode 100644 index 000000000..577407c07 --- /dev/null +++ b/src/theory/arith/arith_preprocess.cpp @@ -0,0 +1,68 @@ +/********************* */ +/*! \file arith_preprocess.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** 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 Arithmetic preprocess + **/ + +#include "theory/arith/arith_preprocess.h" + +namespace CVC4 { +namespace theory { +namespace arith { + +ArithPreprocess::ArithPreprocess(ArithState& state, + InferenceManager& im, + ProofNodeManager* pnm, + const LogicInfo& info) + : d_im(im), d_opElim(pnm, info), d_reduced(state.getUserContext()) +{ +} +TrustNode ArithPreprocess::eliminate(TNode n) { return d_opElim.eliminate(n); } +bool ArithPreprocess::reduceAssertion(TNode atom) +{ + context::CDHashMap::const_iterator it = + d_reduced.find(atom); + if (it != d_reduced.end()) + { + // already computed + return (*it).second; + } + TrustNode tn = eliminate(atom); + if (tn.isNull()) + { + // did not reduce + d_reduced[atom] = false; + return false; + } + Assert(tn.getKind() == TrustNodeKind::REWRITE); + // tn is of kind REWRITE, turn this into a LEMMA here + TrustNode tlem = TrustNode::mkTrustLemma(tn.getProven(), tn.getGenerator()); + // must preprocess + d_im.trustedLemma(tlem, LemmaProperty::PREPROCESS); + // mark the atom as reduced + d_reduced[atom] = true; + return true; +} + +bool ArithPreprocess::isReduced(TNode atom) const +{ + context::CDHashMap::const_iterator it = + d_reduced.find(atom); + if (it == d_reduced.end()) + { + return false; + } + return (*it).second; +} + +} // namespace arith +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/arith/arith_preprocess.h b/src/theory/arith/arith_preprocess.h new file mode 100644 index 000000000..165209bd9 --- /dev/null +++ b/src/theory/arith/arith_preprocess.h @@ -0,0 +1,80 @@ +/********************* */ +/*! \file arith_preprocess.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** 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 Arithmetic preprocess + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__ARITH__ARITH_PREPROCESS_H +#define CVC4__THEORY__ARITH__ARITH_PREPROCESS_H + +#include "context/cdhashmap.h" +#include "theory/arith/arith_state.h" +#include "theory/arith/inference_manager.h" +#include "theory/arith/operator_elim.h" +#include "theory/logic_info.h" + +namespace CVC4 { +namespace theory { +namespace arith { + +/** + * This module can be used for (on demand) elimination of extended arithmetic + * operators like div, mod, to_int, is_int, sqrt, and so on. It uses the + * operator elimination utility for determining how to reduce formulas. It + * extends that utility with the ability to generate lemmas on demand via + * the provided inference manager. + */ +class ArithPreprocess +{ + public: + ArithPreprocess(ArithState& state, + InferenceManager& im, + ProofNodeManager* pnm, + const LogicInfo& info); + ~ArithPreprocess() {} + /** + * Call eliminate operators on formula n, return the resulting trust node, + * which is of TrustNodeKind REWRITE and whose node is the result of + * eliminating extended operators from n. + */ + TrustNode eliminate(TNode n); + /** + * Reduce assertion. This sends a lemma via the inference manager if atom + * contains any extended operators. When applicable, the lemma is of the form: + * atom == d_opElim.eliminate(atom) + * This method returns true if a lemma of the above form was added to + * the inference manager. Note this returns true even if this lemma was added + * on a previous call. + */ + bool reduceAssertion(TNode atom); + /** + * Is the atom reduced? Returns true if a call to method reduceAssertion was + * made for the given atom and returned a lemma. In this case, the atom + * can be ignored. + */ + bool isReduced(TNode atom) const; + + private: + /** Reference to the inference manager */ + InferenceManager& d_im; + /** The operator elimination utility */ + OperatorElim d_opElim; + /** The set of assertions that were reduced */ + context::CDHashMap d_reduced; +}; + +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index bddc8ebcc..e2313e10a 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -45,7 +45,7 @@ TheoryArith::TheoryArith(context::Context* c, d_astate(*d_internal, c, u, valuation), d_inferenceManager(*this, d_astate, pnm), d_nonlinearExtension(nullptr), - d_opElim(pnm, logicInfo) + d_arithPreproc(d_astate, d_inferenceManager, pnm, logicInfo) { smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer); @@ -100,7 +100,7 @@ void TheoryArith::preRegisterTerm(TNode n) TrustNode TheoryArith::expandDefinition(Node node) { // call eliminate operators - return d_opElim.eliminate(node); + return d_arithPreproc.eliminate(node); } void TheoryArith::notifySharedTerm(TNode n) { d_internal->notifySharedTerm(n); } @@ -147,7 +147,7 @@ TrustNode TheoryArith::ppRewriteTerms(TNode n) // example, quantifier instantiation may use TO_INTEGER terms; SyGuS may // introduce non-standard arithmetic terms appearing in grammars. // call eliminate operators - return d_opElim.eliminate(n); + return d_arithPreproc.eliminate(n); } Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 6b279c9ed..b8f2b18fd 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -18,6 +18,7 @@ #pragma once #include "expr/node.h" +#include "theory/arith/arith_preprocess.h" #include "theory/arith/arith_rewriter.h" #include "theory/arith/arith_state.h" #include "theory/arith/inference_manager.h" @@ -144,8 +145,8 @@ class TheoryArith : public Theory { * arithmetic. */ std::unique_ptr d_nonlinearExtension; - /** The operator elimination utility */ - OperatorElim d_opElim; + /** The preprocess utility */ + ArithPreprocess d_arithPreproc; /** The theory rewriter for this theory. */ ArithRewriter d_rewriter; };/* class TheoryArith */ -- 2.30.2