1 files changed, 116 insertions, 0 deletions
diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h
new file mode 100644
index 000000000..1c0678e60
--- /dev/null
+++ b/src/theory/arith/inference_manager.h
@@ -0,0 +1,116 @@
+/*********************                                                        */
+/*! \file inference_manager.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** 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 Customized inference manager for the theory of nonlinear arithmetic
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__ARITH__INFERENCE_MANAGER_H
+#define CVC4__THEORY__ARITH__INFERENCE_MANAGER_H
+
+#include <map>
+#include <vector>
+
+#include "theory/arith/arith_lemma.h"
+#include "theory/arith/arith_state.h"
+#include "theory/arith/nl/inference.h"
+#include "theory/arith/nl/nl_lemma_utils.h"
+#include "theory/inference_manager_buffered.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class TheoryArith;
+
+/**
+ * A specialized variant of the InferenceManagerBuffered, tailored to the
+ * arithmetic theory.
+ *
+ * It adds some convenience methods to send ArithLemma and adds a mechanism for
+ * waiting lemmas that can be flushed into the pending lemmas of the this
+ * buffered inference manager.
+ * It also extends the caching mechanism of TheoryInferenceManager to cache
+ * preprocessing lemmas and non-preprocessing lemmas separately. For the former,
+ * it uses the cache provided by the TheoryInferenceManager base class.
+ */
+class InferenceManager : public InferenceManagerBuffered
+{
+  using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
+
+ public:
+  InferenceManager(TheoryArith& ta, ArithState& astate, ProofNodeManager* pnm);
+
+  /**
+   * Add a lemma as pending lemma to the this inference manager.
+   * If isWaiting is true, the lemma is first stored as waiting lemma and only
+   * added as pending lemma when calling flushWaitingLemmas.
+   */
+  void addPendingArithLemma(std::unique_ptr<ArithLemma> lemma,
+                            bool isWaiting = false);
+  /**
+   * Add a lemma as pending lemma to the this inference manager.
+   * If isWaiting is true, the lemma is first stored as waiting lemma and only
+   * added as pending lemma when calling flushWaitingLemmas.
+   */
+  void addPendingArithLemma(const ArithLemma& lemma, bool isWaiting = false);
+  /**
+   * Add a lemma as pending lemma to the this inference manager.
+   * If isWaiting is true, the lemma is first stored as waiting lemma and only
+   * added as pending lemma when calling flushWaitingLemmas.
+   */
+  void addPendingArithLemma(const Node& lemma,
+                            nl::Inference inftype,
+                            bool isWaiting = false);
+
+  /**
+   * Flush all waiting lemmas to the this inference manager (as pending
+   * lemmas). To actually send them, call doPendingLemmas() afterwards.
+   */
+  void flushWaitingLemmas();
+
+  /** Add a conflict to the this inference manager. */
+  void addConflict(const Node& conf, nl::Inference inftype);
+
+  /** Returns the number of pending lemmas. */
+  std::size_t numWaitingLemmas() const;
+
+  /** Checks whether the given lemma is already present in the cache. */
+  virtual bool hasCachedLemma(TNode lem, LemmaProperty p) override;
+
+ protected:
+  /**
+   * Adds the given lemma to the cache. Returns true if it has not been in the
+   * cache yet.
+   */
+  virtual bool cacheLemma(TNode lem, LemmaProperty p) override;
+
+ private:
+  /**
+   * Checks whether the lemma is entailed to be false. In this case, it is a
+   * conflict.
+   */
+  bool isEntailedFalse(const ArithLemma& lem);
+
+  /** The waiting lemmas. */
+  std::vector<std::unique_ptr<ArithLemma>> d_waitingLem;
+
+  /** cache of all preprocessed lemmas sent on the output channel
+   * (user-context-dependent) */
+  NodeSet d_lemmasPp;
+};
+
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
+
+#endif