From 3153e2d94d1b12562557d60305bcac52d3128b83 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
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 ------------------
 3 files changed, 6 insertions(+), 29 deletions(-)

(limited to 'src/parser')

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;
-- 
cgit v1.2.3