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

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<CVC4::Command>* 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<Expr, std::string> 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<CVC4::Command>* 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<CVC4::Command>* cmd]
           cmd->reset(new EmptyCommand());
         } else if(n == 1) {
           PARSER_STATE->pushScope();
-          PARSER_STATE->pushUnsatCoreNameScope();
           cmd->reset(new PushCommand());
         } else {
           std::unique_ptr<CommandSequence> 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<CVC4::Command>* 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<CVC4::Command>* 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<CommandSequence> 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<CVC4::Command>* 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<Expr, std::string>());
   if( !strictModeEnabled() ) {
     addTheory(Smt2::THEORY_CORE);
   }
@@ -354,10 +353,8 @@ void Smt2::reset() {
   d_logic = LogicInfo();
   operatorKindMap.clear();
   d_lastNamedTerm = std::pair<Expr, std::string>();
-  d_unsatCoreNames = std::stack< std::map<Expr, std::string> >();
   this->Parser::reset();
 
-  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 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<std::string, Kind> operatorKindMap;
   std::pair<Expr, std::string> d_lastNamedTerm;
-  // this is a user-context stack
-  std::stack< std::map<Expr, std::string> > d_unsatCoreNames;
   // for sygus
   std::vector<Expr> 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<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 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<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) {
     AssertCommand cmd(*i);
     toStream(out, &cmd, -1, false, -1);
     out << std::endl;
   }
-}/* Printer::toStream(UnsatCore, std::map<Expr, std::string>) */
+}/* 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<Expr, std::string>& 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<Expr, std::string>& 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<Expr, string>::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<Expr, std::string>& 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<Expr, std::string>& 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<Expr, std::string>& 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<Expr, std::string>& 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<Expr, std::string> d_names;
 public:
   GetUnsatCoreCommand() throw();
-  GetUnsatCoreCommand(const std::map<Expr, std::string>& 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<DatatypeType> 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<std::string, Integer> 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 */