src/theory/arith/inference_manager.h

   1 /*********************                                                        */
   2 /*! \file inference_manager.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Gereon Kremer
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Customized inference manager for the theory of nonlinear arithmetic
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__ARITH__INFERENCE_MANAGER_H
  18 #define CVC4__THEORY__ARITH__INFERENCE_MANAGER_H
  19
  20 #include <map>
  21 #include <vector>
  22
  23 #include "theory/arith/arith_lemma.h"
  24 #include "theory/arith/arith_state.h"
  25 #include "theory/arith/inference_id.h"
  26 #include "theory/arith/nl/nl_lemma_utils.h"
  27 #include "theory/inference_manager_buffered.h"
  28
  29 namespace CVC4 {
  30 namespace theory {
  31 namespace arith {
  32
  33 class TheoryArith;
  34
  35 /**
  36  * A specialized variant of the InferenceManagerBuffered, tailored to the
  37  * arithmetic theory.
  38  *
  39  * It adds some convenience methods to send ArithLemma and adds a mechanism for
  40  * waiting lemmas that can be flushed into the pending lemmas of the this
  41  * buffered inference manager.
  42  * It also extends the caching mechanism of TheoryInferenceManager to cache
  43  * preprocessing lemmas and non-preprocessing lemmas separately. For the former,
  44  * it uses the cache provided by the TheoryInferenceManager base class.
  45  */
  46 class InferenceManager : public InferenceManagerBuffered
  47 {
  48   using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
  49
  50  public:
  51   InferenceManager(TheoryArith& ta, ArithState& astate, ProofNodeManager* pnm);
  52
  53   /**
  54    * Add a lemma as pending lemma to the this inference manager.
  55    * If isWaiting is true, the lemma is first stored as waiting lemma and only
  56    * added as pending lemma when calling flushWaitingLemmas.
  57    */
  58   void addPendingArithLemma(std::unique_ptr<ArithLemma> lemma,
  59                             bool isWaiting = false);
  60   /**
  61    * Add a lemma as pending lemma to the this inference manager.
  62    * If isWaiting is true, the lemma is first stored as waiting lemma and only
  63    * added as pending lemma when calling flushWaitingLemmas.
  64    */
  65   void addPendingArithLemma(const ArithLemma& lemma, bool isWaiting = false);
  66   /**
  67    * Add a lemma as pending lemma to the this inference manager.
  68    * If isWaiting is true, the lemma is first stored as waiting lemma and only
  69    * added as pending lemma when calling flushWaitingLemmas.
  70    */
  71   void addPendingArithLemma(const Node& lemma,
  72                             InferenceId inftype,
  73                             bool isWaiting = false);
  74
  75   /**
  76    * Flush all waiting lemmas to the this inference manager (as pending
  77    * lemmas). To actually send them, call doPendingLemmas() afterwards.
  78    */
  79   void flushWaitingLemmas();
  80
  81   /**
  82    * Removes all waiting lemmas without sending them anywhere.
  83    */
  84   void clearWaitingLemmas();
  85
  86   /** Add a conflict to the this inference manager. */
  87   void addConflict(const Node& conf, InferenceId inftype);
  88
  89   /**
  90    * Checks whether we have made any progress, that is whether a conflict, lemma
  91    * or fact was added or whether a lemma or fact is pending.
  92    */
  93   bool hasUsed() const;
  94
  95   /** Checks whether we have waiting lemmas. */
  96   bool hasWaitingLemma() const;
  97
  98   /** Returns the number of pending lemmas. */
  99   std::size_t numWaitingLemmas() const;
 100
 101   /** Checks whether the given lemma is already present in the cache. */
 102   virtual bool hasCachedLemma(TNode lem, LemmaProperty p) override;
 103
 104  protected:
 105   /**
 106    * Adds the given lemma to the cache. Returns true if it has not been in the
 107    * cache yet.
 108    */
 109   virtual bool cacheLemma(TNode lem, LemmaProperty p) override;
 110
 111  private:
 112   /**
 113    * Checks whether the lemma is entailed to be false. In this case, it is a
 114    * conflict.
 115    */
 116   bool isEntailedFalse(const ArithLemma& lem);
 117
 118   /** The waiting lemmas. */
 119   std::vector<std::unique_ptr<ArithLemma>> d_waitingLem;
 120
 121   /** cache of all preprocessed lemmas sent on the output channel
 122    * (user-context-dependent) */
 123   NodeSet d_lemmasPp;
 124 };
 125
 126 }  // namespace arith
 127 }  // namespace theory
 128 }  // namespace CVC4
 129
 130 #endif