Contains functions to output a GRAT proof. More...

Public Member Functions
	Proof_Writer (ostream &_out)
	Constructor.

void	write_id (size_t id)
	Write identifier.

void	write_cnt (size_t c)
	Write counter.

void	write_lit (lit_t l)
	Write literal.

void	write_Z ()
	Write zero.

void	write_del (size_t id)
	Write deletion. More...

void	write_uprop (size_t id)
	Write unit propagation. More...

void	start_ty (item_type _ty)
	Start writing an item of specified type. More...

void	close ()
	Close current item and flush writer.

Detailed Description

Contains functions to output a GRAT proof.

Parameters

binary True if the proof is output in binary (split) format

Member Function Documentation

template<bool binary>

void Proof_Writer< binary >::start_ty ( item_type _ty )

inline

Start writing an item of specified type.

Parameters

_ty	Type of item. Must not be

See also: item_type::DELETION or; item_type::UNIT_PROP, these items are inserted automatically, triggered by invocations of; write_del and; write_uprop.

template<bool binary>

void Proof_Writer< binary >::write_del ( size_t id )

inline

Write deletion.

Summarizes adjacent deletions.

template<bool binary>

void Proof_Writer< binary >::write_uprop ( size_t id )

inline

Write unit propagation.

Summarizes adjacent unit propagations.

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