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   /** Add a conflict to the this inference manager. */
  82   void addConflict(const Node& conf, InferenceId inftype);
  83
  84   /**
  85    * Checks whether we have made any progress, that is whether a conflict, lemma
  86    * or fact was added or whether a lemma or fact is pending.
  87    */
  88   bool hasUsed() const;
  89
  90   /** Checks whether we have waiting lemmas. */
  91   bool hasWaitingLemma() const;
  92
  93   /** Returns the number of pending lemmas. */
  94   std::size_t numWaitingLemmas() const;
  95
  96   /** Checks whether the given lemma is already present in the cache. */
  97   virtual bool hasCachedLemma(TNode lem, LemmaProperty p) override;
  98
  99  protected:
 100   /**
 101    * Adds the given lemma to the cache. Returns true if it has not been in the
 102    * cache yet.
 103    */
 104   virtual bool cacheLemma(TNode lem, LemmaProperty p) override;
 105
 106  private:
 107   /**
 108    * Checks whether the lemma is entailed to be false. In this case, it is a
 109    * conflict.
 110    */
 111   bool isEntailedFalse(const ArithLemma& lem);
 112
 113   /** The waiting lemmas. */
 114   std::vector<std::unique_ptr<ArithLemma>> d_waitingLem;
 115
 116   /** cache of all preprocessed lemmas sent on the output channel
 117    * (user-context-dependent) */
 118   NodeSet d_lemmasPp;
 119 };
 120
 121 }  // namespace arith
 122 }  // namespace theory
 123 }  // namespace CVC4
 124
 125 #endif