src/theory/rep_set.h

   1 /*********************                                                        */
   2 /*! \file rep_set.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Tim King, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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.\endverbatim
  11  **
  12  ** \brief Representative set class and utilities
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__REP_SET_H
  18 #define CVC4__THEORY__REP_SET_H
  19
  20 #include <map>
  21 #include <vector>
  22
  23 #include "expr/node.h"
  24 #include "expr/type_node.h"
  25
  26 namespace CVC4 {
  27 namespace theory {
  28
  29 class QuantifiersEngine;
  30
  31 /** representative set
  32  *
  33  * This class contains finite lists of values for types, typically values and
  34  * types that exist
  35  * in the equality engine of a model object.  In the following, "representative"
  36  * means a value that exists in this set.
  37  *
  38  * This class is used for finite model finding and other exhaustive
  39  * instantiation-based
  40  * methods. The class goes beyond just maintaining a list of values that occur
  41  * in the equality engine in the following ways:
  42
  43  * (1) It maintains a partial mapping from representatives to a term that has
  44  * that value in the current
  45  * model.  This is important because algorithms like the instantiation method in
  46  * Reynolds et al CADE 2013
  47  * act on "term models" where domains in models are interpreted as a set of
  48  * representative terms. Hence,
  49  * instead of instantiating with e.g. uninterpreted constants u, we instantiate
  50  * with the corresponding term that is interpreted as u.
  51
  52  * (2) It is mutable, calls to add(...) and complete(...) may modify this class
  53  * as necessary, for instance
  54  * in the case that there are no ground terms of a type that occurs in a
  55  * quantified formula, or for
  56  * exhaustive instantiation strategies that enumerate over small interpreted
  57  * finite types.
  58  */
  59 class RepSet {
  60  public:
  61   RepSet(){}
  62
  63   /** map from types to the list of representatives
  64    * TODO : as part of #1199, encapsulate this
  65    */
  66   std::map< TypeNode, std::vector< Node > > d_type_reps;
  67   /** clear the set */
  68   void clear();
  69   /** does this set have representatives of type tn? */
  70   bool hasType(TypeNode tn) const { return d_type_reps.count(tn) > 0; }
  71   /** does this set have representative n of type tn? */
  72   bool hasRep(TypeNode tn, Node n) const;
  73   /** get the number of representatives for type */
  74   size_t getNumRepresentatives(TypeNode tn) const;
  75   /** get representative at index */
  76   Node getRepresentative(TypeNode tn, unsigned i) const;
  77   /**
  78    * Returns the representatives of a type for a `type_node` if one exists.
  79    * Otherwise, returns nullptr.
  80    */
  81   const std::vector<Node>* getTypeRepsOrNull(TypeNode type_node) const;
  82
  83   /** add representative n for type tn, where n has type tn */
  84   void add( TypeNode tn, Node n );
  85   /** returns index in d_type_reps for node n */
  86   int getIndexFor( Node n ) const;
  87   /** complete the list for type t
  88    * Resets d_type_reps[tn] and repopulates by running the type enumerator for
  89    * that type exhaustively.
  90    * This should only be called for small finite interpreted types.
  91    */
  92   bool complete( TypeNode t );
  93   /** get term for representative
  94    * Returns a term that is interpreted as representative n in the current
  95    * model, null otherwise.
  96    */
  97   Node getTermForRepresentative(Node n) const;
  98   /** set term for representative
  99    * Called when t is interpreted as value n. Subsequent class to
 100    * getTermForRepresentative( n ) will return t.
 101    */
 102   void setTermForRepresentative(Node n, Node t);
 103   /** get existing domain value, with possible exclusions
 104     *   This function returns a term in d_type_reps[tn] but not in exclude
 105     */
 106   Node getDomainValue(TypeNode tn, const std::vector<Node>& exclude) const;
 107   /** debug print */
 108   void toStream(std::ostream& out);
 109
 110  private:
 111   /** whether the list of representatives for types are complete */
 112   std::map<TypeNode, bool> d_type_complete;
 113   /** map from representatives to their index in d_type_reps */
 114   std::map<Node, int> d_tmap;
 115   /** map from values to terms they were assigned for */
 116   std::map<Node, Node> d_values_to_terms;
 117 };/* class RepSet */
 118
 119 //representative domain
 120 typedef std::vector< int > RepDomain;
 121
 122 class RepBoundExt;
 123
 124 /**
 125  * Representative set iterator enumeration type, which indicates how the
 126  * bound on a variable was determined.
 127  */
 128 enum RsiEnumType
 129 {
 130   // the bound on the variable is invalid
 131   ENUM_INVALID = 0,
 132   // the bound on the variable was determined in the default way, i.e. based
 133   // on an enumeration of terms in the model.
 134   ENUM_DEFAULT,
 135   // The bound on the variable was determined in a custom way, i.e. via a
 136   // quantifiers module like the BoundedIntegers module.
 137   ENUM_CUSTOM,
 138 };
 139
 140 /** Rep set iterator.
 141  *
 142  * This class is used for iterating over (tuples of) terms
 143  * in the domain(s) of a RepSet.
 144  *
 145  * To use it, first it must
 146  * be initialized with a call to:
 147  * - setQuantifier or setFunctionDomain
 148  * which initializes the d_owner field and sets up
 149  * initial information.
 150  *
 151  * Then, we increment over the tuples of terms in the
 152  * domains of the owner of this iterator using:
 153  * - increment and incrementAtIndex
 154  *
 155  * TODO (#1199): this class needs further documentation.
 156  */
 157 class RepSetIterator {
 158 public:
 159  RepSetIterator(const RepSet* rs, RepBoundExt* rext = nullptr);
 160  ~RepSetIterator() {}
 161  /** set that this iterator will be iterating over instantiations for a
 162   * quantifier */
 163  bool setQuantifier(Node q);
 164  /** set that this iterator will be iterating over the domain of a function */
 165  bool setFunctionDomain(Node op);
 166  /** increment the iterator */
 167  int increment();
 168  /** increment the iterator at index
 169   * This increments the i^th field of the
 170   * iterator, for examples, see operator next_i
 171   * in Figure 2 of Reynolds et al. CADE 2013.
 172   */
 173  int incrementAtIndex(int i);
 174  /** is the iterator finished? */
 175  bool isFinished() const;
 176  /** get domain size of the i^th field of this iterator */
 177  unsigned domainSize(unsigned i);
 178  /** Get the type of terms in the i^th field of this iterator */
 179  TypeNode getTypeOf(unsigned i) const;
 180  /**
 181   * Get the value for the i^th field in the tuple we are currently considering.
 182   * If valTerm is true, we return a term instead of a value by calling
 183   * RepSet::getTermForRepresentative on the value.
 184   */
 185  Node getCurrentTerm(unsigned i, bool valTerm = false) const;
 186  /** get the number of terms in the tuple we are considering */
 187  unsigned getNumTerms() const { return d_index_order.size(); }
 188  /** get current terms */
 189  void getCurrentTerms(std::vector<Node>& terms) const;
 190  /** get index order, returns var # */
 191  unsigned getIndexOrder(unsigned v) { return d_index_order[v]; }
 192  /** get variable order, returns index # */
 193  unsigned getVariableOrder(unsigned i) { return d_var_order[i]; }
 194  /** is incomplete
 195   * Returns true if we are iterating over a strict subset of
 196   * the domain of the quantified formula or function.
 197   */
 198  bool isIncomplete() { return d_incomplete; }
 199  /** debug print methods */
 200  void debugPrint(const char* c);
 201  void debugPrintSmall(const char* c);
 202  // TODO (#1199): these should be private
 203  /** enumeration type for each field */
 204  std::vector<RsiEnumType> d_enum_type;
 205  /** the current tuple we are considering */
 206  std::vector<int> d_index;
 207
 208 private:
 209  /** rep set associated with this iterator */
 210  const RepSet* d_rs;
 211  /** rep set external bound information for this iterator */
 212  RepBoundExt* d_rext;
 213  /** types we are considering */
 214  std::vector<TypeNode> d_types;
 215  /** for each argument, the domain we are iterating over */
 216  std::vector<std::vector<Node> > d_domain_elements;
 217  /** initialize
 218   * This is called when the owner of this iterator is set.
 219   * It initializes the typing information for the types
 220   * that are involved in this iterator, initializes the
 221   * domain elements we are iterating over, and variable
 222   * and index orderings we are considering.
 223   */
 224  bool initialize();
 225  /** owner
 226   * This is the term that we are iterating for, which may either be:
 227   * (1) a quantified formula, or
 228   * (2) a function.
 229   */
 230  Node d_owner;
 231  /** reset index, 1:success, 0:empty, -1:fail */
 232  int resetIndex(unsigned i, bool initial = false);
 233  /** set index order (see below) */
 234  void setIndexOrder(std::vector<unsigned>& indexOrder);
 235  /** do reset increment the iterator at index=counter */
 236  int do_reset_increment(int counter, bool initial = false);
 237  /** ordering for variables we are iterating over
 238  *  For example, given reps = { a, b } and quantifier
 239  *    forall( x, y, z ) P( x, y, z )
 240  *  with d_index_order = { 2, 0, 1 },
 241  *    then we consider instantiations in this order:
 242  *      a/x a/y a/z
 243  *      a/x b/y a/z
 244  *      b/x a/y a/z
 245  *      b/x b/y a/z
 246  *      ...
 247  */
 248  std::vector<unsigned> d_index_order;
 249  /** Map from variables to the index they are considered at
 250  * For example, if d_index_order = { 2, 0, 1 }
 251  *    then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
 252  */
 253  std::map<unsigned, unsigned> d_var_order;
 254  /** incomplete flag */
 255  bool d_incomplete;
 256 };/* class RepSetIterator */
 257
 258 /** Representative bound external
 259  *
 260  * This class manages bound information
 261  * for an instance of a RepSetIterator.
 262  * Its main functionalities are to set
 263  * bounds on the domain of the iterator
 264  * over quantifiers and function arguments.
 265  */
 266 class RepBoundExt
 267 {
 268  public:
 269   virtual ~RepBoundExt() {}
 270   /** set bound
 271    *
 272    * This method initializes the vector "elements"
 273    * with list of terms to iterate over for the i^th
 274    * field of owner, where owner may be :
 275    * (1) A function, in which case we are iterating
 276    *     over domain elements of its argument type,
 277    * (2) A quantified formula, in which case we are
 278    *     iterating over domain elements of the type
 279    *     of its i^th bound variable.
 280    */
 281   virtual RsiEnumType setBound(Node owner,
 282                                unsigned i,
 283                                std::vector<Node>& elements) = 0;
 284   /** reset index
 285    *
 286    * This method initializes iteration for the i^th
 287    * field of owner, based on the current state of
 288    * the iterator rsi. It initializes the vector
 289    * "elements" with all appropriate terms to
 290    * iterate over in this context.
 291    * initial is whether this is the first call
 292    * to this function for this iterator.
 293    *
 294    * This method returns false if we were unable
 295    * to establish (finite) bounds for the current
 296    * field we are considering, which indicates that
 297    * the iterator will terminate with a failure.
 298    */
 299   virtual bool resetIndex(RepSetIterator* rsi,
 300                           Node owner,
 301                           unsigned i,
 302                           bool initial,
 303                           std::vector<Node>& elements)
 304   {
 305     return true;
 306   }
 307   /** initialize representative set for type
 308    *
 309    * Returns true if the representative set associated
 310    * with this bound has been given a complete interpretation
 311    * for type tn.
 312    */
 313   virtual bool initializeRepresentativesForType(TypeNode tn) { return false; }
 314   /** get variable order
 315    * If this method returns true, then varOrder is the order
 316    * in which we want to consider variables for the iterator.
 317    * If this method returns false, then varOrder is unchanged
 318    * and the RepSetIterator is free to choose a default
 319    * variable order.
 320    */
 321   virtual bool getVariableOrder(Node owner, std::vector<unsigned>& varOrder)
 322   {
 323     return false;
 324   }
 325 };
 326
 327 }/* CVC4::theory namespace */
 328 }/* CVC4 namespace */
 329
 330 #endif /* CVC4__THEORY__REP_SET_H */