diff options
-rw-r--r-- | src/main/portfolio.cpp | 10 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 9 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_algebraic.cpp | 6 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_algebraic.h | 4 |
4 files changed, 26 insertions, 3 deletions
diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp index 757b6cd3c..abe27eb06 100644 --- a/src/main/portfolio.cpp +++ b/src/main/portfolio.cpp @@ -20,6 +20,7 @@ #include <boost/exception_ptr.hpp> #include "smt/smt_engine.h" +#include "util/output.h" #include "util/result.h" #include "util/statistics_registry.h" #include "options/options.h" @@ -92,8 +93,17 @@ std::pair<int, S> runPortfolio(int numThreads, threads[t] = boost::thread(boost::bind(runThread<S>, t, threadFns[t], boost::ref(threads_returnValue[t]) ) ); + #endif /* BOOST_HAS_THREAD_ATTR */ + if(Chat.isOn()) { + void *stackaddr; + size_t stacksize; + pthread_attr_t attr; + pthread_getattr_np(threads[t].native_handle(), &attr); + pthread_attr_getstack(&attr, &stackaddr, &stacksize); + Chat() << "Created worker thread " << t << " with stack size " << stacksize << std::endl; + } } if(not driverFn.empty()) diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index e54c8d174..b6238460b 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -135,6 +135,15 @@ Solver::Solver(CVC4::context::Context* c) : , progress_estimate (0) , remove_satisfied (true) + , ca () + + // even though these are temporaries and technically should be set + // before calling, lets intialize them. this will reduces chances of + // non-determinism in portfolio (parallel) solver if variables are + // being (incorrectly) used without initialization. + , seen(), analyze_stack(), analyze_toclear(), add_tmp() + , max_learnts(0.0), learntsize_adjust_confl(0.0), learntsize_adjust_cnt(0) + // Resource constraints: // , conflict_budget (-1) diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 79aa04fc6..4c784ce6f 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -194,6 +194,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() @@ -642,7 +646,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 4ce02cae1..03588a78f 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 */ |