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< Variable >	VarSet
typedef std::set< Literal >	LitSet
typedef std::vector< std::pair < unsigned int, std::vector < Variable > > >	stat_type
typedef char	CharT
typedef const CharT *	ParseIterator
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_set &	DP_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 >
Dimacs &	operator>> (std::basic_istream< charT, traits > &is, Dimacs &obj)
Dimacs &	operator>> (std::fstream &is, Dimacs &obj)
template<typename T >
T &	operator<< (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 >
T &	operator<< (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.

typedef const CharT* OKlib::DPv::ParseIterator

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

enum OKlib::DPv::Return_Value

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
	)

Definition at line 105 of file DPv.hpp.

References cls_insert(), OKlib::DPv::Clause_set::cs, LGAES::Literal(), literal_compliment(), resolvable(), resolvent(), and OKlib::DPv::Variable::v.

Referenced by clause_left(), DP_reduction_inplace(), and main().

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().

Literal OKlib::DPv::literal_compliment ( const Literal & l )

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
	)

Definition at line 46 of file Statistics.hpp.

References clause_count(), clause_left(), ldg(), LGAES::Literal(), literal_compliment(), OKlib::DPv::VariableSet::vars, and vdg().

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
	)

Definition at line 92 of file Input_output.hpp.

References OKlib::DPv::Clause::c, cl_insert(), cls_insert(), and OKlib::DPv::Dimacs::formula.

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<<().

Namespaces

Classes

Typedefs

Enumerations

Functions

Detailed Description

Typedef Documentation

Enumeration Type Documentation

Function Documentation