src/theory/ee_setup_info.h

   1 /*********************                                                        */
   2 /*! \file ee_setup_info.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 Setup information for an equality engine.
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__EE_SETUP_INFO__H
  18 #define CVC4__THEORY__EE_SETUP_INFO__H
  19
  20 #include <string>
  21
  22 namespace CVC4 {
  23 namespace theory {
  24
  25 namespace eq {
  26 class EqualityEngineNotify;
  27 }
  28
  29 /**
  30  * This is a helper class that encapsulates instructions for how a Theory
  31  * wishes to initialize and setup notifications with its official equality
  32  * engine, e.g. via a notification class (eq::EqualityEngineNotify).
  33  *
  34  * This includes (at a basic level) the arguments to the equality engine
  35  * constructor that theories may wish to modify. This information is determined
  36  * by the Theory during needsEqualityEngine.
  37  */
  38 struct EeSetupInfo
  39 {
  40   EeSetupInfo() : d_notify(nullptr), d_constantsAreTriggers(true) {}
  41   /** The notification class of the theory */
  42   eq::EqualityEngineNotify* d_notify;
  43   /** The name of the equality engine */
  44   std::string d_name;
  45   /** Constants are triggers */
  46   bool d_constantsAreTriggers;
  47 };
  48
  49 }  // namespace theory
  50 }  // namespace CVC4
  51
  52 #endif /* CVC4__THEORY__EE_SETUP_INFO__H */