diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-11 06:11:46 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-11 06:11:46 -0500 |
commit | 3153e2d94d1b12562557d60305bcac52d3128b83 (patch) | |
tree | ef4740a54d489b61d92163024a8c516f38aae050 /src/parser | |
parent | 5e2c7c3a25d334c0068b423225f8ff7793260069 (diff) |
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
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/Smt2.g | 14 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 3 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 18 |
3 files changed, 6 insertions, 29 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; |