From: Dejan Jovanović Date: Sun, 13 May 2012 15:51:27 +0000 (+0000) Subject: fixing build warnings X-Git-Tag: cvc5-1.0.0~8184 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=39c17191ad88a50bfffdbbc5ed8b493ad99b3fb5;p=cvc5.git fixing build warnings --- diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index 1d4f2fd42..1afe835fb 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -70,7 +70,7 @@ void DecisionEngine::addAssertions(const vector &assertions) void DecisionEngine::addAssertions (const vector &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 ea516aa54..545ae1770 100644 --- 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 &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 c96b6e4b2..d53507def 100644 --- 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& 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 73ad5bd40..5d514744f 100644 --- 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 dcb33c9af..ed3101459 100644 --- 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 4076a7ee0..bbbfdc1ad 100644 --- 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 46997a04d..a9405fb25 100644 --- 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 fd09d4149..896f77297 100644 --- 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;