src/theory/datatypes/inference_manager.h

   1 /*********************                                                        */
   2 /*! \file inference_manager.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   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 Datatypes inference manager
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__DATATYPES__INFERENCE_MANAGER_H
  18 #define CVC4__THEORY__DATATYPES__INFERENCE_MANAGER_H
  19
  20 #include "context/cdhashmap.h"
  21 #include "expr/node.h"
  22 #include "theory/inference_manager_buffered.h"
  23
  24 namespace CVC4 {
  25 namespace theory {
  26 namespace datatypes {
  27
  28 /**
  29  * A custom inference class. The main feature of this class is that it
  30  * dynamically decides whether to process itself as a fact or as a lemma,
  31  * based on the mustCommunicateFact method below.
  32  */
  33 class DatatypesInference : public SimpleTheoryInternalFact
  34 {
  35  public:
  36   DatatypesInference(Node conc, Node exp, ProofGenerator* pg);
  37   /**
  38    * Must communicate fact method.
  39    * The datatypes decision procedure makes "internal" inferences :
  40    *  (1) Unification : C( t1...tn ) = C( s1...sn ) => ti = si
  41    *  (2) Label : ~is_C1(t) ... ~is_C{i-1}(t) ~is_C{i+1}(t) ... ~is_Cn(t) =>
  42    * is_Ci( t )
  43    *  (3) Instantiate : is_C( t ) => t = C( sel_1( t ) ... sel_n( t ) )
  44    *  (4) collapse selector : S( C( t1...tn ) ) = t'
  45    *  (5) collapse term size : size( C( t1...tn ) ) = 1 + size( t1 ) + ... +
  46    * size( tn )
  47    *  (6) non-negative size : 0 <= size(t)
  48    * This method returns true if the fact must be sent out as a lemma. If it
  49    * returns false, then we assert the fact internally. We may need to
  50    * communicate outwards if the conclusions involve other theories.  Also
  51    * communicate (6) and OR conclusions.
  52    */
  53   static bool mustCommunicateFact(Node n, Node exp);
  54   /**
  55    * Process this fact, possibly as a fact or as a lemma, depending on the
  56    * above method.
  57    */
  58   bool process(TheoryInferenceManager* im) override;
  59 };
  60
  61 /**
  62  * The datatypes inference manager, which uses the above class for
  63  * inferences.
  64  */
  65 class InferenceManager : public InferenceManagerBuffered
  66 {
  67   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
  68
  69  public:
  70   InferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm);
  71   ~InferenceManager() {}
  72   /**
  73    * Add pending inference, which may be processed as either a fact or
  74    * a lemma based on mustCommunicateFact in DatatypesInference above.
  75    */
  76   void addPendingInference(Node conc, Node exp, ProofGenerator* pg = nullptr);
  77   /**
  78    * Process the current lemmas and facts. This is a custom method that can
  79    * be seen as overriding the behavior of calling both doPendingLemmas and
  80    * doPendingFacts. It determines whether facts should be sent as lemmas
  81    * or processed internally.
  82    */
  83   void process();
  84 };
  85
  86 }  // namespace datatypes
  87 }  // namespace theory
  88 }  // namespace CVC4
  89
  90 #endif