1 /********************* */
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
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 class QuantifiersEngine
;
28 /** this class stores a representative set */
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
;
42 bool hasType( TypeNode tn
) const { return d_type_reps
.find( tn
)!=d_type_reps
.end(); }
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
);
56 void toStream(std::ostream
& out
);
59 //representative domain
60 typedef std::vector
< int > RepDomain
;
62 /** this class iterates over a RepSet */
63 class RepSetIterator
{
71 QuantifiersEngine
* d_qe
;
75 std::map
< int, Node
> d_lower_bounds
;
77 std::map
< int, std::vector
< Node
> > d_setm_bounds
;
79 int domainSize( int i
);
80 //node this is rep set iterator is for
82 //reset index, 1:success, 0:empty, -1:fail
83 int resetIndex( int i
, bool initial
= false );
84 /** set index order */
85 void setIndexOrder( std::vector
< int >& indexOrder
);
86 /** do reset increment the iterator at index=counter */
87 int do_reset_increment( int counter
, bool initial
= false );
88 //ordering for variables we are indexing over
89 // for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 },
90 // then we consider instantiations in this order:
96 std::vector
< int > d_index_order
;
97 //variables to index they are considered at
98 // for example, if d_index_order = { 2, 0, 1 }
99 // then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
100 std::map
< int, int > d_var_order
;
101 //are we only considering a strict subset of the domain of the quantifier?
104 RepSetIterator( QuantifiersEngine
* qe
, RepSet
* rs
);
106 //set that this iterator will be iterating over instantiations for a quantifier
107 bool setQuantifier( Node f
);
108 //set that this iterator will be iterating over the domain of a function
109 bool setFunctionDomain( Node op
);
114 std::vector
< int > d_enum_type
;
115 //current tuple we are considering
116 std::vector
< int > d_index
;
117 //types we are considering
118 std::vector
< TypeNode
> d_types
;
119 //domain we are considering
120 std::vector
< RepDomain
> d_domain
;
122 std::map
< int, Node
> d_bounds
[2];
124 /** increment the iterator at index=counter */
125 int increment2( int i
);
126 /** increment the iterator */
128 /** is the iterator finished? */
130 /** get the i_th term we are considering */
131 Node
getCurrentTerm( int v
);
132 /** get the number of terms we are considering */
133 int getNumTerms() { return (int)d_index_order
.size(); }
135 void debugPrint( const char* c
);
136 void debugPrintSmall( const char* c
);
137 //get index order, returns var #
138 int getIndexOrder( int v
) { return d_index_order
[v
]; }
139 //get variable order, returns index #
140 int getVariableOrder( int i
) { return d_var_order
[i
]; }
142 bool isIncomplete() { return d_incomplete
; }
143 };/* class RepSetIterator */
145 }/* CVC4::theory namespace */
146 }/* CVC4 namespace */
148 #endif /* __CVC4__THEORY__REP_SET_H */