CaDiCaL::VeripbTracer Class Reference

#include <veripbtracer.hpp>

Inheritance diagram for CaDiCaL::VeripbTracer:

Collaboration diagram for CaDiCaL::VeripbTracer:

Public Member Functions
	VeripbTracer (Internal *, File *file, bool, bool, bool)
	~VeripbTracer ()
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
void	weaken_minus (int64_t, const vector< int > &) override
void	strengthen (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	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 18 of file veripbtracer.hpp.

Constructor & Destructor Documentation

VeripbTracer()

CaDiCaL::VeripbTracer::VeripbTracer	(	Internal *	i,
		File *	file,
		bool	b,
		bool	a,
		bool	c )

Definition at line 11 of file cadical_veripbtracer.cpp.

    : internal (i), file (f), with_antecedents (a), checked_deletions (c),
      num_clauses (0), size_clauses (0), clauses (0), last_hash (0),
      last_id (0), last_clause (0)
#ifndef CADICAL_QUIET
      ,
      added (0), deleted (0)
#endif
{
  (void) internal;
 
  // Initialize random number table for hash function.
  //
  Random random (42);
  for (unsigned n = 0; n < num_nonces; n++) {
    uint64_t nonce = random.next ();
    if (!(nonce & 1))
      nonce++;
    CADICAL_assert (nonce), CADICAL_assert (nonce & 1);
    nonces[n] = nonce;
  }
#ifndef CADICAL_NDEBUG
  binary = b;
#else
  (void) b;
#endif
}

Here is the call graph for this function:

~VeripbTracer()

CaDiCaL::VeripbTracer::~VeripbTracer

(

)

Definition at line 45 of file cadical_veripbtracer.cpp.

                             {
  LOG ("VERIPB TRACER delete");
  delete file;
  for (size_t i = 0; i < size_clauses; i++)
    for (HashId *c = clauses[i], *next; c; c = next)
      next = c->next, delete_clause (c);
  delete[] clauses;
}

Member Function Documentation

add_derived_clause()

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

override

Definition at line 297 of file cadical_veripbtracer.cpp.

                                                                     {
  if (file->closed ())
    return;
  LOG ("VERIPB TRACER tracing addition of derived clause[%" PRId64 "]", id);
  if (with_antecedents)
    veripb_add_derived_clause (id, redundant, clause, chain);
  else
    veripb_add_derived_clause (id, redundant, clause);
#ifndef CADICAL_QUIET
  added++;
#endif
}

add_original_clause()

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

inlineoverride

Definition at line 82 of file veripbtracer.hpp.

                                                   {} // skip

begin_proof()

void CaDiCaL::VeripbTracer::begin_proof ( int64_t id )

overridevirtual

Reimplemented from CaDiCaL::Tracer.

Definition at line 288 of file cadical_veripbtracer.cpp.

                                          {
  if (file->closed ())
    return;
  LOG ("VERIPB TRACER tracing start of proof with %" PRId64
       "original clauses",
       id);
  veripb_begin_proof (id);
}

close()

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

overridevirtual

Implements CaDiCaL::FileTracer.

Definition at line 372 of file cadical_veripbtracer.cpp.

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

Here is the call graph for this function:

closed()

bool CaDiCaL::VeripbTracer::closed ( )

overridevirtual

Implements CaDiCaL::FileTracer.

Definition at line 354 of file cadical_veripbtracer.cpp.

{ return file->closed (); }

Here is the caller graph for this function:

connect_internal()

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

overridevirtual

Reimplemented from CaDiCaL::InternalTracer.

Definition at line 39 of file cadical_veripbtracer.cpp.

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

delete_clause()

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

override

Definition at line 312 of file cadical_veripbtracer.cpp.

                                                       {
  if (file->closed ())
    return;
  LOG ("VERIPB TRACER tracing deletion of clause[%" PRId64 "]", id);
  veripb_delete_clause (id, redundant);
#ifndef CADICAL_QUIET
  deleted++;
#endif
}

finalize_clause()

void CaDiCaL::VeripbTracer::finalize_clause ( int64_t , const vector< int > &  )

inlineoverride

Definition at line 89 of file veripbtracer.hpp.

{} // skip

flush()

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

overridevirtual

Implements CaDiCaL::FileTracer.

Definition at line 385 of file cadical_veripbtracer.cpp.

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

Here is the call graph for this function:

report_status()

void CaDiCaL::VeripbTracer::report_status ( int status, int64_t conflict_id )

overridevirtual

Reimplemented from CaDiCaL::Tracer.

Definition at line 323 of file cadical_veripbtracer.cpp.

                                                                 {
  if (file->closed ())
    return;
#ifdef LOGGING
  if (conflict_id)
    LOG ("VERIPB TRACER tracing finalization of proof with empty "
         "clause[%" PRId64 "]",
         conflict_id);
#endif
  veripb_report_status (status == UNSATISFIABLE, conflict_id);
}

strengthen()

void CaDiCaL::VeripbTracer::strengthen ( int64_t id )

overridevirtual

Reimplemented from CaDiCaL::Tracer.

Definition at line 345 of file cadical_veripbtracer.cpp.

                                         {
  if (file->closed ())
    return;
  LOG ("VERIPB TRACER tracing strengthen of clause[%" PRId64 "]", id);
  veripb_strengthen (id);
}

weaken_minus()

void CaDiCaL::VeripbTracer::weaken_minus ( int64_t id, const vector< int > &  )

override

Definition at line 335 of file cadical_veripbtracer.cpp.

                                                                {
  if (!checked_deletions)
    return;
  if (file->closed ())
    return;
  LOG ("VERIPB TRACER tracing weaken minus of clause[%" PRId64 "]", id);
  last_id = id;
  insert ();
}

---

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

• src/sat/cadical/veripbtracer.hpp
• src/sat/cadical/cadical_veripbtracer.cpp