diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-07-04 15:34:40 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-07-04 15:34:40 -0400 |
commit | d4f76fdfaed04bf63bb609a5fd26b0d45a9e94f4 (patch) | |
tree | 6b142d25e93d387371dc402fb0970b5059ae8bac /src/theory/bv | |
parent | 99cae2a7cac2019d432a01c07f94faac370abdda (diff) |
initialize variables
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/bv_subtheory_algebraic.cpp | 6 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_algebraic.h | 4 |
2 files changed, 7 insertions, 3 deletions
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 750e67a2d..9dd86b5ea 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -193,6 +193,10 @@ AlgebraicSolver::AlgebraicSolver(context::Context* c, TheoryBV* bv) , d_isDifficult(c, false) , d_budget(options::bitvectorAlgebraicBudget()) , d_explanations() + , d_inputAssertions() + , d_ids() + , d_numSolved(0) + , d_numCalls(0) , d_ctx(new context::Context()) , d_quickXplain(options::bitvectorQuickXplain() ? new QuickXPlain("alg", d_quickSolver) : NULL) , d_statistics() @@ -641,7 +645,7 @@ bool AlgebraicSolver::useHeuristic() { if (d_numCalls == 0) return true; - double success_rate = d_numSolved/d_numCalls; + double success_rate = double(d_numSolved)/double(d_numCalls); d_statistics.d_useHeuristic.setData(success_rate); return success_rate > 0.8; } diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h index a39631696..fbc8c3ff0 100644 --- a/src/theory/bv/bv_subtheory_algebraic.h +++ b/src/theory/bv/bv_subtheory_algebraic.h @@ -174,8 +174,8 @@ class AlgebraicSolver : public SubtheorySolver { std::vector<Node> d_explanations; /**< explanations for assertions indexed by assertion id */ TNodeSet d_inputAssertions; /**< assertions in current context (for debugging purposes only) */ NodeIdMap d_ids; /**< map from assertions to ids */ - double d_numSolved; - double d_numCalls; + uint64_t d_numSolved; + uint64_t d_numCalls; context::Context* d_ctx; QuickXPlain* d_quickXplain; /**< separate quickXplain module as it can reuse the current SAT solver */ |