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   // map from values to terms they were assigned for
  37   std::map< Node, Node > d_values_to_terms;
  38   /** clear the set */
  39   void clear();
  40   /** has type */
  41   bool hasType( TypeNode tn ) const { return d_type_reps.find( tn )!=d_type_reps.end(); }
  42   /** has rep */
  43   bool hasRep( TypeNode tn, Node n );
  44   /** get cardinality for type */
  45   int getNumRepresentatives( TypeNode tn ) const;
  46   /** add representative for type */
  47   void add( TypeNode tn, Node n );
  48   /** returns index in d_type_reps for node n */
  49   int getIndexFor( Node n ) const;
  50   /** complete all values */
  51   bool complete( TypeNode t );
  52   /** debug print */
  53   void toStream(std::ostream& out);
  54 };/* class RepSet */
  55
  56 //representative domain
  57 typedef std::vector< int > RepDomain;
  58
  59
  60 class RepBoundExt {
  61  public:
  62   virtual ~RepBoundExt() {}
  63   virtual bool setBound( Node owner, int i, TypeNode tn, std::vector< Node >& elements ) = 0;
  64 };
  65
  66 /** this class iterates over a RepSet */
  67 class RepSetIterator {
  68 public:
  69   enum {
  70     ENUM_DEFAULT,
  71     ENUM_BOUND_INT,
  72   };
  73 private:
  74   QuantifiersEngine * d_qe;
  75   //initialize function
  76   bool initialize( RepBoundExt* rext = NULL );
  77   //for int ranges
  78   std::map< int, Node > d_lower_bounds;
  79   //for set ranges
  80   std::map< int, std::vector< Node > > d_setm_bounds;
  81   //domain size
  82   int domainSize( int i );
  83   //node this is rep set iterator is for
  84   Node d_owner;
  85   //reset index, 1:success, 0:empty, -1:fail
  86   int resetIndex( int i, bool initial = false );
  87   /** set index order */
  88   void setIndexOrder( std::vector< int >& indexOrder );
  89   /** do reset increment the iterator at index=counter */
  90   int do_reset_increment( int counter, bool initial = false );
  91   //ordering for variables we are indexing over
  92   //  for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 },
  93   //    then we consider instantiations in this order:
  94   //      a/x a/y a/z
  95   //      a/x b/y a/z
  96   //      b/x a/y a/z
  97   //      b/x b/y a/z
  98   //      ...
  99   std::vector< int > d_index_order;
 100   //variables to index they are considered at
 101   //  for example, if d_index_order = { 2, 0, 1 }
 102   //    then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
 103   std::map< int, int > d_var_order;
 104   //are we only considering a strict subset of the domain of the quantifier?
 105   bool d_incomplete;
 106 public:
 107   RepSetIterator( QuantifiersEngine * qe, RepSet* rs );
 108   ~RepSetIterator(){}
 109   //set that this iterator will be iterating over instantiations for a quantifier
 110   bool setQuantifier( Node f, RepBoundExt* rext = NULL );
 111   //set that this iterator will be iterating over the domain of a function
 112   bool setFunctionDomain( Node op, RepBoundExt* rext = NULL );
 113 public:
 114   //pointer to model
 115   RepSet* d_rep_set;
 116   //enumeration type?
 117   std::vector< int > d_enum_type;
 118   //current tuple we are considering
 119   std::vector< int > d_index;
 120   //types we are considering
 121   std::vector< TypeNode > d_types;
 122   //domain we are considering
 123   std::vector< std::vector< Node > > d_domain_elements;
 124 public:
 125   /** increment the iterator at index=counter */
 126   int increment2( int i );
 127   /** increment the iterator */
 128   int increment();
 129   /** is the iterator finished? */
 130   bool isFinished();
 131   /** get the i_th term we are considering */
 132   Node getCurrentTerm( int v );
 133   /** get the number of terms we are considering */
 134   int getNumTerms() { return (int)d_index_order.size(); }
 135   /** debug print */
 136   void debugPrint( const char* c );
 137   void debugPrintSmall( const char* c );
 138   //get index order, returns var #
 139   int getIndexOrder( int v ) { return d_index_order[v]; }
 140   //get variable order, returns index #
 141   int getVariableOrder( int i ) { return d_var_order[i]; }
 142   //is incomplete
 143   bool isIncomplete() { return d_incomplete; }
 144 };/* class RepSetIterator */
 145
 146 }/* CVC4::theory namespace */
 147 }/* CVC4 namespace */
 148
 149 #endif /* __CVC4__THEORY__REP_SET_H */