diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-07-25 09:43:19 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-07-25 09:43:19 -0500 |
commit | 18d42bc7f76b5b144ec498d3b4d3e906224e629f (patch) | |
tree | 739103f85e160de6ba9464d43f52e3d0b47dc555 /src/theory/strings/infer_info.cpp | |
parent | 9ab6fb41bc06883aa7d2071133291aff18466afd (diff) |
Split infer info data structure in strings (#3107)
Diffstat (limited to 'src/theory/strings/infer_info.cpp')
-rw-r--r-- | src/theory/strings/infer_info.cpp | 44 |
1 files changed, 44 insertions, 0 deletions
diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp new file mode 100644 index 000000000..a20f608a6 --- /dev/null +++ b/src/theory/strings/infer_info.cpp @@ -0,0 +1,44 @@ +/********************* */ +/*! \file infer_info.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 inference information utility. + **/ + +#include "theory/strings/infer_info.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace strings { + +std::ostream& operator<<(std::ostream& out, Inference i) +{ + switch (i) + { + case INFER_SSPLIT_CST_PROP: out << "S-Split(CST-P)-prop"; break; + case INFER_SSPLIT_VAR_PROP: out << "S-Split(VAR)-prop"; break; + case INFER_LEN_SPLIT: out << "Len-Split(Len)"; break; + case INFER_LEN_SPLIT_EMP: out << "Len-Split(Emp)"; break; + case INFER_SSPLIT_CST_BINARY: out << "S-Split(CST-P)-binary"; break; + case INFER_SSPLIT_CST: out << "S-Split(CST-P)"; break; + case INFER_SSPLIT_VAR: out << "S-Split(VAR)"; break; + case INFER_FLOOP: out << "F-Loop"; break; + default: out << "?"; break; + } + return out; +} + +InferInfo::InferInfo() : d_id(INFER_NONE), d_index(0), d_rev(false) {} + +} // namespace strings +} // namespace theory +} // namespace CVC4 |