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-2016 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 "expr/node.h"
  21 #include <map>
  22
  23 namespace CVC4 {
  24 namespace theory {
  25
  26 class QuantifiersEngine;
  27
  28 /** this class stores a representative set */
  29 class RepSet {
  30 public:
  31   RepSet(){}
  32   ~RepSet(){}
  33   std::map< TypeNode, std::vector< Node > > d_type_reps;
  34   std::map< TypeNode, bool > d_type_complete;
  35   std::map< Node, int > d_tmap;
  36   std::map< TypeNode, int > d_type_rlv_rep;
  37   // map from values to terms they were assigned for
  38   std::map< Node, Node > d_values_to_terms;
  39   /** clear the set */
  40   void clear();
  41   /** has type */
  42   bool hasType( TypeNode tn ) const { return d_type_reps.find( tn )!=d_type_reps.end(); }
  43   /** has rep */
  44   bool hasRep( TypeNode tn, Node n );
  45   /** get cardinality for type */
  46   int getNumRepresentatives( TypeNode tn ) const;
  47   /** add representative for type */
  48   void add( TypeNode tn, Node n );
  49   /** returns index in d_type_reps for node n */
  50   int getIndexFor( Node n ) const;
  51   /** complete all values */
  52   bool complete( TypeNode t );
  53   /** get number of relevant ground representatives for type */
  54   int getNumRelevantGroundReps( TypeNode t );
  55   /** debug print */
  56   void toStream(std::ostream& out);
  57 };/* class RepSet */
  58
  59 //representative domain
  60 typedef std::vector< int > RepDomain;
  61
  62 /** this class iterates over a RepSet */
  63 class RepSetIterator {
  64 public:
  65   enum {
  66     ENUM_DOMAIN_ELEMENTS,
  67     ENUM_RANGE,
  68   };
  69 private:
  70   QuantifiersEngine * d_qe;
  71   //initialize function
  72   bool initialize();
  73   //for enum ranges
  74   std::map< int, Node > d_lower_bounds;
  75   //domain size
  76   int domainSize( int i );
  77   //node this is rep set iterator is for
  78   Node d_owner;
  79   //reset index
  80   bool resetIndex( int i, bool initial = false );
  81   /** set index order */
  82   void setIndexOrder( std::vector< int >& indexOrder );
  83 public:
  84   RepSetIterator( QuantifiersEngine * qe, RepSet* rs );
  85   ~RepSetIterator(){}
  86   //set that this iterator will be iterating over instantiations for a quantifier
  87   bool setQuantifier( Node f );
  88   //set that this iterator will be iterating over the domain of a function
  89   bool setFunctionDomain( Node op );
  90 public:
  91   //pointer to model
  92   RepSet* d_rep_set;
  93   //enumeration type?
  94   std::vector< int > d_enum_type;
  95   //index we are considering
  96   std::vector< int > d_index;
  97   //types we are considering
  98   std::vector< TypeNode > d_types;
  99   //domain we are considering
 100   std::vector< RepDomain > d_domain;
 101   //are we only considering a strict subset of the domain of the quantifier?
 102   bool d_incomplete;
 103   //ordering for variables we are indexing over
 104   //  for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 },
 105   //    then we consider instantiations in this order:
 106   //      a/x a/y a/z
 107   //      a/x b/y a/z
 108   //      b/x a/y a/z
 109   //      b/x b/y a/z
 110   //      ...
 111   std::vector< int > d_index_order;
 112   //variables to index they are considered at
 113   //  for example, if d_index_order = { 2, 0, 1 }
 114   //    then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
 115   std::map< int, int > d_var_order;
 116   //intervals
 117   std::map< int, Node > d_bounds[2];
 118 public:
 119   /** increment the iterator at index=counter */
 120   int increment2( int counter );
 121   /** increment the iterator */
 122   int increment();
 123   /** is the iterator finished? */
 124   bool isFinished();
 125   /** get the i_th term we are considering */
 126   Node getTerm( int i );
 127   /** get the number of terms we are considering */
 128   int getNumTerms() { return (int)d_index_order.size(); }
 129   /** debug print */
 130   void debugPrint( const char* c );
 131   void debugPrintSmall( const char* c );
 132 };/* class RepSetIterator */
 133
 134 }/* CVC4::theory namespace */
 135 }/* CVC4 namespace */
 136
 137 #endif /* __CVC4__THEORY__REP_SET_H */