CaDiCaL::Eliminator Struct Reference

#include <elim.hpp>

Collaboration diagram for CaDiCaL::Eliminator:

Public Member Functions
	Eliminator (Internal *i)
	~Eliminator ()
Clause *	dequeue ()
void	enqueue (Clause *)

Public Attributes
Internal *	internal
ElimSchedule	schedule
queue< Clause * >	backward
vector< Clause * >	gates
unsigned	definition_unit
vector< proof_clause >	proof_clauses
vector< int >	marked
GateType	gatetype

Detailed Description

Definition at line 33 of file elim.hpp.

Constructor & Destructor Documentation

Eliminator()

CaDiCaL::Eliminator::Eliminator ( Internal * i )

inline

Definition at line 38 of file elim.hpp.

      : internal (i), schedule (elim_more (i)), definition_unit (0),
        gatetype (NO) {}

~Eliminator()

CaDiCaL::Eliminator::~Eliminator

(

)

Definition at line 37 of file cadical_backward.cpp.

                         {
  while (dequeue ())
    ;
}

Here is the call graph for this function:

Member Function Documentation

dequeue()

Clause * CaDiCaL::Eliminator::dequeue

(

)

Definition at line 26 of file cadical_backward.cpp.

                             {
  if (backward.empty ())
    return 0;
  Clause *res = backward.front ();
  backward.pop ();
  CADICAL_assert (res->enqueued);
  res->enqueued = false;
  LOG (res, "backward dequeue");
  return res;
}

Here is the caller graph for this function:

enqueue()

void CaDiCaL::Eliminator::enqueue

(

Clause *

c

)

Definition at line 16 of file cadical_backward.cpp.

                                   {
  if (!internal->opts.elimbackward)
    return;
  if (c->enqueued)
    return;
  LOG (c, "backward enqueue");
  backward.push (c);
  c->enqueued = true;
}

Here is the caller graph for this function:

Member Data Documentation

backward

queue<Clause *> CaDiCaL::Eliminator::backward

Definition at line 43 of file elim.hpp.

definition_unit

unsigned CaDiCaL::Eliminator::definition_unit

Definition at line 49 of file elim.hpp.

gates

vector<Clause *> CaDiCaL::Eliminator::gates

Definition at line 48 of file elim.hpp.

gatetype

GateType CaDiCaL::Eliminator::gatetype

Definition at line 52 of file elim.hpp.

internal

Internal* CaDiCaL::Eliminator::internal

Definition at line 35 of file elim.hpp.

marked

vector<int> CaDiCaL::Eliminator::marked

Definition at line 51 of file elim.hpp.

proof_clauses

vector<proof_clause> CaDiCaL::Eliminator::proof_clauses

Definition at line 50 of file elim.hpp.

schedule

ElimSchedule CaDiCaL::Eliminator::schedule

Definition at line 36 of file elim.hpp.

---

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

• src/sat/cadical/elim.hpp
• src/sat/cadical/cadical_backward.cpp