Naive implementation of subset-minimal unsat core

src/api/MainSolver.cc

@@ -231,7 +231,8 @@ 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();
+    UnsatCoreBuilder unsatCoreBuilder{config, logic, proof, pmanager, termNames};
 
     return unsatCoreBuilder.build();
 }

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_verbosity      = ":verbosity";
   const char* SMTConfig::o_incremental    = ":incremental";
   const char* SMTConfig::o_produce_stats  = ":produce-stats";

src/options/SMTConfig.h

@@ -306,6 +306,8 @@ namespace opensmt {
     static const char* o_sat_split_randomize_lookahead_buf;
     static const char* o_produce_models;
     static const char* o_produce_unsat_cores;
+    // Produce the unsat cores as locally minimal (i.e. subset-minimal)
+    static const char* o_minimal_unsat_cores;
     static const char* o_sat_remove_symmetries;
     static const char* o_dryrun;
     static const char* o_do_substitutions;
@@ -515,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;
+    }
     int          produceStats() const
       { return optionTable.has(o_produce_stats) ?
           optionTable[o_produce_stats]->getValue().numval == 1: false; }

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;       }
 ":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;      }
 ":regular-output-channel"    { yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_REGULAROUTPUTCHANNEL;    }

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_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_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_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_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_PRODUCEMODELS b_value
         {
             $$ = new ASTNode(OPTION_T, $1);
@@ -611,6 +617,8 @@ predef_key: KW_SORTS
         { $$ = $1; }
     | KW_PRODUCEUNSATCORES
         { $$ = $1; }
+    | KW_MINIMALUNSATCORES
+        { $$ = $1; }
     | KW_PRODUCEMODELS
         { $$ = $1; }
     | KW_PRODUCEASSIGNMENTS

src/unsatcores/UnsatCoreBuilder.cc

@@ -1,10 +1,12 @@
 
 #include "UnsatCoreBuilder.h"
 
+#include <api/MainSolver.h>
 #include <api/PartitionManager.h>
 #include <common/PartitionInfo.h>
 #include <common/TermNames.h>
 #include <interpolation/InterpolationUtils.h>
+#include <logics/Logic.h>
 #include <smtsolvers/ResolutionProof.h>
 
 #include <unordered_set>
@@ -14,11 +16,55 @@ namespace opensmt {
 
 using Partitions = ipartitions_t;
 
+std::unique_ptr<SMTConfig> UnsatCoreBuilder::newSmtSolverConfig() const {
+    assert(config.minimal_unsat_cores());
+
+    SMTConfig newConfig;
+    assert(newConfig.isIncremental());
+    assert(newConfig.verbosity() == 0);
+    assert(not newConfig.printSuccess());
+    assert(not newConfig.produceStats());
+    assert(not newConfig.produce_unsat_cores());
+    assert(not newConfig.produce_proof());
+    assert(not newConfig.produce_inter());
+
+    char const * msg = "ok";
+    newConfig.setOption(SMTConfig::o_produce_models, SMTOption(false), msg);
+    assert(not newConfig.produce_models());
+
+    return std::make_unique<SMTConfig>(std::move(newConfig));
+}
+
+std::unique_ptr<UnsatCoreBuilder::SMTSolver> UnsatCoreBuilder::newSmtSolver() const {
+    assert(config.minimal_unsat_cores());
+
+    return std::make_unique<SMTSolver>(logic, *smtSolverConfigPtr, "unsat core solver");
+}
+
+void UnsatCoreBuilder::setSmtSolverConfig() {
+    assert(not smtSolverConfigPtr);
+    smtSolverConfigPtr = newSmtSolverConfig();
+}
+
+void UnsatCoreBuilder::setSmtSolver() {
+    assert(not smtSolverPtr);
+    smtSolverPtr = newSmtSolver();
+}
+
 std::unique_ptr<UnsatCore> UnsatCoreBuilder::build() {
+    buildBody();
+    return buildReturn();
+}
+
+void UnsatCoreBuilder::buildBody() {
     computeClauses();
     computeTerms();
     computeNamedTerms();
 
+    if (config.minimal_unsat_cores()) { minimize(); }
+}
+
+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,12 +111,84 @@ 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);
     }
 }
 
+void UnsatCoreBuilder::minimize() {
+    minimizeInit();
+    minimizeAlg();
+    minimizeFinish();
+}
+
+void UnsatCoreBuilder::minimizeInit() {
+    assert(terms.size() >= namedTerms.size());
+    assert(size_t(namedTerms.size()) == namedTermsIdxs.size());
+
+    setSmtSolverConfig();
+    setSmtSolver();
+}
+
+void UnsatCoreBuilder::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/UnsatCoreBuilder.h

@@ -7,42 +7,70 @@
 #include <options/SMTConfig.h>
 
 #include <memory>
+#include <vector>
 
 namespace opensmt {
 
 class UnsatCore;
 
+class Logic;
 class ResolutionProof;
 class PartitionManager;
 class TermNames;
 
+class MainSolver;
+
 class UnsatCoreBuilder {
 public:
     using Proof = ResolutionProof;
 
-    UnsatCoreBuilder(SMTConfig const & conf, Proof const & proof_, PartitionManager const & pmanager,
+    UnsatCoreBuilder(SMTConfig const & conf, Logic & logic_, Proof const & proof_, PartitionManager const & pmanager,
                      TermNames const & names)
         : config{conf},
+          logic{logic_},
           proof{proof_},
           partitionManager{pmanager},
           termNames{names} {}
 
     std::unique_ptr<UnsatCore> build();
 
 protected:
+    using SMTSolver = MainSolver;
+
+    std::unique_ptr<SMTConfig> newSmtSolverConfig() const;
+    std::unique_ptr<SMTSolver> newSmtSolver() const;
+    void setSmtSolverConfig();
+    void setSmtSolver();
+
+    void buildBody();
+    std::unique_ptr<UnsatCore> buildReturn();
+
     void computeClauses();
     void computeTerms();
     void computeNamedTerms();
 
+    void minimize();
+
+    void minimizeInit();
+    void minimizeAlg() { minimizeAlgNaive(); }
+    void minimizeFinish() {}
+
+    void minimizeAlgNaive();
+
     SMTConfig const & config;
+    Logic & logic;
     Proof const & proof;
     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{};
+
+    std::unique_ptr<SMTConfig> smtSolverConfigPtr{};
+    std::unique_ptr<SMTSolver> smtSolverPtr{};
 };
 
 } // namespace opensmt

test/regression/base/generic/overlap_min_unsat_core.smt2

@@ -0,0 +1,11 @@
+(set-option :produce-unsat-cores true)
+(set-option :minimal-unsat-cores true)
+(set-logic QF_UF)
+(declare-fun b1 () Bool)
+(declare-fun b2 () Bool)
+(assert (! b1 :named a1))
+(assert (! (and b1 b2) :named a2))
+(assert (! (or (not b1) (not b2)) :named a3))
+(check-sat)
+(get-unsat-core)
+(exit)

test/regression/base/generic/overlap_min_unsat_core.smt2.expected.out

@@ -0,0 +1,2 @@
+unsat
+( a2 a3 )

test/regression/base/generic/overlap_unsat_core.smt2

@@ -0,0 +1,10 @@
+(set-option :produce-unsat-cores true)
+(set-logic QF_UF)
+(declare-fun b1 () Bool)
+(declare-fun b2 () Bool)
+(assert (! b1 :named a1))
+(assert (! (and b1 b2) :named a2))
+(assert (! (or (not b1) (not b2)) :named a3))
+(check-sat)
+(get-unsat-core)
+(exit)

test/regression/base/generic/overlap_unsat_core.smt2.expected.out

@@ -0,0 +1,2 @@
+unsat
+( a1 a2 a3 )

test/regression/base/generic/redundant_min_unsat_core.smt2

@@ -0,0 +1,17 @@
+(set-option :produce-unsat-cores true)
+(set-option :minimal-unsat-cores true)
+
+(set-logic QF_UF)
+
+(declare-const b1 Bool)
+(declare-const b2 Bool)
+
+(assert (! b1 :named a1))
+(assert (! b2 :named a2))
+(assert (! (not b1) :named a3))
+(assert (! (and b1 b2) :named x1))
+(assert (! (or b1 b2) :named x2))
+(assert (! (xor b1 b2) :named x3))
+
+(check-sat)
+(get-unsat-core)

test/regression/base/generic/redundant_min_unsat_core.smt2.expected.out

@@ -0,0 +1,2 @@
+unsat
+( a1 a3 )

test/regression/base/generic/redundant_min_unsat_core2.smt2

@@ -0,0 +1,17 @@
+(set-option :produce-unsat-cores true)
+(set-option :minimal-unsat-cores true)
+
+(set-logic QF_UF)
+
+(declare-const b1 Bool)
+(declare-const b2 Bool)
+
+(assert (! (and b1 b2) :named x1))
+(assert (! (or b1 b2) :named x2))
+(assert (! (xor b1 b2) :named x3))
+(assert (! b1 :named a1))
+(assert (! b2 :named a2))
+(assert (! (not b1) :named a3))
+
+(check-sat)
+(get-unsat-core)

test/regression/base/generic/redundant_min_unsat_core2.smt2.expected.out

@@ -0,0 +1,2 @@
+unsat
+( x1 x3 )