CaDiCaL::Checker Class Reference

#include <checker.hpp>

Inheritance diagram for CaDiCaL::Checker:

Collaboration diagram for CaDiCaL::Checker:

Public Member Functions
	Checker (Internal *)
virtual	~Checker ()
void	connect_internal (Internal *i) 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	begin_proof (int64_t) override
void	add_assumption_clause (int64_t, const vector< int > &, const vector< int64_t > &) override
void	print_stats () override
void	dump ()
Public Member Functions inherited from CaDiCaL::StatTracer
	StatTracer ()
virtual	~StatTracer ()
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 54 of file checker.hpp.

Constructor & Destructor Documentation

Checker()

CaDiCaL::Checker::Checker

(

Internal *

i

)

Definition at line 176 of file cadical_checker.cpp.

    : internal (i), size_vars (0), vals (0), inconsistent (false),
      num_clauses (0), num_garbage (0), size_clauses (0), clauses (0),
      garbage (0), next_to_propagate (0), last_hash (0) {
 
  // 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;
  }
 
  memset (&stats, 0, sizeof (stats)); // Initialize statistics.
}

Here is the call graph for this function:

~Checker()

CaDiCaL::Checker::~Checker ( )

virtual

Definition at line 200 of file cadical_checker.cpp.

                   {
  LOG ("CHECKER delete");
  vals -= size_vars;
  delete[] vals;
  for (size_t i = 0; i < size_clauses; i++)
    for (CheckerClause *c = clauses[i], *next; c; c = next)
      next = c->next, delete_clause (c);
  for (CheckerClause *c = garbage, *next; c; c = next)
    next = c->next, delete_clause (c);
  delete[] clauses;
}

Member Function Documentation

add_assumption_clause()

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

override

Definition at line 628 of file cadical_checker.cpp.

                                                                   {
  add_derived_clause (id, true, c, chain);
  delete_clause (id, true, c);
}

Here is the call graph for this function:

add_derived_clause()

void CaDiCaL::Checker::add_derived_clause ( int64_t id, bool , const vector< int > & c, const vector< int64_t > &  )

override

Definition at line 564 of file cadical_checker.cpp.

                                                           {
  if (inconsistent)
    return;
  START (checking);
  LOG (c, "CHECKER addition of derived clause");
  stats.added++;
  stats.derived++;
  import_clause (c);
  last_id = id;
  if (tautological ())
    LOG ("CHECKER ignoring satisfied derived clause");
  else if (!check () && !check_blocked ()) { // needed for ER proof support
    fatal_message_start ();
    fputs ("failed to check derived clause:\n", stderr);
    for (const auto &lit : unsimplified)
      fprintf (stderr, "%d ", lit);
    fputc ('0', stderr);
    fatal_message_end ();
  } else
    add_clause ("derived");
  simplified.clear ();
  unsimplified.clear ();
  STOP (checking);
}

Here is the call graph for this function:

Here is the caller graph for this function:

add_original_clause()

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

override

Definition at line 545 of file cadical_checker.cpp.

                                         {
  if (inconsistent)
    return;
  START (checking);
  LOG (c, "CHECKER addition of original clause");
  stats.added++;
  stats.original++;
  import_clause (c);
  last_id = id;
  if (tautological ())
    LOG ("CHECKER ignoring satisfied original clause");
  else
    add_clause ("original");
  simplified.clear ();
  unsimplified.clear ();
  STOP (checking);
}

begin_proof()

void CaDiCaL::Checker::begin_proof ( int64_t )

inlineoverridevirtual

Reimplemented from CaDiCaL::Tracer.

Definition at line 167 of file checker.hpp.

{}                          // skip

connect_internal()

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

overridevirtual

Reimplemented from CaDiCaL::InternalTracer.

Definition at line 195 of file cadical_checker.cpp.

                                           {
  internal = i;
  LOG ("CHECKER connected to internal");
}

delete_clause()

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

override

Definition at line 592 of file cadical_checker.cpp.

                                                                   {
  if (inconsistent)
    return;
  START (checking);
  LOG (c, "CHECKER checking deletion of clause");
  stats.deleted++;
  simplified.clear ();   // Can be non-empty if clause allocation fails.
  unsimplified.clear (); // Can be non-empty if clause allocation fails.
  import_clause (c);
  last_id = id;
  if (!tautological ()) {
    CheckerClause **p = find (), *d = *p;
    if (d) {
      CADICAL_assert (d->size > 1);
      // Remove from hash table, mark as garbage, connect to garbage list.
      num_garbage++;
      CADICAL_assert (num_clauses);
      num_clauses--;
      *p = d->next;
      d->next = garbage;
      garbage = d;
      d->size = 0;
    } else {
      fatal_message_start ();
      fputs ("deleted clause not in proof:\n", stderr);
      for (const auto &lit : unsimplified)
        fprintf (stderr, "%d ", lit);
      fputc ('0', stderr);
      fatal_message_end ();
    }
  }
  simplified.clear ();
  unsimplified.clear ();
  STOP (checking);
}

Here is the call graph for this function:

dump()

void CaDiCaL::Checker::dump

(

)

Definition at line 636 of file cadical_checker.cpp.

                    {
  int max_var = 0;
  for (uint64_t i = 0; i < size_clauses; i++)
    for (CheckerClause *c = clauses[i]; c; c = c->next)
      for (unsigned i = 0; i < c->size; i++)
        if (abs (c->literals[i]) > max_var)
          max_var = abs (c->literals[i]);
  printf ("p cnf %d %" PRIu64 "\n", max_var, num_clauses);
  for (uint64_t i = 0; i < size_clauses; i++)
    for (CheckerClause *c = clauses[i]; c; c = c->next) {
      for (unsigned i = 0; i < c->size; i++)
        printf ("%d ", c->literals[i]);
      printf ("0\n");
    }
}

finalize_clause()

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

inlineoverride

Definition at line 165 of file checker.hpp.

{} // skip

print_stats()

void CaDiCaL::Checker::print_stats ( )

overridevirtual

Reimplemented from CaDiCaL::StatTracer.

Definition at line 771 of file cadical_stats.cpp.

                           {
 
  if (!stats.added && !stats.deleted)
    return;
 
  SECTION ("checker statistics");
 
  MSG ("checks:          %15" PRId64 "", stats.checks);
  MSG ("assumptions:     %15" PRId64 "   %10.2f    per check",
       stats.assumptions, relative (stats.assumptions, stats.checks));
  MSG ("propagations:    %15" PRId64 "   %10.2f    per check",
       stats.propagations, relative (stats.propagations, stats.checks));
  MSG ("original:        %15" PRId64 "   %10.2f %%  of all clauses",
       stats.original, percent (stats.original, stats.added));
  MSG ("derived:         %15" PRId64 "   %10.2f %%  of all clauses",
       stats.derived, percent (stats.derived, stats.added));
  MSG ("deleted:         %15" PRId64 "   %10.2f %%  of all clauses",
       stats.deleted, percent (stats.deleted, stats.added));
  MSG ("insertions:      %15" PRId64 "   %10.2f %%  of all clauses",
       stats.insertions, percent (stats.insertions, stats.added));
  MSG ("collections:     %15" PRId64 "   %10.2f    deleted per collection",
       stats.collections, relative (stats.collections, stats.deleted));
  MSG ("collisions:      %15" PRId64 "   %10.2f    per search",
       stats.collisions, relative (stats.collisions, stats.searches));
  MSG ("searches:        %15" PRId64 "", stats.searches);
  MSG ("units:           %15" PRId64 "", stats.units);
}

Here is the call graph for this function:

report_status()

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

inlineoverridevirtual

Reimplemented from CaDiCaL::Tracer.

Definition at line 166 of file checker.hpp.

{}                   // skip

Member Data Documentation

added

int64_t CaDiCaL::Checker::added

Definition at line 133 of file checker.hpp.

assumptions

int64_t CaDiCaL::Checker::assumptions

Definition at line 139 of file checker.hpp.

checks

int64_t CaDiCaL::Checker::checks

Definition at line 146 of file checker.hpp.

collections

int64_t CaDiCaL::Checker::collections

Definition at line 148 of file checker.hpp.

collisions

int64_t CaDiCaL::Checker::collisions

Definition at line 143 of file checker.hpp.

deleted

int64_t CaDiCaL::Checker::deleted

Definition at line 137 of file checker.hpp.

derived

int64_t CaDiCaL::Checker::derived

Definition at line 135 of file checker.hpp.

insertions

int64_t CaDiCaL::Checker::insertions

Definition at line 142 of file checker.hpp.

original

int64_t CaDiCaL::Checker::original

Definition at line 134 of file checker.hpp.

propagations

int64_t CaDiCaL::Checker::propagations

Definition at line 140 of file checker.hpp.

searches

int64_t CaDiCaL::Checker::searches

Definition at line 144 of file checker.hpp.

units

int64_t CaDiCaL::Checker::units

Definition at line 149 of file checker.hpp.

---

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

• src/sat/cadical/checker.hpp
• src/sat/cadical/cadical_checker.cpp
• src/sat/cadical/cadical_stats.cpp