diff options
Diffstat (limited to 'src/util/result.h')
-rw-r--r-- | src/util/result.h | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/src/util/result.h b/src/util/result.h index f0cf3f20e..0894007bc 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -24,16 +24,10 @@ #include <iostream> #include <string> -#include "util/Assert.h" +#include "util/exception.h" namespace CVC4 { -// TODO: either templatize Result on its Kind (Sat/Validity) or subclass. -// TODO: INVALID/SAT provide models, etc?---perhaps just by linking back -// into the SmtEngine that produced the Result? -// TODO: make unconstructible except by SmtEngine? That would ensure that -// any Result in the system is bona fide. - class Result; std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC; @@ -137,9 +131,9 @@ public: return d_which == TYPE_NONE; } enum UnknownExplanation whyUnknown() const { - AlwaysAssert( isUnknown(), - "This result is not unknown, so the reason for " - "being unknown cannot be inquired of it" ); + CheckArgument( isUnknown(), this, + "This result is not unknown, so the reason for " + "being unknown cannot be inquired of it" ); return d_unknownExplanation; } |