summaryrefslogtreecommitdiff
path: root/src/theory/rep_set.h
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2014-11-05 19:57:24 +0100
committerajreynol <andrew.j.reynolds@gmail.com>2014-11-05 19:57:30 +0100
commit2b64e19e84787c7f510a2e7a536be563072e1c8e (patch)
treefcc7d8072951ab7ff2eef90c1b3b524c92cafa73 /src/theory/rep_set.h
parent7e8413ccb5a5f831b9814edd025d0c239b104d9f (diff)
Fix model bug in --mbqi=fmc. Minor cleanup in datatypes.
Diffstat (limited to 'src/theory/rep_set.h')
-rw-r--r--src/theory/rep_set.h2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index 23db36ead..19bb6d3d3 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -37,6 +37,8 @@ public:
void clear();
/** has type */
bool hasType( TypeNode tn ) const { return d_type_reps.find( tn )!=d_type_reps.end(); }
+ /** has rep */
+ bool hasRep( TypeNode tn, Node n );
/** get cardinality for type */
int getNumRepresentatives( TypeNode tn ) const;
/** add representative for type */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback