CaDiCaL::Wrapper Struct Reference

Inheritance diagram for CaDiCaL::Wrapper:

Collaboration diagram for CaDiCaL::Wrapper:

Public Member Functions
bool	terminate ()
bool	learning (int size)
void	learn (int lit)
	Wrapper ()
	~Wrapper ()
Public Member Functions inherited from CaDiCaL::Learner
virtual	~Learner ()
Public Member Functions inherited from CaDiCaL::Terminator
virtual	~Terminator ()

Public Attributes
Solver *	solver
struct {
void *   state
int(*   function )(void *)
}	terminator
struct {
void *   state
int   max_length
int *   begin_clause
int *   end_clause
int *   capacity_clause
void(*   function )(void *, int *)
}	learner

Detailed Description

Definition at line 12 of file cadical_ccadical.cpp.

Constructor & Destructor Documentation

Wrapper()

CaDiCaL::Wrapper::Wrapper ( )

inline

Definition at line 55 of file cadical_ccadical.cpp.

             : solver (new Solver ()) {
    memset (&terminator, 0, sizeof terminator);
    memset (&learner, 0, sizeof learner);
  }

Here is the call graph for this function:

~Wrapper()

CaDiCaL::Wrapper::~Wrapper ( )

inline

Definition at line 60 of file cadical_ccadical.cpp.

              {
    terminator.function = 0;
    if (learner.begin_clause)
      free (learner.begin_clause);
    delete solver;
  }

Here is the call graph for this function:

Member Function Documentation

learn()

void CaDiCaL::Wrapper::learn ( int lit )

inlinevirtual

Implements CaDiCaL::Learner.

Definition at line 39 of file cadical_ccadical.cpp.

                       {
    if (learner.end_clause == learner.capacity_clause) {
      size_t count = learner.end_clause - learner.begin_clause;
      size_t size = count ? 2 * count : 1;
      learner.begin_clause =
          (int *) realloc (learner.begin_clause, size * sizeof (int));
      learner.end_clause = learner.begin_clause + count;
      learner.capacity_clause = learner.begin_clause + size;
    }
    *learner.end_clause++ = lit;
    if (lit)
      return;
    learner.function (learner.state, learner.begin_clause);
    learner.end_clause = learner.begin_clause;
  }

Here is the call graph for this function:

learning()

bool CaDiCaL::Wrapper::learning ( int size )

inlinevirtual

Implements CaDiCaL::Learner.

Definition at line 33 of file cadical_ccadical.cpp.

                           {
    if (!learner.function)
      return false;
    return size <= learner.max_length;
  }

terminate()

bool CaDiCaL::Wrapper::terminate ( )

inlinevirtual

Implements CaDiCaL::Terminator.

Definition at line 27 of file cadical_ccadical.cpp.

                    {
    if (!terminator.function)
      return false;
    return terminator.function (terminator.state);
  }

Member Data Documentation

begin_clause

int* CaDiCaL::Wrapper::begin_clause

Definition at line 23 of file cadical_ccadical.cpp.

capacity_clause

int * CaDiCaL::Wrapper::capacity_clause

Definition at line 23 of file cadical_ccadical.cpp.

end_clause

int * CaDiCaL::Wrapper::end_clause

Definition at line 23 of file cadical_ccadical.cpp.

function [1/2]

int(* CaDiCaL::Wrapper::function) (void *)

Definition at line 17 of file cadical_ccadical.cpp.

function [2/2]

void(* CaDiCaL::Wrapper::function) (void *, int *)

Definition at line 24 of file cadical_ccadical.cpp.

[struct]

struct { ... } CaDiCaL::Wrapper::learner

max_length

int CaDiCaL::Wrapper::max_length

Definition at line 22 of file cadical_ccadical.cpp.

solver

Solver* CaDiCaL::Wrapper::solver

Definition at line 14 of file cadical_ccadical.cpp.

state

void* CaDiCaL::Wrapper::state

Definition at line 16 of file cadical_ccadical.cpp.

[struct]

struct { ... } CaDiCaL::Wrapper::terminator

---

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

• src/sat/cadical/cadical_ccadical.cpp