#include <lidruptracer.hpp>

Inheritance diagram for CaDiCaL::LidrupTracer:

[legend]

Collaboration diagram for CaDiCaL::LidrupTracer:

[legend]

Public Member Functions
	LidrupTracer (Internal , File file, bool)

	~LidrupTracer ()

void	add_derived_clause (int64_t, bool, const vector< int > &, const vector< int64_t > &) override

void	add_assumption_clause (int64_t, const vector< int > &, const vector< int64_t > &) override

void	weaken_minus (int64_t, const vector< int > &) override

void	delete_clause (int64_t, bool, const vector< int > &) override

void	add_original_clause (int64_t, bool, const vector< int > &, bool=false) override

void	report_status (int, int64_t) override

void	conclude_sat (const vector< int > &) override

void	conclude_unsat (ConclusionType, const vector< int64_t > &) override

void	conclude_unknown (const vector< int > &) override

void	solve_query () override

void	add_assumption (int) override

void	reset_assumptions () override

void	begin_proof (int64_t) override

void	finalize_clause (int64_t, const vector< int > &) override

void	strengthen (int64_t) override

void	add_constraint (const vector< int > &) override

void	connect_internal (Internal *i) 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	add_constraint (const std::vector< int > &)

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 20 of file lidruptracer.hpp.

Constructor & Destructor Documentation

◆ LidrupTracer()

CaDiCaL::LidrupTracer::LidrupTracer	(	Internal *	i,
		File *	file,
		bool	b )

Definition at line 11 of file cadical_lidruptracer.cpp.

    : internal (i), file (f), binary (b), 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
  piping = file->piping ();
}

Here is the call graph for this function:

◆ ~LidrupTracer()

CaDiCaL::LidrupTracer::~LidrupTracer ( )

Definition at line 45 of file cadical_lidruptracer.cpp.

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

Member Function Documentation

◆ add_assumption()

void CaDiCaL::LidrupTracer::add_assumption ( int lit )

overridevirtual

Reimplemented from CaDiCaL::Tracer.

Definition at line 594 of file cadical_lidruptracer.cpp.

                                          {
  LOG ("LIDRUP TRACER tracing addition of assumption %d", lit);
  assumptions.push_back (lit);
}

◆ add_assumption_clause()

void CaDiCaL::LidrupTracer::add_assumption_clause	(	int64_t	id,
		const vector< int > &	clause,
		const vector< int64_t > &	chain )

override

Definition at line 478 of file cadical_lidruptracer.cpp.

                                                                        {
  if (file->closed ())
    return;
  CADICAL_assert (imported_clause.empty ());
  LOG (clause,
       "LIDRUP TRACER tracing addition of assumption clause[%" PRId64 "]",
       id);
  for (auto &lit : clause)
    imported_clause.push_back (lit);
  for (auto &cid : chain)
    imported_chain.push_back (cid);
  last_id = id;
  insert ();
  imported_clause.clear ();
  imported_chain.clear ();
}

◆ add_constraint()

void CaDiCaL::LidrupTracer::add_constraint ( const vector< int > & )

inlineoverride

Definition at line 106 of file lidruptracer.hpp.

106{}

◆ add_derived_clause()

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

override

Definition at line 465 of file cadical_lidruptracer.cpp.

                                                                     {
  if (file->closed ())
    return;
  CADICAL_assert (imported_clause.empty ());
  LOG (clause, "LIDRUP TRACER tracing addition of derived clause");
  lidrup_add_derived_clause (id, clause, chain);
#ifndef CADICAL_QUIET
  added++;
#endif
}

◆ add_original_clause()

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

override

Definition at line 538 of file cadical_lidruptracer.cpp.

                                                       {
  if (file->closed ())
    return;
  if (!restored) {
    LOG (clause, "LIDRUP TRACER tracing addition of original clause");
#ifndef CADICAL_QUIET
    original++;
#endif
    return lidrup_add_original_clause (id, clause);
  }
  CADICAL_assert (restored);
  if (find_and_delete (id)) {
    LOG (clause,
         "LIDRUP TRACER the clause was not yet weakened, so no restore");
    return;
  }
  LOG (clause, "LIDRUP TRACER tracing addition of restored clause");
  lidrup_add_restored_clause (id);
#ifndef CADICAL_QUIET
  restore++;
#endif
}

◆ begin_proof()

void CaDiCaL::LidrupTracer::begin_proof ( int64_t )

inlineoverridevirtual

Reimplemented from CaDiCaL::Tracer.

Definition at line 103 of file lidruptracer.hpp.

103{}

◆ close()

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

overridevirtual

Implements CaDiCaL::FileTracer.

Definition at line 633 of file cadical_lidruptracer.cpp.

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

Here is the call graph for this function:

◆ closed()

bool CaDiCaL::LidrupTracer::closed ( )

overridevirtual

Implements CaDiCaL::FileTracer.

Definition at line 606 of file cadical_lidruptracer.cpp.

606{ return file->closed (); }

Here is the caller graph for this function:

◆ conclude_sat()

void CaDiCaL::LidrupTracer::conclude_sat ( const vector< int > & model )

override

Definition at line 570 of file cadical_lidruptracer.cpp.

                                                         {
  if (file->closed ())
    return;
  LOG (model, "LIDRUP TRACER tracing conclusion of model");
  lidrup_conclude_sat (model);
}

◆ conclude_unknown()

void CaDiCaL::LidrupTracer::conclude_unknown ( const vector< int > & entrailed )

override

Definition at line 577 of file cadical_lidruptracer.cpp.

                                                                 {
  if (file->closed ())
    return;
  LOG (entrailed, "LIDRUP TRACER tracing conclusion of UNK");
  lidrup_conclude_unknown (entrailed);
}

◆ conclude_unsat()

void CaDiCaL::LidrupTracer::conclude_unsat	(	ConclusionType	,
		const vector< int64_t > &	conclusion )

override

Definition at line 529 of file cadical_lidruptracer.cpp.

                                                                      {
  if (file->closed ())
    return;
  CADICAL_assert (imported_clause.empty ());
  LOG (conclusion, "LIDRUP TRACER tracing conclusion of clause(s)");
  lidrup_conclude_and_delete (conclusion);
}

◆ connect_internal()

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

overridevirtual

Reimplemented from CaDiCaL::InternalTracer.

Definition at line 39 of file cadical_lidruptracer.cpp.

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

◆ delete_clause()

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

override

Definition at line 497 of file cadical_lidruptracer.cpp.

                                                                       {
  if (file->closed ())
    return;
  CADICAL_assert (imported_clause.empty ());
  LOG ("LIDRUP TRACER tracing deletion of clause[%" PRId64 "]", id);
  if (find_and_delete (id)) {
    CADICAL_assert (imported_clause.empty ());
    if (!batch_delete.empty () || !batch_restore.empty ())
      lidrup_batch_weaken_restore_and_delete ();
    batch_weaken.push_back (id);
#ifndef CADICAL_QUIET
    weakened++;
#endif
  } else {
    if (!batch_weaken.empty () || !batch_restore.empty ())
      lidrup_batch_weaken_restore_and_delete ();
    batch_delete.push_back (id);
#ifndef CADICAL_QUIET
    deleted++;
#endif
  }
}

◆ finalize_clause()

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

inlineoverride

Definition at line 104 of file lidruptracer.hpp.

104{}

◆ flush()

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

overridevirtual

Implements CaDiCaL::FileTracer.

Definition at line 646 of file cadical_lidruptracer.cpp.

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

Here is the call graph for this function:

◆ report_status()

void CaDiCaL::LidrupTracer::report_status	(	int	status,
		int64_t	)

overridevirtual

Reimplemented from CaDiCaL::Tracer.

Definition at line 563 of file cadical_lidruptracer.cpp.

                                                     {
  if (file->closed ())
    return;
  LOG ("LIDRUP TRACER tracing report of status %d", status);
  lidrup_report_status (status);
}

◆ reset_assumptions()

void CaDiCaL::LidrupTracer::reset_assumptions ( )

overridevirtual

Reimplemented from CaDiCaL::Tracer.

Definition at line 599 of file cadical_lidruptracer.cpp.

                                      {
  LOG (assumptions, "LIDRUP TRACER tracing reset of assumptions");
  assumptions.clear ();
}

◆ solve_query()

void CaDiCaL::LidrupTracer::solve_query ( )

overridevirtual

Reimplemented from CaDiCaL::Tracer.

Definition at line 584 of file cadical_lidruptracer.cpp.

                                {
  if (file->closed ())
    return;
  LOG (assumptions, "LIDRUP TRACER tracing solve query with assumptions");
  lidrup_solve_query ();
#ifndef CADICAL_QUIET
  solved++;
#endif
}

◆ strengthen()

void CaDiCaL::LidrupTracer::strengthen ( int64_t )

inlineoverridevirtual

Reimplemented from CaDiCaL::Tracer.

Definition at line 105 of file lidruptracer.hpp.

105{}

◆ weaken_minus()

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

override

Definition at line 520 of file cadical_lidruptracer.cpp.

                                                                {
  if (file->closed ())
    return;
  CADICAL_assert (imported_clause.empty ());
  LOG ("LIDRUP 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/lidruptracer.hpp
src/sat/cadical/cadical_lidruptracer.cpp

Public Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ LidrupTracer()

◆ ~LidrupTracer()

Member Function Documentation

◆ add_assumption()

◆ add_assumption_clause()

◆ add_constraint()

◆ add_derived_clause()

◆ add_original_clause()

◆ begin_proof()

◆ close()

◆ closed()

◆ conclude_sat()

◆ conclude_unknown()

◆ conclude_unsat()

◆ connect_internal()

◆ delete_clause()

◆ finalize_clause()

◆ flush()

◆ report_status()

◆ reset_assumptions()

◆ solve_query()

◆ strengthen()

◆ weaken_minus()