From 3153e2d94d1b12562557d60305bcac52d3128b83 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 11 Oct 2017 06:11:46 -0500 Subject: Move unsat core names to smt engine (#1192) * Move unsat core names to SmtEnginePrivate. Adds a SetExpressionNameCommand to do this. Removes the names field from GetUnsatCoreCommand. * Comment * Pass expression names by reference. * Update throw specifiers. * Minor * Switch expression names to CDMap, simplify interface for printing unsat core names. * Revert throw specifier change. * Minor simplifcations --- src/parser/smt2/Smt2.g | 14 ++++++------ src/parser/smt2/smt2.cpp | 3 --- src/parser/smt2/smt2.h | 18 ---------------- src/printer/printer.cpp | 7 +----- src/printer/printer.h | 3 --- src/printer/smt2/smt2_printer.cpp | 10 +++++---- src/printer/smt2/smt2_printer.h | 6 +++++- src/proof/unsat_core.cpp | 7 ------ src/proof/unsat_core.h | 8 ++++--- src/smt/command.cpp | 36 +++++++++++++++++++++++++------ src/smt/command.h | 29 +++++++++++++++++++++---- src/smt/smt_engine.cpp | 45 +++++++++++++++++++++++++++++++++++++-- src/smt/smt_engine.h | 14 ++++++++++++ 13 files changed, 135 insertions(+), 65 deletions(-) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 1b3d7b23f..ce1cd1fbd 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -416,7 +416,11 @@ command [std::unique_ptr* cmd] { bool inUnsatCore = PARSER_STATE->lastNamedTerm().first == expr; cmd->reset(new AssertCommand(expr, inUnsatCore)); if(inUnsatCore) { - PARSER_STATE->registerUnsatCoreName(PARSER_STATE->lastNamedTerm()); + // set the expression name, if there was a named term + std::pair namedTerm = PARSER_STATE->lastNamedTerm(); + Command* csen = new SetExpressionNameCommand(namedTerm.first, namedTerm.second); + csen->setMuted(true); + PARSER_STATE->preemptCommand(csen); } } | /* check-sat */ @@ -443,7 +447,7 @@ command [std::unique_ptr* cmd] { cmd->reset(new GetProofCommand()); } | /* get-unsat-core */ GET_UNSAT_CORE_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { cmd->reset(new GetUnsatCoreCommand(PARSER_STATE->getUnsatCoreNames())); } + { cmd->reset(new GetUnsatCoreCommand); } | /* push */ PUSH_TOK { PARSER_STATE->checkThatLogicIsSet(); } { if( PARSER_STATE->sygus() ){ @@ -456,13 +460,11 @@ command [std::unique_ptr* cmd] cmd->reset(new EmptyCommand()); } else if(n == 1) { PARSER_STATE->pushScope(); - PARSER_STATE->pushUnsatCoreNameScope(); cmd->reset(new PushCommand()); } else { std::unique_ptr seq(new CommandSequence()); do { PARSER_STATE->pushScope(); - PARSER_STATE->pushUnsatCoreNameScope(); Command* push_cmd = new PushCommand(); push_cmd->setMuted(n > 1); seq->addCommand(push_cmd); @@ -477,7 +479,6 @@ command [std::unique_ptr* cmd] "PUSH. Maybe you want (push 1)?"); } else { PARSER_STATE->pushScope(); - PARSER_STATE->pushUnsatCoreNameScope(); cmd->reset(new PushCommand()); } } ) @@ -495,13 +496,11 @@ command [std::unique_ptr* cmd] if(n == 0) { cmd->reset(new EmptyCommand()); } else if(n == 1) { - PARSER_STATE->popUnsatCoreNameScope(); PARSER_STATE->popScope(); cmd->reset(new PopCommand()); } else { std::unique_ptr seq(new CommandSequence()); do { - PARSER_STATE->popUnsatCoreNameScope(); PARSER_STATE->popScope(); Command* pop_command = new PopCommand(); pop_command->setMuted(n > 1); @@ -516,7 +515,6 @@ command [std::unique_ptr* cmd] "Strict compliance mode demands an integer to be provided to POP." "Maybe you want (pop 1)?"); } else { - PARSER_STATE->popUnsatCoreNameScope(); PARSER_STATE->popScope(); cmd->reset(new PopCommand()); } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index a6830d95d..a186c052e 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -36,7 +36,6 @@ namespace parser { Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) : Parser(exprManager,input,strictMode,parseOnly), d_logicSet(false) { - d_unsatCoreNames.push(std::map()); if( !strictModeEnabled() ) { addTheory(Smt2::THEORY_CORE); } @@ -354,10 +353,8 @@ void Smt2::reset() { d_logic = LogicInfo(); operatorKindMap.clear(); d_lastNamedTerm = std::pair(); - d_unsatCoreNames = std::stack< std::map >(); this->Parser::reset(); - d_unsatCoreNames.push(std::map()); if( !strictModeEnabled() ) { addTheory(Smt2::THEORY_CORE); } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 46f1c631b..9614c5524 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -61,8 +61,6 @@ private: LogicInfo d_logic; std::unordered_map operatorKindMap; std::pair d_lastNamedTerm; - // this is a user-context stack - std::stack< std::map > d_unsatCoreNames; // for sygus std::vector d_sygusVars, d_sygusConstraints, d_sygusFunSymbols; std::map< Expr, bool > d_sygusVarPrimed; @@ -156,22 +154,6 @@ public: return d_lastNamedTerm; } - void pushUnsatCoreNameScope() { - d_unsatCoreNames.push(d_unsatCoreNames.top()); - } - - void popUnsatCoreNameScope() { - d_unsatCoreNames.pop(); - } - - void registerUnsatCoreName(std::pair name) { - d_unsatCoreNames.top().insert(name); - } - - std::map getUnsatCoreNames() { - return d_unsatCoreNames.top(); - } - bool isAbstractValue(const std::string& name) { return name.length() >= 2 && name[0] == '@' && name[1] != '0' && name.find_first_not_of("0123456789", 1) == std::string::npos; diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 5e349d123..fd7a4ee19 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -84,17 +84,12 @@ void Printer::toStream(std::ostream& out, const Model& m) const throw() { }/* Printer::toStream(Model) */ void Printer::toStream(std::ostream& out, const UnsatCore& core) const throw() { - std::map names; - toStream(out, core, names); -}/* Printer::toStream(UnsatCore) */ - -void Printer::toStream(std::ostream& out, const UnsatCore& core, const std::map& names) const throw() { for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) { AssertCommand cmd(*i); toStream(out, &cmd, -1, false, -1); out << std::endl; } -}/* Printer::toStream(UnsatCore, std::map) */ +}/* Printer::toStream(UnsatCore) */ Printer* Printer::getPrinter(OutputLanguage lang) throw() { if(lang == language::output::LANG_AUTO) { diff --git a/src/printer/printer.h b/src/printer/printer.h index ec1f92604..ea4865fce 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -77,9 +77,6 @@ public: /** Write an UnsatCore out to a stream with this Printer. */ virtual void toStream(std::ostream& out, const UnsatCore& core) const throw(); - /** Write an UnsatCore out to a stream with this Printer. */ - virtual void toStream(std::ostream& out, const UnsatCore& core, const std::map& names) const throw(); - };/* class Printer */ }/* CVC4 namespace */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 147fefa04..0a8020651 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1141,13 +1141,15 @@ void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const thro }/* Smt2Printer::toStream(CommandStatus*) */ -void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core, const std::map& names) const throw() { +void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core) const throw() { out << "(" << std::endl; + SmtEngine * smt = core.getSmtEngine(); + Assert( smt!=NULL ); for(UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i) { - map::const_iterator j = names.find(*i); - if (j != names.end()) { + std::string name; + if (smt->getExpressionName(*i,name)) { // Named assertions always get printed - out << maybeQuoteSymbol((*j).second) << endl; + out << maybeQuoteSymbol(name) << endl; } else if (options::dumpUnsatCoresFull()) { // Unnamed assertions only get printed if the option is set out << *i << endl; diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index f6438ae87..b7e9e1f40 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -48,7 +48,11 @@ public: void toStream(std::ostream& out, const CommandStatus* s) const throw(); void toStream(std::ostream& out, const SExpr& sexpr) const throw(); void toStream(std::ostream& out, const Model& m) const throw(); - void toStream(std::ostream& out, const UnsatCore& core, const std::map& names) const throw(); + /** print the unsat core to the stream out. + * We use the expression names that are stored in the SMT engine associated + * with the core (UnsatCore::getSmtEngine) for printing named assertions. + */ + void toStream(std::ostream& out, const UnsatCore& core) const throw(); };/* class Smt2Printer */ }/* CVC4::printer::smt2 namespace */ diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp index c8696868e..3e5e493f1 100644 --- a/src/proof/unsat_core.cpp +++ b/src/proof/unsat_core.cpp @@ -44,13 +44,6 @@ void UnsatCore::toStream(std::ostream& out) const { Printer::getPrinter(options::outputLanguage())->toStream(out, *this); } -void UnsatCore::toStream(std::ostream& out, const std::map& names) const { - Assert(d_smt != NULL); - smt::SmtScope smts(d_smt); - expr::ExprDag::Scope scope(out, false); - Printer::getPrinter(options::outputLanguage())->toStream(out, *this, names); -} - std::ostream& operator<<(std::ostream& out, const UnsatCore& core) { core.toStream(out); return out; diff --git a/src/proof/unsat_core.h b/src/proof/unsat_core.h index 6f03dfa5e..46a368372 100644 --- a/src/proof/unsat_core.h +++ b/src/proof/unsat_core.h @@ -52,7 +52,7 @@ public: ~UnsatCore() {} /** get the smt engine that this unsat core is hooked up to */ - SmtEngine* getSmtEngine() { return d_smt; } + SmtEngine* getSmtEngine() const { return d_smt; } size_t size() const { return d_core.size(); } @@ -61,9 +61,11 @@ public: 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 + */ void toStream(std::ostream& out) const; - void toStream(std::ostream& out, const std::map& names) const; };/* class UnsatCore */ diff --git a/src/smt/command.cpp b/src/smt/command.cpp index a4f0c6320..82b494382 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1353,9 +1353,6 @@ std::string GetQuantifierEliminationCommand::getCommandName() const throw() { GetUnsatCoreCommand::GetUnsatCoreCommand() throw() { } -GetUnsatCoreCommand::GetUnsatCoreCommand(const std::map& names) throw() : d_names(names) { -} - void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) { try { d_result = smtEngine->getUnsatCore(); @@ -1371,7 +1368,7 @@ void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) con if(! ok()) { this->Command::printResult(out, verbosity); } else { - d_result.toStream(out, d_names); + d_result.toStream(out); } } @@ -1381,13 +1378,13 @@ const UnsatCore& GetUnsatCoreCommand::getUnsatCore() const throw() { } Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names); + GetUnsatCoreCommand* c = new GetUnsatCoreCommand; c->d_result = d_result; return c; } Command* GetUnsatCoreCommand::clone() const { - GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names); + GetUnsatCoreCommand* c = new GetUnsatCoreCommand; c->d_result = d_result; return c; } @@ -1692,6 +1689,33 @@ std::string GetOptionCommand::getCommandName() const throw() { return "get-option"; } + +/* class SetExpressionNameCommand */ + +SetExpressionNameCommand::SetExpressionNameCommand(Expr expr, std::string name) throw() : +d_expr(expr), d_name(name) { + +} + +void SetExpressionNameCommand::invoke(SmtEngine* smtEngine) { + smtEngine->setExpressionName(d_expr, d_name); + d_commandStatus = CommandSuccess::instance(); +} + +Command* SetExpressionNameCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + SetExpressionNameCommand* c = new SetExpressionNameCommand(d_expr.exportTo(exprManager, variableMap), d_name); + return c; +} + +Command* SetExpressionNameCommand::clone() const { + SetExpressionNameCommand* c = new SetExpressionNameCommand(d_expr, d_name); + return c; +} + +std::string SetExpressionNameCommand::getCommandName() const throw() { + return "set-expr-name"; +} + /* class DatatypeDeclarationCommand */ DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() : diff --git a/src/smt/command.h b/src/smt/command.h index 0e07583b2..839927fc1 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -687,12 +687,8 @@ public: };/* class GetQuantifierEliminationCommand */ class CVC4_PUBLIC GetUnsatCoreCommand : public Command { -protected: - UnsatCore d_result; - std::map d_names; public: GetUnsatCoreCommand() throw(); - GetUnsatCoreCommand(const std::map& names) throw(); ~GetUnsatCoreCommand() throw() {} void invoke(SmtEngine* smtEngine); void printResult(std::ostream& out, uint32_t verbosity = 2) const; @@ -700,6 +696,10 @@ public: Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; std::string getCommandName() const throw(); + +protected: + // the result of the unsat core call + UnsatCore d_result; };/* class GetUnsatCoreCommand */ class CVC4_PUBLIC GetAssertionsCommand : public Command { @@ -804,6 +804,27 @@ public: std::string getCommandName() const throw(); };/* 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: + Expr d_expr; + std::string d_name; +public: + SetExpressionNameCommand(Expr expr, std::string name) throw(); + ~SetExpressionNameCommand() throw() {} + void invoke(SmtEngine* smtEngine); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class SetExpressionNameCommand */ + + class CVC4_PUBLIC DatatypeDeclarationCommand : public Command { private: std::vector d_datatypes; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index bc335f2df..099980653 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -33,6 +33,7 @@ #include "base/listener.h" #include "base/modal_exception.h" #include "base/output.h" +#include "context/cdhashmap.h" #include "context/cdhashset.h" #include "context/cdlist.h" #include "context/context.h" @@ -546,7 +547,11 @@ class SmtEnginePrivate : public NodeManagerListener { /** TODO: whether certain preprocess steps are necessary */ //bool d_needsExpandDefs; - + + //------------------------------- expression names + /** mapping from expressions to name */ + context::CDHashMap< Node, std::string, NodeHashFunction > d_exprNames; + //------------------------------- end expression names public: /** * Map from skolem variables to index in d_assertions containing @@ -671,6 +676,7 @@ public: d_abstractValues(), d_simplifyAssertionsDepth(0), //d_needsExpandDefs(true), //TODO? + d_exprNames(smt.d_userContext), d_iteSkolemMap(), d_iteRemover(smt.d_userContext), d_pbsProcessor(smt.d_userContext), @@ -806,10 +812,17 @@ public: */ void processAssertions(); + /** Process a user push. + */ + void notifyPush() { + + } + /** * Process a user pop. Clears out the non-context-dependent stuff in this * SmtEnginePrivate. Necessary to clear out our assertion vectors in case - * someone does a push-assert-pop without a check-sat. + * someone does a push-assert-pop without a check-sat. It also pops the + * last map of expression names from notifyPush. */ void notifyPop() { d_assertions.clear(); @@ -946,6 +959,24 @@ public: std::ostream* getReplayLog() const { return d_managedReplayLog.getReplayLog(); } + + //------------------------------- expression names + // implements setExpressionName, as described in smt_engine.h + void setExpressionName(Expr e, std::string name) { + d_exprNames[Node::fromExpr(e)] = name; + } + + // implements getExpressionName, as described in smt_engine.h + bool getExpressionName(Expr e, std::string& name) const { + context::CDHashMap< Node, std::string, NodeHashFunction >::const_iterator it = d_exprNames.find(e); + if(it!=d_exprNames.end()) { + name = (*it).second; + return true; + }else{ + return false; + } + } + //------------------------------- end expression names };/* class SmtEnginePrivate */ @@ -5327,6 +5358,7 @@ void SmtEngine::push() throw(ModalException, LogicException, UnsafeInterruptExce finalOptionsAreSet(); doPendingPops(); Trace("smt") << "SMT push()" << endl; + d_private->notifyPush(); d_private->processAssertions(); if(Dump.isOn("benchmark")) { Dump("benchmark") << PushCommand(); @@ -5648,6 +5680,15 @@ void SmtEngine::setReplayStream(ExprStream* replayStream) { AlwaysAssert(!d_fullyInited, "Cannot set replay stream once fully initialized"); d_replayStream = replayStream; +} + +bool SmtEngine::getExpressionName(Expr e, std::string& name) const { + return d_private->getExpressionName(e, name); +} + +void SmtEngine::setExpressionName(Expr e, const std::string& name) { + Trace("smt-debug") << "Set expression name " << e << " to " << name << std::endl; + d_private->setExpressionName(e,name); } }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 735364db8..48ae24898 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -251,6 +251,7 @@ class CVC4_PUBLIC SmtEngine { * Verbosity of various commands. */ std::map d_commandVerbosity; + /** ReplayStream for the solver. */ ExprStream* d_replayStream; @@ -743,6 +744,19 @@ public: * translation. */ void setReplayStream(ExprStream* exprStream); + + /** get expression name + * Returns true if e has an expression name in the current context. + * If it returns true, the name of e is stored in name. + */ + bool getExpressionName(Expr e, std::string& name) const; + + /** set expression name + * Sets the expression name of e to name. + * This information is user-context-dependent. + * If e already has a name, it is overwritten. + */ + void setExpressionName(Expr e, const std::string& name); };/* class SmtEngine */ -- cgit v1.2.3