From: Andrew Reynolds Date: Thu, 19 Nov 2020 12:42:04 +0000 (-0600) Subject: Use symbol manager for unsat cores (#5468) X-Git-Tag: cvc5-1.0.0~2582 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b0130a1e032c201fab3c4b19f25871428b761967;p=cvc5.git 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. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 47903ccae..c570dfdb4 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -219,8 +219,6 @@ libcvc4_add_sources( smt/dump.h smt/dump_manager.cpp smt/dump_manager.h - smt/expr_names.cpp - smt/expr_names.h smt/listeners.cpp smt/listeners.h smt/logic_exception.h diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp index 75ffa4f62..a163e503d 100644 --- a/src/expr/symbol_manager.cpp +++ b/src/expr/symbol_manager.cpp @@ -77,18 +77,20 @@ bool SymbolManager::Implementation::setExpressionName(api::Term t, const std::string& name, bool isAssertion) { + Trace("sym-manager") << "set expression name: " << t << " -> " << name + << ", isAssertion=" << isAssertion << std::endl; // cannot name subexpressions under quantifiers PrettyCheckArgument( !d_hasPushedScope.get(), name, "cannot name function in a scope"); + if (isAssertion) + { + d_namedAsserts.insert(t); + } if (d_names.find(t) != d_names.end()) { // already named assertion return false; } - if (isAssertion) - { - d_namedAsserts.insert(t); - } d_names[t] = name; return true; } diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 2b32afa15..f81bfc163 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -365,12 +365,7 @@ command [std::unique_ptr* cmd] // set the expression name, if there was a named term std::pair namedTerm = PARSER_STATE->lastNamedTerm(); - // TODO (projects-248) - // SYM_MAN->setExpressionName(namedTerm.first, namedTerm.second, true); - Command* csen = - new SetExpressionNameCommand(namedTerm.first, namedTerm.second); - csen->setMuted(true); - PARSER_STATE->preemptCommand(csen); + SYM_MAN->setExpressionName(namedTerm.first, namedTerm.second, true); } } | /* check-sat */ diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 8e29c25f1..71c1de2fa 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -121,6 +121,8 @@ using namespace CVC4::parser; #define PARSER_STATE ((Tptp*)PARSER->super) #undef SOLVER #define SOLVER PARSER_STATE->getSolver() +#undef SYM_MAN +#define SYM_MAN PARSER_STATE->getSymbolManager() #undef MK_TERM #define MK_TERM SOLVER->mkTerm #define UNSUPPORTED PARSER_STATE->unimplementedFeature @@ -164,9 +166,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr, expr); if( !aexpr.isNull() ){ // set the expression name (e.g. used with unsat core printing) - Command* csen = new SetExpressionNameCommand(aexpr, name); - csen->setMuted(true); - PARSER_STATE->preemptCommand(csen); + SYM_MAN->setExpressionName(aexpr, name, true); } // make the command to assert the formula cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ true, true); @@ -178,9 +178,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr); if( !aexpr.isNull() ){ // set the expression name (e.g. used with unsat core printing) - Command* csen = new SetExpressionNameCommand(aexpr, name); - csen->setMuted(true); - PARSER_STATE->preemptCommand(csen); + SYM_MAN->setExpressionName(aexpr, name, true); } // make the command to assert the formula cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ false, true); @@ -194,9 +192,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr); if( !aexpr.isNull() ){ // set the expression name (e.g. used with unsat core printing) - Command* csen = new SetExpressionNameCommand(aexpr, name); - csen->setMuted(true); - PARSER_STATE->preemptCommand(csen); + SYM_MAN->setExpressionName(aexpr, name, true); } // make the command to assert the formula cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ false, true); @@ -219,9 +215,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] if (!aexpr.isNull()) { // set the expression name (e.g. used with unsat core printing) - Command* csen = new SetExpressionNameCommand(aexpr, name); - csen->setMuted(true); - PARSER_STATE->preemptCommand(csen); + SYM_MAN->setExpressionName(aexpr, name, true); } // make the command to assert the formula cmd = PARSER_STATE->makeAssertCommand( 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& 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; } } diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp index 92bbc52e8..c93f3593a 100644 --- a/src/printer/tptp/tptp_printer.cpp +++ b/src/printer/tptp/tptp_printer.cpp @@ -71,15 +71,20 @@ void TptpPrinter::toStream(std::ostream& out, void TptpPrinter::toStream(std::ostream& out, const UnsatCore& core) const { out << "% SZS output start UnsatCore " << 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 << 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& cnames = core.getCoreNames(); + for (const std::string& cn : cnames) + { + out << cn << std::endl; + } + } + else + { + // otherwise, use the formulas + for (UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i) + { out << *i << endl; } } diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp index cfa6dfb59..dd470b299 100644 --- a/src/proof/unsat_core.cpp +++ b/src/proof/unsat_core.cpp @@ -10,8 +10,6 @@ ** directory for licensing information.\endverbatim ** ** \brief Representation of unsat cores - ** - ** Representation of unsat cores. **/ #include "proof/unsat_core.h" @@ -24,10 +22,24 @@ namespace CVC4 { -void UnsatCore::initMessage() const { +UnsatCore::UnsatCore(const std::vector& core) + : d_useNames(false), d_core(core), d_names() +{ Debug("core") << "UnsatCore size " << d_core.size() << std::endl; } +UnsatCore::UnsatCore(std::vector& names) + : d_useNames(true), d_core(), d_names(names) +{ + Debug("core") << "UnsatCore (names) size " << d_names.size() << std::endl; +} + +const std::vector& UnsatCore::getCore() const { return d_core; } +const std::vector& UnsatCore::getCoreNames() const +{ + return d_names; +} + UnsatCore::const_iterator UnsatCore::begin() const { return d_core.begin(); } @@ -37,8 +49,6 @@ UnsatCore::const_iterator UnsatCore::end() const { } void UnsatCore::toStream(std::ostream& out) const { - Assert(d_smt != NULL); - smt::SmtScope smts(d_smt); expr::ExprDag::Scope scope(out, false); Printer::getPrinter(options::outputLanguage())->toStream(out, *this); } diff --git a/src/proof/unsat_core.h b/src/proof/unsat_core.h index b0e3de24e..fb3401876 100644 --- a/src/proof/unsat_core.h +++ b/src/proof/unsat_core.h @@ -9,10 +9,7 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file + ** \brief Representation of unsat cores. **/ #include "cvc4_private.h" @@ -27,44 +24,45 @@ namespace CVC4 { -class SmtEngine; - +/** + * An unsat core, which can optionally be initialized as a list of names + * or as a list of formulas. + */ class UnsatCore { - /** The SmtEngine we're associated with */ - SmtEngine* d_smt; - - std::vector d_core; - - void initMessage() const; - -public: - UnsatCore() : d_smt(NULL) {} - - UnsatCore(SmtEngine* smt, const std::vector& core) - : d_smt(smt), d_core(core) - { - initMessage(); - } - + public: + UnsatCore() {} + /** Initialize using assertions */ + UnsatCore(const std::vector& core); + /** Initialize using assertion names */ + UnsatCore(std::vector& names); ~UnsatCore() {} - /** get the smt engine that this unsat core is hooked up to */ - SmtEngine* getSmtEngine() const { return d_smt; } - - size_t size() const { return d_core.size(); } + /** Whether we are using names for this unsat core */ + bool useNames() const { return d_useNames; } + /** Get the assertions in the unsat core */ + const std::vector& getCore() const; + /** Get their names */ + const std::vector& getCoreNames() const; typedef std::vector::const_iterator iterator; typedef std::vector::const_iterator const_iterator; const_iterator begin() const; const_iterator end() const; - - /** prints this UnsatCore object to the stream out. - * We use the expression names stored in the SmtEngine d_smt - */ + + /** + * prints this UnsatCore object to the stream out. + */ void toStream(std::ostream& out) const; + private: + /** Whether we are using names for this unsat core */ + bool d_useNames; + /** The unsat core */ + std::vector d_core; + /** The names of assertions in the above core */ + std::vector d_names; };/* class UnsatCore */ /** Print the unsat core to stream out */ diff --git a/src/smt/command.cpp b/src/smt/command.cpp index c8362fae1..717d423fe 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -2289,12 +2289,12 @@ void GetUnsatAssumptionsCommand::toStream(std::ostream& out, /* class GetUnsatCoreCommand */ /* -------------------------------------------------------------------------- */ -GetUnsatCoreCommand::GetUnsatCoreCommand() {} +GetUnsatCoreCommand::GetUnsatCoreCommand() : d_sm(nullptr) {} void GetUnsatCoreCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { - d_solver = solver; + d_sm = sm; d_result = solver->getUnsatCore(); d_commandStatus = CommandSuccess::instance(); @@ -2318,8 +2318,20 @@ void GetUnsatCoreCommand::printResult(std::ostream& out, } else { - UnsatCore ucr(d_solver->getSmtEngine(), api::termVectorToNodes(d_result)); - ucr.toStream(out); + if (options::dumpUnsatCoresFull()) + { + // use the assertions + UnsatCore ucr(api::termVectorToNodes(d_result)); + ucr.toStream(out); + } + else + { + // otherwise, use the names + std::vector names; + d_sm->getExpressionNames(d_result, names, true); + UnsatCore ucr(names); + ucr.toStream(out); + } } } @@ -2332,7 +2344,7 @@ const std::vector& GetUnsatCoreCommand::getUnsatCore() const Command* GetUnsatCoreCommand::clone() const { GetUnsatCoreCommand* c = new GetUnsatCoreCommand; - c->d_solver = d_solver; + c->d_sm = d_sm; c->d_result = d_result; return c; } @@ -2709,42 +2721,6 @@ void GetOptionCommand::toStream(std::ostream& out, Printer::getPrinter(language)->toStreamCmdGetOption(out, d_flag); } -/* -------------------------------------------------------------------------- */ -/* class SetExpressionNameCommand */ -/* -------------------------------------------------------------------------- */ - -SetExpressionNameCommand::SetExpressionNameCommand(api::Term term, - std::string name) - : d_term(term), d_name(name) -{ -} - -void SetExpressionNameCommand::invoke(api::Solver* solver, SymbolManager* sm) -{ - solver->getSmtEngine()->setExpressionName(d_term.getExpr(), d_name); - d_commandStatus = CommandSuccess::instance(); -} - -Command* SetExpressionNameCommand::clone() const -{ - SetExpressionNameCommand* c = new SetExpressionNameCommand(d_term, d_name); - return c; -} - -std::string SetExpressionNameCommand::getCommandName() const -{ - return "set-expr-name"; -} - -void SetExpressionNameCommand::toStream(std::ostream& out, - int toDepth, - size_t dag, - OutputLanguage language) const -{ - Printer::getPrinter(language)->toStreamCmdSetExpressionName( - out, d_term.getNode(), d_name); -} - /* -------------------------------------------------------------------------- */ /* class DatatypeDeclarationCommand */ /* -------------------------------------------------------------------------- */ diff --git a/src/smt/command.h b/src/smt/command.h index 85897458d..96a6938d6 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -1221,8 +1221,8 @@ class CVC4_PUBLIC GetUnsatCoreCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; protected: - /** The solver we were invoked with */ - api::Solver* d_solver; + /** The symbol manager we were invoked with */ + SymbolManager* d_sm; /** the result of the unsat core call */ std::vector d_result; }; /* class GetUnsatCoreCommand */ @@ -1376,32 +1376,6 @@ class CVC4_PUBLIC GetOptionCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetOptionCommand */ -// Set expression name command -// Note this is not an official smt2 command -// Conceptually: -// (assert (! expr :named name)) -// is converted to -// (assert expr) -// (set-expr-name expr name) -class CVC4_PUBLIC SetExpressionNameCommand : public Command -{ - protected: - api::Term d_term; - std::string d_name; - - public: - SetExpressionNameCommand(api::Term term, std::string name); - - void invoke(api::Solver* solver, SymbolManager* sm) override; - Command* clone() const override; - std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; -}; /* class SetExpressionNameCommand */ - class CVC4_PUBLIC DatatypeDeclarationCommand : public Command { private: diff --git a/src/smt/expr_names.cpp b/src/smt/expr_names.cpp deleted file mode 100644 index ccced2cac..000000000 --- a/src/smt/expr_names.cpp +++ /dev/null @@ -1,39 +0,0 @@ -/********************* */ -/*! \file expr_names.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Utility for maintaining expression names. - **/ - -#include "smt/expr_names.h" - -namespace CVC4 { -namespace smt { - -ExprNames::ExprNames(context::UserContext* u) - : d_exprNames(u) -{ -} - -void ExprNames::setExpressionName(const Node& e, const std::string& name) { - d_exprNames[e] = name; -} - -bool ExprNames::getExpressionName(const Node& e, std::string& name) const { - auto it = d_exprNames.find(e); - if(it!=d_exprNames.end()) { - name = (*it).second; - return true; - } - return false; -} - -} // namespace smt -} // namespace CVC4 diff --git a/src/smt/expr_names.h b/src/smt/expr_names.h deleted file mode 100644 index 9a13b0c08..000000000 --- a/src/smt/expr_names.h +++ /dev/null @@ -1,59 +0,0 @@ -/********************* */ -/*! \file expr_names.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Aina Niemetz, Kshitij Bansal - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Utility for maintaining expression names. - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__SMT__EXPR_NAMES_H -#define CVC4__SMT__EXPR_NAMES_H - -#include - -#include "context/cdhashmap.h" -#include "expr/node.h" - -namespace CVC4 { -namespace smt { - -/** - * This utility is responsible for maintaining names for expressions. - */ -class ExprNames -{ - public: - ExprNames(context::UserContext* u); - /** - * Get expression name. - * - * Return true if given expression has a name in the current context. - * If it returns true, the name of expression 'e' is stored in 'name'. - */ - bool getExpressionName(const Node& e, std::string& name) const; - - /** - * Set name of given expression 'e' to 'name'. - * - * This information is user-context-dependent. - * If 'e' already has a name, it is overwritten. - */ - void setExpressionName(const Node& e, const std::string& name); - - private: - /** mapping from expressions to name */ - context::CDHashMap< Node, std::string, NodeHashFunction > d_exprNames; -}; - -} // namespace smt -} // namespace CVC4 - -#endif diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8aad05235..27bcdc036 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -38,7 +38,6 @@ #include "smt/check_models.h" #include "smt/defined_function.h" #include "smt/dump_manager.h" -#include "smt/expr_names.h" #include "smt/interpolation_solver.h" #include "smt/listeners.h" #include "smt/logic_request.h" @@ -80,7 +79,6 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_nodeManager(d_exprManager->getNodeManager()), d_absValues(new AbstractValues(d_nodeManager)), d_asserts(new Assertions(getUserContext(), *d_absValues.get())), - d_exprNames(new ExprNames(getUserContext())), d_dumpm(new DumpManager(getUserContext())), d_routListener(new ResourceOutListener(*this)), d_snmListener(new SmtNodeManagerListener(*d_dumpm.get(), d_outMgr)), @@ -334,7 +332,6 @@ SmtEngine::~SmtEngine() d_absValues.reset(nullptr); d_asserts.reset(nullptr); - d_exprNames.reset(nullptr); d_dumpm.reset(nullptr); d_sygusSolver.reset(nullptr); @@ -1391,7 +1388,7 @@ UnsatCore SmtEngine::getUnsatCoreInternal() } d_proofManager->traceUnsatCore(); // just to trigger core creation - return UnsatCore(this, d_proofManager->extractUnsatCore()); + return UnsatCore(d_proofManager->extractUnsatCore()); #else /* IS_PROOFS_BUILD */ throw ModalException( "This build of CVC4 doesn't have proof support (required for unsat " @@ -1418,7 +1415,8 @@ void SmtEngine::checkUnsatCore() { coreChecker->declareSepHeap(sepLocType, sepDataType); } - Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core.size() << ")" << endl; + Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions" + << std::endl; for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) { Node assertionAfterExpansion = expandDefinitions(*i); Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i @@ -1857,15 +1855,6 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const return SExpr::parseAtom(d_options.getOption(key)); } -bool SmtEngine::getExpressionName(const Node& e, std::string& name) const { - return d_exprNames->getExpressionName(e, name); -} - -void SmtEngine::setExpressionName(const Node& e, const std::string& name) { - Trace("smt-debug") << "Set expression name " << e << " to " << name << std::endl; - d_exprNames->setExpressionName(e,name); -} - Options& SmtEngine::getOptions() { return d_options; } const Options& SmtEngine::getOptions() const { return d_options; } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index d8d2ea171..6c721b9b0 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -822,22 +822,6 @@ class CVC4_PUBLIC SmtEngine const std::vector& expr_values, const std::string& str_value); - /** - * Get expression name. - * - * Return true if given expressoion has a name in the current context. - * If it returns true, the name of expression 'e' is stored in 'name'. - */ - bool getExpressionName(const Node& e, std::string& name) const; - - /** - * Set name of given expression 'e' to 'name'. - * - * This information is user-context-dependent. - * If 'e' already has a name, it is overwritten. - */ - void setExpressionName(const Node& e, const std::string& name); - /** Get the options object (const and non-const versions) */ Options& getOptions(); const Options& getOptions() const; @@ -1049,8 +1033,6 @@ class CVC4_PUBLIC SmtEngine std::unique_ptr d_absValues; /** Assertions manager */ std::unique_ptr d_asserts; - /** Expression names */ - std::unique_ptr d_exprNames; /** The dump manager */ std::unique_ptr d_dumpm; /** Resource out listener */