fixing build warnings

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 1d4f2fd42c13406fd53c881c2ece0754d6c7624c..1afe835fbf4f211bd30699e99ae9d521113a9c0c 100644 (file)
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -70,7 +70,7 @@ void DecisionEngine::addAssertions(const vector<Node> &assertions)
 
 void DecisionEngine::addAssertions
   (const vector<Node> &assertions,
-   int assertionsEnd,
+   unsigned assertionsEnd,
    IteSkolemMap iteSkolemMap) 
 {
   // new assertions, reset whatever result we knew

diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index ea516aa548a4321f9a6708df7beeceb912d3e67c..545ae1770f2af2d63ab360cb2057684f3899d8e3 100644 (file)
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -160,7 +160,7 @@ public:
    * removal. Hence, iteSkolemMap maps into only these.
    */
   void addAssertions(const vector<Node> &assertions,
-                     int assertionsEnd,
+                     unsigned assertionsEnd,
                      IteSkolemMap iteSkolemMap);
 
   /* add a single assertion */

diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index c96b6e4b2c94342db8f827faca38ed74d2a3a1d7..d53507def4a48dda87fd5913a1aed9dc632d9139 100644 (file)
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -102,6 +102,7 @@ Solver::Solver(CVC4::context::Context* c) :
   , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)
 
   , only_bcp(false)
+  , clause_added(false)
   , ok                 (true)
   , cla_inc            (1)
   , var_inc            (1)
@@ -118,7 +119,6 @@ Solver::Solver(CVC4::context::Context* c) :
   , conflict_budget    (-1)
   , propagation_budget (-1)
   , asynch_interrupt   (false)
-  , clause_added(false)
 {
   // Create the constant variables
   varTrue = newVar(true, false);
@@ -415,7 +415,7 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip
         out_btlevel       = level(var(p));
     }
 
-    if (out_learnt.size() > 0 && clause_all_marker && CVC4::Options::current()->bitvector_share_lemmas) {
+    if (out_learnt.size() > 0 && clause_all_marker && CVC4::Options::current()->bitvectorShareLemmas) {
       notify->notify(out_learnt);
     }
 

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 73ad5bd405b75acc91863f164327069df83d1c2f..5d514744fa1bfd3629fda4d2ceebe507f5a830cc 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1102,7 +1102,7 @@ void SmtEnginePrivate::processAssertions() {
 
   // begin: INVARIANT to maintain: no reordering of assertions or
   // introducing new ones
-  int iteRewriteAssertionsEnd = d_assertionsToCheck.size();
+  unsigned iteRewriteAssertionsEnd = d_assertionsToCheck.size();
 
   Trace("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl;
   Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;

diff --git a/src/theory/bv/bv_sat.cpp b/src/theory/bv/bv_sat.cpp
index dcb33c9af340bd0fee293426320745ad9df62777..ed31014590a8fd545c81f081182a99b9a2ef774a 100644 (file)
--- a/src/theory/bv/bv_sat.cpp
+++ b/src/theory/bv/bv_sat.cpp
@@ -100,7 +100,7 @@ void Bitblaster::bbAtom(TNode node) {
   // do boolean simplifications if possible
   Node rewritten = Rewriter::rewrite(atom_definition);
 
-  if (!Options::current()->bitvector_eager_bitblast) {
+  if (!Options::current()->bitvectorEagerBitblast) {
     d_cnfStream->convertAndAssert(rewritten, true, false);
     d_bitblastedAtoms.insert(node);
   } else {
@@ -164,7 +164,7 @@ Node Bitblaster::bbOptimize(TNode node) {
 /// Public methods
 
 void Bitblaster::addAtom(TNode atom) {
-  if (!Options::current()->bitvector_eager_bitblast) {
+  if (!Options::current()->bitvectorEagerBitblast) {
     d_cnfStream->ensureLiteral(atom);
     SatLiteral lit = d_cnfStream->getLiteral(atom);
     d_satSolver->addMarkerLiteral(lit);

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 4076a7ee053a03aa1ec642dbde5287df4281dc51..bbbfdc1ad0d06b18e04ad82162938e9488441d6c 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -41,8 +41,8 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel&
     d_assertions(c),
     d_bitblaster(new Bitblaster(c, this) ),
     d_alreadyPropagatedSet(c),
-    d_statistics(),
     d_sharedTermsSet(c),
+    d_statistics(),
     d_notify(*this),
     d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"),
     d_conflict(c, false),
@@ -109,7 +109,7 @@ TheoryBV::Statistics::~Statistics() {
 void TheoryBV::preRegisterTerm(TNode node) {
   BVDebug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
 
-  if (Options::current()->bitvector_eager_bitblast) {
+  if (Options::current()->bitvectorEagerBitblast) {
     // don't use the equality engine in the eager bit-blasting
     return;
   }
@@ -140,7 +140,7 @@ void TheoryBV::check(Effort e)
 {
   BVDebug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
 
-  if (Options::current()->bitvector_eager_bitblast) {
+  if (Options::current()->bitvectorEagerBitblast) {
     while (!done()) {
       Assertion assertion = get();
       TNode fact = assertion.assertion;
@@ -207,7 +207,7 @@ void TheoryBV::check(Effort e)
     return;
   }
 
-  if (e == EFFORT_FULL || Options::current()->bitvector_eager_fullcheck) {
+  if (e == EFFORT_FULL || Options::current()->bitvectorEagerFullcheck) {
     Assert(done() && !d_conflict);
     BVDebug("bitvector") << "TheoryBV::check " << e << "\n";
     bool ok = d_bitblaster->solve();
@@ -401,7 +401,7 @@ Node TheoryBV::explain(TNode node) {
 void TheoryBV::addSharedTerm(TNode t) {
   Debug("bitvector::sharing") << spaces(getSatContext()->getLevel()) << "TheoryBV::addSharedTerm(" << t << ")" << std::endl;
   d_sharedTermsSet.insert(t); 
-  if (!Options::current()->bitvector_eager_bitblast && d_useEqualityEngine) {
+  if (!Options::current()->bitvectorEagerBitblast && d_useEqualityEngine) {
     d_equalityEngine.addTriggerTerm(t);
   }
 }
@@ -409,7 +409,7 @@ void TheoryBV::addSharedTerm(TNode t) {
 
 EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
 {
-  if (Options::current()->bitvector_eager_bitblast) {
+  if (Options::current()->bitvectorEagerBitblast) {
     return EQUALITY_UNKNOWN;
   }
 

diff --git a/src/util/options.cpp b/src/util/options.cpp
index 46997a04d3bb698aa40bae76fd081e25b88885c5..a9405fb25d238f5a3c7439641b1919050f9b98e0 100644 (file)
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -123,9 +123,9 @@ Options::Options() :
   thread_id(-1),
   separateOutput(false),
   sharingFilterByLength(-1),
-  bitvector_eager_bitblast(false),
-  bitvector_share_lemmas(false),
-  bitvector_eager_fullcheck(false),
+  bitvectorEagerBitblast(false),
+  bitvectorEagerFullcheck(false),
+  bitvectorShareLemmas(false),
   sat_refine_conflicts(false)
 {
 }
@@ -942,17 +942,17 @@ throw(OptionException) {
       }
     case BITVECTOR_EAGER_BITBLAST:
       {
-        bitvector_eager_bitblast = true;
+        bitvectorEagerBitblast = true;
         break;
       }
     case BITVECTOR_EAGER_FULLCHECK:
       {
-        bitvector_eager_fullcheck = true;
+        bitvectorEagerFullcheck = true;
         break;
       }
     case BITVECTOR_SHARE_LEMMAS:
       {
-        bitvector_share_lemmas = true;
+        bitvectorShareLemmas = true;
         break;
       }
     case SAT_REFINE_CONFLICTS:

diff --git a/src/util/options.h b/src/util/options.h
index fd09d4149c9ff7c6000a5e4819a8e1a88e4ddc21..896f77297b9c5c270e124ad95638f00603c0eb93 100644 (file)
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -149,6 +149,11 @@ struct CVC4_PUBLIC Options {
   /** Whether to do the ite-simplification pass */
   bool doITESimp;
 
+  /**
+   * Whether the user explicitly requested ite simplification
+   */
+  bool doITESimpSetByUser;
+
   /** Whether we're in interactive mode or not */
   bool interactive;
 
@@ -252,11 +257,6 @@ struct CVC4_PUBLIC Options {
    */
   bool ufSymmetryBreakerSetByUser;
 
-  /**
-   * Whether the user explicitly requested ite simplification
-   */
-  bool doITESimpSetByUser;
-
   /**
    * Whether to do the linear diophantine equation solver
    * in Arith as described by Griggio JSAT 2012 (on by default).
@@ -297,13 +297,13 @@ struct CVC4_PUBLIC Options {
   int sharingFilterByLength;
 
   /** Bitblast eagerly to the main sat solver */
-  bool bitvector_eager_bitblast;
+  bool bitvectorEagerBitblast;
 
   /** Fullcheck at each check */
-  bool bitvector_eager_fullcheck;
+  bool bitvectorEagerFullcheck;
 
   /** Bitblast eagerly to the main sat solver */
-  bool bitvector_share_lemmas;
+  bool bitvectorShareLemmas;
 
   /** Refine conflicts by doing another full check after a conflict */
   bool sat_refine_conflicts;