Improved SMT-LIBv2 language support for unsat cores.

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<Expr, std::string>& 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<Expr, std::string> d_names;
 public:
   GetUnsatCoreCommand() throw();
+  GetUnsatCoreCommand(const std::map<Expr, std::string>& 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>(), 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<Expr, std::string>());
   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 <string>
 #include <sstream>
+#include <utility>
+#include <stack>
 
 namespace CVC4 {
 
@@ -54,7 +57,9 @@ private:
   bool d_logicSet;
   LogicInfo d_logic;
   std::hash_map<std::string, Kind, StringHashFunction> operatorKindMap;
-  Expr d_lastNamedTerm;
+  std::pair<Expr, std::string> d_lastNamedTerm;
+  // this is a user-context stack
+  std::stack< std::map<Expr, std::string> > 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<Expr, std::string> lastNamedTerm() {
     return d_lastNamedTerm;
   }
 
+  void pushUnsatCoreNameScope() {
+    d_unsatCoreNames.push(d_unsatCoreNames.top());
+  }
+
+  void popUnsatCoreNameScope() {
+    d_unsatCoreNames.pop();
+  }
+
+  void registerUnsatCoreName(std::pair<Expr, std::string> name) {
+    d_unsatCoreNames.top().insert(name);
+  }
+
+  std::map<Expr, std::string> 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<Expr, std::string> names;
+  toStream(out, core, names);
+}/* Printer::toStream(UnsatCore) */
+
+void Printer::toStream(std::ostream& out, const UnsatCore& core, const std::map<Expr, std::string>& 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<Expr, std::string>) */
 
 }/* 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 <map>
+#include <string>
+
 #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<Expr, std::string>& 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<Expr, std::string>& names) const throw() {
+  out << "(" << std::endl;
+  for(UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i) {
+    map<Expr, string>::const_iterator j = names.find(*i);
+    if(j == names.end()) {
+      out << *i << endl;
+    } else {
+      out << (*j).second << endl;
+    }
+  }
   out << ")" << endl;
-}
+}/* Smt2Printer::toStream(UnsatCore, map<Expr, string>) */
 
 
 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<Expr, std::string>& 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<Expr, std::string>& 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<Expr, std::string>& names) const;
 
 };/* class UnsatCore */