CVC3  2.4.1
Classes | Namespaces | Constant Groups | Typedefs | Functions
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"

Go to the source code of this file.

Classes

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

Namespaces

 MiniSat
 

Constant Groups

 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.