Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Aina Niemetz
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2024 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.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * Setup information for an equality engine.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "cvc5_private.h"
      17                 :            : 
      18                 :            : #ifndef CVC5__THEORY__EE_SETUP_INFO__H
      19                 :            : #define CVC5__THEORY__EE_SETUP_INFO__H
      20                 :            : 
      21                 :            : #include <string>
      22                 :            : 
      23                 :            : namespace cvc5::internal {
      24                 :            : namespace theory {
      25                 :            : 
      26                 :            : namespace eq {
      27                 :            : class EqualityEngineNotify;
      28                 :            : }
      29                 :            : 
      30                 :            : /**
      31                 :            :  * This is a helper class that encapsulates instructions for how a Theory
      32                 :            :  * wishes to initialize and setup notifications with its official equality
      33                 :            :  * engine, e.g. via a notification class (eq::EqualityEngineNotify).
      34                 :            :  *
      35                 :            :  * This includes (at a basic level) the arguments to the equality engine
      36                 :            :  * constructor that theories may wish to modify. This information is determined
      37                 :            :  * by the Theory during needsEqualityEngine.
      38                 :            :  */
      39                 :            : struct EeSetupInfo
      40                 :            : {
      41                 :     786752 :   EeSetupInfo()
      42                 :     786752 :       : d_notify(nullptr),
      43                 :            :         d_constantsAreTriggers(true),
      44                 :            :         d_notifyNewClass(false),
      45                 :            :         d_notifyMerge(false),
      46                 :            :         d_notifyDisequal(false),
      47                 :     786752 :         d_useMaster(false)
      48                 :            :   {
      49                 :     786752 :   }
      50                 :            :   /** The notification class of the theory */
      51                 :            :   eq::EqualityEngineNotify* d_notify;
      52                 :            :   /** The name of the equality engine */
      53                 :            :   std::string d_name;
      54                 :            :   /** Constants are triggers */
      55                 :            :   bool d_constantsAreTriggers;
      56                 :            :   //-------------------------- fine grained notifications
      57                 :            :   /** Whether we need to be notified of new equivalence classes */
      58                 :            :   bool d_notifyNewClass;
      59                 :            :   /** Whether we need to be notified of merged equivalence classes */
      60                 :            :   bool d_notifyMerge;
      61                 :            :   /** Whether we need to be notified of disequal equivalence classes */
      62                 :            :   bool d_notifyDisequal;
      63                 :            :   //-------------------------- end fine grained notifications
      64                 :            :   /**
      65                 :            :    * Whether we want our state to use the master equality engine. This should
      66                 :            :    * be true exclusively for the theory of quantifiers.
      67                 :            :    */
      68                 :            :   bool d_useMaster;
      69                 :            :   /** Does it need notifications when equivalence classes are created? */
      70                 :        590 :   bool needsNotifyNewClass() const { return d_notifyNewClass; }
      71                 :            :   /** Does it need notifications when equivalence classes are merged? */
      72                 :        590 :   bool needsNotifyMerge() const { return d_notifyMerge; }
      73                 :            :   /** Does it need notifications when disequalities are generated? */
      74                 :        590 :   bool needsNotifyDisequal() const { return d_notifyDisequal; }
      75                 :            : };
      76                 :            : 
      77                 :            : }  // namespace theory
      78                 :            : }  // namespace cvc5::internal
      79                 :            : 
      80                 :            : #endif /* CVC5__THEORY__EE_SETUP_INFO__H */