strengthen.h File Reference

#include <stdbool.h>
#include "global.h"

Include dependency graph for strengthen.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions
struct clause *	kissat_on_the_fly_strengthen (struct kissat *, struct clause *, unsigned lit)
void	kissat_on_the_fly_subsume (struct kissat *, struct clause *, struct clause *)
bool	issat_strengthen_clause (struct kissat *, struct clause *, unsigned)

Function Documentation

issat_strengthen_clause()

bool issat_strengthen_clause	(	struct kissat *	,
		struct clause *	,
		unsigned	)

kissat_on_the_fly_strengthen()

struct clause * kissat_on_the_fly_strengthen	(	struct kissat *	solver,
		struct clause *	c,
		unsigned	lit )

Definition at line 144 of file strengthen.c.

                                                    {
  KISSAT_assert (!c->garbage);
  KISSAT_assert (solver->antecedent_size > 2);
  if (!c->redundant)
    kissat_mark_removed_literal (solver, lit);
  clause *res;
  if (solver->antecedent_size == 3)
    res = binary_on_the_fly_strengthen (solver, c, lit);
  else
    res = large_on_the_fly_strengthen (solver, c, lit);
  return res;
}

Here is the caller graph for this function:

kissat_on_the_fly_subsume()

void kissat_on_the_fly_subsume	(	struct kissat *	solver,
		struct clause *	c,
		struct clause *	d )

Definition at line 158 of file strengthen.c.

                                                                      {
  LOGCLS (c, "on-the-fly subsuming");
  LOGCLS (d, "on-the-fly subsumed");
  KISSAT_assert (c != d);
  KISSAT_assert (!d->garbage);
  KISSAT_assert (c->size > 1);
  KISSAT_assert (c->size <= d->size);
  kissat_mark_clause_as_garbage (solver, d);
  INC (on_the_fly_subsumed);
  if (d->redundant) {
    if (c->redundant && c->glue > d->glue)
      kissat_promote_clause (solver, c, d->glue);
    return;
  }
  if (!c->redundant)
    return;
  if (c->size > 2) {
    c->redundant = false;
    LOGCLS (c, "turned");
    kissat_update_last_irredundant (solver, c);
  }
  statistics *statistics = &solver->statistics_;
  if (c->size > 2) {
    KISSAT_assert (statistics->clauses_irredundant < UINT64_MAX);
    statistics->clauses_irredundant++;
  } else {
    KISSAT_assert (statistics->clauses_binary < UINT64_MAX);
    statistics->clauses_binary++;
  }
  KISSAT_assert (statistics->clauses_redundant > 0);
  statistics->clauses_redundant--;
}

Here is the call graph for this function:

Here is the caller graph for this function: