Branch data     Line data    Source code

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