diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-25 06:56:14 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-25 06:56:14 +0000 |
commit | cb7363eef352200615e1a0d3729cea8b2c74d265 (patch) | |
tree | d57f6a9cfab879c1027e7282f63d0fae14fc0153 /src/util/language.cpp | |
parent | e39882bd8a308711135a1ff644293fd9c46e6433 (diff) |
Weekend work. The main points:
* Type::getCardinality() returns the cardinality for for all types.
Theories give a cardinality in the their kinds file. For
cardinalities that depend on a type argument, a "cardinality
computer" function is named in the kinds file, which takes a
TypeNode and returns its cardinality.
* There's a bitmap for the set of "active theories" in the
TheoryEngine. Theories become "active" when a term that is owned by
them, or whose type is owned by them, is pre-registered (run CVC4
with --verbose to see theory activation). Non-active theories don't
get any calls for check() or propagate() or anything, and if we're
running in single-theory mode, the shared term manager doesn't have
to get involved. This is really important for get() performance
(which can only skimp on walking the entire sub-DAG only if the
theory doesn't require it AND the shared term manager doesn't
require it).
* TheoryEngine now does not call presolve(), registerTerm(),
notifyRestart(), etc., on a Theory if that theory doesn't declare
that property in its kinds file. To avoid coding errors,
mktheorytraits greps the theory header and gives warnings if:
+ the theory appears to declare one of the functions (check,
propagate, etc.) that isn't listed among its kinds file properties
(but probably should be)
+ the theory appears NOT to declare one of the functions listed in
its kinds file properties
* some bounded token stream work
Diffstat (limited to 'src/util/language.cpp')
-rw-r--r-- | src/util/language.cpp | 65 |
1 files changed, 65 insertions, 0 deletions
diff --git a/src/util/language.cpp b/src/util/language.cpp new file mode 100644 index 000000000..da54a4783 --- /dev/null +++ b/src/util/language.cpp @@ -0,0 +1,65 @@ +/********************* */ +/*! \file language.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Definition of input and output languages + ** + ** Definition of input and output languages. + **/ + +#include "util/language.h" + +namespace CVC4 { +namespace language { + +InputLanguage toInputLanguage(OutputLanguage language) { + switch(language) { + case output::LANG_SMTLIB: + case output::LANG_SMTLIB_V2: + case output::LANG_CVC4: + // these entries directly correspond (by design) + return InputLanguage(int(language)); + + default: { + std::stringstream ss; + ss << "Cannot map output language `" << language + << "' to an input language."; + throw CVC4::Exception(ss.str()); + } + }/* switch(language) */ +}/* toInputLanguage() */ + +OutputLanguage toOutputLanguage(InputLanguage language) { + switch(language) { + case input::LANG_SMTLIB: + case input::LANG_SMTLIB_V2: + case input::LANG_CVC4: + // these entries directly correspond (by design) + return OutputLanguage(int(language)); + + default: + // Revert to the default (AST) language. + // + // We used to throw an exception here, but that's not quite right. + // We often call this while constructing exceptions, for one, and + // it's better to output SOMETHING related to the original + // exception rather than mask it with another exception. Also, + // the input language isn't always defined---e.g. during the + // initial phase of the main CVC4 driver while it determines which + // language is appropriate, and during unit tests. Also, when + // users are writing their own code against the library. + return output::LANG_AST; + }/* switch(language) */ +}/* toOutputLanguage() */ + +}/* CVC4::language namespace */ +}/* CVC4 namespace */ |