diff options
Diffstat (limited to 'src/theory/quantifiers/fmf/bounded_integers.h')
| -rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.h | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index c6293f1fe..90928c0bc 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -62,6 +62,14 @@ private: //set membership range std::map< Node, std::map< Node, Node > > d_setm_range; std::map< Node, std::map< Node, Node > > d_setm_range_lit; + /** set membership element choice functions + * + * For each set S and integer n, d_setm_choice[S][n] is the canonical + * representation for the (n+1)^th member of set S. It is of the form: + * choice x. (|S| <= n OR ( x in S AND + * distinct( x, d_setm_choice[S][0], ..., d_setm_choice[S][n-1] ) ) ) + */ + std::map<Node, std::vector<Node> > d_setm_choice; //fixed finite set range std::map< Node, std::map< Node, std::vector< Node > > > d_fixed_set_gr_range; std::map< Node, std::map< Node, std::vector< Node > > > d_fixed_set_ngr_range; |