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

4 files changed, 112 insertions, 12 deletions

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 */