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/smt | |
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/smt')
-rw-r--r-- | src/smt/command.cpp | 36 | ||||
-rw-r--r-- | src/smt/command.h | 29 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 45 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 14 |
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 */ |