Added getting term names out of NamedUnsatCore-s

Author: Tomaqa

src/unsatcores/UnsatCore.cc

@@ -37,6 +37,22 @@ void NamedUnsatCore::printTerm(std::ostream & os, PTRef term) const {
     os << termNames.nameForTerm(term);
 }
 
+std::vector<std::string> NamedUnsatCore::makeTermNamesTp(vec<PTRef> const & terms) const {
+    std::vector<std::string> names;
+    for (PTRef term : terms) {
+        names.push_back(termNames.nameForTerm(term));
+    }
+    return names;
+}
+
+std::vector<std::string> NamedUnsatCore::makeTermNames() const {
+    return makeTermNamesTp(getTerms());
+}
+
+std::vector<std::string> NamedUnsatCore::makeHiddenTermNames() const {
+    return makeTermNamesTp(getHiddenTerms());
+}
+
 void FullUnsatCore::printTerm(std::ostream & os, PTRef term) const {
     os << logic.printTerm(term);
 }

src/unsatcores/UnsatCore.h

@@ -36,6 +36,9 @@ class NamedUnsatCore : public UnsatCore {
 
     vec<PTRef> const & getHiddenTerms() const { return hiddenTerms; }
 
+    std::vector<std::string> makeTermNames() const;
+    std::vector<std::string> makeHiddenTermNames() const;
+
 protected:
     friend class UnsatCoreBuilder;
 
@@ -47,6 +50,9 @@ class NamedUnsatCore : public UnsatCore {
 
     vec<PTRef> namedTerms;
     vec<PTRef> hiddenTerms;
+
+private:
+    std::vector<std::string> makeTermNamesTp(vec<PTRef> const &) const;
 };
 
 class FullUnsatCore : public UnsatCore {