Fix compiler warnings (mostly unused variables).

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index b4ab572835948c6e100308843180f2850a343bb7..37d4c503de596332641f9a7cd9cf26a5726618b8 100644 (file)
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -416,6 +416,8 @@ bool Expr::isAtomicFormula() const {
     case CVC4::kind::IFF:
     case CVC4::kind::IMPLIES:
       return false;
+    default:
+      ; /* fall through */
   }
   for (Expr::iterator k = begin(), kend=end(); k != kend; ++k) {
     if (!CVC3::Expr(*k).isAtomic()) {
@@ -450,8 +452,9 @@ bool Expr::isBoolConnective() const {
   case CVC4::kind::XOR:
   case CVC4::kind::ITE:
     return true;
+  default:
+    return false;
   }
-  return false;
 }
 
 bool Expr::isPropLiteral() const {

diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index ab8a7b2bc2c63508cc85fa4e4bbf9195a0e18964..02bc0784719f0a05f5c138f696a41f06396d32b5 100644 (file)
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -86,7 +86,7 @@ class ProofManager {
   VarSet     d_propVars;
 
   Proof* d_fullProof;
-  ProofFormat d_format;
+  ProofFormat d_format; // used for now only in debug builds
 
 protected:
   std::string d_logic;

diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index c4fe58fd7e921bd321abcf85b394ff3f9058cd03..e4956ecc82067a13059b92cbd7a892f7ba13e68d 100644 (file)
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -29,7 +29,6 @@ using namespace CVC4::prop;
 
 MinisatSatSolver::MinisatSatSolver() :
   d_minisat(NULL),
-  d_theoryProxy(NULL),
   d_context(NULL)
 {}
 

diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 201879eb0508a90254aee924ce65ad5f1cfb95b5..a919bbcc4597f252ac9b23a92fefb215c4c3e466 100644 (file)
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -30,9 +30,6 @@ class MinisatSatSolver : public DPLLSatSolverInterface {
   /** The SatSolver used */
   Minisat::SimpSolver* d_minisat;
 
-  /** The SatSolver uses this to communicate with the theories */
-  TheoryProxy* d_theoryProxy;
-
   /** Context we will be using to synchronize the sat solver */
   context::Context* d_context;
 

diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 92c81616b86f97ad65fb93b69b8bbcd73dbc2f1e..f07f5487e693c1d6bd3c50e52cf71e137422eafa 100644 (file)
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -57,9 +57,6 @@ class TheoryProxy {
   /** The theory engine we are using */
   TheoryEngine* d_theoryEngine;
 
-  /** Context we will be using to synchronzie the sat solver */
-  context::Context* d_context;
-
   /** Queue of asserted facts */
   context::CDQueue<TNode> d_queue;
 
@@ -135,7 +132,6 @@ inline TheoryProxy::TheoryProxy(PropEngine* propEngine,
   d_cnfStream(cnfStream),
   d_decisionEngine(decisionEngine),
   d_theoryEngine(theoryEngine),
-  d_context(context),
   d_queue(context)
 {}
 

diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index 3a767b5c3c02b018046519075811b3a0f82863fe..7669a99149687e29dfdd7421cee9518ad397d2c6 100644 (file)
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -23,7 +23,6 @@ using namespace theory;
 
 SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context)
 : ContextNotifyObj(context)
-, d_context(context)
 , d_statSharedTerms("theory::shared_terms", 0)
 , d_addedSharedTermsSize(context, 0)
 , d_termsToTheories(context)

diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index f5724f4889f35044530572912d0d4c5d7256c631..dba904cdf0332b1c08fef3fced58f9179a10b561 100644 (file)
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -39,9 +39,6 @@ public:
 
 private:
 
-  /** The context */
-  context::Context* d_context;
-
   /** Some statistics */
   IntStat d_statSharedTerms;
 

diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 8572a6abdf767d42738e30978f9c1e1c6461e9b8..48b8fa7e891ee9a228259bbdb649d8540d30ff16 100644 (file)
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -53,9 +53,6 @@ private:
 
   typedef std::hash_map<Node, Node, NodeHashFunction> NodeCache;
 
-  /** The context within which this SubstitutionMap was constructed. */
-  context::Context* d_context;
-
   /** The variables, in order of addition */
   NodeMap d_substitutions;
 
@@ -98,7 +95,6 @@ private:
 public:
 
   SubstitutionMap(context::Context* context, bool substituteUnderQuantifiers = true, bool solvedForm = false) :
-    d_context(context),
     d_substitutions(context),
     d_substitutionCache(),
     d_substituteUnderQuantifiers(substituteUnderQuantifiers),