MiniSat Namespace Reference

Classes

Typedefs

Functions

Variables


Typedef Documentation

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

Definition at line 110 of file minisat_solver.h.

typedef int MiniSat::Var

Definition at line 55 of file minisat_types.h.


Function Documentation

template<class T >
static T MiniSat::min ( x,
y 
) [inline, static]

template<class T >
static T MiniSat::max ( x,
y 
) [inline, static]

template<class T >
static T* MiniSat::xmalloc ( size_t  size  )  [inline, static]

Definition at line 70 of file minisat_global.h.

References DebugAssert.

template<class T >
static T* MiniSat::xrealloc ( T *  ptr,
size_t  size 
) [inline, static]

Definition at line 75 of file minisat_global.h.

References DebugAssert.

Referenced by MiniSat::vec< T >::grow().

template<class T >
static void MiniSat::xfree ( T *  ptr  )  [inline, static]

static double MiniSat::drand ( double &  seed  )  [inline, static]

Definition at line 89 of file minisat_global.h.

Referenced by irand().

static int MiniSat::irand ( double &  seed,
int  size 
) [inline, static]

Definition at line 96 of file minisat_global.h.

References drand().

int MiniSat::toInt ( lbool  l  )  [inline]

lbool MiniSat::toLbool ( int  v  )  [inline]

Definition at line 212 of file minisat_global.h.

Referenced by MiniSat::Solver::getValue(), and MiniSat::VarOrder::select().

template<class T >
static bool MiniSat::operator!= ( const T &  x,
const T &  y 
) [inline, static]

Definition at line 225 of file minisat_global.h.

template<class T >
static bool MiniSat::operator> ( const T &  x,
const T &  y 
) [inline, static]

Definition at line 226 of file minisat_global.h.

template<class T >
static bool MiniSat::operator<= ( const T &  x,
const T &  y 
) [inline, static]

Definition at line 227 of file minisat_global.h.

template<class T >
static bool MiniSat::operator>= ( const T &  x,
const T &  y 
) [inline, static]

Definition at line 228 of file minisat_global.h.

static int MiniSat::left ( int  i  )  [inline, static]

static int MiniSat::right ( int  i  )  [inline, static]

Definition at line 54 of file minisat_heap.h.

Referenced by CVC3::CompleteInstPreProcessor::collect_forall_index(), MiniSat::Derivation::createProof(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArith3::doSolve(), CVC3::TheoryArithOld::findBounds(), CVC3::TheoryArithNew::findBounds(), CVC3::TheoryArith3::findBounds(), CVC3::TheoryArithNew::findCoefficient(), MiniSat::Heap< VarOrder_lt >::heapProperty(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::CompleteInstPreProcessor::isGoodQuant(), CVC3::CompleteInstPreProcessor::isMacro(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArith3::isolateVariable(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer3::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArith3::normalizeProjectIneqs(), MiniSat::Heap< VarOrder_lt >::percolateDown(), CVC3::ArithTheoremProducerOld::plusPredicate(), CVC3::ArithTheoremProducer3::plusPredicate(), CVC3::ArithTheoremProducer::plusPredicate(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), and CVC3::TheoryArithNew::substAndCanonizeTableaux().

static int MiniSat::parent ( int  i  )  [inline, static]

Var MiniSat::cvcToMiniSat ( const SAT::Var var  )  [inline]

conversions between MiniSat and CVC data types:

Definition at line 128 of file minisat_solver.h.

References SAT::Var::getIndex().

Referenced by MiniSat::Solver::addClause(), MiniSat::Solver::cvcToMiniSat(), cvcToMiniSat(), and SAT::DPLLTMiniSat::getValue().

SAT::Var MiniSat::miniSatToCVC ( Var  var  )  [inline]

Lit MiniSat::cvcToMiniSat ( const SAT::Lit literal  )  [inline]

Definition at line 137 of file minisat_solver.h.

References cvcToMiniSat(), SAT::Lit::getVar(), and SAT::Lit::isPositive().

SAT::Lit MiniSat::miniSatToCVC ( Lit  literal  )  [inline]

Definition at line 141 of file minisat_solver.h.

References miniSatToCVC(), MiniSat::Lit::sign(), and MiniSat::Lit::var().

bool MiniSat::cvcToMiniSat ( const SAT::Clause clause,
std::vector< Lit > &  literals 
)

conversions between MiniSat and CVC data types:

Definition at line 121 of file minisat_solver.cpp.

References SAT::Clause::begin(), cvcToMiniSat(), SAT::Clause::end(), SAT::Lit::isFalse(), and SAT::Lit::isTrue().

void* MiniSat::malloc_clause ( const vector< Lit > &  ps  ) 

Definition at line 39 of file minisat_types.cpp.

References clause_mem_base, and max().

Referenced by Clause_new(), and Lemma_new().

Clause * MiniSat::Clause_new ( const vector< Lit > &  ps,
CVC3::Theorem  theorem,
int  id 
)

Clause * MiniSat::Lemma_new ( const vector< Lit > &  ps,
int  id,
int  pushID 
)

Definition at line 49 of file minisat_types.cpp.

References malloc_clause().

Referenced by MiniSat::Solver::analyze(), and MiniSat::Solver::insertLemma().

const Lit MiniSat::lit_Undef ( var_Undef  ,
false   
)

const Lit MiniSat::lit_Error ( var_Undef  ,
true   
)


Variable Documentation

const lbool MiniSat::l_True = toLbool( 1)

const lbool MiniSat::l_False = toLbool(-1)

const lbool MiniSat::l_Undef = toLbool( 0)

Initial value:

    sizeof(unsigned int)
    + 2 * sizeof(int)
    + sizeof(float)
    + sizeof (CVC3::Theorem)

Definition at line 33 of file minisat_types.cpp.

Referenced by malloc_clause().

const int MiniSat::var_Undef = -1


Generated on Thu Oct 15 22:27:12 2009 for CVC3 by  doxygen 1.5.8