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                 :            :  * [[ Add lengthier description here ]]
      11                 :            :  * \todo document this file
      12                 :            :  */
      13                 :            : 
      14                 :            : #include "cvc5_private.h"
      15                 :            : 
      16                 :            : #pragma once
      17                 :            : 
      18                 :            : #include <unordered_map>
      19                 :            : 
      20                 :            : #include "context/context.h"
      21                 :            : #include "smt/env_obj.h"
      22                 :            : #include "theory/shared_terms_database.h"
      23                 :            : 
      24                 :            : namespace cvc5::internal {
      25                 :            : 
      26                 :            : class TheoryEngine;
      27                 :            : 
      28                 :            : /**
      29                 :            :  * Visitor that calls the appropriate theory to pre-register the term. The
      30                 :            :  * visitor also keeps track of the sets of theories that are involved in the
      31                 :            :  * terms, so that it can say if there are multiple theories involved.
      32                 :            :  *
      33                 :            :  * A sub-term has been visited if the theories of both the parent and the term
      34                 :            :  * itself have already visited this term.
      35                 :            :  *
      36                 :            :  * Computation of the set of theories in the original term are computed in the
      37                 :            :  * alreadyVisited method so as no to skip any theories.
      38                 :            :  */
      39                 :            : class PreRegisterVisitor : protected EnvObj
      40                 :            : {
      41                 :            :   /** The engine */
      42                 :            :   TheoryEngine* d_engine;
      43                 :            : 
      44                 :            :   typedef context::CDHashMap<TNode, theory::TheoryIdSet> TNodeToTheorySetMap;
      45                 :            : 
      46                 :            :   /**
      47                 :            :    * Map from terms to the theories that have already had this term
      48                 :            :    * pre-registered.
      49                 :            :    */
      50                 :            :   TNodeToTheorySetMap d_visited;
      51                 :            : 
      52                 :            :   /**
      53                 :            :    * String representation of the visited map, for debugging purposes.
      54                 :            :    */
      55                 :            :   std::string toString() const;
      56                 :            : 
      57                 :            :  public:
      58                 :            :   /** required to instantiate template for NodeVisitor */
      59                 :            :   using return_type = void;
      60                 :            : 
      61                 :            :   PreRegisterVisitor(Env& env, TheoryEngine* engine);
      62                 :            : 
      63                 :            :   /**
      64                 :            :    * Returns true is current has already been pre-registered with both current
      65                 :            :    * and parent theories.
      66                 :            :    */
      67                 :            :   bool alreadyVisited(TNode current, TNode parent);
      68                 :            : 
      69                 :            :   /**
      70                 :            :    * Pre-registeres current with any of the current and parent theories that
      71                 :            :    * haven't seen the term yet.
      72                 :            :    */
      73                 :            :   void visit(TNode current, TNode parent);
      74                 :            : 
      75                 :            :   /**
      76                 :            :    * Marks the node as the starting literal, which does nothing. This method
      77                 :            :    * is required to instantiate template for NodeVisitor.
      78                 :            :    */
      79                 :            :   void start(TNode node);
      80                 :            : 
      81                 :            :   /** Called when the visitor is finished with a term, do nothing */
      82                 :   13679494 :   void done(CVC5_UNUSED TNode node) {}
      83                 :            : 
      84                 :            :   /**
      85                 :            :    * Preregister the term current occuring under term parent.  This calls
      86                 :            :    * Theory::preRegisterTerm for the theories of current and parent, as well
      87                 :            :    * as the theory of current's type, if it is finite.
      88                 :            :    *
      89                 :            :    * This method takes a set of theories visitedTheories that have already
      90                 :            :    * preregistered current and updates this set with the theories that
      91                 :            :    * preregister current during this call
      92                 :            :    *
      93                 :            :    * @param te Pointer to the theory engine containing the theories
      94                 :            :    * @param visitedTheories The theories that have already preregistered current
      95                 :            :    * @param current The term to preregister
      96                 :            :    * @param parent The parent term of current
      97                 :            :    * @param preregTheories The theories that have already preregistered current.
      98                 :            :    * If there is no theory sharing, this coincides with visitedTheories.
      99                 :            :    * Otherwise, visitedTheories may be a subset of preregTheories.
     100                 :            :    */
     101                 :            :   static void preRegister(Env& env,
     102                 :            :                           TheoryEngine* te,
     103                 :            :                           theory::TheoryIdSet& visitedTheories,
     104                 :            :                           TNode current,
     105                 :            :                           TNode parent,
     106                 :            :                           theory::TheoryIdSet preregTheories);
     107                 :            : 
     108                 :            :  private:
     109                 :            :   /**
     110                 :            :    * Helper for above, called whether we wish to register a term with a theory
     111                 :            :    * given by an identifier id.
     112                 :            :    */
     113                 :            :   static void preRegisterWithTheory(TheoryEngine* te,
     114                 :            :                                     theory::TheoryIdSet& visitedTheories,
     115                 :            :                                     theory::TheoryId id,
     116                 :            :                                     TNode current,
     117                 :            :                                     TNode parent,
     118                 :            :                                     theory::TheoryIdSet preregTheories);
     119                 :            : };
     120                 :            : 
     121                 :            : /**
     122                 :            :  * The reason why we need to make this outside of the pre-registration loop is
     123                 :            :  * because we need a shared term x to be associated with every atom that
     124                 :            :  * contains it. For example, if given f(x) >= 0 and f(x) + 1 >= 0, although f(x)
     125                 :            :  * has been visited already, we need to visit it again, since we need to
     126                 :            :  * associate it with both atoms.
     127                 :            :  */
     128                 :            : class SharedTermsVisitor : protected EnvObj
     129                 :            : {
     130                 :            :   using TNodeVisitedMap = std::unordered_map<TNode, theory::TheoryIdSet>;
     131                 :            :   using TNodeToTheorySetMap = context::CDHashMap<TNode, theory::TheoryIdSet>;
     132                 :            :   /**
     133                 :            :    * String representation of the visited map, for debugging purposes.
     134                 :            :    */
     135                 :            :   std::string toString() const;
     136                 :            : 
     137                 :            :   /**
     138                 :            :    * The initial atom.
     139                 :            :    */
     140                 :            :   TNode d_atom;
     141                 :            : 
     142                 :            :  public:
     143                 :            :   /** required to instantiate template for NodeVisitor */
     144                 :            :   using return_type = void;
     145                 :            : 
     146                 :            :   SharedTermsVisitor(Env& env,
     147                 :            :                      TheoryEngine* te,
     148                 :            :                      SharedTermsDatabase& sharedTerms);
     149                 :            : 
     150                 :            :   /**
     151                 :            :    * Returns true is current has already been pre-registered with both current
     152                 :            :    * and parent theories.
     153                 :            :    */
     154                 :            :   bool alreadyVisited(TNode current, TNode parent) const;
     155                 :            : 
     156                 :            :   /**
     157                 :            :    * Pre-registeres current with any of the current and parent theories that
     158                 :            :    * haven't seen the term yet.
     159                 :            :    */
     160                 :            :   void visit(TNode current, TNode parent);
     161                 :            : 
     162                 :            :   /**
     163                 :            :    * Marks the node as the starting literal, which clears the state.
     164                 :            :    */
     165                 :            :   void start(TNode node);
     166                 :            : 
     167                 :            :   /**
     168                 :            :    * Just clears the state.
     169                 :            :    */
     170                 :            :   void done(TNode node);
     171                 :            : 
     172                 :            :   /**
     173                 :            :    * Clears the internal state.
     174                 :            :    */
     175                 :            :   void clear();
     176                 :            : 
     177                 :            :  private:
     178                 :            :   /** The engine */
     179                 :            :   TheoryEngine* d_engine;
     180                 :            :   /** The shared terms database */
     181                 :            :   SharedTermsDatabase& d_sharedTerms;
     182                 :            :   /** Cache of nodes we have visited in this traversal */
     183                 :            :   TNodeVisitedMap d_visited;
     184                 :            :   /** (Global) cache of nodes we have preregistered in this SAT context */
     185                 :            :   TNodeToTheorySetMap d_preregistered;
     186                 :            : };
     187                 :            : 
     188                 :            : }  // namespace cvc5::internal