From 525e7328cad1ac8afbc60ed8103e06665cf5b163 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 25 Aug 2014 18:40:06 -0400 Subject: [PATCH] Improved SMT-LIBv2 language support for unsat cores. --- src/expr/command.cpp | 14 ++++++++++--- src/expr/command.h | 3 +++ src/main/command_executor.cpp | 6 +++--- src/parser/smt2/Smt2.g | 16 +++++++++++---- src/parser/smt2/smt2.cpp | 1 + src/parser/smt2/smt2.h | 33 +++++++++++++++++++++++++++---- src/printer/printer.cpp | 10 ++++++++-- src/printer/printer.h | 6 ++++++ src/printer/smt2/smt2_printer.cpp | 15 ++++++++++---- src/printer/smt2/smt2_printer.h | 2 +- src/util/unsat_core.cpp | 16 +++++++++------ src/util/unsat_core.h | 1 + 12 files changed, 96 insertions(+), 27 deletions(-) diff --git a/src/expr/command.cpp b/src/expr/command.cpp index a07076281..a3f5170fa 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -1121,6 +1121,9 @@ std::string GetInstantiationsCommand::getCommandName() const throw() { GetUnsatCoreCommand::GetUnsatCoreCommand() throw() { } +GetUnsatCoreCommand::GetUnsatCoreCommand(const std::map& names) throw() : d_names(names) { +} + void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() { try { d_result = smtEngine->getUnsatCore(); @@ -1134,18 +1137,23 @@ void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) con if(! ok()) { this->Command::printResult(out, verbosity); } else { - d_result.toStream(out); + d_result.toStream(out, d_names); } } +const UnsatCore& GetUnsatCoreCommand::getUnsatCore() const throw() { + // of course, this will be empty if the command hasn't been invoked yet + return d_result; +} + Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetUnsatCoreCommand* c = new GetUnsatCoreCommand(); + GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names); c->d_result = d_result; return c; } Command* GetUnsatCoreCommand::clone() const { - GetUnsatCoreCommand* c = new GetUnsatCoreCommand(); + GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names); c->d_result = d_result; return c; } diff --git a/src/expr/command.h b/src/expr/command.h index e84c53d09..4d2957b7c 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -602,11 +602,14 @@ public: 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) throw(); void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + const UnsatCore& getUnsatCore() const throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; std::string getCommandName() const throw(); diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 950728fab..fee7e23a2 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -165,12 +165,12 @@ bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out) void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString, const std::string& curStatsString) { if(prvsStatsString == "") { - out << curStatsString; - return; + out << curStatsString; + return; } // read each line - // if a number, subtract and add that to parantheses + // if a number, subtract and add that to parentheses std::istringstream issPrvs(prvsStatsString); std::istringstream issCur(curStatsString); diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index e1547d23d..2adad092e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -377,9 +377,13 @@ command returns [CVC4::Command* cmd = NULL] { cmd = new GetAssignmentCommand(); } | /* assertion */ ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); } + { PARSER_STATE->clearLastNamedTerm(); } term[expr, expr2] - { cmd = new AssertCommand(expr, /* inUnsatCore */ PARSER_STATE->lastNamedTerm() == expr); - PARSER_STATE->setLastNamedTerm(Expr()); + { bool inUnsatCore = PARSER_STATE->lastNamedTerm().first == expr; + cmd = new AssertCommand(expr, inUnsatCore); + if(inUnsatCore) { + PARSER_STATE->registerUnsatCoreName(PARSER_STATE->lastNamedTerm()); + } } | /* check-sat */ CHECKSAT_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -398,7 +402,7 @@ command returns [CVC4::Command* cmd = NULL] { cmd = new GetProofCommand(); } | /* get-unsat-core */ GET_UNSAT_CORE_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { cmd = new GetUnsatCoreCommand(); } + { cmd = new GetUnsatCoreCommand(PARSER_STATE->getUnsatCoreNames()); } | /* push */ PUSH_TOK { PARSER_STATE->checkThatLogicIsSet(); } ( k=INTEGER_LITERAL @@ -407,11 +411,13 @@ command returns [CVC4::Command* cmd = NULL] cmd = new EmptyCommand(); } else if(n == 1) { PARSER_STATE->pushScope(); + PARSER_STATE->pushUnsatCoreNameScope(); cmd = new PushCommand(); } else { CommandSequence* seq = new CommandSequence(); do { PARSER_STATE->pushScope(); + PARSER_STATE->pushUnsatCoreNameScope(); Command* c = new PushCommand(); c->setMuted(n > 1); seq->addCommand(c); @@ -434,11 +440,13 @@ command returns [CVC4::Command* cmd = NULL] if(n == 0) { cmd = new EmptyCommand(); } else if(n == 1) { + PARSER_STATE->popUnsatCoreNameScope(); PARSER_STATE->popScope(); cmd = new PopCommand(); } else { CommandSequence* seq = new CommandSequence(); do { + PARSER_STATE->popUnsatCoreNameScope(); PARSER_STATE->popScope(); Command* c = new PopCommand(); c->setMuted(n > 1); @@ -1213,7 +1221,7 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] // define it Expr func = PARSER_STATE->mkFunction(name, expr.getType()); // remember the last term to have been given a :named attribute - PARSER_STATE->setLastNamedTerm(expr); + PARSER_STATE->setLastNamedTerm(expr, name); // bind name to expr with define-fun Command* c = new DefineNamedFunctionCommand(name, func, std::vector(), expr); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index fecccfa44..21b6a1e5b 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -31,6 +31,7 @@ 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); } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 7ecd2e5b1..290bbc975 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -24,7 +24,10 @@ #include "theory/logic_info.h" #include "util/abstract_value.h" +#include #include +#include +#include namespace CVC4 { @@ -54,7 +57,9 @@ private: bool d_logicSet; LogicInfo d_logic; std::hash_map operatorKindMap; - Expr d_lastNamedTerm; + std::pair d_lastNamedTerm; + // this is a user-context stack + std::stack< std::map > d_unsatCoreNames; protected: Smt2(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); @@ -106,14 +111,34 @@ public: void includeFile(const std::string& filename); - void setLastNamedTerm(Expr e) { - d_lastNamedTerm = e; + void setLastNamedTerm(Expr e, std::string name) { + d_lastNamedTerm = std::make_pair(e, name); } - Expr lastNamedTerm() { + void clearLastNamedTerm() { + d_lastNamedTerm = std::make_pair(Expr(), ""); + } + + std::pair lastNamedTerm() { 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 7a90f5a49..dd2e180e1 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -154,10 +154,16 @@ 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) { - toStream(out, Node::fromExpr(*i), -1, false, -1); + AssertCommand cmd(*i); + toStream(out, &cmd, -1, false, -1); out << std::endl; } -}/* Printer::toStream(UnsatCore) */ +}/* Printer::toStream(UnsatCore, std::map) */ }/* CVC4 namespace */ diff --git a/src/printer/printer.h b/src/printer/printer.h index 9a9ee19d1..e0b80ddfc 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -19,6 +19,9 @@ #ifndef __CVC4__PRINTER__PRINTER_H #define __CVC4__PRINTER__PRINTER_H +#include +#include + #include "util/language.h" #include "util/sexpr.h" #include "util/model.h" @@ -106,6 +109,9 @@ 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 */ /** diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 543079576..cb1fe87b2 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -771,11 +771,18 @@ void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const thro }/* Smt2Printer::toStream(CommandStatus*) */ -void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core) const throw() { - out << "(" << endl; - this->Printer::toStream(out, core); +void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core, const std::map& names) const throw() { + out << "(" << std::endl; + for(UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i) { + map::const_iterator j = names.find(*i); + if(j == names.end()) { + out << *i << endl; + } else { + out << (*j).second << endl; + } + } out << ")" << endl; -} +}/* Smt2Printer::toStream(UnsatCore, map) */ void Smt2Printer::toStream(std::ostream& out, const Model& m) const throw() { diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index e825d3f4c..dbbc67fc2 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -46,7 +46,7 @@ public: void toStream(std::ostream& out, const Result& r) 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 throw(); + void toStream(std::ostream& out, const UnsatCore& core, const std::map& names) const throw(); };/* class Smt2Printer */ }/* CVC4::printer::smt2 namespace */ diff --git a/src/util/unsat_core.cpp b/src/util/unsat_core.cpp index 6344b3eda..929d5e909 100644 --- a/src/util/unsat_core.cpp +++ b/src/util/unsat_core.cpp @@ -30,15 +30,19 @@ UnsatCore::const_iterator UnsatCore::end() const { } void UnsatCore::toStream(std::ostream& out) const { - for(UnsatCore::const_iterator i = begin(); i != end(); ++i) { - out << AssertCommand(*i) << std::endl; - } + smt::SmtScope smts(d_smt); + Expr::dag::Scope scope(out, false); + Printer::getPrinter(options::outputLanguage())->toStream(out, *this); } -std::ostream& operator<<(std::ostream& out, const UnsatCore& core) { - smt::SmtScope smts(core.d_smt); +void UnsatCore::toStream(std::ostream& out, const std::map& names) const { + smt::SmtScope smts(d_smt); Expr::dag::Scope scope(out, false); - Printer::getPrinter(options::outputLanguage())->toStream(out, core); + 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/util/unsat_core.h b/src/util/unsat_core.h index c67a6e448..27cf86488 100644 --- a/src/util/unsat_core.h +++ b/src/util/unsat_core.h @@ -57,6 +57,7 @@ public: const_iterator end() const; void toStream(std::ostream& out) const; + void toStream(std::ostream& out, const std::map& names) const; };/* class UnsatCore */ -- 2.30.2