cadical_congruence.cpp File Reference

#include "global.h"
#include "congruence.hpp"
#include "internal.hpp"
#include <algorithm>
#include <cstdint>
#include <iterator>
#include <utility>
#include <vector>

Include dependency graph for cadical_congruence.cpp:

Go to the source code of this file.

Classes
struct	CaDiCaL::compact_binary_rank
struct	CaDiCaL::compact_binary_order
struct	CaDiCaL::sort_literals_by_var_rank
struct	CaDiCaL::sort_literals_by_var_rank_except
struct	CaDiCaL::sort_literals_by_var_smaller_except
struct	CaDiCaL::sort_literals_by_var_smaller
struct	CaDiCaL::congruence_occurrences_rank
struct	CaDiCaL::congruence_occurrences_larger
struct	CaDiCaL::smaller_pair_first_rank
struct	CaDiCaL::litpair_rank
struct	CaDiCaL::litpair_smaller

Namespaces
namespace	CaDiCaL

Functions
void	CaDiCaL::update_ite_flags (Gate *g)
void	CaDiCaL::check_correct_ite_flags (const Gate *const g)
bool	CaDiCaL::gate_contains (Gate *g, int lit)
bool	CaDiCaL::parity_lits (const vector< int > &lits)
void	CaDiCaL::inc_lits (vector< int > &lits)
std::string	CaDiCaL::string_of_gate (Gate_Type t)
void	CaDiCaL::check_ite_lits_normalized (const std::vector< int > &lits)
bool	CaDiCaL::less_litpair (lit_equivalence p, lit_equivalence q)