src/theory/rep_set.h

   1 /*********************                                                        */
   2 /*! \file rep_set.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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   unsigned 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 /** Rep set iterator.
 125  *
 126  * This class is used for iterating over (tuples of) terms
 127  * in the domain(s) of a RepSet.
 128  *
 129  * To use it, first it must
 130  * be initialized with a call to:
 131  * - setQuantifier or setFunctionDomain
 132  * which initializes the d_owner field and sets up
 133  * initial information.
 134  *
 135  * Then, we increment over the tuples of terms in the
 136  * domains of the owner of this iterator using:
 137  * - increment and incrementAtIndex
 138  *
 139  * TODO (#1199): this class needs further documentation.
 140  */
 141 class RepSetIterator {
 142 public:
 143  enum RsiEnumType
 144  {
 145    ENUM_INVALID = 0,
 146    ENUM_DEFAULT,
 147    ENUM_BOUND_INT,
 148  };
 149
 150 public:
 151  RepSetIterator(const RepSet* rs, RepBoundExt* rext = nullptr);
 152  ~RepSetIterator() {}
 153  /** set that this iterator will be iterating over instantiations for a
 154   * quantifier */
 155  bool setQuantifier(Node q);
 156  /** set that this iterator will be iterating over the domain of a function */
 157  bool setFunctionDomain(Node op);
 158  /** increment the iterator */
 159  int increment();
 160  /** increment the iterator at index
 161   * This increments the i^th field of the
 162   * iterator, for examples, see operator next_i
 163   * in Figure 2 of Reynolds et al. CADE 2013.
 164   */
 165  int incrementAtIndex(int i);
 166  /** is the iterator finished? */
 167  bool isFinished() const;
 168  /** get domain size of the i^th field of this iterator */
 169  unsigned domainSize(unsigned i);
 170  /** get the i^th term in the tuple we are considering */
 171  Node getCurrentTerm(unsigned v, bool valTerm = false) const;
 172  /** get the number of terms in the tuple we are considering */
 173  unsigned getNumTerms() const { return d_index_order.size(); }
 174  /** get current terms */
 175  void getCurrentTerms(std::vector<Node>& terms) const;
 176  /** get index order, returns var # */
 177  unsigned getIndexOrder(unsigned v) { return d_index_order[v]; }
 178  /** get variable order, returns index # */
 179  unsigned getVariableOrder(unsigned i) { return d_var_order[i]; }
 180  /** is incomplete
 181   * Returns true if we are iterating over a strict subset of
 182   * the domain of the quantified formula or function.
 183   */
 184  bool isIncomplete() { return d_incomplete; }
 185  /** debug print methods */
 186  void debugPrint(const char* c);
 187  void debugPrintSmall(const char* c);
 188  // TODO (#1199): these should be private
 189  /** enumeration type for each field */
 190  std::vector<RsiEnumType> d_enum_type;
 191  /** the current tuple we are considering */
 192  std::vector<int> d_index;
 193
 194 private:
 195  /** rep set associated with this iterator */
 196  const RepSet* d_rs;
 197  /** rep set external bound information for this iterator */
 198  RepBoundExt* d_rext;
 199  /** types we are considering */
 200  std::vector<TypeNode> d_types;
 201  /** for each argument, the domain we are iterating over */
 202  std::vector<std::vector<Node> > d_domain_elements;
 203  /** initialize
 204   * This is called when the owner of this iterator is set.
 205   * It initializes the typing information for the types
 206   * that are involved in this iterator, initializes the
 207   * domain elements we are iterating over, and variable
 208   * and index orderings we are considering.
 209   */
 210  bool initialize();
 211  /** owner
 212   * This is the term that we are iterating for, which may either be:
 213   * (1) a quantified formula, or
 214   * (2) a function.
 215   */
 216  Node d_owner;
 217  /** reset index, 1:success, 0:empty, -1:fail */
 218  int resetIndex(unsigned i, bool initial = false);
 219  /** set index order (see below) */
 220  void setIndexOrder(std::vector<unsigned>& indexOrder);
 221  /** do reset increment the iterator at index=counter */
 222  int do_reset_increment(int counter, bool initial = false);
 223  /** ordering for variables we are iterating over
 224  *  For example, given reps = { a, b } and quantifier
 225  *    forall( x, y, z ) P( x, y, z )
 226  *  with d_index_order = { 2, 0, 1 },
 227  *    then we consider instantiations in this order:
 228  *      a/x a/y a/z
 229  *      a/x b/y a/z
 230  *      b/x a/y a/z
 231  *      b/x b/y a/z
 232  *      ...
 233  */
 234  std::vector<unsigned> d_index_order;
 235  /** Map from variables to the index they are considered at
 236  * For example, if d_index_order = { 2, 0, 1 }
 237  *    then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
 238  */
 239  std::map<unsigned, unsigned> d_var_order;
 240  /** incomplete flag */
 241  bool d_incomplete;
 242 };/* class RepSetIterator */
 243
 244 /** Representative bound external
 245  *
 246  * This class manages bound information
 247  * for an instance of a RepSetIterator.
 248  * Its main functionalities are to set
 249  * bounds on the domain of the iterator
 250  * over quantifiers and function arguments.
 251  */
 252 class RepBoundExt
 253 {
 254  public:
 255   virtual ~RepBoundExt() {}
 256   /** set bound
 257    *
 258    * This method initializes the vector "elements"
 259    * with list of terms to iterate over for the i^th
 260    * field of owner, where owner may be :
 261    * (1) A function, in which case we are iterating
 262    *     over domain elements of its argument type,
 263    * (2) A quantified formula, in which case we are
 264    *     iterating over domain elements of the type
 265    *     of its i^th bound variable.
 266    */
 267   virtual RepSetIterator::RsiEnumType setBound(Node owner,
 268                                                unsigned i,
 269                                                std::vector<Node>& elements) = 0;
 270   /** reset index
 271    *
 272    * This method initializes iteration for the i^th
 273    * field of owner, based on the current state of
 274    * the iterator rsi. It initializes the vector
 275    * "elements" with all appropriate terms to
 276    * iterate over in this context.
 277    * initial is whether this is the first call
 278    * to this function for this iterator.
 279    *
 280    * This method returns false if we were unable
 281    * to establish (finite) bounds for the current
 282    * field we are considering, which indicates that
 283    * the iterator will terminate with a failure.
 284    */
 285   virtual bool resetIndex(RepSetIterator* rsi,
 286                           Node owner,
 287                           unsigned i,
 288                           bool initial,
 289                           std::vector<Node>& elements)
 290   {
 291     return true;
 292   }
 293   /** initialize representative set for type
 294    *
 295    * Returns true if the representative set associated
 296    * with this bound has been given a complete interpretation
 297    * for type tn.
 298    */
 299   virtual bool initializeRepresentativesForType(TypeNode tn) { return false; }
 300   /** get variable order
 301    * If this method returns true, then varOrder is the order
 302    * in which we want to consider variables for the iterator.
 303    * If this method returns false, then varOrder is unchanged
 304    * and the RepSetIterator is free to choose a default
 305    * variable order.
 306    */
 307   virtual bool getVariableOrder(Node owner, std::vector<unsigned>& varOrder)
 308   {
 309     return false;
 310   }
 311 };
 312
 313 }/* CVC4::theory namespace */
 314 }/* CVC4 namespace */
 315
 316 #endif /* __CVC4__THEORY__REP_SET_H */