From b0130a1e032c201fab3c4b19f25871428b761967 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 19 Nov 2020 06:42:04 -0600 Subject: Use symbol manager for unsat cores (#5468) This PR uses the symbol manager for handling names for unsat cores. This replaces interfaces in SmtEngine for managing expression names. It removes the SetExpressionName command. --- src/smt/command.h | 30 ++---------------------------- 1 file changed, 2 insertions(+), 28 deletions(-) (limited to 'src/smt/command.h') diff --git a/src/smt/command.h b/src/smt/command.h index 85897458d..96a6938d6 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -1221,8 +1221,8 @@ class CVC4_PUBLIC GetUnsatCoreCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; protected: - /** The solver we were invoked with */ - api::Solver* d_solver; + /** The symbol manager we were invoked with */ + SymbolManager* d_sm; /** the result of the unsat core call */ std::vector d_result; }; /* class GetUnsatCoreCommand */ @@ -1376,32 +1376,6 @@ class CVC4_PUBLIC GetOptionCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* 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: - api::Term d_term; - std::string d_name; - - public: - SetExpressionNameCommand(api::Term term, std::string name); - - void invoke(api::Solver* solver, SymbolManager* sm) override; - Command* clone() const override; - std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; -}; /* class SetExpressionNameCommand */ - class CVC4_PUBLIC DatatypeDeclarationCommand : public Command { private: -- cgit v1.2.3