eliminate.c File Reference

#include "eliminate.h"
#include "allocate.h"
#include "backtrack.h"
#include "collect.h"
#include "dense.h"
#include "forward.h"
#include "inline.h"
#include "inlineheap.h"
#include "kitten.h"
#include "print.h"
#include "propdense.h"
#include "report.h"
#include "resolve.h"
#include "terminate.h"
#include "trail.h"
#include "weaken.h"
#include <inttypes.h>
#include <math.h>

Include dependency graph for eliminate.c:

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START bool	kissat_eliminating (kissat *solver)
void	kissat_update_variable_score (kissat *solver, unsigned idx)
void	kissat_eliminate_binary (kissat *solver, unsigned lit, unsigned other)
void	kissat_eliminate_clause (kissat *solver, clause *c, unsigned lit)
void	kissat_flush_units_while_connected (kissat *solver)
int	kissat_eliminate (kissat *solver)

Function Documentation

kissat_eliminate()

int kissat_eliminate

(

kissat *

solver

)

Definition at line 597 of file eliminate.c.

                                      {
  KISSAT_assert (!solver->inconsistent);
  INC (eliminations);
  eliminate (solver);
  kissat_classify (solver);
  UPDATE_CONFLICT_LIMIT (eliminate, eliminations, NLOG2N, true);
  solver->last.ticks.eliminate = solver->statistics_.search_ticks;
  return solver->inconsistent ? 20 : 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_eliminate_binary()

void kissat_eliminate_binary	(	kissat *	solver,
		unsigned	lit,
		unsigned	other )

Definition at line 121 of file eliminate.c.

                                              {
  kissat_disconnect_binary (solver, other, lit);
  kissat_delete_binary (solver, lit, other);
  update_after_removing_variable (solver, IDX (other));
}

Here is the call graph for this function:

kissat_eliminate_clause()

void kissat_eliminate_clause	(	kissat *	solver,
		clause *	c,
		unsigned	lit )

Definition at line 128 of file eliminate.c.

                                                                       {
  kissat_mark_clause_as_garbage (solver, c);
  update_after_removing_clause (solver, c, lit);
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_eliminating()

ABC_NAMESPACE_IMPL_START bool kissat_eliminating

(

kissat *

solver

)

Definition at line 23 of file eliminate.c.

                                         {
  if (!solver->enabled.eliminate)
    return false;
  statistics *statistics = &solver->statistics_;
  if (!statistics->clauses_irredundant)
    return false;
  const uint64_t conflicts = statistics->conflicts;
  if (solver->last.conflicts.reduce == conflicts)
    return false;
  limits *limits = &solver->limits;
  if (limits->eliminate.conflicts > conflicts)
    return false;
  if (limits->eliminate.variables.eliminate <
      statistics->variables_eliminate)
    return true;
  if (limits->eliminate.variables.subsume < statistics->variables_subsume)
    return true;
  return false;
}

Here is the caller graph for this function:

kissat_flush_units_while_connected()

void kissat_flush_units_while_connected

(

kissat *

solver

)

Definition at line 162 of file eliminate.c.

                                                         {
  const unsigned *propagate = solver->propagate;
  const unsigned *end_trail = END_ARRAY (solver->trail);
  KISSAT_assert (propagate <= end_trail);
  const size_t units = end_trail - propagate;
  if (!units)
    return;
#ifdef LOGGING
  LOG ("propagating and flushing %zu units", units);
#endif
  if (!kissat_dense_propagate (solver))
    return;
  LOG ("marking and flushing unit satisfied clauses");
 
  end_trail = END_ARRAY (solver->trail);
  while (propagate != end_trail) {
    const unsigned unit = *propagate++;
    watches *unit_watches = &WATCHES (unit);
    watch *begin = BEGIN_WATCHES (*unit_watches), *q = begin;
    const watch *const end = END_WATCHES (*unit_watches), *p = q;
    if (begin == end)
      continue;
    LOG ("marking %s satisfied clauses as garbage", LOGLIT (unit));
    while (p != end) {
      const watch watch = *q++ = *p++;
      if (watch.type.binary) {
        const unsigned other = watch.binary.lit;
        if (!solver->values[other])
          update_after_removing_variable (solver, IDX (other));
      } else {
        const reference ref = watch.large.ref;
        clause *c = kissat_dereference_clause (solver, ref);
        if (!c->garbage)
          kissat_eliminate_clause (solver, c, unit);
        KISSAT_assert (c->garbage);
        q--;
      }
    }
    KISSAT_assert (q <= end);
    size_t flushed = end - q;
    if (!flushed)
      continue;
    LOG ("flushing %zu references satisfied by %s", flushed, LOGLIT (unit));
    SET_END_OF_WATCHES (*unit_watches, q);
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_update_variable_score()

void kissat_update_variable_score	(	kissat *	solver,
		unsigned	idx )

Definition at line 82 of file eliminate.c.

                                                                 {
  update_variable_score (solver, &solver->schedule, idx);
}

Here is the caller graph for this function: