#include <factor.hpp>

Collaboration diagram for CaDiCaL::Factoring:

[legend]

Public Member Functions
	Factoring (Internal *, int64_t)

	~Factoring ()

Public Attributes
Internal *	internal

int64_t	limit

FactorSchedule	schedule

int	initial

int	bound

vector< unsigned >	count

vector< int >	fresh

vector< int >	counted

vector< int >	nounted

vector< Clause * >	flauses

struct {

Quotient * first

Quotient * last

}	quotients

Detailed Description

Definition at line 35 of file factor.hpp.

Constructor & Destructor Documentation

◆ Factoring()

CaDiCaL::Factoring::Factoring	(	Internal *	i,
		int64_t	l )

Definition at line 117 of file cadical_factor.cpp.

    : internal (i), limit (l), schedule (i) {
  const unsigned max_var = internal->max_var;
  const unsigned max_lit = 2 * (max_var + 1);
  initial = max_var;
  bound = internal->lim.elimbound;
  enlarge_zero (count, max_lit);
  quotients.first = quotients.last = 0;
}

◆ ~Factoring()

CaDiCaL::Factoring::~Factoring ( )

Definition at line 127 of file cadical_factor.cpp.

                       {
  CADICAL_assert (counted.empty ());
  CADICAL_assert (nounted.empty ());
  CADICAL_assert (flauses.empty ());
  internal->release_quotients (*this);
  schedule.erase (); // actually not necessary
}

Member Data Documentation

◆ bound

int CaDiCaL::Factoring::bound

Definition at line 45 of file factor.hpp.

◆ count

vector<unsigned> CaDiCaL::Factoring::count

Definition at line 46 of file factor.hpp.

◆ counted

vector<int> CaDiCaL::Factoring::counted

Definition at line 48 of file factor.hpp.

◆ first

Quotient* CaDiCaL::Factoring::first

Definition at line 52 of file factor.hpp.

◆ flauses

vector<Clause *> CaDiCaL::Factoring::flauses

Definition at line 50 of file factor.hpp.

◆ fresh

vector<int> CaDiCaL::Factoring::fresh

Definition at line 47 of file factor.hpp.

◆ initial

int CaDiCaL::Factoring::initial

Definition at line 44 of file factor.hpp.

◆ internal

Internal* CaDiCaL::Factoring::internal

Definition at line 40 of file factor.hpp.

◆ last

Quotient * CaDiCaL::Factoring::last

Definition at line 52 of file factor.hpp.

◆ limit

int64_t CaDiCaL::Factoring::limit

Definition at line 41 of file factor.hpp.

◆ nounted

vector<int> CaDiCaL::Factoring::nounted

Definition at line 49 of file factor.hpp.

◆ [struct]

struct { ... } CaDiCaL::Factoring::quotients

◆ schedule

FactorSchedule CaDiCaL::Factoring::schedule

Definition at line 42 of file factor.hpp.

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

src/sat/cadical/factor.hpp
src/sat/cadical/cadical_factor.cpp

Public Member Functions

Public Attributes