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                 :            :  * Representative set class.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "cvc5_private.h"
      14                 :            : 
      15                 :            : #ifndef CVC5__THEORY__REP_SET_H
      16                 :            : #define CVC5__THEORY__REP_SET_H
      17                 :            : 
      18                 :            : #include <map>
      19                 :            : #include <vector>
      20                 :            : 
      21                 :            : #include "expr/node.h"
      22                 :            : #include "expr/type_node.h"
      23                 :            : 
      24                 :            : namespace cvc5::internal {
      25                 :            : namespace theory {
      26                 :            : 
      27                 :            : /** representative set
      28                 :            :  *
      29                 :            :  * This class contains finite lists of values for types, typically values and
      30                 :            :  * types that exist
      31                 :            :  * in the equality engine of a model object.  In the following, "representative"
      32                 :            :  * means a value that exists in this set.
      33                 :            :  *
      34                 :            :  * This class is used for finite model finding and other exhaustive
      35                 :            :  * instantiation-based
      36                 :            :  * methods. The class goes beyond just maintaining a list of values that occur
      37                 :            :  * in the equality engine in the following ways:
      38                 :            :  
      39                 :            :  * (1) It maintains a partial mapping from representatives to a term that has
      40                 :            :  * that value in the current
      41                 :            :  * model.  This is important because algorithms like the instantiation method in
      42                 :            :  * Reynolds et al CADE 2013
      43                 :            :  * act on "term models" where domains in models are interpreted as a set of
      44                 :            :  * representative terms. Hence,
      45                 :            :  * instead of instantiating with e.g. uninterpreted constants u, we instantiate
      46                 :            :  * with the corresponding term that is interpreted as u.
      47                 :            :  
      48                 :            :  * (2) It is mutable, calls to add(...) and complete(...) may modify this class
      49                 :            :  * as necessary, for instance
      50                 :            :  * in the case that there are no ground terms of a type that occurs in a
      51                 :            :  * quantified formula, or for
      52                 :            :  * exhaustive instantiation strategies that enumerate over small interpreted
      53                 :            :  * finite types.
      54                 :            :  */
      55                 :            : class RepSet {
      56                 :            :  public:
      57                 :      50263 :   RepSet(){}
      58                 :            : 
      59                 :            :   /** map from types to the list of representatives
      60                 :            :    * TODO : as part of #1199, encapsulate this
      61                 :            :    */
      62                 :            :   std::map< TypeNode, std::vector< Node > > d_type_reps;
      63                 :            :   /** clear the set */
      64                 :            :   void clear();
      65                 :            :   /** does this set have representatives of type tn? */
      66                 :      19543 :   bool hasType(TypeNode tn) const { return d_type_reps.count(tn) > 0; }
      67                 :            :   /** does this set have representative n of type tn? */
      68                 :            :   bool hasRep(TypeNode tn, Node n) const;
      69                 :            :   /** get the number of representatives for type */
      70                 :            :   size_t getNumRepresentatives(TypeNode tn) const;
      71                 :            :   /** get representative at index */
      72                 :            :   Node getRepresentative(TypeNode tn, unsigned i) const;
      73                 :            :   /**
      74                 :            :    * Returns the representatives of a type for a `type_node` if one exists.
      75                 :            :    * Otherwise, returns nullptr.
      76                 :            :    */
      77                 :            :   const std::vector<Node>* getTypeRepsOrNull(TypeNode type_node) const;
      78                 :            : 
      79                 :            :   /** add representative n for type tn, where n has type tn */
      80                 :            :   void add( TypeNode tn, Node n );
      81                 :            :   /** returns index in d_type_reps for node n */
      82                 :            :   int getIndexFor( Node n ) const;
      83                 :            :   /** complete the list for type t
      84                 :            :    * Resets d_type_reps[tn] and repopulates by running the type enumerator for
      85                 :            :    * that type exhaustively.
      86                 :            :    * This should only be called for small finite interpreted types.
      87                 :            :    */
      88                 :            :   bool complete( TypeNode t );
      89                 :            :   /** get term for representative
      90                 :            :    * Returns a term that is interpreted as representative n in the current
      91                 :            :    * model, null otherwise.
      92                 :            :    */
      93                 :            :   Node getTermForRepresentative(Node n) const;
      94                 :            :   /** set term for representative
      95                 :            :    * Called when t is interpreted as value n. Subsequent class to
      96                 :            :    * getTermForRepresentative( n ) will return t.
      97                 :            :    */
      98                 :            :   void setTermForRepresentative(Node n, Node t);
      99                 :            :   /** get existing domain value, with possible exclusions
     100                 :            :     *   This function returns a term in d_type_reps[tn] but not in exclude
     101                 :            :     */
     102                 :            :   Node getDomainValue(TypeNode tn, const std::vector<Node>& exclude) const;
     103                 :            :   /** debug print */
     104                 :            :   void toStream(std::ostream& out);
     105                 :            : 
     106                 :            :  private:
     107                 :            :   /** whether the list of representatives for types are complete */
     108                 :            :   std::map<TypeNode, bool> d_type_complete;
     109                 :            :   /** map from representatives to their index in d_type_reps */
     110                 :            :   std::map<Node, int> d_tmap;
     111                 :            :   /** map from values to terms they were assigned for */
     112                 :            :   std::map<Node, Node> d_values_to_terms;
     113                 :            : };/* class RepSet */
     114                 :            : 
     115                 :            : 
     116                 :            : }  // namespace theory
     117                 :            : }  // namespace cvc5::internal
     118                 :            : 
     119                 :            : #endif /* CVC5__THEORY__REP_SET_H */