congruence.hpp File Reference

#include "global.h"
#include <algorithm>
#include <array>
#include <cassert>
#include <cstddef>
#include <cstdint>
#include <queue>
#include <string>
#include <sys/types.h>
#include <unordered_set>
#include <vector>
#include "clause.hpp"
#include "inttypes.hpp"
#include "util.hpp"
#include "watch.hpp"

Include dependency graph for congruence.hpp:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	CaDiCaL::lit_implication
struct	CaDiCaL::lit_equivalence
struct	CaDiCaL::LitClausePair
struct	CaDiCaL::LitIdPair
struct	CaDiCaL::ClauseSize
struct	CaDiCaL::smaller_clause_size_rank
struct	CaDiCaL::Gate
struct	CaDiCaL::GateEqualTo
struct	CaDiCaL::CompactBinary
struct	CaDiCaL::Hash
struct	CaDiCaL::Rewrite
struct	CaDiCaL::Closure

Namespaces
namespace	CaDiCaL

Macros
#define	LD_MAX_ARITY   26
#define	MAX_ARITY   ((1 << LD_MAX_ARITY) - 1)

Typedefs
typedef int64_t	CaDiCaL::LRAT_ID
typedef std::vector< lit_implication >	CaDiCaL::lit_implications
typedef std::vector< lit_equivalence >	CaDiCaL::lit_equivalences
typedef vector< Gate * >	CaDiCaL::GOccs

Enumerations
enum class	CaDiCaL::Gate_Type { CaDiCaL::And_Gate , CaDiCaL::XOr_Gate , CaDiCaL::ITE_Gate }
enum	CaDiCaL::Special_ITE_GATE {   CaDiCaL::NORMAL = 0 , CaDiCaL::NO_PLUS_THEN = (1 << 0) , CaDiCaL::NO_NEG_THEN = (1 << 1) , CaDiCaL::NO_THEN = NO_PLUS_THEN + NO_NEG_THEN ,   CaDiCaL::NO_PLUS_ELSE = (1 << 2) , CaDiCaL::NO_NEG_ELSE = (1 << 3) , CaDiCaL::NO_ELSE = NO_PLUS_ELSE + NO_NEG_ELSE , CaDiCaL::COND_LHS = NO_NEG_THEN + NO_PLUS_ELSE ,   CaDiCaL::UCOND_LHS = NO_PLUS_THEN + NO_NEG_ELSE }

Functions
std::string	CaDiCaL::string_of_gate (Gate_Type t)
bool	CaDiCaL::ite_flags_no_then_clauses (int8_t flag)
bool	CaDiCaL::ite_flags_no_else_clauses (int8_t flag)
bool	CaDiCaL::ite_flags_neg_cond_lhs (int8_t flag)
bool	CaDiCaL::ite_flags_cond_lhs (int8_t flag)

Macro Definition Documentation

LD_MAX_ARITY

#define LD_MAX_ARITY   26

Definition at line 73 of file congruence.hpp.

MAX_ARITY

#define MAX_ARITY   ((1 << LD_MAX_ARITY) - 1)

Definition at line 74 of file congruence.hpp.