1 files changed, 15 insertions, 8 deletions
diff --git a/src/expr/command.h b/src/expr/command.h
index 606618d21..4d2957b7c 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -35,6 +35,7 @@
 #include "util/sexpr.h"
 #include "util/datatype.h"
 #include "util/proof.h"
+#include "util/unsat_core.h"
 
 namespace CVC4 {
 
@@ -309,8 +310,9 @@ public:
 class CVC4_PUBLIC AssertCommand : public Command {
 protected:
   Expr d_expr;
+  bool d_inUnsatCore;
 public:
-  AssertCommand(const Expr& e) throw();
+  AssertCommand(const Expr& e, bool inUnsatCore = true) throw();
   ~AssertCommand() throw() {}
   Expr getExpr() const throw();
   void invoke(SmtEngine* smtEngine) throw();
@@ -439,12 +441,12 @@ class CVC4_PUBLIC SetUserAttributeCommand : public Command {
 protected:
   std::string d_attr;
   Expr d_expr;
-  //std::vector<Expr> d_expr_values;
-  //std::string d_str_value;
+  std::vector<Expr> d_expr_values;
+  std::string d_str_value;
 public:
   SetUserAttributeCommand( const std::string& attr, Expr expr ) throw();
-  //SetUserAttributeCommand( const std::string& id, Expr expr, std::vector<Expr>& values ) throw();
-  //SetUserAttributeCommand( const std::string& id, Expr expr, std::string& value ) throw();
+  SetUserAttributeCommand( const std::string& attr, Expr expr, std::vector<Expr>& values ) throw();
+  SetUserAttributeCommand( const std::string& attr, Expr expr, const std::string& value ) throw();
   ~SetUserAttributeCommand() throw() {}
   void invoke(SmtEngine* smtEngine) throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
@@ -457,9 +459,10 @@ class CVC4_PUBLIC CheckSatCommand : public Command {
 protected:
   Expr d_expr;
   Result d_result;
+  bool d_inUnsatCore;
 public:
   CheckSatCommand() throw();
-  CheckSatCommand(const Expr& expr) throw();
+  CheckSatCommand(const Expr& expr, bool inUnsatCore = true) throw();
   ~CheckSatCommand() throw() {}
   Expr getExpr() const throw();
   void invoke(SmtEngine* smtEngine) throw();
@@ -474,8 +477,9 @@ class CVC4_PUBLIC QueryCommand : public Command {
 protected:
   Expr d_expr;
   Result d_result;
+  bool d_inUnsatCore;
 public:
-  QueryCommand(const Expr& e) throw();
+  QueryCommand(const Expr& e, bool inUnsatCore = true) throw();
   ~QueryCommand() throw() {}
   Expr getExpr() const throw();
   void invoke(SmtEngine* smtEngine) throw();
@@ -597,12 +601,15 @@ public:
 
 class CVC4_PUBLIC GetUnsatCoreCommand : public Command {
 protected:
-  //UnsatCore* d_result;
+  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) throw();
   void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+  const UnsatCore& getUnsatCore() const throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
   Command* clone() const;
   std::string getCommandName() const throw();