diff options
Diffstat (limited to 'src/util/options.h')
-rw-r--r-- | src/util/options.h | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/src/util/options.h b/src/util/options.h index 7fcf35f00..c79bc93b1 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -47,6 +47,12 @@ struct CVC4_PUBLIC Options { /** The input language */ parser::InputLanguage lang; + /** Enumeration of UF implementation choices */ + typedef enum { TIM, MORGAN } UfImplementation; + + /** Which implementation of uninterpreted function theory to use */ + UfImplementation uf_implementation; + /** Should we exit after parsing? */ bool parseOnly; @@ -65,6 +71,7 @@ struct CVC4_PUBLIC Options { err(0), verbosity(0), lang(parser::LANG_AUTO), + uf_implementation(MORGAN), parseOnly(false), semanticChecks(true), memoryMap(false), @@ -72,6 +79,21 @@ struct CVC4_PUBLIC Options { {} };/* struct Options */ +inline std::ostream& operator<<(std::ostream& out, Options::UfImplementation uf) { + switch(uf) { + case Options::TIM: + out << "TIM"; + break; + case Options::MORGAN: + out << "MORGAN"; + break; + default: + out << "UfImplementation:UNKNOWN![" << unsigned(uf) << "]"; + } + + return out; +} + }/* CVC4 namespace */ #endif /* __CVC4__OPTIONS_H */ |