Boolean assignments with queue for (elementary) assignments to be processed. More...
#include <AssignmentsWithBuffer.hpp>
Public Types | |
| typedef Lit | literal_type |
| typedef OKlib::Literals::traits::var_type < literal_type >::type | variable_type |
| typedef OKlib::Variables::traits::index_type < variable_type >::type | index_type |
| typedef OKlib::Satisfiability::Values::Assignment_status | value_type |
Public Member Functions | |
| BAssignmentWithQueue () | |
| n is the maximal variable index | |
| BAssignmentWithQueue (const index_type n_) | |
| BAssignmentWithQueue (const BAssignmentWithQueue &other) | |
| BAssignmentWithQueue & | operator= (const BAssignmentWithQueue &rhs) |
| void | resize (const index_type n_) |
| enlarging the capacity | |
| value_type | operator[] (const variable_type v) const |
| the value of the partial assignment for variable v | |
| value_type | operator() (const literal_type x) const |
| the value of the partial assignment for literal x | |
| bool | push (const literal_type x) |
| push x -> 1 on the buffer and enter into the assignment, in both cases only if not already present, checking with the current assignment; returns false iff inconsistent with current assignment (and thus not pushed) | |
| literal_type | top () const |
| return the next literal (assigned to true) to be processed | |
| void | pop () |
| remove the next literal to be processed | |
| index_type | size () const |
| the size of the buffer | |
| bool | empty () const |
| whether the buffer is empty | |
Detailed Description
template<typename Lit>
class OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >
Boolean assignments with queue for (elementary) assignments to be processed.
- Todo:
- Provide specification
- Todo:
- Write unit-tests
- Todo:
- Improve implementation
- Regarding member functions push, [] and () it seems that the code needs clean-up w.r.t. the various auxiliary values computed.
Definition at line 50 of file AssignmentsWithBuffer.hpp.
Member Typedef Documentation
| typedef OKlib::Variables::traits::index_type<variable_type>::type OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >::index_type |
Definition at line 55 of file AssignmentsWithBuffer.hpp.
| typedef Lit OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >::literal_type |
Definition at line 53 of file AssignmentsWithBuffer.hpp.
| typedef OKlib::Satisfiability::Values::Assignment_status OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >::value_type |
Definition at line 57 of file AssignmentsWithBuffer.hpp.
| typedef OKlib::Literals::traits::var_type<literal_type>::type OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >::variable_type |
Definition at line 54 of file AssignmentsWithBuffer.hpp.
Constructor & Destructor Documentation
| OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >::BAssignmentWithQueue | ( | ) | [inline] |
n is the maximal variable index
Definition at line 60 of file AssignmentsWithBuffer.hpp.
| OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >::BAssignmentWithQueue | ( | const index_type | n_ | ) | [inline] |
Definition at line 61 of file AssignmentsWithBuffer.hpp.
| OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >::BAssignmentWithQueue | ( | const BAssignmentWithQueue< Lit > & | other | ) | [inline] |
Definition at line 66 of file AssignmentsWithBuffer.hpp.
References OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >::size().
Member Function Documentation
| bool OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >::empty | ( | ) | const [inline] |
whether the buffer is empty
Definition at line 140 of file AssignmentsWithBuffer.hpp.
Referenced by OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >::top().
| value_type OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >::operator() | ( | const literal_type | x | ) | const [inline] |
the value of the partial assignment for literal x
Definition at line 98 of file AssignmentsWithBuffer.hpp.
References OKlib::Literals::cond(), and OKlib::Literals::var().
| BAssignmentWithQueue& OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >::operator= | ( | const BAssignmentWithQueue< Lit > & | rhs | ) | [inline] |
Definition at line 72 of file AssignmentsWithBuffer.hpp.
References OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >::size().
| value_type OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >::operator[] | ( | const variable_type | v | ) | const [inline] |
the value of the partial assignment for variable v
Definition at line 93 of file AssignmentsWithBuffer.hpp.
| void OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >::pop | ( | ) | [inline] |
remove the next literal to be processed
Definition at line 133 of file AssignmentsWithBuffer.hpp.
| bool OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >::push | ( | const literal_type | x | ) | [inline] |
push x -> 1 on the buffer and enter into the assignment, in both cases only if not already present, checking with the current assignment; returns false iff inconsistent with current assignment (and thus not pushed)
Definition at line 112 of file AssignmentsWithBuffer.hpp.
References OKlib::Literals::cond(), OKlib::Satisfiability::Values::val0, OKlib::Satisfiability::Values::val1, and OKlib::Literals::var().
Referenced by OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithRQueue< Lit >::push_forced().
| void OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >::resize | ( | const index_type | n_ | ) | [inline] |
enlarging the capacity
Definition at line 83 of file AssignmentsWithBuffer.hpp.
References OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >::size(), and OKlib::Satisfiability::Values::unassigned.
| index_type OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >::size | ( | ) | const [inline] |
the size of the buffer
Definition at line 138 of file AssignmentsWithBuffer.hpp.
Referenced by OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >::BAssignmentWithQueue(), OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >::operator=(), and OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >::resize().
| literal_type OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >::top | ( | ) | const [inline] |
return the next literal (assigned to true) to be processed
Definition at line 128 of file AssignmentsWithBuffer.hpp.
References OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >::empty().
The documentation for this class was generated from the following file:
- Satisfiability/Assignments/TotalAssignments/AssignmentsWithBuffer.hpp