src/theory/rep_set.h

   1 /*********************                                                        */
   2 /*! \file rep_set.h
   3  ** \verbatim
   4  ** Original author: ajreynol
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009-2012  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__REP_SET_H
  18 #define __CVC4__REP_SET_H
  19
  20 #include "expr/node.h"
  21 #include <map>
  22
  23 namespace CVC4 {
  24 namespace theory {
  25
  26 /** this class stores a representative set */
  27 class RepSet {
  28 public:
  29   RepSet(){}
  30   ~RepSet(){}
  31   std::map< TypeNode, std::vector< Node > > d_type_reps;
  32   std::map< TypeNode, bool > d_type_complete;
  33   std::map< Node, int > d_tmap;
  34   /** clear the set */
  35   void clear();
  36   /** has type */
  37   bool hasType( TypeNode tn ) const { return d_type_reps.find( tn )!=d_type_reps.end(); }
  38   /** get cardinality for type */
  39   int getNumRepresentatives( TypeNode tn ) const;
  40   /** add representative for type */
  41   void add( Node n );
  42   /** returns index in d_type_reps for node n */
  43   int getIndexFor( Node n ) const;
  44   /** complete all values */
  45   void complete( TypeNode t );
  46   /** debug print */
  47   void toStream(std::ostream& out);
  48 };
  49
  50 //representative domain
  51 typedef std::vector< int > RepDomain;
  52
  53 /** this class iterates over a RepSet */
  54 class RepSetIterator {
  55 private:
  56   //initialize function
  57   bool initialize();
  58 public:
  59   RepSetIterator( RepSet* rs );
  60   ~RepSetIterator(){}
  61   //set that this iterator will be iterating over instantiations for a quantifier
  62   bool setQuantifier( Node f );
  63   //set that this iterator will be iterating over the domain of a function
  64   bool setFunctionDomain( Node op );
  65 public:
  66   //pointer to model
  67   RepSet* d_rep_set;
  68   //index we are considering
  69   std::vector< int > d_index;
  70   //types we are considering
  71   std::vector< TypeNode > d_types;
  72   //domain we are considering
  73   std::vector< RepDomain > d_domain;
  74   //are we only considering a strict subset of the domain of the quantifier?
  75   bool d_incomplete;
  76   //ordering for variables we are indexing over
  77   //  for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 },
  78   //    then we consider instantiations in this order:
  79   //      a/x a/y a/z
  80   //      a/x b/y a/z
  81   //      b/x a/y a/z
  82   //      b/x b/y a/z
  83   //      ...
  84   std::vector< int > d_index_order;
  85   //variables to index they are considered at
  86   //  for example, if d_index_order = { 2, 0, 1 }
  87   //    then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
  88   std::map< int, int > d_var_order;
  89 public:
  90   /** set index order */
  91   void setIndexOrder( std::vector< int >& indexOrder );
  92   /** set domain */
  93   void setDomain( std::vector< RepDomain >& domain );
  94   /** increment the iterator at index=counter */
  95   void increment2( int counter );
  96   /** increment the iterator */
  97   void increment();
  98   /** is the iterator finished? */
  99   bool isFinished();
 100   /** get the i_th term we are considering */
 101   Node getTerm( int i );
 102   /** get the number of terms we are considering */
 103   int getNumTerms() { return (int)d_index_order.size(); }
 104   /** debug print */
 105   void debugPrint( const char* c );
 106   void debugPrintSmall( const char* c );
 107 };
 108
 109 }
 110 }
 111
 112 #endif