diff options
author | Tim King <taking@cs.nyu.edu> | 2018-02-05 15:17:45 -0800 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-05 17:17:45 -0600 |
commit | 66a7932c7d4bd986665a041293ed23f8f58570f4 (patch) | |
tree | a69141491694be5653d1708884aa42b3ff138926 /src/theory/rep_set.h | |
parent | b458d1768202f7f9e117693b83985794665f73e2 (diff) |
Cleaning up the printing of theory model representative sets. (#1538)
Diffstat (limited to 'src/theory/rep_set.h')
-rw-r--r-- | src/theory/rep_set.h | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index 5b75fa943..a75918b5a 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -57,9 +57,9 @@ class QuantifiersEngine; * finite types. */ class RepSet { -public: + public: RepSet(){} - ~RepSet(){} + /** map from types to the list of representatives * TODO : as part of #1199, encapsulate this */ @@ -67,15 +67,19 @@ public: /** clear the set */ void clear(); /** does this set have representatives of type tn? */ - bool hasType( TypeNode tn ) const { return d_type_reps.find( tn )!=d_type_reps.end(); } + bool hasType(TypeNode tn) const { return d_type_reps.count(tn) > 0; } /** does this set have representative n of type tn? */ bool hasRep(TypeNode tn, Node n) const; /** get the number of representatives for type */ unsigned getNumRepresentatives(TypeNode tn) const; /** get representative at index */ Node getRepresentative(TypeNode tn, unsigned i) const; - /** get representatives of type tn, appends them to reps */ - void getRepresentatives(TypeNode tn, std::vector<Node>& reps) const; + /** + * Returns the representatives of a type for a `type_node` if one exists. + * Otherwise, returns nullptr. + */ + const std::vector<Node>* getTypeRepsOrNull(TypeNode type_node) const; + /** add representative n for type tn, where n has type tn */ void add( TypeNode tn, Node n ); /** returns index in d_type_reps for node n */ |