OKlibrary  0.2.1.6
OKlib::DPv Namespace Reference

Deprecated namespace containing components for Davis-Putnam resolution. More...

Namespaces

namespace  Error
namespace  Input
namespace  Output
namespace  Testobjects

Classes

struct  Literal
struct  Variable
struct  Clause
struct  Clause_set
struct  LiteralSet
struct  VariableSet
struct  Stat_comp
struct  Dimacs
class  ParserLiteral
class  DimacsParser
class  Test_ParserLiteral
class  Test_DimacsParser_ClauseSet

Typedefs

typedef int int_type
typedef std::set< VariableVarSet
typedef std::set< LiteralLitSet
typedef std::vector< std::pair
< unsigned int, std::vector
< Variable > > > 
stat_type
typedef char CharT
typedef const CharTParseIterator
typedef boost::spirit::rule Rule

Enumerations

enum  Return_Value { SAT, USAT, Unknown }

Functions

bool operator!= (const Literal lhs, const Literal rhs)
bool operator> (const Literal lhs, const Literal rhs)
bool operator<= (const Literal lhs, const Literal rhs)
bool operator>= (const Literal lhs, const Literal rhs)
bool operator!= (const Variable lhs, const Variable rhs)
bool operator> (const Variable lhs, const Variable rhs)
bool operator<= (const Variable lhs, const Variable rhs)
bool operator>= (const Variable lhs, const Variable rhs)
bool operator!= (const Clause lhs, const Clause rhs)
bool operator> (const Clause lhs, const Clause rhs)
bool operator<= (const Clause lhs, const Clause rhs)
bool operator>= (const Clause lhs, const Clause rhs)
void cl_insert (const Literal &l, Clause &cl)
void cls_insert (const Clause &cl, Clause_set &cls)
Literal literal_compliment (const Literal &l)
Clause clause_compliment (const Clause &cl)
bool resolvable (const Clause &lhs, const Clause &rhs)
bool resolvable (const Variable &v, const Clause &lhs, const Clause &rhs)
Clause resolvent (const Clause &lhs, const Clause &rhs)
Clause_set DP_reduction (const Variable &v, const Clause_set &cls)
Clause_setDP_reduction_inplace (const Variable &v, Clause_set &cls)
bool final_form (const Clause_set &cls)
Return_Value is_sat (const Clause_set &cls)
template<typename VariableSet , typename ClauseSet , typename Stats >
Stats & DPv_opt_stats (VariableSet &vs, ClauseSet &cls, Stats &values)
template<typename T >
void Best_order (const T &stat)
template<typename charT , typename traits >
Dimacsoperator>> (std::basic_istream< charT, traits > &is, Dimacs &obj)
Dimacsoperator>> (std::fstream &is, Dimacs &obj)
template<typename T >
Toperator<< (T &os, Dimacs &obj)
unsigned int clause_count (const Clause_set &cls)
unsigned int ldg (const Literal l, const Clause_set &cls)
unsigned int vdg (const Variable v, const Clause_set &cls)
unsigned int clause_left (const Variable &v, const Clause_set &cls)
template<typename T >
Toperator<< (T &os, const Clause_set &cls)

Detailed Description

Deprecated namespace containing components for Davis-Putnam resolution.

Deprecated:

Typedef Documentation

typedef char OKlib::DPv::CharT

Definition at line 127 of file Input_output.hpp.

typedef int OKlib::DPv::int_type

Definition at line 24 of file BasicDataStructure.hpp.

typedef std::set<Literal> OKlib::DPv::LitSet

Definition at line 160 of file BasicDataStructure.hpp.

Definition at line 128 of file Input_output.hpp.

typedef boost::spirit::rule OKlib::DPv::Rule

Definition at line 129 of file Input_output.hpp.

typedef std::vector<std::pair<unsigned int, std::vector<Variable> > > OKlib::DPv::stat_type

Definition at line 155 of file DPv.hpp.

typedef std::set<Variable> OKlib::DPv::VarSet

Definition at line 159 of file BasicDataStructure.hpp.


Enumeration Type Documentation

Enumerator:
SAT 
USAT 
Unknown 

Definition at line 138 of file DPv.hpp.


Function Documentation

template<typename T >
void OKlib::DPv::Best_order ( const T stat)

Definition at line 192 of file DPv.hpp.

Referenced by main().

void OKlib::DPv::cl_insert ( const Literal l,
Clause &  cl 
)

Definition at line 130 of file BasicDataStructure.hpp.

References OKlib::DPv::Clause::c.

Referenced by clause_compliment(), and operator>>().

Clause OKlib::DPv::clause_compliment ( const Clause &  cl)

Definition at line 53 of file DPv.hpp.

References OKlib::DPv::Clause::c, cl_insert(), and literal_compliment().

Referenced by resolvable(), and resolvent().

unsigned int OKlib::DPv::clause_count ( const Clause_set &  cls)

Definition at line 24 of file Statistics.hpp.

References OKlib::DPv::Clause_set::cs.

Referenced by clause_left(), DPv_opt_stats(), and operator<<().

unsigned int OKlib::DPv::clause_left ( const Variable &  v,
const Clause_set &  cls 
)

Definition at line 41 of file Statistics.hpp.

References clause_count(), and DP_reduction().

Referenced by operator<<().

void OKlib::DPv::cls_insert ( const Clause &  cl,
Clause_set &  cls 
)

Definition at line 155 of file BasicDataStructure.hpp.

References OKlib::DPv::Clause_set::cs.

Referenced by DP_reduction(), and operator>>().

Clause_set OKlib::DPv::DP_reduction ( const Variable &  v,
const Clause_set &  cls 
)
Clause_set& OKlib::DPv::DP_reduction_inplace ( const Variable &  v,
Clause_set &  cls 
)

Definition at line 128 of file DPv.hpp.

References OKlib::DPv::Clause_set::cs, and DP_reduction().

Referenced by DPv_opt_stats().

template<typename VariableSet , typename ClauseSet , typename Stats >
Stats& OKlib::DPv::DPv_opt_stats ( VariableSet &  vs,
ClauseSet &  cls,
Stats &  values 
)

Definition at line 159 of file DPv.hpp.

References clause_count(), DP_reduction_inplace(), and OKlib::DPv::VariableSet::vars.

Referenced by main().

bool OKlib::DPv::final_form ( const Clause_set &  cls)

Definition at line 133 of file DPv.hpp.

Referenced by is_sat().

Return_Value OKlib::DPv::is_sat ( const Clause_set &  cls)

Definition at line 140 of file DPv.hpp.

References OKlib::DPv::Clause_set::cs, final_form(), SAT, Unknown, and USAT.

unsigned int OKlib::DPv::ldg ( const Literal  l,
const Clause_set &  cls 
)

Definition at line 28 of file Statistics.hpp.

References OKlib::DPv::Clause_set::cs.

Referenced by operator<<(), and vdg().

Definition at line 47 of file DPv.hpp.

References OKlib::DPv::Literal::l.

Referenced by clause_compliment(), DP_reduction(), operator<<(), and resolvent().

bool OKlib::DPv::operator!= ( const Literal  lhs,
const Literal  rhs 
) [inline]

Definition at line 40 of file BasicDataStructure.hpp.

References OKlib::DPv::Literal::l.

bool OKlib::DPv::operator!= ( const Variable  lhs,
const Variable  rhs 
) [inline]

Definition at line 73 of file BasicDataStructure.hpp.

References OKlib::DPv::Variable::v.

bool OKlib::DPv::operator!= ( const Clause  lhs,
const Clause  rhs 
) [inline]

Definition at line 114 of file BasicDataStructure.hpp.

References OKlib::DPv::Clause::c.

template<typename T >
T& OKlib::DPv::operator<< ( T os,
const Clause_set &  cls 
)
template<typename T >
T& OKlib::DPv::operator<< ( T os,
Dimacs &  obj 
)

Definition at line 211 of file Input_output.hpp.

References OKlib::DPv::Dimacs::formula.

bool OKlib::DPv::operator<= ( const Literal  lhs,
const Literal  rhs 
) [inline]

Definition at line 48 of file BasicDataStructure.hpp.

References OKlib::DPv::Literal::l.

bool OKlib::DPv::operator<= ( const Variable  lhs,
const Variable  rhs 
) [inline]

Definition at line 81 of file BasicDataStructure.hpp.

References OKlib::DPv::Variable::v.

bool OKlib::DPv::operator<= ( const Clause  lhs,
const Clause  rhs 
) [inline]

Definition at line 122 of file BasicDataStructure.hpp.

References OKlib::DPv::Clause::c.

bool OKlib::DPv::operator> ( const Literal  lhs,
const Literal  rhs 
) [inline]

Definition at line 44 of file BasicDataStructure.hpp.

References OKlib::DPv::Literal::l.

bool OKlib::DPv::operator> ( const Variable  lhs,
const Variable  rhs 
) [inline]

Definition at line 77 of file BasicDataStructure.hpp.

References OKlib::DPv::Variable::v.

bool OKlib::DPv::operator> ( const Clause  lhs,
const Clause  rhs 
) [inline]

Definition at line 118 of file BasicDataStructure.hpp.

References OKlib::DPv::Clause::c.

bool OKlib::DPv::operator>= ( const Literal  lhs,
const Literal  rhs 
) [inline]

Definition at line 52 of file BasicDataStructure.hpp.

References OKlib::DPv::Literal::l.

bool OKlib::DPv::operator>= ( const Variable  lhs,
const Variable  rhs 
) [inline]

Definition at line 85 of file BasicDataStructure.hpp.

References OKlib::DPv::Variable::v.

bool OKlib::DPv::operator>= ( const Clause  lhs,
const Clause  rhs 
) [inline]

Definition at line 126 of file BasicDataStructure.hpp.

References OKlib::DPv::Clause::c.

template<typename charT , typename traits >
Dimacs& OKlib::DPv::operator>> ( std::basic_istream< charT, traits > &  is,
Dimacs &  obj 
)

Definition at line 88 of file Input_output.hpp.

Dimacs& OKlib::DPv::operator>> ( std::fstream &  is,
Dimacs &  obj 
)
bool OKlib::DPv::resolvable ( const Clause &  lhs,
const Clause &  rhs 
)

Definition at line 61 of file DPv.hpp.

References OKlib::DPv::Clause::c, and clause_compliment().

Referenced by DP_reduction(), and resolvent().

bool OKlib::DPv::resolvable ( const Variable &  v,
const Clause &  lhs,
const Clause &  rhs 
)

Definition at line 71 of file DPv.hpp.

References OKlib::DPv::Clause::c, and clause_compliment().

Clause OKlib::DPv::resolvent ( const Clause &  lhs,
const Clause &  rhs 
)

Definition at line 83 of file DPv.hpp.

References OKlib::DPv::Clause::c, clause_compliment(), literal_compliment(), and resolvable().

Referenced by DP_reduction().

unsigned int OKlib::DPv::vdg ( const Variable  v,
const Clause_set &  cls 
)

Definition at line 37 of file Statistics.hpp.

References ldg(), LGAES::Literal(), and OKlib::DPv::Variable::v.

Referenced by operator<<().