CaDiCaL::vivify_clause_later Struct Reference

Collaboration diagram for CaDiCaL::vivify_clause_later:

Public Member Functions
	vivify_clause_later (Internal *i)
bool	operator() (Clause *a, Clause *b) const

Public Attributes
Internal *	internal

Detailed Description

Definition at line 380 of file cadical_vivify.cpp.

Constructor & Destructor Documentation

vivify_clause_later()

CaDiCaL::vivify_clause_later::vivify_clause_later ( Internal * i )

inline

Definition at line 384 of file cadical_vivify.cpp.

: internal (i) {}

Member Function Documentation

operator()()

bool CaDiCaL::vivify_clause_later::operator() ( Clause * a, Clause * b ) const

inline

Definition at line 386 of file cadical_vivify.cpp.

                                               {
 
    if (a == b)
      return false;
 
    // First focus on clauses scheduled in the last vivify round but not
    // checked yet since then.
    //
    if (!a->vivify && b->vivify)
      return true;
    if (a->vivify && !b->vivify)
      return false;
 
    // Among redundant clauses (in redundant mode) prefer small glue.
    //
    if (a->redundant) {
      CADICAL_assert (b->redundant);
      if (a->glue > b->glue)
        return true;
      if (a->glue < b->glue)
        return false;
    }
 
    // Then prefer shorter size.
    //
    if (a->size > b->size)
      return true;
    if (a->size < b->size)
      return false;
 
    // Now compare literals in the clauses lexicographically with respect to
    // the literal order 'vivify_more_noccs' assuming literals are sorted
    // decreasingly with respect to that order.
    //
    const auto eoa = a->end (), eob = b->end ();
    auto j = b->begin ();
    for (auto i = a->begin (); i != eoa && j != eob; i++, j++)
      if (*i != *j)
        return vivify_more_noccs (internal) (*j, *i);
 
    return j == eob; // Prefer shorter clauses to be vivified first.
  }

Here is the call graph for this function:

Member Data Documentation

internal

Internal* CaDiCaL::vivify_clause_later::internal

Definition at line 382 of file cadical_vivify.cpp.

---

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

• src/sat/cadical/cadical_vivify.cpp