summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/smt/command.cpp4
-rw-r--r--src/smt/command.h15
2 files changed, 10 insertions, 9 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index c10b2c4ea..86fb5cdde 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1214,8 +1214,8 @@ std::string GetProofCommand::getCommandName() const throw() {
/* class GetInstantiationsCommand */
-GetInstantiationsCommand::GetInstantiationsCommand() throw() {
-}
+GetInstantiationsCommand::GetInstantiationsCommand() throw()
+ : d_smtEngine(nullptr) {}
void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) {
try {
diff --git a/src/smt/command.h b/src/smt/command.h
index 2091028eb..1db414cde 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -633,19 +633,20 @@ public:
};/* class GetProofCommand */
class CVC4_PUBLIC GetInstantiationsCommand : public Command {
-protected:
- //Instantiations* d_result;
- SmtEngine* d_smtEngine;
-public:
+ public:
GetInstantiationsCommand() throw();
~GetInstantiationsCommand() throw() {}
void invoke(SmtEngine* smtEngine);
- //Instantiations* getResult() const throw();
+ // Instantiations* getResult() const throw();
void printResult(std::ostream& out, uint32_t verbosity = 2) const;
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
-};/* class GetInstantiationsCommand */
+
+ protected:
+ SmtEngine* d_smtEngine;
+}; /* class GetInstantiationsCommand */
class CVC4_PUBLIC GetSynthSolutionCommand : public Command {
public:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback