Branch data     Line data    Source code

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