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.
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
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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
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);
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); }
// 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) {
#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"
* 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 */
projects / cvc5.git / commitdiff