sat::Clause Class Reference

Clause class with watch literals. More...

#include <Clause.hpp>

Public Member Functions
	Clause ()=default
	Clause (std::vector< Literal > literals)
short	getRank (Literal l) const
std::size_t	getIndex (short rank) const
bool	setWatcher (Literal l, short watcherNo)
Literal	getWatcherByRank (short rank) const
auto	begin () const -> std::vector< Literal >::const_iterator
auto	end () const -> std::vector< Literal >::const_iterator
Literal	operator[] (std::size_t index) const
bool	isEmpty () const
std::size_t	size () const
bool	sameLiterals (const Clause &other) const

Detailed Description

Clause class with watch literals.

In order for it to model the clause_like concept, you must implement the begin() and end() member functions. I recommend that you store the Literals in a private member of type std::vector<Literal>. Then, to implement begin() and end(), you can simply return the iterators returned from std::vector<Literal>::begin() and end() respectively

Constructor & Destructor Documentation

Clause() [1/2]

sat::Clause::Clause ( )

default

Default CTor. If you want, you can remove it or adapt it to your needs

Clause() [2/2]

sat::Clause::Clause

(

std::vector< Literal >

literals

)

CTor

Parameters

literals

list of literals of the clause @TODO The tests require a single argument constructor. But you can add more arguments with default values @TODO (for example a flag that tells the constructor if the literals are already sorted) @TODO or even further constructors if you want.

Member Function Documentation

begin()

auto sat::Clause::begin

(

)

const -> std::vector<Literal>::const_iterator

Iterator to first Literal in the clause

Returns

end()

auto sat::Clause::end

(

)

const -> std::vector<Literal>::const_iterator

Past-the-end iterator

Returns

getIndex()

std::size_t sat::Clause::getIndex

(

short

rank

)

const

Gets the index of the watcher with the given rank

Parameters

rank	rank of the watcher

Returns

first watcher index if rank is 0, second watcher index otherwise

getRank()

short sat::Clause::getRank

(

Literal

l

)

const

Gets the watcher rank of the given Literal

Parameters

l

Returns

0 if first watcher, 1 if second watcher, -1 if no watcher

getWatcherByRank()

Literal sat::Clause::getWatcherByRank

(

short

rank

)

const

Get the watch literal identified by the given rank

Parameters

rank	rank of the watcher in {0, 1}

Returns

watch literal

isEmpty()

bool sat::Clause::isEmpty

(

)

const

Whether the clause is empty

Returns

operator[]()

Literal sat::Clause::operator[]

(

std::size_t

index

)

const

Array subscript operator

Parameters

index

index for access

Returns

Literal at given index

sameLiterals()

bool sat::Clause::sameLiterals

(

const Clause &

other

)

const

Whether the other clause contains the same literals (independent of ordering)

Parameters

other

clause to compare to

Returns

true if both clauses contain exactly the same literals. @TODO for your implementation you need to either sort the literals or implement your own logic for the order @TODO independent comparison

setWatcher()

bool sat::Clause::setWatcher	(	Literal	l,
		short	watcherNo
	)

Sets the given literal as watcher

Parameters

l	Literal to be the new watcher
watcherNo	number of the watcher to be replaced

Returns

true if setting watcher was successful, false if literal is not contained in clause

size()

std::size_t sat::Clause::size

(

)

const

size of the clause

Returns

---

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

• Solver/Clause.hpp
• Solver/Clause.cpp