forward.c File Reference

#include "forward.h"
#include "allocate.h"
#include "eliminate.h"
#include "inline.h"
#include "print.h"
#include "rank.h"
#include "report.h"
#include "sort.h"
#include "terminate.h"
#include <inttypes.h>

Include dependency graph for forward.c:

Go to the source code of this file.

Macros
#define	GET_SIZE_OF_REFERENCE(REF)

Functions
bool	kissat_forward_subsume_during_elimination (kissat *solver)

Macro Definition Documentation

GET_SIZE_OF_REFERENCE

#define GET_SIZE_OF_REFERENCE

(

REF

)

Value:

  get_size_of_reference (solver, arena, (REF))

Definition at line 177 of file forward.c.

#define GET_SIZE_OF_REFERENCE(REF) \
  get_size_of_reference (solver, arena, (REF))

Function Documentation

kissat_forward_subsume_during_elimination()

bool kissat_forward_subsume_during_elimination

(

kissat *

solver

)

Definition at line 680 of file forward.c.

                                                                {
  START (subsume);
  START (forward);
  KISSAT_assert (GET_OPTION (forward));
  INC (forward_subsumptions);
  KISSAT_assert (!solver->watching);
  remove_all_duplicated_binary_clauses (solver);
  bool complete = true;
  if (!solver->inconsistent)
    complete = forward_subsume_all_clauses (solver);
  STOP (forward);
  STOP (subsume);
  return complete;
}