CaDiCaL::FratTracer Class Reference

#include <frattracer.hpp>

Inheritance diagram for CaDiCaL::FratTracer:

Collaboration diagram for CaDiCaL::FratTracer:

Public Member Functions
	FratTracer (Internal *, File *file, bool binary, bool antecedents)
	~FratTracer ()
void	connect_internal (Internal *i) override
void	begin_proof (int64_t) override
void	add_original_clause (int64_t, bool, const vector< int > &, bool=false) override
void	add_derived_clause (int64_t, bool, const vector< int > &, const vector< int64_t > &) override
void	delete_clause (int64_t, bool, const vector< int > &) override
void	finalize_clause (int64_t, const vector< int > &) override
void	report_status (int, int64_t) override
bool	closed () override
void	close (bool) override
void	flush (bool) override
Public Member Functions inherited from CaDiCaL::FileTracer
	FileTracer ()
virtual	~FileTracer ()
Public Member Functions inherited from CaDiCaL::InternalTracer
	InternalTracer ()
virtual	~InternalTracer ()
Public Member Functions inherited from CaDiCaL::Tracer
	Tracer ()
virtual	~Tracer ()
virtual void	add_original_clause (int64_t, bool, const std::vector< int > &, bool=false)
virtual void	add_derived_clause (int64_t, bool, const std::vector< int > &, const std::vector< int64_t > &)
virtual void	delete_clause (int64_t, bool, const std::vector< int > &)
virtual void	demote_clause (uint64_t, const std::vector< int > &)
virtual void	weaken_minus (int64_t, const std::vector< int > &)
virtual void	strengthen (int64_t)
virtual void	finalize_clause (int64_t, const std::vector< int > &)
virtual void	solve_query ()
virtual void	add_assumption (int)
virtual void	add_constraint (const std::vector< int > &)
virtual void	reset_assumptions ()
virtual void	add_assumption_clause (int64_t, const std::vector< int > &, const std::vector< int64_t > &)
virtual void	conclude_unsat (ConclusionType, const std::vector< int64_t > &)
virtual void	conclude_sat (const std::vector< int > &)
virtual void	conclude_unknown (const std::vector< int > &)

Detailed Description

Definition at line 10 of file frattracer.hpp.

Constructor & Destructor Documentation

FratTracer()

CaDiCaL::FratTracer::FratTracer	(	Internal *	i,
		File *	file,
		bool	binary,
		bool	antecedents )

Definition at line 11 of file cadical_frattracer.cpp.

    : internal (i), file (f), binary (b), with_antecedents (a)
#ifndef CADICAL_QUIET
      ,
      added (0), deleted (0), finalized (0), original (0)
#endif
{
  (void) internal;
}

~FratTracer()

CaDiCaL::FratTracer::~FratTracer

(

)

Definition at line 27 of file cadical_frattracer.cpp.

                         {
  LOG ("FRAT TRACER delete");
  delete file;
}

Member Function Documentation

add_derived_clause()

void CaDiCaL::FratTracer::add_derived_clause ( int64_t id, bool , const vector< int > & clause, const vector< int64_t > & chain )

override

Definition at line 199 of file cadical_frattracer.cpp.

                                                                   {
  if (file->closed ())
    return;
  LOG ("FRAT TRACER tracing addition of derived clause");
  if (with_antecedents)
    frat_add_derived_clause (id, clause, chain);
  else
    frat_add_derived_clause (id, clause);
#ifndef CADICAL_QUIET
  added++;
#endif
}

add_original_clause()

void CaDiCaL::FratTracer::add_original_clause ( int64_t id, bool , const vector< int > & clause, bool = false )

override

Definition at line 191 of file cadical_frattracer.cpp.

                                                                       {
  if (file->closed ())
    return;
  LOG ("FRAT TRACER tracing addition of original clause");
  frat_add_original_clause (id, clause);
}

begin_proof()

void CaDiCaL::FratTracer::begin_proof ( int64_t )

inlineoverridevirtual

Reimplemented from CaDiCaL::Tracer.

Definition at line 42 of file frattracer.hpp.

{} // skip

close()

void CaDiCaL::FratTracer::close ( bool print )

overridevirtual

Implements CaDiCaL::FileTracer.

Definition at line 255 of file cadical_frattracer.cpp.

                                  {
  CADICAL_assert (!closed ());
  file->close ();
#ifndef CADICAL_QUIET
  if (print) {
    MSG ("FRAT proof file '%s' closed", file->name ());
    print_statistics ();
  }
#else
  (void) print;
#endif
}

Here is the call graph for this function:

closed()

bool CaDiCaL::FratTracer::closed ( )

overridevirtual

Implements CaDiCaL::FileTracer.

Definition at line 234 of file cadical_frattracer.cpp.

{ return file->closed (); }

Here is the caller graph for this function:

connect_internal()

void CaDiCaL::FratTracer::connect_internal ( Internal * i )

overridevirtual

Reimplemented from CaDiCaL::InternalTracer.

Definition at line 21 of file cadical_frattracer.cpp.

                                              {
  internal = i;
  file->connect_internal (internal);
  LOG ("FRAT TRACER connected to internal");
}

delete_clause()

void CaDiCaL::FratTracer::delete_clause ( int64_t id, bool , const vector< int > & clause )

override

Definition at line 214 of file cadical_frattracer.cpp.

                                                           {
  if (file->closed ())
    return;
  LOG ("FRAT TRACER tracing deletion of clause");
  frat_delete_clause (id, clause);
#ifndef CADICAL_QUIET
  deleted++;
#endif
}

finalize_clause()

void CaDiCaL::FratTracer::finalize_clause ( int64_t id, const vector< int > & clause )

override

Definition at line 225 of file cadical_frattracer.cpp.

                                                                       {
  if (file->closed ())
    return;
  LOG ("FRAT TRACER tracing finalization of clause");
  frat_finalize_clause (id, clause);
}

flush()

void CaDiCaL::FratTracer::flush ( bool print )

overridevirtual

Implements CaDiCaL::FileTracer.

Definition at line 268 of file cadical_frattracer.cpp.

                                  {
  CADICAL_assert (!closed ());
  file->flush ();
#ifndef CADICAL_QUIET
  if (print) {
    MSG ("FRAT proof file '%s' flushed", file->name ());
    print_statistics ();
  }
#else
  (void) print;
#endif
}

Here is the call graph for this function:

report_status()

void CaDiCaL::FratTracer::report_status ( int , int64_t  )

inlineoverridevirtual

Reimplemented from CaDiCaL::Tracer.

Definition at line 54 of file frattracer.hpp.

{} // skip

---

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

• src/sat/cadical/frattracer.hpp
• src/sat/cadical/cadical_frattracer.cpp