diff options
Diffstat (limited to 'src/theory/incomplete_id.cpp')
| -rw-r--r-- | src/theory/incomplete_id.cpp | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/src/theory/incomplete_id.cpp b/src/theory/incomplete_id.cpp new file mode 100644 index 000000000..340e2c208 --- /dev/null +++ b/src/theory/incomplete_id.cpp @@ -0,0 +1,55 @@ +/********************* */ +/*! \file incomplete_id.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of incompleteness enumeration. + **/ + +#include "theory/incomplete_id.h" + +#include <iostream> + +namespace cvc5 { +namespace theory { + +const char* toString(IncompleteId i) +{ + switch (i) + { + case IncompleteId::ARITH_NL_DISABLED: return "ARITH_NL_DISABLED"; + case IncompleteId::ARITH_NL: return "ARITH_NL"; + case IncompleteId::QUANTIFIERS: return "QUANTIFIERS"; + case IncompleteId::QUANTIFIERS_SYGUS_NO_VERIFY: + return "QUANTIFIERS_SYGUS_NO_VERIFY"; + case IncompleteId::QUANTIFIERS_CEGQI: return "QUANTIFIERS_CEGQI"; + case IncompleteId::QUANTIFIERS_FMF: return "QUANTIFIERS_FMF"; + case IncompleteId::QUANTIFIERS_RECORDED_INST: + return "QUANTIFIERS_RECORDED_INST"; + case IncompleteId::SEP: return "SEP"; + case IncompleteId::SETS_RELS_CARD: return "SETS_RELS_CARD"; + case IncompleteId::STRINGS_LOOP_SKIP: return "STRINGS_LOOP_SKIP"; + case IncompleteId::STRINGS_REGEXP_NO_SIMPLIFY: + return "STRINGS_REGEXP_NO_SIMPLIFY"; + case IncompleteId::UF_HO_EXT_DISABLED: return "UF_HO_EXT_DISABLED"; + case IncompleteId::UF_CARD_DISABLED: return "UF_CARD_DISABLED"; + case IncompleteId::UF_CARD_MODE: return "UF_CARD_MODE"; + case IncompleteId::UNKNOWN: return "UNKNOWN"; + default: return "?IncompleteId?"; + } +} + +std::ostream& operator<<(std::ostream& out, IncompleteId i) +{ + out << toString(i); + return out; +} + +} // namespace theory +} // namespace cvc5 |