OKlibrary  0.2.1.6
OKlib::Satisfiability::FiniteFunctions::QuineMcCluskey< n, ClauseContainer > Class Template Reference

Functor, computing all prime implicates of a full clause-set. More...

#include <QuineMcCluskey.hpp>

List of all members.

Public Types

typedef boost::range_value
< typename boost::range_value
< ClauseContainer >::type >
::type 
literal_type
 boolean literals as integers
typedef literal_type variable_type
 boolean variables as integers
typedef boost::range_value
< ClauseContainer >::type 
clause_type
 clauses as given by the clause-container
typedef ClauseContainer clause_set_type
 clause-sets as given by the template parameter
typedef
boost::range_const_iterator
< const clause_type >::type 
const_clause_iterator_type
 iterator for clauses
typedef
boost::range_const_iterator
< const clause_set_type >
::type 
const_clause_set_iterator_type
 iterator for clause-sets
typedef std::vector< bool > HashTable
 hash-table to represent an arbitrary clause-set over n variables
typedef HashTable::size_type hash_index_type
 hash-values used as indices for hash-tables

Public Member Functions

 BOOST_STATIC_ASSERT (num_vars >=1)
const hash_index_typefill_pow3 ()
 QuineMcCluskey ()
 ~QuineMcCluskey ()
hash_index_type hash_clause (const clause_type &clause)
 Computes the hash-value of a clause.
hash_index_type flip_literal (const hash_index_type hash, const literal_type literal)
 From a hash-value for a clause compute the new hash-value where a.
hash_index_type remove_literal (const hash_index_type hash, const literal_type literal)
 From a hash-value for a clause compute the new hash-value where.
unsigned int hash2clause (hash_index_type hash, int clause[])
 Computes the clause represented by a hash-value.
clause_set_type operator() (const clause_set_type &input_cs)
 Compute all prime clauses of a clause-set.

Public Attributes

const hash_index_type *const pow3
 pow3[i] = 3^i for 0 <= i <= num_vars

Static Public Attributes

static const int num_vars = n
 the number of variables

Detailed Description

template<int n = 4, class ClauseContainer = std::vector<std::vector<int> >>
class OKlib::Satisfiability::FiniteFunctions::QuineMcCluskey< n, ClauseContainer >

Functor, computing all prime implicates of a full clause-set.

The Maxima input/output specification is min_2resolution_closure_cs in ComputerAlgebra/Satisfiability/Lisp/Primality/PrimeImplicatesImplicants.mac.

For ease of use the helper-function FiniteFunctions::quine_mccluskey is provided below.

Definition at line 50 of file QuineMcCluskey.hpp.


Member Typedef Documentation

template<int n = 4, class ClauseContainer = std::vector<std::vector<int> >>
typedef ClauseContainer OKlib::Satisfiability::FiniteFunctions::QuineMcCluskey< n, ClauseContainer >::clause_set_type

clause-sets as given by the template parameter

Definition at line 63 of file QuineMcCluskey.hpp.

template<int n = 4, class ClauseContainer = std::vector<std::vector<int> >>
typedef boost::range_value<ClauseContainer>::type OKlib::Satisfiability::FiniteFunctions::QuineMcCluskey< n, ClauseContainer >::clause_type

clauses as given by the clause-container

Definition at line 61 of file QuineMcCluskey.hpp.

template<int n = 4, class ClauseContainer = std::vector<std::vector<int> >>
typedef boost::range_const_iterator<const clause_type>::type OKlib::Satisfiability::FiniteFunctions::QuineMcCluskey< n, ClauseContainer >::const_clause_iterator_type

iterator for clauses

Definition at line 65 of file QuineMcCluskey.hpp.

template<int n = 4, class ClauseContainer = std::vector<std::vector<int> >>
typedef boost::range_const_iterator<const clause_set_type>::type OKlib::Satisfiability::FiniteFunctions::QuineMcCluskey< n, ClauseContainer >::const_clause_set_iterator_type

iterator for clause-sets

Definition at line 67 of file QuineMcCluskey.hpp.

template<int n = 4, class ClauseContainer = std::vector<std::vector<int> >>
typedef HashTable::size_type OKlib::Satisfiability::FiniteFunctions::QuineMcCluskey< n, ClauseContainer >::hash_index_type

hash-values used as indices for hash-tables

Definition at line 72 of file QuineMcCluskey.hpp.

template<int n = 4, class ClauseContainer = std::vector<std::vector<int> >>
typedef std::vector<bool> OKlib::Satisfiability::FiniteFunctions::QuineMcCluskey< n, ClauseContainer >::HashTable

hash-table to represent an arbitrary clause-set over n variables

Definition at line 70 of file QuineMcCluskey.hpp.

template<int n = 4, class ClauseContainer = std::vector<std::vector<int> >>
typedef boost::range_value<typename boost::range_value<ClauseContainer>::type >::type OKlib::Satisfiability::FiniteFunctions::QuineMcCluskey< n, ClauseContainer >::literal_type

boolean literals as integers

Definition at line 57 of file QuineMcCluskey.hpp.

template<int n = 4, class ClauseContainer = std::vector<std::vector<int> >>
typedef literal_type OKlib::Satisfiability::FiniteFunctions::QuineMcCluskey< n, ClauseContainer >::variable_type

boolean variables as integers

Definition at line 59 of file QuineMcCluskey.hpp.


Constructor & Destructor Documentation

template<int n = 4, class ClauseContainer = std::vector<std::vector<int> >>
OKlib::Satisfiability::FiniteFunctions::QuineMcCluskey< n, ClauseContainer >::QuineMcCluskey ( ) [inline]

Definition at line 88 of file QuineMcCluskey.hpp.

template<int n = 4, class ClauseContainer = std::vector<std::vector<int> >>
OKlib::Satisfiability::FiniteFunctions::QuineMcCluskey< n, ClauseContainer >::~QuineMcCluskey ( ) [inline]

Member Function Documentation

template<int n = 4, class ClauseContainer = std::vector<std::vector<int> >>
OKlib::Satisfiability::FiniteFunctions::QuineMcCluskey< n, ClauseContainer >::BOOST_STATIC_ASSERT ( num_vars >=  1)
template<int n = 4, class ClauseContainer = std::vector<std::vector<int> >>
hash_index_type OKlib::Satisfiability::FiniteFunctions::QuineMcCluskey< n, ClauseContainer >::flip_literal ( const hash_index_type  hash,
const literal_type  literal 
) [inline]
template<int n = 4, class ClauseContainer = std::vector<std::vector<int> >>
unsigned int OKlib::Satisfiability::FiniteFunctions::QuineMcCluskey< n, ClauseContainer >::hash2clause ( hash_index_type  hash,
int  clause[] 
) [inline]

Computes the clause represented by a hash-value.

The return-value is the number of literals in the clause, while the reference-parameter "clause" contains the clause itself.

Here a clause is an array of integers, where the length k of the clause must be known (so that only clause[0], ..., clause[k-1] are to be used).

Definition at line 134 of file QuineMcCluskey.hpp.

References OKlib::Satisfiability::FiniteFunctions::QuineMcCluskey< n, ClauseContainer >::num_vars, and OKlib::Satisfiability::FiniteFunctions::QuineMcCluskey< n, ClauseContainer >::pow3.

Referenced by OKlib::Satisfiability::FiniteFunctions::QuineMcCluskey< n, ClauseContainer >::operator()().

template<int n = 4, class ClauseContainer = std::vector<std::vector<int> >>
hash_index_type OKlib::Satisfiability::FiniteFunctions::QuineMcCluskey< n, ClauseContainer >::hash_clause ( const clause_type clause) [inline]

Computes the hash-value of a clause.

The clause-hash is the sum of c * 3^(i-1) over all variables i in the clause (recall that variables are natural numbers > 0), where c is 0, 1 or 2 respectively if variable i does not occur or occurs negatively resp. positively in the clause.

Definition at line 99 of file QuineMcCluskey.hpp.

References OKlib::Satisfiability::FiniteFunctions::QuineMcCluskey< n, ClauseContainer >::pow3.

Referenced by OKlib::Satisfiability::FiniteFunctions::QuineMcCluskey< n, ClauseContainer >::operator()().

template<int n = 4, class ClauseContainer = std::vector<std::vector<int> >>
hash_index_type OKlib::Satisfiability::FiniteFunctions::QuineMcCluskey< n, ClauseContainer >::remove_literal ( const hash_index_type  hash,
const literal_type  literal 
) [inline]

Member Data Documentation


The documentation for this class was generated from the following file: