diff options
| -rw-r--r-- | src/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/theory/arith/arith_preprocess.cpp | 68 | ||||
| -rw-r--r-- | src/theory/arith/arith_preprocess.h | 80 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith.cpp | 6 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith.h | 5 |
5 files changed, 156 insertions, 5 deletions
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<Node, bool, NodeHashFunction>::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<Node, bool, NodeHashFunction>::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<Node, bool, NodeHashFunction> 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<nl::NonlinearExtension> 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 */ |