diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-25 20:45:45 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-25 20:45:45 +0000 |
commit | 70c23e23c3bfc8aa3fdf285fc643b0438359d22a (patch) | |
tree | 3f8f1797e0f8dd3d977f983c1ab823c682f51551 /src/prop/minisat/minisat.h | |
parent | 0d080430206880ffc19050acfa01aae1475f1978 (diff) |
moving minisat implementation into their respective directories (regular and bv)
Diffstat (limited to 'src/prop/minisat/minisat.h')
-rw-r--r-- | src/prop/minisat/minisat.h | 101 |
1 files changed, 101 insertions, 0 deletions
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h new file mode 100644 index 000000000..81a12c491 --- /dev/null +++ b/src/prop/minisat/minisat.h @@ -0,0 +1,101 @@ +/********************* */ +/*! \file minisat.h + ** \verbatim + ** Original author: dejan + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief SAT Solver. + ** + ** Implementation of the minisat for cvc4. + **/ + +#pragma once + +#include "prop/sat_solver.h" +#include "prop/minisat/simp/SimpSolver.h" + +namespace CVC4 { +namespace prop { + +class DPLLMinisatSatSolver : public DPLLSatSolverInterface { + + /** The SatSolver used */ + Minisat::SimpSolver* d_minisat; + + + /** The SatSolver uses this to communicate with the theories */ + TheoryProxy* d_theoryProxy; + + /** Context we will be using to synchronzie the sat solver */ + context::Context* d_context; + + DPLLMinisatSatSolver (); + +public: + + ~DPLLMinisatSatSolver(); + static SatVariable toSatVariable(Minisat::Var var); + static Minisat::Lit toMinisatLit(SatLiteral lit); + static SatLiteral toSatLiteral(Minisat::Lit lit); + static SatLiteralValue toSatLiteralValue(bool res); + static SatLiteralValue toSatLiteralValue(Minisat::lbool res); + + static void toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause); + static void toSatClause (Minisat::vec<Minisat::Lit>& clause, SatClause& sat_clause); + + void initialize(context::Context* context, TheoryProxy* theoryProxy); + + void addClause(SatClause& clause, bool removable); + + SatVariable newVar(bool theoryAtom = false); + + SatLiteralValue solve(); + SatLiteralValue solve(long unsigned int&); + + void interrupt(); + + SatLiteralValue value(SatLiteral l); + + SatLiteralValue modelValue(SatLiteral l); + + bool properExplanation(SatLiteral lit, SatLiteral expl) const; + + /** Incremental interface */ + + int getAssertionLevel() const; + + void push(); + + void pop(); + + void unregisterVar(SatLiteral lit); + + void renewVar(SatLiteral lit, int level = -1); + + class Statistics { + private: + 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(); + void init(Minisat::SimpSolver* d_minisat); + }; + Statistics d_statistics; + + friend class SatSolverFactory; +}; + +} // prop namespace +} // cvc4 namespace + |