summaryrefslogtreecommitdiff
path: root/src/prop
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop')
-rw-r--r--src/prop/bvminisat/bvminisat.cpp103
-rw-r--r--src/prop/bvminisat/bvminisat.h24
-rw-r--r--src/prop/bvminisat/simp/SimpSolver.h2
-rw-r--r--src/prop/minisat/minisat.cpp65
-rw-r--r--src/prop/minisat/minisat.h25
-rw-r--r--src/prop/prop_engine.cpp3
-rw-r--r--src/prop/sat_solver.h5
-rw-r--r--src/prop/sat_solver_factory.cpp9
-rw-r--r--src/prop/sat_solver_factory.h6
-rw-r--r--src/prop/theory_proxy.cpp11
-rw-r--r--src/prop/theory_proxy.h6
11 files changed, 143 insertions, 116 deletions
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index ab157844a..be266b6d8 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -17,21 +17,23 @@
**/
#include "prop/bvminisat/bvminisat.h"
+
#include "prop/bvminisat/simp/SimpSolver.h"
+#include "util/statistics_registry.h"
-using namespace CVC4;
-using namespace prop;
+namespace CVC4 {
+namespace prop {
-BVMinisatSatSolver::BVMinisatSatSolver(context::Context* mainSatContext, const std::string& name)
+BVMinisatSatSolver::BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name)
: context::ContextNotifyObj(mainSatContext, false),
d_minisat(new BVMinisat::SimpSolver(mainSatContext)),
d_minisatNotify(0),
d_assertionsCount(0),
d_assertionsRealCount(mainSatContext, 0),
d_lastPropagation(mainSatContext, 0),
- d_statistics(name)
+ d_statistics(registry, name)
{
- d_statistics.init(d_minisat);
+ d_statistics.init(d_minisat);
}
@@ -208,59 +210,63 @@ void BVMinisatSatSolver::toSatClause(BVMinisat::vec<BVMinisat::Lit>& clause,
// Satistics for BVMinisatSatSolver
-BVMinisatSatSolver::Statistics::Statistics(const std::string& prefix) :
- 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_registerStats(!prefix.empty())
+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_registerStats(!prefix.empty())
{
- if (!d_registerStats)
+ if (!d_registerStats){
return;
+ }
- StatisticsRegistry::registerStat(&d_statStarts);
- StatisticsRegistry::registerStat(&d_statDecisions);
- StatisticsRegistry::registerStat(&d_statRndDecisions);
- StatisticsRegistry::registerStat(&d_statPropagations);
- StatisticsRegistry::registerStat(&d_statConflicts);
- StatisticsRegistry::registerStat(&d_statClausesLiterals);
- StatisticsRegistry::registerStat(&d_statLearntsLiterals);
- StatisticsRegistry::registerStat(&d_statMaxLiterals);
- StatisticsRegistry::registerStat(&d_statTotLiterals);
- StatisticsRegistry::registerStat(&d_statEliminatedVars);
- StatisticsRegistry::registerStat(&d_statCallsToSolve);
- StatisticsRegistry::registerStat(&d_statSolveTime);
+ d_registry->registerStat(&d_statStarts);
+ d_registry->registerStat(&d_statDecisions);
+ d_registry->registerStat(&d_statRndDecisions);
+ d_registry->registerStat(&d_statPropagations);
+ d_registry->registerStat(&d_statConflicts);
+ d_registry->registerStat(&d_statClausesLiterals);
+ d_registry->registerStat(&d_statLearntsLiterals);
+ d_registry->registerStat(&d_statMaxLiterals);
+ d_registry->registerStat(&d_statTotLiterals);
+ d_registry->registerStat(&d_statEliminatedVars);
+ d_registry->registerStat(&d_statCallsToSolve);
+ d_registry->registerStat(&d_statSolveTime);
}
BVMinisatSatSolver::Statistics::~Statistics() {
- if (!d_registerStats)
+ if (!d_registerStats){
return;
- StatisticsRegistry::unregisterStat(&d_statStarts);
- StatisticsRegistry::unregisterStat(&d_statDecisions);
- StatisticsRegistry::unregisterStat(&d_statRndDecisions);
- StatisticsRegistry::unregisterStat(&d_statPropagations);
- StatisticsRegistry::unregisterStat(&d_statConflicts);
- StatisticsRegistry::unregisterStat(&d_statClausesLiterals);
- StatisticsRegistry::unregisterStat(&d_statLearntsLiterals);
- StatisticsRegistry::unregisterStat(&d_statMaxLiterals);
- StatisticsRegistry::unregisterStat(&d_statTotLiterals);
- StatisticsRegistry::unregisterStat(&d_statEliminatedVars);
- StatisticsRegistry::unregisterStat(&d_statCallsToSolve);
- StatisticsRegistry::unregisterStat(&d_statSolveTime);
+ }
+ d_registry->unregisterStat(&d_statStarts);
+ d_registry->unregisterStat(&d_statDecisions);
+ d_registry->unregisterStat(&d_statRndDecisions);
+ d_registry->unregisterStat(&d_statPropagations);
+ d_registry->unregisterStat(&d_statConflicts);
+ d_registry->unregisterStat(&d_statClausesLiterals);
+ d_registry->unregisterStat(&d_statLearntsLiterals);
+ d_registry->unregisterStat(&d_statMaxLiterals);
+ d_registry->unregisterStat(&d_statTotLiterals);
+ d_registry->unregisterStat(&d_statEliminatedVars);
+ d_registry->unregisterStat(&d_statCallsToSolve);
+ d_registry->unregisterStat(&d_statSolveTime);
}
void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){
- if (!d_registerStats)
+ if (!d_registerStats){
return;
-
+ }
+
d_statStarts.setData(minisat->starts);
d_statDecisions.setData(minisat->decisions);
d_statRndDecisions.setData(minisat->rnd_decisions);
@@ -272,3 +278,6 @@ void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){
d_statTotLiterals.setData(minisat->tot_literals);
d_statEliminatedVars.setData(minisat->eliminated_vars);
}
+
+} /* namespace CVC4::prop */
+} /* namespace CVC4 */
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index fc5b29e89..986fbf339 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -20,9 +20,10 @@
#pragma once
-#include "prop/sat_solver.h"
-#include "prop/bvminisat/simp/SimpSolver.h"
#include "context/cdo.h"
+#include "prop/bvminisat/simp/SimpSolver.h"
+#include "prop/sat_solver.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace prop {
@@ -67,13 +68,7 @@ protected:
public:
- BVMinisatSatSolver() :
- ContextNotifyObj(NULL, false),
- d_assertionsRealCount(NULL, (unsigned)0),
- d_lastPropagation(NULL, (unsigned)0),
- d_statistics("")
- { Unreachable(); }
- BVMinisatSatSolver(context::Context* mainSatContext, const std::string& name = "");
+ BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name = "");
~BVMinisatSatSolver() throw(AssertionException);
void setNotify(Notify* notify);
@@ -90,7 +85,7 @@ public:
void markUnremovable(SatLiteral lit);
void interrupt();
-
+
SatValue solve();
SatValue solve(long unsigned int&);
void getUnsatCore(SatClause& unsatCore);
@@ -117,11 +112,16 @@ public:
void explain(SatLiteral lit, std::vector<SatLiteral>& explanation);
SatValue assertAssumption(SatLiteral lit, bool propagate);
-
+
void popAssumption();
+private:
+ /* Disable the default constructor. */
+ BVMinisatSatSolver() CVC4_UNUSED;
+
class Statistics {
public:
+ StatisticsRegistry* d_registry;
ReferenceStat<uint64_t> d_statStarts, d_statDecisions;
ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations;
ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals;
@@ -131,7 +131,7 @@ public:
IntStat d_statCallsToSolve;
BackedStat<double> d_statSolveTime;
bool d_registerStats;
- Statistics(const std::string& prefix);
+ Statistics(StatisticsRegistry* registry, const std::string& prefix);
~Statistics();
void init(BVMinisat::SimpSolver* minisat);
};
diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h
index bef8e0a70..85556e935 100644
--- a/src/prop/bvminisat/simp/SimpSolver.h
+++ b/src/prop/bvminisat/simp/SimpSolver.h
@@ -22,9 +22,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#define BVMinisat_SimpSolver_h
#include "context/context.h"
-#include "expr/statistics_registry.h"
#include "prop/bvminisat/core/Solver.h"
#include "prop/bvminisat/mtl/Queue.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace BVMinisat {
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index d9b8bb4f8..ce5c1eb92 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -23,15 +23,17 @@
#include "options/prop_options.h"
#include "options/smt_options.h"
#include "prop/minisat/simp/SimpSolver.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace prop {
//// DPllMinisatSatSolver
-MinisatSatSolver::MinisatSatSolver() :
+MinisatSatSolver::MinisatSatSolver(StatisticsRegistry* registry) :
d_minisat(NULL),
- d_context(NULL)
+ d_context(NULL),
+ d_statistics(registry)
{}
MinisatSatSolver::~MinisatSatSolver() throw()
@@ -229,38 +231,41 @@ void MinisatSatSolver::pop() {
/// Statistics for MinisatSatSolver
-MinisatSatSolver::Statistics::Statistics() :
- d_statStarts("sat::starts"),
- d_statDecisions("sat::decisions"),
- d_statRndDecisions("sat::rnd_decisions"),
- d_statPropagations("sat::propagations"),
- d_statConflicts("sat::conflicts"),
- d_statClausesLiterals("sat::clauses_literals"),
- d_statLearntsLiterals("sat::learnts_literals"),
- d_statMaxLiterals("sat::max_literals"),
- d_statTotLiterals("sat::tot_literals")
+MinisatSatSolver::Statistics::Statistics(StatisticsRegistry* registry) :
+ d_registry(registry),
+ d_statStarts("sat::starts"),
+ d_statDecisions("sat::decisions"),
+ d_statRndDecisions("sat::rnd_decisions"),
+ d_statPropagations("sat::propagations"),
+ d_statConflicts("sat::conflicts"),
+ d_statClausesLiterals("sat::clauses_literals"),
+ d_statLearntsLiterals("sat::learnts_literals"),
+ d_statMaxLiterals("sat::max_literals"),
+ d_statTotLiterals("sat::tot_literals")
{
- StatisticsRegistry::registerStat(&d_statStarts);
- StatisticsRegistry::registerStat(&d_statDecisions);
- StatisticsRegistry::registerStat(&d_statRndDecisions);
- StatisticsRegistry::registerStat(&d_statPropagations);
- StatisticsRegistry::registerStat(&d_statConflicts);
- StatisticsRegistry::registerStat(&d_statClausesLiterals);
- StatisticsRegistry::registerStat(&d_statLearntsLiterals);
- StatisticsRegistry::registerStat(&d_statMaxLiterals);
- StatisticsRegistry::registerStat(&d_statTotLiterals);
+ d_registry->registerStat(&d_statStarts);
+ d_registry->registerStat(&d_statDecisions);
+ d_registry->registerStat(&d_statRndDecisions);
+ d_registry->registerStat(&d_statPropagations);
+ d_registry->registerStat(&d_statConflicts);
+ d_registry->registerStat(&d_statClausesLiterals);
+ d_registry->registerStat(&d_statLearntsLiterals);
+ d_registry->registerStat(&d_statMaxLiterals);
+ d_registry->registerStat(&d_statTotLiterals);
}
+
MinisatSatSolver::Statistics::~Statistics() {
- StatisticsRegistry::unregisterStat(&d_statStarts);
- StatisticsRegistry::unregisterStat(&d_statDecisions);
- StatisticsRegistry::unregisterStat(&d_statRndDecisions);
- StatisticsRegistry::unregisterStat(&d_statPropagations);
- StatisticsRegistry::unregisterStat(&d_statConflicts);
- StatisticsRegistry::unregisterStat(&d_statClausesLiterals);
- StatisticsRegistry::unregisterStat(&d_statLearntsLiterals);
- StatisticsRegistry::unregisterStat(&d_statMaxLiterals);
- StatisticsRegistry::unregisterStat(&d_statTotLiterals);
+ d_registry->unregisterStat(&d_statStarts);
+ d_registry->unregisterStat(&d_statDecisions);
+ d_registry->unregisterStat(&d_statRndDecisions);
+ d_registry->unregisterStat(&d_statPropagations);
+ d_registry->unregisterStat(&d_statConflicts);
+ d_registry->unregisterStat(&d_statClausesLiterals);
+ d_registry->unregisterStat(&d_statLearntsLiterals);
+ d_registry->unregisterStat(&d_statMaxLiterals);
+ d_registry->unregisterStat(&d_statTotLiterals);
}
+
void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){
d_statStarts.setData(d_minisat->starts);
d_statDecisions.setData(d_minisat->decisions);
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 2564572c2..f279b3a5b 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -20,23 +20,15 @@
#include "prop/sat_solver.h"
#include "prop/minisat/simp/SimpSolver.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace prop {
class MinisatSatSolver : public DPLLSatSolverInterface {
-
- /** The SatSolver used */
- Minisat::SimpSolver* d_minisat;
-
- /** Context we will be using to synchronize the sat solver */
- context::Context* d_context;
-
- void setupOptions();
-
public:
- MinisatSatSolver();
+ MinisatSatSolver(StatisticsRegistry* registry);
~MinisatSatSolver() throw();
;
@@ -83,15 +75,26 @@ public:
bool isDecision(SatVariable decn) const;
+private:
+
+ /** The SatSolver used */
+ Minisat::SimpSolver* d_minisat;
+
+ /** Context we will be using to synchronize the sat solver */
+ context::Context* d_context;
+
+ void setupOptions();
+
class Statistics {
private:
+ StatisticsRegistry* d_registry;
ReferenceStat<uint64_t> d_statStarts, d_statDecisions;
ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations;
ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals;
ReferenceStat<uint64_t> d_statLearntsLiterals, d_statMaxLiterals;
ReferenceStat<uint64_t> d_statTotLiterals;
public:
- Statistics();
+ Statistics(StatisticsRegistry* registry);
~Statistics();
void init(Minisat::SimpSolver* d_minisat);
};/* class MinisatSatSolver::Statistics */
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 96ca7480f..630825103 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -36,6 +36,7 @@
#include "prop/sat_solver.h"
#include "prop/sat_solver_factory.h"
#include "prop/theory_proxy.h"
+#include "smt/smt_statistics_registry.h"
#include "smt_util/command.h"
#include "theory/theory_engine.h"
#include "theory/theory_registrar.h"
@@ -83,7 +84,7 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext
Debug("prop") << "Constructing the PropEngine" << endl;
- d_satSolver = SatSolverFactory::createDPLLMinisat();
+ d_satSolver = SatSolverFactory::createDPLLMinisat(smtStatisticsRegistry());
d_registrar = new theory::TheoryRegistrar(d_theoryEngine);
d_cnfStream = new CVC4::prop::TseitinCnfStream
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 960881844..1c1dae410 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -24,9 +24,10 @@
#include <string>
#include "context/cdlist.h"
+#include "context/context.h"
#include "expr/node.h"
-#include "expr/statistics_registry.h"
#include "prop/sat_solver_types.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace prop {
@@ -101,7 +102,7 @@ public:
virtual void notify(SatClause& clause) = 0;
virtual void spendResource(unsigned ammount) = 0;
virtual void safePoint(unsigned ammount) = 0;
-
+
};/* class BVSatSolverInterface::Notify */
virtual void setNotify(Notify* notify) = 0;
diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index 98b8fce47..c131ca475 100644
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -15,18 +15,19 @@
**/
#include "prop/sat_solver_factory.h"
+
#include "prop/minisat/minisat.h"
#include "prop/bvminisat/bvminisat.h"
namespace CVC4 {
namespace prop {
-BVSatSolverInterface* SatSolverFactory::createMinisat(context::Context* mainSatContext, const std::string& name) {
- return new BVMinisatSatSolver(mainSatContext, name);
+BVSatSolverInterface* SatSolverFactory::createMinisat(context::Context* mainSatContext, StatisticsRegistry* registry, const std::string& name) {
+ return new BVMinisatSatSolver(registry, mainSatContext, name);
}
-DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat() {
- return new MinisatSatSolver();
+DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat(StatisticsRegistry* registry) {
+ return new MinisatSatSolver(registry);
}
} /* CVC4::prop namespace */
diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h
index e0446eb4a..434bf849d 100644
--- a/src/prop/sat_solver_factory.h
+++ b/src/prop/sat_solver_factory.h
@@ -21,7 +21,9 @@
#include <string>
#include <vector>
+#include "context/context.h"
#include "prop/sat_solver.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace prop {
@@ -29,8 +31,8 @@ namespace prop {
class SatSolverFactory {
public:
- static BVSatSolverInterface* createMinisat(context::Context* mainSatContext, const std::string& name = "");
- static DPLLSatSolverInterface* createDPLLMinisat();
+ static BVSatSolverInterface* createMinisat(context::Context* mainSatContext, StatisticsRegistry* registry, const std::string& name = "");
+ static DPLLSatSolverInterface* createDPLLMinisat(StatisticsRegistry* registry);
};/* class SatSolverFactory */
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index d0830b9a5..e87046ad5 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -19,14 +19,15 @@
#include "context/context.h"
#include "decision/decision_engine.h"
#include "expr/expr_stream.h"
-#include "expr/statistics_registry.h"
#include "options/decision_options.h"
#include "prop/cnf_stream.h"
#include "prop/prop_engine.h"
#include "smt_util/lemma_input_channel.h"
#include "smt_util/lemma_output_channel.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/rewriter.h"
#include "theory/theory_engine.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace prop {
@@ -42,11 +43,15 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine,
d_decisionEngine(decisionEngine),
d_theoryEngine(theoryEngine),
d_globals(globals),
- d_queue(context)
-{}
+ d_queue(context),
+ d_replayedDecisions("prop::theoryproxy::replayedDecisions", 0)
+{
+ smtStatisticsRegistry()->registerStat(&d_replayedDecisions);
+}
TheoryProxy::~TheoryProxy() {
/* nothing to do for now */
+ smtStatisticsRegistry()->unregisterStat(&d_replayedDecisions);
}
/** The lemma input channel we are using. */
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 59bc859cb..261db8c87 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -27,12 +27,12 @@
#include "context/cdqueue.h"
#include "expr/node.h"
-#include "expr/statistics_registry.h"
#include "prop/sat_solver.h"
#include "smt/smt_globals.h"
#include "smt_util/lemma_output_channel.h"
#include "smt_util/lemma_input_channel.h"
#include "theory/theory.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
@@ -137,8 +137,8 @@ public:
/**
* Statistic: the number of replayed decisions (via --replay).
*/
- KEEP_STATISTIC(IntStat, d_replayedDecisions,
- "prop::theoryproxy::replayedDecisions", 0);
+ IntStat d_replayedDecisions;
+
};/* class SatSolver */
}/* CVC4::prop namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback