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:33:51 -0500 |
commit | a72276859f0af0f5e800434879eca111d8bf6644 (patch) | |
tree | aa94d9c9c1406d37aa56fbd816e3dcfa856d8689 /src | |
parent | 8d28109c7d6305c606fca9cf9869d606df9f661d (diff) |
make datatypes enumerator behavior clearer (no exceptions in normal operation)
Diffstat (limited to 'src')
-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; } } |