Treat named and full unsat cores separately but with common interface…

…; moved printing to `UnsatCore`; divided minimization into separate class `Minimize`

src/api/Interpret.cc

@@ -1284,22 +1284,7 @@ void Interpret::getProof()
 
 void Interpret::getUnsatCore() {
     auto const unsatCore = main_solver->getUnsatCore();
-    std::cout << "(\n";
-    auto const & termNames = main_solver->getTermNames();
-    if (not config.print_cores_full()) {
-        // this is the default: we care only about ':named' terms and their names
-        for (PTRef fla : unsatCore->getNamedTerms()) {
-            assert(termNames.contains(fla));
-            auto const & name = termNames.nameForTerm(fla);
-            std::cout << name << '\n';
-        }
-    } else {
-        // we explicitly asked to include all terms and to ignore ':named' terms at all
-        for (PTRef fla : unsatCore->getTerms()) {
-            std::cout << logic->printTerm(fla) << '\n';
-        }
-    }
-    std::cout << ')' << std::endl;
+    unsatCore->print();
 }
 
 void Interpret::getInterpolants(const ASTNode& n)

src/api/MainSolver.cc

@@ -272,8 +272,7 @@ std::unique_ptr<UnsatCore> MainSolver::getUnsatCore() const {
     if (not config.produce_unsat_cores()) { throw ApiException("Producing unsat cores is not enabled"); }
     if (status != s_False) { throw ApiException("Unsat core cannot be extracted if solver is not in UNSAT state"); }
 
-    auto & proof = smt_solver->getResolutionProof();
-    UnsatCoreBuilder unsatCoreBuilder{config, logic, proof, pmanager, termNames};
+    UnsatCoreBuilder unsatCoreBuilder{*this};
 
     return unsatCoreBuilder.build();
 }

src/api/MainSolver.h

@@ -138,6 +138,8 @@ class MainSolver {
     static std::unique_ptr<Theory> createTheory(Logic & logic, SMTConfig & config);
 
 protected:
+    friend class UnsatCoreBuilderBase;
+
     using FrameId = uint32_t;
 
     struct PushFrame {

src/common/TermNames.h

@@ -2,9 +2,12 @@
 #define OPENSMT_TERMNAMES_H
 
 #include "ScopedVector.h"
+#include "TypeUtils.h"
 
+#include <options/SMTConfig.h>
 #include <pterms/PTRef.h>
 
+#include <algorithm>
 #include <optional>
 #include <string>
 #include <type_traits>

src/unsatcores/CMakeLists.txt

@@ -4,6 +4,7 @@ target_sources(unsatcores
 PUBLIC
     "${CMAKE_CURRENT_SOURCE_DIR}/UnsatCore.h"
 PRIVATE
+    "${CMAKE_CURRENT_SOURCE_DIR}/UnsatCore.cc"
     "${CMAKE_CURRENT_SOURCE_DIR}/UnsatCoreBuilder.h"
     "${CMAKE_CURRENT_SOURCE_DIR}/UnsatCoreBuilder.cc"
 )

src/unsatcores/UnsatCore.cc

@@ -0,0 +1,44 @@
+#include "UnsatCore.h"
+
+#include <common/TermNames.h>
+#include <logics/Logic.h>
+
+#include <iostream>
+
+namespace opensmt {
+
+void UnsatCore::print() const {
+    print(std::cout);
+}
+
+void UnsatCore::print(std::ostream & os) const {
+    printBegin(os);
+    printBody(os);
+    printEnd(os);
+}
+
+void UnsatCore::printBegin(std::ostream & os) const {
+    os << "(\n";
+}
+
+void UnsatCore::printBody(std::ostream & os) const {
+    for (PTRef term : getTerms()) {
+        printTerm(os, term);
+        os << '\n';
+    }
+}
+
+void UnsatCore::printEnd(std::ostream & os) const {
+    os << ')' << std::endl;
+}
+
+void NamedUnsatCore::printTerm(std::ostream & os, PTRef term) const {
+    assert(termNames.contains(term));
+    os << termNames.nameForTerm(term);
+}
+
+void FullUnsatCore::printTerm(std::ostream & os, PTRef term) const {
+    os << logic.printTerm(term);
+}
+
+} // namespace opensmt

src/unsatcores/UnsatCore.h

@@ -4,25 +4,77 @@
 #include <minisat/mtl/Vec.h>
 #include <pterms/PTRef.h>
 
+#include <iosfwd>
+
 namespace opensmt {
 
+class Logic;
+class TermNames;
+
 class UnsatCore {
 public:
+    virtual ~UnsatCore() = default;
+
+    virtual vec<PTRef> const & getTerms() const = 0;
+
+    void print() const;
+    void print(std::ostream &) const;
+
+protected:
+    UnsatCore() = default;
+
+    void printBegin(std::ostream &) const;
+    void printBody(std::ostream &) const;
+    void printEnd(std::ostream &) const;
+
+    virtual void printTerm(std::ostream &, PTRef) const = 0;
+};
+
+class NamedUnsatCore : public UnsatCore {
+public:
+    vec<PTRef> const & getTerms() const override { return namedTerms; }
+
+    vec<PTRef> const & getHiddenTerms() const { return hiddenTerms; }
+
+protected:
     friend class UnsatCoreBuilder;
 
-    vec<PTRef> const & getTerms() const { return terms; }
-    vec<PTRef> const & getNamedTerms() const { return namedTerms; }
+    inline NamedUnsatCore(TermNames const &, vec<PTRef> && namedTerms_, vec<PTRef> && hiddenTerms_);
+
+    void printTerm(std::ostream &, PTRef) const override;
+
+    TermNames const & termNames;
+
+    vec<PTRef> namedTerms;
+    vec<PTRef> hiddenTerms;
+};
+
+class FullUnsatCore : public UnsatCore {
+public:
+    vec<PTRef> const & getTerms() const override { return terms; }
 
 protected:
-    inline UnsatCore(vec<PTRef> && terms_, vec<PTRef> && namedTerms_);
+    friend class UnsatCoreBuilder;
+
+    inline FullUnsatCore(Logic const &, vec<PTRef> && terms_);
+
+    void printTerm(std::ostream &, PTRef) const override;
+
+    Logic const & logic;
 
     vec<PTRef> terms;
-    vec<PTRef> namedTerms;
 };
 
-UnsatCore::UnsatCore(vec<PTRef> && terms_, vec<PTRef> && namedTerms_)
-    : terms{std::move(terms_)},
-      namedTerms{std::move(namedTerms_)} {
+////////////////////////////////////////////////////////////////////////////////
+
+NamedUnsatCore::NamedUnsatCore(TermNames const & termNames_, vec<PTRef> && namedTerms_, vec<PTRef> && hiddenTerms_)
+    : termNames{termNames_},
+      namedTerms{std::move(namedTerms_)},
+      hiddenTerms{std::move(hiddenTerms_)} {
+    assert(namedTerms.size() > 0 || hiddenTerms.size() > 0);
+}
+
+FullUnsatCore::FullUnsatCore(Logic const & logic_, vec<PTRef> && terms_) : logic{logic_}, terms{std::move(terms_)} {
     assert(terms.size() > 0);
 }