CaDiCaL::LratChecker Class Reference

#include <lratchecker.hpp>

Inheritance diagram for CaDiCaL::LratChecker:

Collaboration diagram for CaDiCaL::LratChecker:

Public Member Functions
	LratChecker (Internal *)
virtual	~LratChecker ()
void	connect_internal (Internal *i) override
void	begin_proof (int64_t) override
void	add_original_clause (int64_t, bool, const vector< int > &, bool restore) override
void	restore_clause (int64_t, const vector< int > &)
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	weaken_minus (int64_t, const vector< int > &) override
void	finalize_clause (int64_t, const vector< int > &) override
void	add_assumption_clause (int64_t, const vector< int > &, const vector< int64_t > &) override
void	add_assumption (int) override
void	add_constraint (const vector< int > &) override
void	reset_assumptions () override
void	report_status (int, int64_t) override
void	conclude_unsat (ConclusionType, 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_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 36 of file lratchecker.hpp.

Constructor & Destructor Documentation

LratChecker()

CaDiCaL::LratChecker::LratChecker

(

Internal *

i

)

Definition at line 120 of file cadical_lratchecker.cpp.

    : internal (i), size_vars (0), concluded (false), num_clauses (0),
      num_finalized (0), num_garbage (0), size_clauses (0), clauses (0),
      garbage (0), last_hash (0), last_id (0), current_id (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:

~LratChecker()

CaDiCaL::LratChecker::~LratChecker ( )

virtual

Definition at line 144 of file cadical_lratchecker.cpp.

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

Member Function Documentation

add_assumption()

void CaDiCaL::LratChecker::add_assumption ( int a )

overridevirtual

Reimplemented from CaDiCaL::Tracer.

Definition at line 549 of file cadical_lratchecker.cpp.

{ assumptions.push_back (a); }

add_assumption_clause()

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

override

Definition at line 530 of file cadical_lratchecker.cpp.

                                                                       {
  for (auto &lit : c) {
    if (std::find (assumptions.begin (), assumptions.end (), -lit) !=
        assumptions.end ())
      continue;
    if (std::find (constraint.begin (), constraint.end (), -lit) !=
        constraint.end ())
      continue;
    fatal_message_start ();
    fputs ("clause contains non assumptions or constraint literals\n",
           stderr);
    fatal_message_end ();
  }
  add_derived_clause (id, true, c, chain);
  delete_clause (id, true, c);
  assumption_clauses.push_back (id);
}

Here is the call graph for this function:

add_constraint()

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

override

Definition at line 551 of file cadical_lratchecker.cpp.

                                                      {
  constraint.clear ();
  for (auto &lit : c) {
    CADICAL_assert (lit);
    if (std::find (constraint.begin (), constraint.end (), lit) !=
        constraint.end ())
      continue;
    constraint.push_back (lit);
  }
}

add_derived_clause()

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

override

Definition at line 481 of file cadical_lratchecker.cpp.

                                                                          {
  START (checking);
  LOG (c, "LRAT CHECKER addition of derived clause[%" PRId64 "]", id);
  stats.added++;
  stats.derived++;
  import_clause (c);
  last_id = id;
  CADICAL_assert (id == current_id + 1);
  current_id = id;
  if (size_clauses) {
    LratCheckerClause **p = find (id), *d = *p;
    if (d) {
      fatal_message_start ();
      fputs ("different clause with id ", stderr);
      fprintf (stderr, "%" PRId64, id);
      fputs (" already present\n", stderr);
      fatal_message_end ();
    }
  }
  CADICAL_assert (id);
  bool failed = true;
  if (check (proof_chain) && check_resolution (proof_chain)) {
    failed = false;
  } else if (check_blocked (proof_chain)) {
    failed = false;
  }
  if (failed) {
    LOG (proof_chain, "LRAT CHECKER check failed with chain");
#ifdef LOGGING
    for (const auto &pid : proof_chain) {
      const int64_t aid = abs (pid);
      LratCheckerClause **p = find (aid), *d = *p;
      LOG (d->literals, d->size, "clause[%" PRId64 "]", pid);
    }
#endif
    fatal_message_start ();
    fputs ("failed to check derived clause:\n", stderr);
    for (const auto &lit : imported_clause)
      fprintf (stderr, "%d ", lit);
    fputc ('0', stderr);
    fatal_message_end ();
  } else
    insert ();
  imported_clause.clear ();
  STOP (checking);
}

Here is the call graph for this function:

Here is the caller graph for this function:

add_original_clause()

void CaDiCaL::LratChecker::add_original_clause ( int64_t id, bool , const vector< int > & c, bool restore )

override

Definition at line 452 of file cadical_lratchecker.cpp.

                                                                           {
  START (checking);
  LOG (c, "LRAT CHECKER addition of original clause[%" PRId64 "]", id);
  if (restore)
    restore_clause (id, c);
  stats.added++;
  stats.original++;
  import_clause (c);
  last_id = id;
  if (!restore && id == 1 + current_id)
    current_id = id;
 
  if (size_clauses && !restore) {
    LratCheckerClause **p = find (id), *d = *p;
    if (d) {
      fatal_message_start ();
      fputs ("different clause with id ", stderr);
      fprintf (stderr, "%" PRId64, id);
      fputs (" already present\n", stderr);
      fatal_message_end ();
    }
  }
  CADICAL_assert (id);
  insert ();
  imported_clause.clear ();
  STOP (checking);
}

Here is the call graph for this function:

begin_proof()

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

overridevirtual

Reimplemented from CaDiCaL::Tracer.

Definition at line 831 of file cadical_lratchecker.cpp.

{ current_id = id; }

conclude_unsat()

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

override

Definition at line 569 of file cadical_lratchecker.cpp.

                                                              {
  if (concluded) {
    fatal_message_start ();
    fputs ("already concluded\n", stderr);
    fatal_message_end ();
  }
  concluded = true;
  if (conclusion == CONFLICT) {
    LratCheckerClause **p = find (ids.back ()), *d = *p;
    if (!d || d->size) {
      fatal_message_start ();
      fputs ("empty clause not in proof\n", stderr);
      fatal_message_end ();
    }
    return;
  } else if (conclusion == ASSUMPTIONS) {
    if (ids.size () != 1 || assumption_clauses.size () != 1) {
      fatal_message_start ();
      fputs ("expected exactly one assumption clause\n", stderr);
      fatal_message_end ();
    }
    if (ids.back () != assumption_clauses.back ()) {
      fatal_message_start ();
      fputs ("conclusion is not an assumption clause\n", stderr);
      fatal_message_end ();
    }
    return;
  } else {
    CADICAL_assert (conclusion == CONSTRAINT);
    if (constraint.size () != ids.size ()) {
      fatal_message_start ();
      fputs ("not complete conclusion given for constraint\n", stderr);
      fputs ("The constraint contains the literals: ", stderr);
      for (auto c : constraint) {
        fprintf (stderr, "%d ", c);
      }
 
      fputs ("\nThe ids are: ", stderr);
      for (auto c : ids) {
        fprintf (stderr, "%" PRId64 " ", c);
      }
      fatal_message_end ();
    }
    for (auto &id : ids) {
      if (std::find (assumption_clauses.begin (), assumption_clauses.end (),
                     id) != assumption_clauses.end ())
        continue;
      fatal_message_start ();
      fputs ("assumption clause for constraint missing\n", stderr);
      fatal_message_end ();
    }
  }
}

Here is the call graph for this function:

connect_internal()

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

overridevirtual

Reimplemented from CaDiCaL::InternalTracer.

Definition at line 139 of file cadical_lratchecker.cpp.

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

delete_clause()

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

override

Definition at line 626 of file cadical_lratchecker.cpp.

                                                                       {
  START (checking);
  LOG (c, "LRAT CHECKER checking deletion of clause[%" PRId64 "]", id);
  stats.deleted++;
  import_clause (c);
  last_id = id;
  LratCheckerClause **p = find (id), *d = *p;
  if (d) {
    for (const auto &lit : imported_clause)
      mark (lit) = true;
    const int *dp = d->literals;
    for (unsigned i = 0; i < d->size; i++) {
      int lit = *(dp + i);
      if (!mark (lit)) {        // should never happen since ids
        fatal_message_start (); // are unique.
        fputs ("deleted clause not in proof:\n", stderr);
        for (const auto &lit : imported_clause)
          fprintf (stderr, "%d ", lit);
        fputc ('0', stderr);
        fatal_message_end ();
      }
    }
    for (const auto &lit : imported_clause)
      mark (lit) = false;
 
    // 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->garbage = true;
 
    // If there are enough garbage clauses collect them.
    // TODO: probably can just delete clause directly without
    // specific garbage collection phase.
    if (num_garbage > 0.5 * max ((size_t) size_clauses, (size_t) size_vars))
      collect_garbage_clauses ();
  } else {
    fatal_message_start ();
    fputs ("deleted clause not in proof:\n", stderr);
    for (const auto &lit : imported_clause)
      fprintf (stderr, "%d ", lit);
    fputc ('0', stderr);
    fatal_message_end ();
  }
  imported_clause.clear ();
  STOP (checking);
}

Here is the call graph for this function:

dump()

void CaDiCaL::LratChecker::dump

(

)

Definition at line 815 of file cadical_lratchecker.cpp.

                        {
  int max_var = 0;
  for (uint64_t i = 0; i < size_clauses; i++)
    for (LratCheckerClause *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 (LratCheckerClause *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::LratChecker::finalize_clause ( int64_t id, const vector< int > & c )

override

Definition at line 757 of file cadical_lratchecker.cpp.

                                                                   {
  START (checking);
  LOG (c, "LRAT CHECKER checking finalize of clause[%" PRId64 "]", id);
  stats.finalized++;
  num_finalized++;
  import_clause (c);
  CADICAL_assert (id <= current_id);
  last_id = id;
  LratCheckerClause **p = find (id), *d = *p;
  if (d) {
    for (const auto &lit : imported_clause)
      mark (lit) = true;
    const int *dp = d->literals;
    for (unsigned i = 0; i < d->size; i++) {
      int lit = *(dp + i);
      if (!mark (lit)) {        // should never happen since ids
        fatal_message_start (); // are unique.
        fputs ("deleted clause not in proof:\n", stderr);
        for (const auto &lit : imported_clause)
          fprintf (stderr, "%d ", lit);
        fputc ('0', stderr);
        fatal_message_end ();
      }
    }
    for (const auto &lit : imported_clause)
      mark (lit) = false;
 
  } else {
    fatal_message_start ();
    fputs ("deleted clause not in proof:\n", stderr);
    for (const auto &lit : imported_clause)
      fprintf (stderr, "%d ", lit);
    fputc ('0', stderr);
    fatal_message_end ();
  }
  imported_clause.clear ();
  STOP (checking);
}

Here is the call graph for this function:

print_stats()

void CaDiCaL::LratChecker::print_stats ( )

overridevirtual

Reimplemented from CaDiCaL::StatTracer.

Definition at line 799 of file cadical_stats.cpp.

                               {
 
  if (!stats.added && !stats.deleted)
    return;
 
  SECTION ("lrat checker statistics");
 
  MSG ("checks:          %15" PRId64 "", stats.checks);
  MSG ("insertions:      %15" PRId64 "   %10.2f %%  of all clauses",
       stats.insertions, percent (stats.insertions, stats.added));
  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 ("finalized:       %15" PRId64 "   %10.2f %%  of all clauses",
       stats.finalized, percent (stats.finalized, 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);
}

Here is the call graph for this function:

report_status()

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

overridevirtual

Reimplemented from CaDiCaL::Tracer.

Definition at line 797 of file cadical_lratchecker.cpp.

                                             {
  START (checking);
  if (num_finalized == num_clauses) {
    num_finalized = 0;
    LOG ("LRAT CHECKER successful finalize check, all clauses have been "
         "deleted");
  } else {
    fatal_message_start ();
    fputs ("finalize check failed ", stderr);
    fprintf (stderr, "%" PRIu64, num_clauses);
    fputs (" are not finalized", stderr);
    fatal_message_end ();
  }
  STOP (checking);
}

Here is the call graph for this function:

reset_assumptions()

void CaDiCaL::LratChecker::reset_assumptions ( )

overridevirtual

Reimplemented from CaDiCaL::Tracer.

Definition at line 562 of file cadical_lratchecker.cpp.

                                     {
  assumption_clauses.clear ();
  assumptions.clear ();
  concluded = false;
  // constraint.clear ();
}

restore_clause()

void CaDiCaL::LratChecker::restore_clause	(	int64_t	id,
		const vector< int > &	c )

Definition at line 718 of file cadical_lratchecker.cpp.

                                                                  {
  LOG (c, "LRAT CHECKER check of restoration of clause[%" PRId64 "]", id);
  if (clauses_to_reconstruct.find (id) == end (clauses_to_reconstruct)) {
    fatal_message_start ();
    fputs ("restoring clauses not deleted previously:\n", stderr);
    for (const auto &lit : c)
      fprintf (stderr, "%d ", lit);
    fputc ('0', stderr);
    fatal_message_end ();
  }
  vector<int> e = c;
  sort (begin (e), end (e));
  const vector<int> &d = clauses_to_reconstruct.find (id)->second;
  bool eq = true;
  if (c.size () != d.size ()) {
    eq = false;
  }
 
  for (std::vector<int>::size_type i = 0; i < e.size () && eq; ++i) {
    eq = (e[i] == d[i]);
  }
 
  if (!eq) {
    fatal_message_start ();
    fputs ("restoring clause that is different than the one imported:\n",
           stderr);
    for (const auto &lit : c)
      fprintf (stderr, "%d ", lit);
    fputc ('0', stderr);
    fputs ("vs:\n", stderr);
    for (const auto &lit : d)
      fprintf (stderr, "%d ", lit);
    fputc ('0', stderr);
    fatal_message_end ();
  }
 
  clauses_to_reconstruct.erase (id);
}

Here is the call graph for this function:

Here is the caller graph for this function:

weaken_minus()

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

override

Definition at line 679 of file cadical_lratchecker.cpp.

                                                                {
  LOG (c, "LRAT CHECKER saving clause[%" PRId64 "] to restore later", id);
  import_clause (c);
 
  CADICAL_assert (id <= current_id);
  last_id = id;
  LratCheckerClause **p = find (id), *d = *p;
  if (d) {
    for (const auto &lit : imported_clause)
      mark (lit) = true;
    const int *dp = d->literals;
    for (unsigned i = 0; i < d->size; i++) {
      int lit = *(dp + i);
      if (!mark (lit)) {        // should never happen since ids
        fatal_message_start (); // are unique.
        fputs ("deleted clause not in proof:\n", stderr);
        for (const auto &lit : imported_clause)
          fprintf (stderr, "%d ", lit);
        fputc ('0', stderr);
        fatal_message_end ();
      }
    }
    for (const auto &lit : imported_clause)
      mark (lit) = false;
  } else {
    fatal_message_start ();
    fputs ("weakened clause not in proof:\n", stderr);
    for (const auto &lit : imported_clause)
      fprintf (stderr, "%d ", lit);
    fputc ('0', stderr);
    fatal_message_end ();
  }
  imported_clause.clear ();
 
  vector<int> e = c;
  sort (begin (e), end (e));
  clauses_to_reconstruct[id] = e;
}

Here is the call graph for this function:

Member Data Documentation

added

int64_t CaDiCaL::LratChecker::added

Definition at line 103 of file lratchecker.hpp.

checks

int64_t CaDiCaL::LratChecker::checks

Definition at line 114 of file lratchecker.hpp.

collections

int64_t CaDiCaL::LratChecker::collections

Definition at line 116 of file lratchecker.hpp.

collisions

int64_t CaDiCaL::LratChecker::collisions

Definition at line 111 of file lratchecker.hpp.

deleted

int64_t CaDiCaL::LratChecker::deleted

Definition at line 107 of file lratchecker.hpp.

derived

int64_t CaDiCaL::LratChecker::derived

Definition at line 105 of file lratchecker.hpp.

finalized

int64_t CaDiCaL::LratChecker::finalized

Definition at line 108 of file lratchecker.hpp.

insertions

int64_t CaDiCaL::LratChecker::insertions

Definition at line 110 of file lratchecker.hpp.

original

int64_t CaDiCaL::LratChecker::original

Definition at line 104 of file lratchecker.hpp.

searches

int64_t CaDiCaL::LratChecker::searches

Definition at line 112 of file lratchecker.hpp.

---

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

• src/sat/cadical/lratchecker.hpp
• src/sat/cadical/cadical_lratchecker.cpp
• src/sat/cadical/cadical_stats.cpp