diff options
Diffstat (limited to 'src/smt/command.h')
-rw-r--r-- | src/smt/command.h | 29 |
1 files changed, 25 insertions, 4 deletions
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; |