From 5b655946e1c73f511719d0264f92715b063e867f Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Tue, 21 Aug 2018 15:25:00 -0700
Subject: Removing unused bool members in command.cpp. Also initializes a bool
 member. (#2321)

---
 src/smt/command.cpp | 33 ++++++++++++++-------------------
 1 file changed, 14 insertions(+), 19 deletions(-)

(limited to 'src/smt/command.cpp')

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 2805d8793..3d838d21c 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -387,10 +387,8 @@ std::string PopCommand::getCommandName() const { return "pop"; }
 /* -------------------------------------------------------------------------- */
 
 CheckSatCommand::CheckSatCommand() : d_expr() {}
-CheckSatCommand::CheckSatCommand(const Expr& expr, bool inUnsatCore)
-    : d_expr(expr), d_inUnsatCore(inUnsatCore)
-{
-}
+
+CheckSatCommand::CheckSatCommand(const Expr& expr) : d_expr(expr) {}
 
 Expr CheckSatCommand::getExpr() const { return d_expr; }
 void CheckSatCommand::invoke(SmtEngine* smtEngine)
@@ -422,15 +420,15 @@ void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const
 Command* CheckSatCommand::exportTo(ExprManager* exprManager,
                                    ExprManagerMapCollection& variableMap)
 {
-  CheckSatCommand* c = new CheckSatCommand(
-      d_expr.exportTo(exprManager, variableMap), d_inUnsatCore);
+  CheckSatCommand* c =
+      new CheckSatCommand(d_expr.exportTo(exprManager, variableMap));
   c->d_result = d_result;
   return c;
 }
 
 Command* CheckSatCommand::clone() const
 {
-  CheckSatCommand* c = new CheckSatCommand(d_expr, d_inUnsatCore);
+  CheckSatCommand* c = new CheckSatCommand(d_expr);
   c->d_result = d_result;
   return c;
 }
@@ -441,14 +439,10 @@ std::string CheckSatCommand::getCommandName() const { return "check-sat"; }
 /* class CheckSatAssumingCommand                                              */
 /* -------------------------------------------------------------------------- */
 
-CheckSatAssumingCommand::CheckSatAssumingCommand(Expr term) : d_terms()
-{
-  d_terms.push_back(term);
-}
+CheckSatAssumingCommand::CheckSatAssumingCommand(Expr term) : d_terms({term}) {}
 
-CheckSatAssumingCommand::CheckSatAssumingCommand(const std::vector<Expr>& terms,
-                                                 bool inUnsatCore)
-    : d_terms(terms), d_inUnsatCore(inUnsatCore)
+CheckSatAssumingCommand::CheckSatAssumingCommand(const std::vector<Expr>& terms)
+    : d_terms(terms)
 {
 }
 
@@ -496,16 +490,14 @@ Command* CheckSatAssumingCommand::exportTo(
   {
     exportedTerms.push_back(e.exportTo(exprManager, variableMap));
   }
-  CheckSatAssumingCommand* c =
-      new CheckSatAssumingCommand(exportedTerms, d_inUnsatCore);
+  CheckSatAssumingCommand* c = new CheckSatAssumingCommand(exportedTerms);
   c->d_result = d_result;
   return c;
 }
 
 Command* CheckSatAssumingCommand::clone() const
 {
-  CheckSatAssumingCommand* c =
-      new CheckSatAssumingCommand(d_terms, d_inUnsatCore);
+  CheckSatAssumingCommand* c = new CheckSatAssumingCommand(d_terms);
   c->d_result = d_result;
   return c;
 }
@@ -1779,7 +1771,10 @@ std::string GetSynthSolutionCommand::getCommandName() const
 /* class GetQuantifierEliminationCommand                                      */
 /* -------------------------------------------------------------------------- */
 
-GetQuantifierEliminationCommand::GetQuantifierEliminationCommand() : d_expr() {}
+GetQuantifierEliminationCommand::GetQuantifierEliminationCommand()
+    : d_expr(), d_doFull(true)
+{
+}
 GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(
     const Expr& expr, bool doFull)
     : d_expr(expr), d_doFull(doFull)
-- 
cgit v1.2.3