diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-17 17:21:26 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-18 16:39:42 -0400 |
commit | 066191d91d9f42f34a412162203be818e202aeba (patch) | |
tree | 10638c91da6e626c90e1a70e85b211852cbca4b5 /src/theory/theoryof_mode.h | |
parent | bd9b95170b21ad066e87a59db78fac8ab7f24629 (diff) |
Fixes to theoryof-mode; no longer static in Theory class.
Diffstat (limited to 'src/theory/theoryof_mode.h')
-rw-r--r-- | src/theory/theoryof_mode.h | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/src/theory/theoryof_mode.h b/src/theory/theoryof_mode.h index cd8c68b1a..c50960257 100644 --- a/src/theory/theoryof_mode.h +++ b/src/theory/theoryof_mode.h @@ -14,10 +14,10 @@ ** Option selection for theoryOf() operation. **/ -#pragma once - #include "cvc4_public.h" +#pragma once + namespace CVC4 { namespace theory { @@ -29,6 +29,18 @@ enum TheoryOfMode { THEORY_OF_TERM_BASED };/* enum TheoryOfMode */ +inline std::ostream& operator<<(std::ostream& out, TheoryOfMode m) throw() CVC4_PUBLIC; + +inline std::ostream& operator<<(std::ostream& out, TheoryOfMode m) throw() { + switch(m) { + case THEORY_OF_TYPE_BASED: return out << "THEORY_OF_TYPE_BASED"; + case THEORY_OF_TERM_BASED: return out << "THEORY_OF_TERM_BASED"; + default: return out << "TheoryOfMode!UNKNOWN"; + } + + Unreachable(); +} + }/* CVC4::theory namespace */ }/* CVC4 namespace */ |