d_numVariables(0),
d_okay(true),
d_statistics(registry, name)
+{
+}
+
+void CryptoMinisatSolver::init()
{
d_true = newVar();
d_false = newVar();
std::vector<CMSat::Lit> clause(1);
clause[0] = CMSat::Lit(d_true, false);
d_solver->add_clause(clause);
-
+
clause[0] = CMSat::Lit(d_false, true);
d_solver->add_clause(clause);
}
-
CryptoMinisatSolver::~CryptoMinisatSolver() {}
ClauseId CryptoMinisatSolver::addXorClause(SatClause& clause,
namespace CVC4 {
namespace prop {
-class CryptoMinisatSolver : public SatSolver {
+class CryptoMinisatSolver : public SatSolver
+{
+ friend class SatSolverFactory;
-private:
- std::unique_ptr<CMSat::SATSolver> d_solver;
- proof::ClausalBitVectorProof* d_bvp;
- unsigned d_numVariables;
- bool d_okay;
- SatVariable d_true;
- SatVariable d_false;
-public:
- CryptoMinisatSolver(StatisticsRegistry* registry,
- const std::string& name = "");
+ public:
~CryptoMinisatSolver() override;
ClauseId addClause(SatClause& clause, bool removable) override;
bool nativeXor() override { return true; }
- SatVariable newVar(bool isTheoryAtom = false, bool preRegister = false, bool canErase = true) override;
+ SatVariable newVar(bool isTheoryAtom = false,
+ bool preRegister = false,
+ bool canErase = true) override;
SatVariable trueVar() override;
SatVariable falseVar() override;
void markUnremovable(SatLiteral lit);
void interrupt() override;
-
+
SatValue solve() override;
SatValue solve(long unsigned int&) override;
SatValue solve(const std::vector<SatLiteral>& assumptions) override;
unsigned getAssertionLevel() const override;
void setClausalProofLog(proof::ClausalBitVectorProof* bvp) override;
- class Statistics {
- public:
+ private:
+ class Statistics
+ {
+ public:
StatisticsRegistry* d_registry;
IntStat d_statCallsToSolve;
IntStat d_xorClausesAdded;
IntStat d_clausesAdded;
TimerStat d_solveTime;
bool d_registerStats;
- Statistics(StatisticsRegistry* registry,
- const std::string& prefix);
+ Statistics(StatisticsRegistry* registry, const std::string& prefix);
~Statistics();
};
+ /**
+ * Private to disallow creation outside of SatSolverFactory.
+ * Function init() must be called after creation.
+ */
+ CryptoMinisatSolver(StatisticsRegistry* registry,
+ const std::string& name = "");
+ /**
+ * Initialize SAT solver instance.
+ * Note: Split out to not call virtual functions in constructor.
+ */
+ void init();
+
+ std::unique_ptr<CMSat::SATSolver> d_solver;
+ proof::ClausalBitVectorProof* d_bvp;
+ unsigned d_numVariables;
+ bool d_okay;
+ SatVariable d_true;
+ SatVariable d_false;
+
Statistics d_statistics;
};