src/theory/rep_set.h

   1 /*********************                                                        */
   2 /*! \file rep_set.h
   3  ** \verbatim
   4  ** Original author: Andrew Reynolds
   5  ** Major contributors: Morgan Deters
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** 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   /** clear the set */
  37   void clear();
  38   /** has type */
  39   bool hasType( TypeNode tn ) const { return d_type_reps.find( tn )!=d_type_reps.end(); }
  40   /** get cardinality for type */
  41   int getNumRepresentatives( TypeNode tn ) const;
  42   /** add representative for type */
  43   void add( TypeNode tn, Node n );
  44   /** returns index in d_type_reps for node n */
  45   int getIndexFor( Node n ) const;
  46   /** complete all values */
  47   void complete( TypeNode t );
  48   /** debug print */
  49   void toStream(std::ostream& out);
  50 };/* class RepSet */
  51
  52 //representative domain
  53 typedef std::vector< int > RepDomain;
  54
  55 /** this class iterates over a RepSet */
  56 class RepSetIterator {
  57 public:
  58   enum {
  59     ENUM_DOMAIN_ELEMENTS,
  60     ENUM_RANGE,
  61   };
  62 private:
  63   QuantifiersEngine * d_qe;
  64   //initialize function
  65   bool initialize();
  66   //for enum ranges
  67   std::map< int, Node > d_lower_bounds;
  68   //domain size
  69   int domainSize( int i );
  70   //node this is rep set iterator is for
  71   Node d_owner;
  72   //reset index
  73   bool resetIndex( int i, bool initial = false );
  74   /** set index order */
  75   void setIndexOrder( std::vector< int >& indexOrder );
  76 public:
  77   RepSetIterator( QuantifiersEngine * qe, RepSet* rs );
  78   ~RepSetIterator(){}
  79   //set that this iterator will be iterating over instantiations for a quantifier
  80   bool setQuantifier( Node f );
  81   //set that this iterator will be iterating over the domain of a function
  82   bool setFunctionDomain( Node op );
  83 public:
  84   //pointer to model
  85   RepSet* d_rep_set;
  86   //enumeration type?
  87   std::vector< int > d_enum_type;
  88   //index we are considering
  89   std::vector< int > d_index;
  90   //types we are considering
  91   std::vector< TypeNode > d_types;
  92   //domain we are considering
  93   std::vector< RepDomain > d_domain;
  94   //are we only considering a strict subset of the domain of the quantifier?
  95   bool d_incomplete;
  96   //ordering for variables we are indexing over
  97   //  for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 },
  98   //    then we consider instantiations in this order:
  99   //      a/x a/y a/z
 100   //      a/x b/y a/z
 101   //      b/x a/y a/z
 102   //      b/x b/y a/z
 103   //      ...
 104   std::vector< int > d_index_order;
 105   //variables to index they are considered at
 106   //  for example, if d_index_order = { 2, 0, 1 }
 107   //    then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
 108   std::map< int, int > d_var_order;
 109   //intervals
 110   std::map< int, Node > d_bounds[2];
 111 public:
 112   /** increment the iterator at index=counter */
 113   int increment2( int counter );
 114   /** increment the iterator */
 115   int increment();
 116   /** is the iterator finished? */
 117   bool isFinished();
 118   /** get the i_th term we are considering */
 119   Node getTerm( int i );
 120   /** get the number of terms we are considering */
 121   int getNumTerms() { return (int)d_index_order.size(); }
 122   /** debug print */
 123   void debugPrint( const char* c );
 124   void debugPrintSmall( const char* c );
 125 };/* class RepSetIterator */
 126
 127 }/* CVC4::theory namespace */
 128 }/* CVC4 namespace */
 129
 130 #endif /* __CVC4__THEORY__REP_SET_H */