minisat_solver.h File Reference

Adaptation of MiniSat to DPLL(T). More...

#include "minisat_types.h"
#include "minisat_varorder.h"
#include "minisat_derivation.h"
#include "dpllt.h"
#include <queue>
#include <stack>
#include <vector>
#include <limits>
#include "hash_set.h"

Include dependency graph for minisat_solver.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

• struct MiniSat::SolverStats
• struct MiniSat::PushEntry
• struct MiniSat::SearchParams
• class MiniSat::Solver

Namespaces

• namespace MiniSat

Typedefs

• typedef std::vector< int >
  ::size_type MiniSat::size_type

Functions

• Var MiniSat::cvcToMiniSat (const SAT::Var &var)
• SAT::Var MiniSat::miniSatToCVC (Var var)
• Lit MiniSat::cvcToMiniSat (const SAT::Lit &literal)
• SAT::Lit MiniSat::miniSatToCVC (Lit literal)
• bool MiniSat::cvcToMiniSat (const SAT::Clause &clause, std::vector< Lit > &literals)

---

Detailed Description

Adaptation of MiniSat to DPLL(T).

Author: Alexander Fuchs

Created: Fri Sep 08 11:04:00 2006

---

License to use, copy, modify, sell and/or distribute this software and its documentation for any purpose is hereby granted without royalty, subject to the terms and conditions defined in the LICENSE file provided with this distribution.

---

Definition in file minisat_solver.h.