diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-06 21:30:35 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-06 21:32:58 -0500 |
commit | 816630a9e9e6b13f7299535a18fe87c5f8180def (patch) | |
tree | a390e45205fe570fda9ca18d8dd06cd57e1b2aa0 /src/theory | |
parent | 1ea7caf0ef8e4ef3db22b6392c9624345eb974e3 (diff) |
make datatypes enumerator behavior clearer (no exceptions in normal operation)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/datatypes/type_enumerator.h | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 2a14d7fba..8ee275f70 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -139,11 +139,10 @@ public: DatatypesEnumerator& operator++() throw() { if(d_ctor < d_datatype.getNumConstructors()) { for(size_t a = d_datatype[d_ctor].getNumArgs(); a > 0; --a) { - try { - *++*d_argEnumerators[a - 1]; - return *this; - } catch(NoMoreValuesException&) { + if((++*d_argEnumerators[a - 1]).isFinished()) { *d_argEnumerators[a - 1] = TypeEnumerator(Node::fromExpr(d_datatype[d_ctor][a - 1].getSelector()).getType()[1]); + } else { + return *this; } } |