CaDiCaL::lit_equivalence Struct Reference

#include <congruence.hpp>

Collaboration diagram for CaDiCaL::lit_equivalence:

Public Member Functions
void	check_invariant ()
	lit_equivalence (int f, Clause *f_id, int s, Clause *s_id)
	lit_equivalence (int f, int s)
	lit_equivalence ()
lit_equivalence	swap ()
lit_equivalence	negate_both ()

Public Attributes
int	first
int	second
Clause *	first_clause
Clause *	second_clause

Detailed Description

Definition at line 92 of file congruence.hpp.

Constructor & Destructor Documentation

lit_equivalence() [1/3]

CaDiCaL::lit_equivalence::lit_equivalence ( int f, Clause * f_id, int s, Clause * s_id )

inline

Definition at line 109 of file congruence.hpp.

      : first (f), second (s), first_clause (f_id), second_clause (s_id) {}

Here is the caller graph for this function:

lit_equivalence() [2/3]

CaDiCaL::lit_equivalence::lit_equivalence ( int f, int s )

inline

Definition at line 111 of file congruence.hpp.

      : first (f), second (s), first_clause (nullptr),
        second_clause (nullptr) {}

lit_equivalence() [3/3]

CaDiCaL::lit_equivalence::lit_equivalence ( )

inline

Definition at line 114 of file congruence.hpp.

      : first (0), second (0), first_clause (nullptr),
        second_clause (nullptr) {}

Member Function Documentation

check_invariant()

void CaDiCaL::lit_equivalence::check_invariant ( )

inline

Definition at line 97 of file congruence.hpp.

                          {
    CADICAL_assert (second_clause);
    CADICAL_assert (first_clause);
    CADICAL_assert (std::find (begin (*first_clause), end (*first_clause), first) !=
            end (*first_clause));
    CADICAL_assert (std::find (begin (*second_clause), end (*second_clause),
                       second) != end (*second_clause));
    CADICAL_assert (std::find (begin (*first_clause), end (*first_clause),
                       -second) != end (*first_clause));
    CADICAL_assert (std::find (begin (*second_clause), end (*second_clause),
                       -first) != end (*second_clause));
  }

Here is the caller graph for this function:

negate_both()

lit_equivalence CaDiCaL::lit_equivalence::negate_both ( )

inline

Definition at line 122 of file congruence.hpp.

                                 {
    first = -first;
    second = -second;
    std::swap (first_clause, second_clause);
    return *this;
  }

Here is the call graph for this function:

Here is the caller graph for this function:

swap()

lit_equivalence CaDiCaL::lit_equivalence::swap ( )

inline

Definition at line 117 of file congruence.hpp.

                          {
    std::swap (first, second);
    std::swap (first_clause, second_clause);
    return *this;
  }

Here is the call graph for this function:

Here is the caller graph for this function:

Member Data Documentation

first

int CaDiCaL::lit_equivalence::first

Definition at line 93 of file congruence.hpp.

first_clause

Clause* CaDiCaL::lit_equivalence::first_clause

Definition at line 95 of file congruence.hpp.

second

int CaDiCaL::lit_equivalence::second

Definition at line 94 of file congruence.hpp.

second_clause

Clause* CaDiCaL::lit_equivalence::second_clause

Definition at line 96 of file congruence.hpp.

---

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

• src/sat/cadical/congruence.hpp