Branch data     Line data    Source code

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