Naive implementation of subset-minimal unsat core

.clang-files

@@ -109,6 +109,8 @@
 ./src/tsolvers/stpsolver/STPSolver.h
 ./src/tsolvers/stpsolver/STPStore.h
 
+./src/unsatcores/MinUnsatCoreBuilder.cc
+./src/unsatcores/MinUnsatCoreBuilder.h
 ./src/unsatcores/UnsatCore.h
 ./src/unsatcores/UnsatCoreBuilder.cc
 ./src/unsatcores/UnsatCoreBuilder.h

src/api/MainSolver.cc

@@ -21,8 +21,11 @@
 #include <tsolvers/IDLTHandler.h>
 #include <tsolvers/LATHandler.h>
 #include <tsolvers/RDLTHandler.h>
+#include <unsatcores/MinUnsatCoreBuilder.h>
 #include <unsatcores/UnsatCoreBuilder.h>
 
+#include <variant>
+
 namespace opensmt {
 
 bool stop;
@@ -231,9 +234,15 @@ 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"); }
 
-    UnsatCoreBuilder unsatCoreBuilder{config, smt_solver->getResolutionProof(), pmanager, termNames};
+    auto & proof = smt_solver->getResolutionProof();
+    auto unsatCoreBuilder = [&]() -> std::variant<UnsatCoreBuilder, MinUnsatCoreBuilder> {
+        if (not config.minimal_unsat_cores()) { return UnsatCoreBuilder{config, proof, pmanager, termNames}; }
+
+        auto auxSMTSolver = std::make_unique<MainSolver>(logic, config, "unsat core solver");
+        return MinUnsatCoreBuilder{config, proof, pmanager, termNames, std::move(auxSMTSolver)};
+    }();
 
-    return unsatCoreBuilder.build();
+    return std::visit([](auto & builder) { return builder.build(); }, unsatCoreBuilder);
 }
 
 lbool MainSolver::getTermValue(PTRef tr) const {

src/options/SMTConfig.cc

@@ -447,6 +447,7 @@ namespace opensmt {
 
   const char* SMTConfig::o_produce_models = ":produce-models";
   const char* SMTConfig::o_produce_unsat_cores = ":produce-unsat-cores";
+  const char* SMTConfig::o_minimal_unsat_cores = ":minimal-unsat-cores";
   const char* SMTConfig::o_print_cores_full = ":print-cores-full";
   const char* SMTConfig::o_verbosity      = ":verbosity";
   const char* SMTConfig::o_incremental    = ":incremental";

src/options/SMTConfig.h

@@ -306,6 +306,7 @@ namespace opensmt {
     static const char* o_sat_split_randomize_lookahead_buf;
     static const char* o_produce_models;
     static const char* o_produce_unsat_cores;
+    static const char* o_minimal_unsat_cores;
     static const char* o_print_cores_full;
     static const char* o_sat_remove_symmetries;
     static const char* o_dryrun;
@@ -516,6 +517,9 @@ namespace opensmt {
     bool produce_unsat_cores() const {
         return optionTable.has(o_produce_unsat_cores) && optionTable[o_produce_unsat_cores]->getValue().numval > 0;
     }
+    bool minimal_unsat_cores() const {
+        return optionTable.has(o_minimal_unsat_cores) && optionTable[o_minimal_unsat_cores]->getValue().numval > 0;
+    }
     bool print_cores_full() const {
         return optionTable.has(o_print_cores_full) && optionTable[o_print_cores_full]->getValue().numval > 0;
     }

src/parsers/smt2new/smt2newlexer.ll

@@ -117,6 +117,7 @@ using namespace opensmt::tokens;
 ":interactive-mode"          { yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_INTERACTIVEMODE;         }
 ":produce-proofs"            { yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_PRODUCEPROOFS;           }
 ":produce-unsat-cores"       { yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_PRODUCEUNSATCORES;       }
+":minimal-unsat-cores"       { yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_MINIMALUNSATCORES;       }
 ":print-cores-full"          { yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_PRINTCORESFULL;          }
 ":produce-models"            { yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_PRODUCEMODELS;           }
 ":produce-assignments"       { yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_PRODUCEASSIGNMENTS;      }

src/parsers/smt2new/smt2newparser.yy

@@ -84,13 +84,13 @@ void osmt_yyerror( YYLTYPE* locp, Smt2newContext* context, const char * s )
 %token TK_AS TK_DECIMAL TK_EXISTS TK_FORALL TK_LET TK_NUMERAL TK_PAR TK_STRING
 %token TK_ASSERT TK_CHECKSAT TK_DECLARESORT TK_DECLAREFUN TK_DECLARECONST TK_DEFINESORT TK_DEFINEFUN TK_EXIT TK_GETASSERTIONS TK_GETASSIGNMENT TK_GETINFO TK_GETOPTION TK_GETPROOF TK_GETUNSATCORE TK_GETVALUE TK_GETMODEL TK_POP TK_PUSH TK_SETLOGIC TK_SETINFO TK_SETOPTION TK_THEORY TK_GETITPS TK_WRSTATE TK_RDSTATE TK_SIMPLIFY TK_WRFUNS TK_ECHO
 %token TK_NUM TK_SYM TK_QSYM TK_KEY TK_STR TK_DEC TK_HEX TK_BIN
-%token KW_SORTS KW_FUNS KW_SORTSDESCRIPTION KW_FUNSDESCRIPTION KW_DEFINITION KW_NOTES KW_THEORIES KW_EXTENSIONS KW_VALUES KW_PRINTSUCCESS KW_EXPANDDEFINITIONS KW_INTERACTIVEMODE KW_PRODUCEPROOFS KW_PRODUCEUNSATCORES KW_PRINTCORESFULL KW_PRODUCEMODELS KW_PRODUCEASSIGNMENTS KW_REGULAROUTPUTCHANNEL KW_DIAGNOSTICOUTPUTCHANNEL KW_RANDOMSEED KW_VERBOSITY KW_ERRORBEHAVIOR KW_NAME KW_NAMED KW_AUTHORS KW_VERSION KW_STATUS KW_REASONUNKNOWN KW_ALLSTATISTICS
+%token KW_SORTS KW_FUNS KW_SORTSDESCRIPTION KW_FUNSDESCRIPTION KW_DEFINITION KW_NOTES KW_THEORIES KW_EXTENSIONS KW_VALUES KW_PRINTSUCCESS KW_EXPANDDEFINITIONS KW_INTERACTIVEMODE KW_PRODUCEPROOFS KW_PRODUCEUNSATCORES KW_MINIMALUNSATCORES KW_PRINTCORESFULL KW_PRODUCEMODELS KW_PRODUCEASSIGNMENTS KW_REGULAROUTPUTCHANNEL KW_DIAGNOSTICOUTPUTCHANNEL KW_RANDOMSEED KW_VERBOSITY KW_ERRORBEHAVIOR KW_NAME KW_NAMED KW_AUTHORS KW_VERSION KW_STATUS KW_REASONUNKNOWN KW_ALLSTATISTICS
 
 %type <tok> TK_AS TK_DECIMAL TK_EXISTS TK_FORALL TK_LET TK_NUMERAL TK_PAR TK_STRING
 %type <tok> TK_ASSERT TK_CHECKSAT TK_DECLARESORT TK_DECLAREFUN TK_DECLARECONST TK_DEFINESORT TK_DEFINEFUN TK_EXIT TK_GETASSERTIONS TK_GETASSIGNMENT TK_GETINFO TK_GETOPTION TK_GETPROOF TK_GETUNSATCORE TK_GETVALUE TK_GETMODEL TK_POP TK_PUSH TK_SETLOGIC TK_SETINFO TK_SETOPTION TK_THEORY TK_GETITPS TK_WRSTATE TK_RDSTATE TK_SIMPLIFY TK_WRFUNS TK_ECHO
 
 %type <str> TK_NUM TK_SYM TK_QSYM TK_KEY TK_STR TK_DEC TK_HEX TK_BIN
-%type <str> KW_SORTS KW_FUNS KW_SORTSDESCRIPTION KW_FUNSDESCRIPTION KW_DEFINITION KW_NOTES KW_THEORIES KW_EXTENSIONS KW_VALUES KW_PRINTSUCCESS KW_EXPANDDEFINITIONS KW_INTERACTIVEMODE KW_PRODUCEPROOFS KW_PRODUCEUNSATCORES KW_PRINTCORESFULL KW_PRODUCEMODELS KW_PRODUCEASSIGNMENTS KW_REGULAROUTPUTCHANNEL KW_DIAGNOSTICOUTPUTCHANNEL KW_RANDOMSEED KW_VERBOSITY KW_ERRORBEHAVIOR KW_NAME KW_NAMED KW_AUTHORS KW_VERSION KW_STATUS KW_REASONUNKNOWN KW_ALLSTATISTICS predef_key
+%type <str> KW_SORTS KW_FUNS KW_SORTSDESCRIPTION KW_FUNSDESCRIPTION KW_DEFINITION KW_NOTES KW_THEORIES KW_EXTENSIONS KW_VALUES KW_PRINTSUCCESS KW_EXPANDDEFINITIONS KW_INTERACTIVEMODE KW_PRODUCEPROOFS KW_PRODUCEUNSATCORES KW_MINIMALUNSATCORES KW_PRINTCORESFULL KW_PRODUCEMODELS KW_PRODUCEASSIGNMENTS KW_REGULAROUTPUTCHANNEL KW_DIAGNOSTICOUTPUTCHANNEL KW_RANDOMSEED KW_VERBOSITY KW_ERRORBEHAVIOR KW_NAME KW_NAMED KW_AUTHORS KW_VERSION KW_STATUS KW_REASONUNKNOWN KW_ALLSTATISTICS predef_key
 %type <snode> symbol identifier sort command attribute attribute_value s_expr spec_const qual_identifier var_binding sorted_var term const_val
 %type <snode_list> sort_list command_list s_expr_list numeral_list term_list var_binding_list attribute_list sorted_var_list symbol_list
 %type <snode> b_value option info_flag
@@ -539,6 +539,12 @@ option: KW_PRINTSUCCESS b_value
             $$->children = new std::vector<ASTNode*>();
             $$->children->push_back($2);
         }
+    | KW_MINIMALUNSATCORES b_value
+        {
+            $$ = new ASTNode(OPTION_T, $1);
+            $$->children = new std::vector<ASTNode*>();
+            $$->children->push_back($2);
+        }
     | KW_PRINTCORESFULL b_value
         {
             $$ = new ASTNode(OPTION_T, $1);
@@ -617,6 +623,8 @@ predef_key: KW_SORTS
         { $$ = $1; }
     | KW_PRODUCEUNSATCORES
         { $$ = $1; }
+    | KW_MINIMALUNSATCORES
+        { $$ = $1; }
     | KW_PRINTCORESFULL
         { $$ = $1; }
     | KW_PRODUCEMODELS

src/unsatcores/CMakeLists.txt

@@ -6,6 +6,8 @@ PUBLIC
 PRIVATE
     "${CMAKE_CURRENT_SOURCE_DIR}/UnsatCoreBuilder.h"
     "${CMAKE_CURRENT_SOURCE_DIR}/UnsatCoreBuilder.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/MinUnsatCoreBuilder.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/MinUnsatCoreBuilder.cc"
 )
 
 install(FILES UnsatCore.h

src/unsatcores/MinUnsatCoreBuilder.cc

@@ -0,0 +1,82 @@
+
+#include "MinUnsatCoreBuilder.h"
+
+#include <api/MainSolver.h>
+
+namespace opensmt {
+
+std::unique_ptr<UnsatCore> MinUnsatCoreBuilder::build() {
+    buildBody();
+    return buildReturn();
+}
+
+void MinUnsatCoreBuilder::buildBody() {
+    UnsatCoreBuilder::buildBody();
+    minimize();
+}
+
+void MinUnsatCoreBuilder::minimize() {
+    minimizeInit();
+    minimizeAlg();
+    minimizeFinish();
+}
+
+void MinUnsatCoreBuilder::minimizeInit() {
+    assert(terms.size() >= namedTerms.size());
+    assert(size_t(namedTerms.size()) == namedTermsIdxs.size());
+}
+
+void MinUnsatCoreBuilder::minimizeAlgNaive() {
+    if (namedTerms.size() == 0) return;
+
+    auto const namedTermsIdxsEnd = namedTermsIdxs.end();
+    auto const isNamedTerm = [namedTermsIdxsEnd](size_t idx, auto namedTermsIdxsIt) {
+        if (namedTermsIdxsIt == namedTermsIdxsEnd) { return false; }
+        assert(idx <= *namedTermsIdxsIt);
+        return (idx == *namedTermsIdxsIt);
+    };
+    decltype(terms) newTerms;
+    size_t const termsSize = terms.size();
+    for (auto [idx, namedTermsIdxsIt] = std::tuple{size_t{0}, namedTermsIdxs.begin()}; idx < termsSize; ++idx) {
+        if (isNamedTerm(idx, namedTermsIdxsIt)) {
+            ++namedTermsIdxsIt;
+            continue;
+        }
+        PTRef term = terms[idx];
+        smtSolverPtr->insertFormula(term);
+        newTerms.push(term);
+    }
+
+    decltype(terms) newNamedTerms;
+    size_t const namedTermsSize = namedTerms.size();
+    for (size_t namedIdx = 0; namedIdx < namedTermsSize; ++namedIdx) {
+        smtSolverPtr->push();
+
+        // try to ignore namedTerms[namedIdx]
+
+        for (size_t keptNamedIdx = namedIdx + 1; keptNamedIdx < namedTermsSize; ++keptNamedIdx) {
+            PTRef term = namedTerms[keptNamedIdx];
+            smtSolverPtr->insertFormula(term);
+        }
+
+        sstat const res = smtSolverPtr->check();
+        assert(res == s_True || res == s_False);
+        bool const isRedundant = (res == s_False);
+
+        smtSolverPtr->pop();
+
+        if (isRedundant) continue;
+
+        // namedTerms[namedIdx] is not redundant - include it
+
+        PTRef term = namedTerms[namedIdx];
+        smtSolverPtr->insertFormula(term);
+        newTerms.push(term);
+        newNamedTerms.push(term);
+    }
+
+    terms = std::move(newTerms);
+    namedTerms = std::move(newNamedTerms);
+}
+
+} // namespace opensmt

src/unsatcores/MinUnsatCoreBuilder.h

@@ -0,0 +1,37 @@
+#ifndef OPENSMT_MINUNSATCOREBUILDER_H
+#define OPENSMT_MINUNSATCOREBUILDER_H
+
+#include "UnsatCoreBuilder.h"
+
+namespace opensmt {
+
+class MainSolver;
+
+class MinUnsatCoreBuilder : public UnsatCoreBuilder {
+public:
+    using SMTSolver = MainSolver;
+
+    MinUnsatCoreBuilder(SMTConfig const & conf, Proof const & proof_, PartitionManager const & pmanager,
+                        TermNames const & names, std::unique_ptr<SMTSolver> && smtSolver)
+        : UnsatCoreBuilder(conf, proof_, pmanager, names),
+          smtSolverPtr{std::move(smtSolver)} {}
+
+    std::unique_ptr<UnsatCore> build();
+
+protected:
+    void buildBody();
+
+    void minimize();
+
+    void minimizeInit();
+    void minimizeAlg() { minimizeAlgNaive(); }
+    void minimizeFinish() {}
+
+    void minimizeAlgNaive();
+
+    std::unique_ptr<SMTSolver> smtSolverPtr;
+};
+
+} // namespace opensmt
+
+#endif // OPENSMT_MINUNSATCOREBUILDER_H

src/unsatcores/UnsatCoreBuilder.cc

@@ -15,10 +15,17 @@ namespace opensmt {
 using Partitions = ipartitions_t;
 
 std::unique_ptr<UnsatCore> UnsatCoreBuilder::build() {
+    buildBody();
+    return buildReturn();
+}
+
+void UnsatCoreBuilder::buildBody() {
     computeClauses();
     computeTerms();
     computeNamedTerms();
+}
 
+std::unique_ptr<UnsatCore> UnsatCoreBuilder::buildReturn() {
     // Not using `make_unique` because only UnsatCoreBuilder is a friend of UnsatCore
     return std::unique_ptr<UnsatCore>{new UnsatCore{std::move(terms), std::move(namedTerms)}};
 }
@@ -65,11 +72,16 @@ void UnsatCoreBuilder::computeTerms() {
 void UnsatCoreBuilder::computeNamedTerms() {
     assert(terms.size() > 0);
     namedTerms.clear();
+    namedTermsIdxs.clear();
 
     if (termNames.empty()) return;
 
-    for (PTRef term : terms) {
-        if (termNames.contains(term)) { namedTerms.push(term); }
+    size_t const termsSize = terms.size();
+    for (size_t idx = 0; idx < termsSize; ++idx) {
+        PTRef term = terms[idx];
+        if (not termNames.contains(term)) { continue; }
+        namedTerms.push(term);
+        namedTermsIdxs.push_back(idx);
     }
 }
 

src/unsatcores/UnsatCoreBuilder.h

@@ -7,6 +7,7 @@
 #include <options/SMTConfig.h>
 
 #include <memory>
+#include <vector>
 
 namespace opensmt {
 
@@ -30,6 +31,9 @@ class UnsatCoreBuilder {
     std::unique_ptr<UnsatCore> build();
 
 protected:
+    void buildBody();
+    std::unique_ptr<UnsatCore> buildReturn();
+
     void computeClauses();
     void computeTerms();
     void computeNamedTerms();
@@ -39,10 +43,11 @@ class UnsatCoreBuilder {
     PartitionManager const & partitionManager;
     TermNames const & termNames;
 
-private:
-    vec<CRef> clauses;
-    vec<PTRef> terms;
-    vec<PTRef> namedTerms;
+    vec<CRef> clauses{};
+    vec<PTRef> terms{};
+    vec<PTRef> namedTerms{};
+
+    std::vector<size_t> namedTermsIdxs{};
 };
 
 } // namespace opensmt