src/theory/rep_set.h

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