delete d_minisatNotify;
}
+void BVMinisatSatSolver::MinisatNotify::notify(
+ BVMinisat::vec<BVMinisat::Lit>& clause)
+{
+ SatClause satClause;
+ for (unsigned i = 0, n = clause.size(); i < n; ++i)
+ {
+ satClause.push_back(toSatLiteral(clause[i]));
+ }
+ d_notify->notify(satClause);
+}
+
void BVMinisatSatSolver::setNotify(Notify* notify) {
d_minisatNotify = new MinisatNotify(notify);
d_minisat->setNotify(d_minisatNotify);
d_minisat->interrupt();
}
-SatValue BVMinisatSatSolver::solve(){
+SatValue BVMinisatSatSolver::solve()
+{
+ TimerStat::CodeTimer solveTimer(d_statistics.d_statSolveTime);
++d_statistics.d_statCallsToSolve;
return toSatLiteralValue(d_minisat->solve());
}
SatValue BVMinisatSatSolver::solve(long unsigned int& resource){
Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
+ TimerStat::CodeTimer solveTimer(d_statistics.d_statSolveTime);
++d_statistics.d_statCallsToSolve;
if(resource == 0) {
d_minisat->budgetOff();
// Satistics for BVMinisatSatSolver
-BVMinisatSatSolver::Statistics::Statistics(StatisticsRegistry* registry, const std::string& prefix)
+BVMinisatSatSolver::Statistics::Statistics(StatisticsRegistry* registry,
+ const std::string& prefix)
: d_registry(registry),
- d_statStarts("theory::bv::"+prefix+"bvminisat::starts"),
- d_statDecisions("theory::bv::"+prefix+"bvminisat::decisions"),
- d_statRndDecisions("theory::bv::"+prefix+"bvminisat::rnd_decisions"),
- d_statPropagations("theory::bv::"+prefix+"bvminisat::propagations"),
- d_statConflicts("theory::bv::"+prefix+"bvminisat::conflicts"),
- d_statClausesLiterals("theory::bv::"+prefix+"bvminisat::clauses_literals"),
- d_statLearntsLiterals("theory::bv::"+prefix+"bvminisat::learnts_literals"),
- d_statMaxLiterals("theory::bv::"+prefix+"bvminisat::max_literals"),
- d_statTotLiterals("theory::bv::"+prefix+"bvminisat::tot_literals"),
- d_statEliminatedVars("theory::bv::"+prefix+"bvminisat::eliminated_vars"),
- d_statCallsToSolve("theory::bv::"+prefix+"bvminisat::calls_to_solve", 0),
- d_statSolveTime("theory::bv::"+prefix+"bvminisat::solve_time", 0),
+ d_statStarts("theory::bv::" + prefix + "bvminisat::starts"),
+ d_statDecisions("theory::bv::" + prefix + "bvminisat::decisions"),
+ d_statRndDecisions("theory::bv::" + prefix + "bvminisat::rnd_decisions"),
+ d_statPropagations("theory::bv::" + prefix + "bvminisat::propagations"),
+ d_statConflicts("theory::bv::" + prefix + "bvminisat::conflicts"),
+ d_statClausesLiterals("theory::bv::" + prefix
+ + "bvminisat::clauses_literals"),
+ d_statLearntsLiterals("theory::bv::" + prefix
+ + "bvminisat::learnts_literals"),
+ d_statMaxLiterals("theory::bv::" + prefix + "bvminisat::max_literals"),
+ d_statTotLiterals("theory::bv::" + prefix + "bvminisat::tot_literals"),
+ d_statEliminatedVars("theory::bv::" + prefix
+ + "bvminisat::eliminated_vars"),
+ d_statCallsToSolve("theory::bv::" + prefix
+ + "bvminisat::calls_to_solve", 0),
+ d_statSolveTime("theory::bv::" + prefix + "bvminisat::solve_time"),
d_registerStats(!prefix.empty())
{
- if (!d_registerStats){
+ if (!d_registerStats)
+ {
return;
}
namespace CVC4 {
namespace prop {
-class BVMinisatSatSolver : public BVSatSolverInterface, public context::ContextNotifyObj {
-
-private:
-
- class MinisatNotify : public BVMinisat::Notify {
+class BVMinisatSatSolver : public BVSatSolverInterface,
+ public context::ContextNotifyObj
+{
+ private:
+ class MinisatNotify : public BVMinisat::Notify
+ {
BVSatSolverInterface::Notify* d_notify;
- public:
- MinisatNotify(BVSatSolverInterface::Notify* notify)
- : d_notify(notify)
- {}
- bool notify(BVMinisat::Lit lit) {
- return d_notify->notify(toSatLiteral(lit));
- }
- void notify(BVMinisat::vec<BVMinisat::Lit>& clause) {
- SatClause satClause;
- for (int i = 0; i < clause.size(); ++i) {
- satClause.push_back(toSatLiteral(clause[i]));
- }
- d_notify->notify(satClause);
- }
- void spendResource(unsigned ammount) {
- d_notify->spendResource(ammount);
- }
- void safePoint(unsigned ammount) {
- d_notify->safePoint(ammount);
+ public:
+ MinisatNotify(BVSatSolverInterface::Notify* notify) : d_notify(notify) {}
+ bool notify(BVMinisat::Lit lit)
+ {
+ return d_notify->notify(toSatLiteral(lit));
}
+ void notify(BVMinisat::vec<BVMinisat::Lit>& clause);
+ void spendResource(unsigned amount) { d_notify->spendResource(amount); }
+ void safePoint(unsigned amount) { d_notify->safePoint(amount); }
};
BVMinisat::SimpSolver* d_minisat;
ReferenceStat<uint64_t> d_statTotLiterals;
ReferenceStat<int> d_statEliminatedVars;
IntStat d_statCallsToSolve;
- BackedStat<double> d_statSolveTime;
+ TimerStat d_statSolveTime;
bool d_registerStats;
Statistics(StatisticsRegistry* registry, const std::string& prefix);
~Statistics();