summaryrefslogtreecommitdiff
path: root/src/util/cardinality.h
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2015-02-13 14:12:32 +0100
committerajreynol <andrew.j.reynolds@gmail.com>2015-02-13 14:12:41 +0100
commit82fbac8829cbc41927216b36ab064b50e50b2fa0 (patch)
tree346361d002c109b8ac2254f4f215a12dfc7643d2 /src/util/cardinality.h
parent3ba153b4be4c2fe8ad7decf8ebc7cf5d8815a0e9 (diff)
Handle recursive singleton case for codatatypes, add regression. Simplify implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes.
Diffstat (limited to 'src/util/cardinality.h')
-rw-r--r--src/util/cardinality.h4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/util/cardinality.h b/src/util/cardinality.h
index 524d9cda4..113cb954c 100644
--- a/src/util/cardinality.h
+++ b/src/util/cardinality.h
@@ -156,6 +156,10 @@ public:
bool isFinite() const throw() {
return d_card > 0;
}
+ /** Returns true iff this cardinality is one */
+ bool isOne() const throw() {
+ return d_card == 1;
+ }
/**
* Returns true iff this cardinality is finite and large (i.e.,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback