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                 :            :  * quantifier module
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "cvc5_private.h"
      14                 :            : 
      15                 :            : #ifndef CVC5__THEORY__QUANTIFIERS__QUANT_MODULE_H
      16                 :            : #define CVC5__THEORY__QUANTIFIERS__QUANT_MODULE_H
      17                 :            : 
      18                 :            : #include <iostream>
      19                 :            : #include <map>
      20                 :            : #include <vector>
      21                 :            : 
      22                 :            : #include "smt/env_obj.h"
      23                 :            : #include "theory/quantifiers/quantifiers_inference_manager.h"
      24                 :            : #include "theory/quantifiers/quantifiers_registry.h"
      25                 :            : #include "theory/quantifiers/quantifiers_state.h"
      26                 :            : #include "theory/quantifiers/term_registry.h"
      27                 :            : #include "theory/theory.h"
      28                 :            : #include "theory/uf/equality_engine.h"
      29                 :            : 
      30                 :            : namespace cvc5::internal {
      31                 :            : namespace theory {
      32                 :            : namespace quantifiers {
      33                 :            : class TermDb;
      34                 :            : 
      35                 :            : /** QuantifiersModule class
      36                 :            :  *
      37                 :            :  * This is the virtual class for defining subsolvers of the quantifiers theory.
      38                 :            :  * It has a similar interface to a Theory object.
      39                 :            :  */
      40                 :            : class QuantifiersModule : protected EnvObj
      41                 :            : {
      42                 :            :  public:
      43                 :            :   /** effort levels for quantifiers modules check */
      44                 :            :   enum QEffort
      45                 :            :   {
      46                 :            :     // conflict effort, for conflict-based instantiation
      47                 :            :     QEFFORT_CONFLICT,
      48                 :            :     // standard effort, for heuristic instantiation
      49                 :            :     QEFFORT_STANDARD,
      50                 :            :     // model effort, for model-based instantiation
      51                 :            :     QEFFORT_MODEL,
      52                 :            :     // last call effort, for last resort techniques
      53                 :            :     QEFFORT_LAST_CALL,
      54                 :            :     // none
      55                 :            :     QEFFORT_NONE,
      56                 :            :   };
      57                 :            : 
      58                 :            :  public:
      59                 :            :   QuantifiersModule(Env& env,
      60                 :            :                     quantifiers::QuantifiersState& qs,
      61                 :            :                     quantifiers::QuantifiersInferenceManager& qim,
      62                 :            :                     quantifiers::QuantifiersRegistry& qr,
      63                 :            :                     quantifiers::TermRegistry& tr);
      64                 :     277659 :   virtual ~QuantifiersModule() {}
      65                 :            :   /** Presolve.
      66                 :            :    *
      67                 :            :    * Called at the beginning of check-sat call.
      68                 :            :    */
      69                 :     137180 :   virtual void presolve() {}
      70                 :            :   /** Needs check.
      71                 :            :    *
      72                 :            :    * Returns true if this module wishes a call to be made
      73                 :            :    * to check(e) during QuantifiersEngine::check(e).
      74                 :            :    */
      75                 :          0 :   virtual bool needsCheck(Theory::Effort e)
      76                 :            :   {
      77                 :          0 :     return e >= Theory::EFFORT_LAST_CALL;
      78                 :            :   }
      79                 :            :   /** Needs model.
      80                 :            :    *
      81                 :            :    * Whether this module needs a model built during a
      82                 :            :    * call to QuantifiersEngine::check(e)
      83                 :            :    * It returns one of QEFFORT_* from the enumeration above.
      84                 :            :    * which specifies the quantifiers effort in which it requires the model to
      85                 :            :    * be built.
      86                 :            :    */
      87                 :            :   virtual QEffort needsModel(Theory::Effort e);
      88                 :            :   /** Reset.
      89                 :            :    *
      90                 :            :    * Called at the beginning of QuantifiersEngine::check(e).
      91                 :            :    */
      92                 :     116108 :   virtual void reset_round(CVC5_UNUSED Theory::Effort e) {}
      93                 :            :   /** Check.
      94                 :            :    *
      95                 :            :    *   Called during QuantifiersEngine::check(e) depending
      96                 :            :    *   if needsCheck(e) returns true.
      97                 :            :    */
      98                 :            :   virtual void check(Theory::Effort e, QEffort quant_e) = 0;
      99                 :            :   /** Check complete?
     100                 :            :    *
     101                 :            :    * Returns false if the module's reasoning was globally incomplete
     102                 :            :    * (e.g. "sat" must be replaced with "incomplete").
     103                 :            :    *
     104                 :            :    * This is called just before the quantifiers engine will return
     105                 :            :    * with no lemmas added during a LAST_CALL effort check.
     106                 :            :    *
     107                 :            :    * If this method returns false, it should update incId to the reason for
     108                 :            :    * why the module was incomplete.
     109                 :            :    */
     110                 :      37476 :   virtual bool checkComplete(CVC5_UNUSED IncompleteId& incId) { return true; }
     111                 :            :   /** Check was complete for quantified formula q
     112                 :            :    *
     113                 :            :    * If for each quantified formula q, some module returns true for
     114                 :            :    * checkCompleteFor( q ),
     115                 :            :    * and no lemmas are added by the quantifiers theory, then we may answer
     116                 :            :    * "sat", unless
     117                 :            :    * we are incomplete for other reasons.
     118                 :            :    */
     119                 :      12760 :   virtual bool checkCompleteFor(CVC5_UNUSED Node q) { return false; }
     120                 :            :   /** Check ownership
     121                 :            :    *
     122                 :            :    * Called once for new quantified formulas that are registered by the
     123                 :            :    * quantifiers theory. The primary purpose of this function is to establish
     124                 :            :    * if this module is the owner of quantified formula q.
     125                 :            :    */
     126                 :      90569 :   virtual void checkOwnership(CVC5_UNUSED Node q) {}
     127                 :            :   /** Register quantifier
     128                 :            :    *
     129                 :            :    * Called once for new quantified formulas q that are pre-registered by the
     130                 :            :    * quantifiers theory, after internal ownership of quantified formulas is
     131                 :            :    * finalized. This does context-independent initialization of this module
     132                 :            :    * for quantified formula q.
     133                 :            :    */
     134                 :     122974 :   virtual void registerQuantifier(CVC5_UNUSED Node q) {}
     135                 :            :   /** Pre-register quantifier
     136                 :            :    *
     137                 :            :    * Called once for new quantified formulas that are
     138                 :            :    * pre-registered by the quantifiers theory, after
     139                 :            :    * internal ownership of quantified formulas is finalized.
     140                 :            :    */
     141                 :     255927 :   virtual void preRegisterQuantifier(CVC5_UNUSED Node q) {}
     142                 :            :   /** Assert node.
     143                 :            :    *
     144                 :            :    * Called when a quantified formula q is asserted to the quantifiers theory
     145                 :            :    */
     146                 :     581651 :   virtual void assertNode(CVC5_UNUSED Node q) {}
     147                 :            :   /** notify preprocessed assertion */
     148                 :     309746 :   virtual void ppNotifyAssertions(
     149                 :            :       CVC5_UNUSED const std::vector<Node>& assertions)
     150                 :            :   {
     151                 :     309746 :   }
     152                 :            :   /**
     153                 :            :    * Identify this module (for debugging, dynamic configuration, etc..).
     154                 :            :    * This name is printed in -o inst-strategy.
     155                 :            :    */
     156                 :            :   virtual std::string identify() const = 0;
     157                 :            :   //----------------------------general queries
     158                 :            :   /** get currently used the equality engine */
     159                 :            :   eq::EqualityEngine* getEqualityEngine() const;
     160                 :            :   /** are n1 and n2 equal in the current used equality engine? */
     161                 :            :   bool areEqual(TNode n1, TNode n2) const;
     162                 :            :   /** are n1 and n2 disequal in the current used equality engine? */
     163                 :            :   bool areDisequal(TNode n1, TNode n2) const;
     164                 :            :   /** get the representative of n in the current used equality engine */
     165                 :            :   TNode getRepresentative(TNode n) const;
     166                 :            :   /** get currently used term database */
     167                 :            :   quantifiers::TermDb* getTermDatabase() const;
     168                 :            :   /** get the quantifiers state */
     169                 :            :   quantifiers::QuantifiersState& getState();
     170                 :            :   /** get the quantifiers inference manager */
     171                 :            :   quantifiers::QuantifiersInferenceManager& getInferenceManager();
     172                 :            :   /** get the quantifiers registry */
     173                 :            :   quantifiers::QuantifiersRegistry& getQuantifiersRegistry();
     174                 :            :   /** get the term registry */
     175                 :            :   quantifiers::TermRegistry& getTermRegistry();
     176                 :            :   //----------------------------end general queries
     177                 :            :  protected:
     178                 :            :   /** Begin debug call for -t inst-strategy and -o inst-strategy */
     179                 :            :   void beginCallDebug();
     180                 :            :   /** End debug call for -t inst-strategy and -o inst-strategy */
     181                 :            :   void endCallDebug();
     182                 :            :   /** Reference to the state of the quantifiers engine */
     183                 :            :   quantifiers::QuantifiersState& d_qstate;
     184                 :            :   /** Reference to the quantifiers inference manager */
     185                 :            :   quantifiers::QuantifiersInferenceManager& d_qim;
     186                 :            :   /** Reference to the quantifiers registry */
     187                 :            :   quantifiers::QuantifiersRegistry& d_qreg;
     188                 :            :   /** Reference to the term registry */
     189                 :            :   quantifiers::TermRegistry& d_treg;
     190                 :            : }; /* class QuantifiersModule */
     191                 :            : 
     192                 :            : }  // namespace quantifiers
     193                 :            : }  // namespace theory
     194                 :            : }  // namespace cvc5::internal
     195                 :            : 
     196                 :            : #endif /* CVC5__THEORY__QUANTIFIERS__QUANT_MODULE_H */