Implemented smt2 option ":print-cores-full" (from CVC5)

src/api/Interpret.cc

@@ -1285,13 +1285,24 @@ void Interpret::getProof()
 
 void Interpret::getUnsatCore() {
     auto const unsatCore = main_solver->getUnsatCore();
-    auto const & unsatCoreTerms = unsatCore->getNamedTerms();
     std::cout << "( ";
     auto & termNames = main_solver->getTermNames();
-    for (PTRef fla : unsatCoreTerms) {
-        assert(termNames.contains(fla));
-        auto const & name = termNames.nameForTerm(fla);
-        std::cout << name << ' ';
+    if (not config.print_cores_full()) {
+        for (PTRef fla : unsatCore->getNamedTerms()) {
+            assert(termNames.contains(fla));
+            auto const & name = termNames.nameForTerm(fla);
+            std::cout << name << ' ';
+        }
+    } else {
+        for (PTRef fla : unsatCore->getTerms()) {
+            if (termNames.contains(fla)) {
+                std::cout << termNames.nameForTerm(fla);
+            }
+            else {
+                std::cout << logic->printTerm(fla);
+            }
+            std::cout << ' ';
+        }
     }
     std::cout << ')' << std::endl;
 }

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_print_cores_full = ":print-cores-full";
   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,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_print_cores_full;
     static const char* o_sat_remove_symmetries;
     static const char* o_dryrun;
     static const char* o_do_substitutions;
@@ -515,6 +516,9 @@ namespace opensmt {
     bool produce_unsat_cores() const {
         return optionTable.has(o_produce_unsat_cores) && optionTable[o_produce_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;
+    }
     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;       }
+":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;      }
 ":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_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_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_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_PRINTCORESFULL 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_PRINTCORESFULL
+        { $$ = $1; }
     | KW_PRODUCEMODELS
         { $$ = $1; }
     | KW_PRODUCEASSIGNMENTS

test/regression/base/generic/trivial_unsat_core2.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)
+(assert (! b2 :named a2))
+(assert (! (not b1) :named a3))
+(check-sat)
+(get-unsat-core)
+(exit)

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

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

test/regression/base/generic/trivial_unsat_core2_full.smt2

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

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

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

test/regression/base/generic/trivial_unsat_core3.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 (! b2 :named a2))
+(assert (not b1))
+(check-sat)
+(get-unsat-core)
+(exit)

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

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

test/regression/base/generic/trivial_unsat_core3_full.smt2

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

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

@@ -0,0 +1,2 @@
+unsat
+( a1 (not b1) )