diff options
Diffstat (limited to 'src/prop/cryptominisat.h')
-rw-r--r-- | src/prop/cryptominisat.h | 49 |
1 files changed, 32 insertions, 17 deletions
diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h index d3c5aeb30..25d6cce02 100644 --- a/src/prop/cryptominisat.h +++ b/src/prop/cryptominisat.h @@ -36,18 +36,11 @@ namespace CMSat { 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; @@ -55,7 +48,9 @@ public: 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; @@ -63,7 +58,7 @@ public: void markUnremovable(SatLiteral lit); void interrupt() override; - + SatValue solve() override; SatValue solve(long unsigned int&) override; SatValue solve(const std::vector<SatLiteral>& assumptions) override; @@ -75,19 +70,39 @@ public: 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; }; |