1 /********************* */
4 ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com>
5 ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu>
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Representative set class and utilities
15 #include "cvc4_private.h"
17 #ifndef __CVC4__THEORY__REP_SET_H
18 #define __CVC4__THEORY__REP_SET_H
20 #include "expr/node.h"
26 /** this class stores a representative set */
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
;
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 */
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
);
47 void toStream(std::ostream
& out
);
50 //representative domain
51 typedef std::vector
< int > RepDomain
;
53 /** this class iterates over a RepSet */
54 class RepSetIterator
{
59 RepSetIterator( RepSet
* rs
);
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
);
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?
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:
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
;
90 /** set index order */
91 void setIndexOrder( std::vector
< int >& indexOrder
);
93 void setDomain( std::vector
< RepDomain
>& domain
);
94 /** increment the iterator at index=counter */
95 void increment2( int counter
);
96 /** increment the iterator */
98 /** is the iterator finished? */
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(); }
105 void debugPrint( const char* c
);
106 void debugPrintSmall( const char* c
);
107 };/* class RepSetIterator */
109 }/* CVC4::theory namespace */
110 }/* CVC4 namespace */
112 #endif /* __CVC4__THEORY__REP_SET_H */