1 files changed, 27 insertions, 0 deletions
diff --git a/src/expr/command.h b/src/expr/command.h
index 70e71a111..5786f4e71 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -475,6 +475,21 @@ public:
   Command* clone() const;
 };/* class SimplifyCommand */
 
+class CVC4_PUBLIC ExpandDefinitionsCommand : public Command {
+protected:
+  Expr d_term;
+  Expr d_result;
+public:
+  ExpandDefinitionsCommand(Expr term) throw();
+  ~ExpandDefinitionsCommand() throw() {}
+  Expr getTerm() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
+  Expr getResult() const throw();
+  void printResult(std::ostream& out) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
+};/* class ExpandDefinitionsCommand */
+
 class CVC4_PUBLIC GetValueCommand : public Command {
 protected:
   std::vector<Expr> d_terms;
@@ -531,6 +546,18 @@ public:
   Command* clone() const;
 };/* class GetProofCommand */
 
+class CVC4_PUBLIC GetUnsatCoreCommand : public Command {
+protected:
+  //UnsatCore* d_result;
+public:
+  GetUnsatCoreCommand() throw();
+  ~GetUnsatCoreCommand() throw() {}
+  void invoke(SmtEngine* smtEngine) throw();
+  void printResult(std::ostream& out) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
+};/* class GetUnsatCoreCommand */
+
 class CVC4_PUBLIC GetAssertionsCommand : public Command {
 protected:
   std::string d_result;