diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-19 06:42:04 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-19 06:42:04 -0600 |
commit | b0130a1e032c201fab3c4b19f25871428b761967 (patch) | |
tree | f18039906a287a4d55345b1c4bd0ac86cf5232c5 /src/printer/smt2 | |
parent | 2901ee18f824d1f9e4338ef2853da0ab4ccbff0e (diff) |
Use symbol manager for unsat cores (#5468)
This PR uses the symbol manager for handling names for unsat cores.
This replaces interfaces in SmtEngine for managing expression names. It removes the SetExpressionName command.
Diffstat (limited to 'src/printer/smt2')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 23 |
1 files changed, 14 insertions, 9 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index bed6a890b..9eb5569e3 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1319,15 +1319,20 @@ void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core) const { out << "(" << std::endl; - SmtEngine * smt = core.getSmtEngine(); - Assert(smt != NULL); - for(UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i) { - std::string name; - if (smt->getExpressionName(*i,name)) { - // Named assertions always get printed - out << CVC4::quoteSymbol(name) << endl; - } else if (options::dumpUnsatCoresFull()) { - // Unnamed assertions only get printed if the option is set + if (core.useNames()) + { + // use the names + const std::vector<std::string>& cnames = core.getCoreNames(); + for (const std::string& cn : cnames) + { + out << CVC4::quoteSymbol(cn) << std::endl; + } + } + else + { + // otherwise, use the formulas + for (UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i) + { out << *i << endl; } } |