CaDiCaL Namespace Reference

Classes
struct	analyze_bumped_rank
struct	analyze_bumped_smaller
struct	analyze_trail_larger
struct	analyze_trail_negative_rank
class	Arena
struct	Averages
struct	Bin
struct	block_more_occs_size
class	Blocker
class	Checker
struct	CheckerClause
struct	CheckerWatch
struct	Clause
struct	clause_covered_or_smaller
struct	clause_lit_less_than
struct	clause_smaller_size
struct	ClauseCopier
class	ClauseCounter
class	ClauseIterator
struct	ClauseSize
class	ClauseWriter
struct	Closure
struct	compact_binary_order
struct	compact_binary_rank
struct	CompactBinary
struct	Config
struct	congruence_occurrences_larger
struct	congruence_occurrences_rank
struct	Coveror
struct	CubesWithStatus
struct	DeferDeleteArray
struct	DeferDeletePtr
struct	definition_extractor
struct	Delay
struct	DFS
class	DratTracer
struct	elim_more
struct	Eliminator
struct	EMA
struct	External
class	ExternalPropagator
struct	factor_occs_size
struct	Factoring
class	File
class	FileTracer
class	FixedAssignmentListener
struct	Flags
class	Format
class	FratTracer
struct	Gate
struct	GateEqualTo
class	Handler
struct	Hash
struct	HashId
class	heap
struct	IdrupClause
class	IdrupTracer
struct	Inc
class	Instantiator
struct	Internal
struct	InternalTracer
struct	Last
class	Learner
struct	less_conditioned
struct	Level
struct	LidrupClause
class	LidrupTracer
struct	Limit
struct	Link
struct	lit_equivalence
struct	lit_implication
struct	lit_smaller
struct	LitClausePair
struct	literal_occ
struct	LitIdPair
struct	litpair_rank
struct	litpair_smaller
class	LratChecker
struct	LratCheckerClause
class	LratTracer
struct	Mapper
struct	minimize_trail_level_positive_rank
struct	minimize_trail_level_smaller
struct	minimize_trail_positive_rank
struct	minimize_trail_smaller
struct	NameVal
struct	Option
class	Options
class	Parser
struct	Phases
struct	pointer_rank
struct	probe_negated_noccs_rank
class	Proof
struct	proof_clause
struct	Queue
struct	Quotient
class	Random
class	Range
struct	rank_sweep_candidate
struct	reduce_less_useful
class	Reluctant
struct	Rewrite
class	Sange
struct	score_smaller
struct	shrink_trail_larger
struct	shrink_trail_negative_rank
class	Signal
struct	smaller_clause_size_rank
struct	smaller_pair_first_rank
class	Solver
struct	sort_assumptions_positive_rank
struct	sort_assumptions_smaller
struct	sort_literals_by_var_rank
struct	sort_literals_by_var_rank_except
struct	sort_literals_by_var_smaller
struct	sort_literals_by_var_smaller_except
struct	Stats
class	StatTracer
struct	subsume_less_noccs
struct	sweep_binary
struct	sweep_blocked_clause
struct	sweep_candidate
struct	sweep_proof_clause
struct	Sweeper
class	Terminal
class	Terminator
class	Testing
class	Tracer
struct	Var
class	VeripbTracer
struct	Vivifier
struct	vivify_better_watch
struct	vivify_clause_later
struct	vivify_flush_smaller
struct	vivify_inversesize_rank
struct	vivify_inversesize_smaller
struct	vivify_more_noccs
struct	vivify_more_noccs_kissat
struct	vivify_ref
struct	vivify_refcount_rank
struct	vivify_refcount_smaller
struct	Walker
struct	Watch
struct	WitnessCopier
class	WitnessIterator
struct	WitnessWriter
struct	Wrapper

Typedefs
typedef vector< Bin >	Bins
typedef heap< block_more_occs_size >	BlockSchedule
typedef vector< CheckerWatch >	CheckerWatcher
typedef int *	literal_iterator
typedef const int *	const_literal_iterator
typedef int64_t	LRAT_ID
typedef std::vector< lit_implication >	lit_implications
typedef std::vector< lit_equivalence >	lit_equivalences
typedef vector< Gate * >	GOccs
typedef heap< elim_more >	ElimSchedule
typedef heap< factor_occs_size >	FactorSchedule
typedef vector< Clause * >	Occs
typedef Occs::iterator	occs_iterator
typedef Occs::const_iterator	const_occs_iterator
typedef std::vector< Link >	Links
typedef heap< score_smaller >	ScoreSchedule
typedef vector< Watch >	Watches
typedef Watches::iterator	watch_iterator
typedef Watches::const_iterator	const_watch_iterator

Enumerations
enum	Status { SATISFIABLE = 10 , UNSATISFIABLE = 20 , UNKNOWN = 0 }
enum	State {   INITIALIZING = 1 , CONFIGURING = 2 , STEADY = 4 , ADDING = 8 ,   SOLVING = 16 , SATISFIED = 32 , UNSATISFIED = 64 , DELETING = 128 ,   INCONCLUSIVE = 256 , READY = CONFIGURING | STEADY | SATISFIED | UNSATISFIED | INCONCLUSIVE , VALID = READY | ADDING , INVALID = INITIALIZING | DELETING }
enum class	Gate_Type { And_Gate , XOr_Gate , ITE_Gate }
enum	Special_ITE_GATE {   NORMAL = 0 , NO_PLUS_THEN = (1 << 0) , NO_NEG_THEN = (1 << 1) , NO_THEN = NO_PLUS_THEN + NO_NEG_THEN ,   NO_PLUS_ELSE = (1 << 2) , NO_NEG_ELSE = (1 << 3) , NO_ELSE = NO_PLUS_ELSE + NO_NEG_ELSE , COND_LHS = NO_NEG_THEN + NO_PLUS_ELSE ,   UCOND_LHS = NO_PLUS_THEN + NO_NEG_ELSE }
enum	GateType {   NO = 0 , EQUI = 1 , AND = 2 , ITE = 3 ,   XOR = 4 , DEF = 5 }
enum	ConclusionType { CONFLICT = 1 , ASSUMPTIONS = 2 , CONSTRAINT = 4 }
enum class	Vivify_Mode { TIER1 , TIER2 , TIER3 , IRREDUNDANT }

Functions
void	shrink_bins (Bins &bs)
void	erase_bins (Bins &bs)
void	update_ite_flags (Gate *g)
void	check_correct_ite_flags (const Gate *const g)
bool	gate_contains (Gate *g, int lit)
bool	parity_lits (const vector< int > &lits)
void	inc_lits (vector< int > &lits)
std::string	string_of_gate (Gate_Type t)
void	check_ite_lits_normalized (const std::vector< int > &lits)
bool	less_litpair (lit_equivalence p, lit_equivalence q)
bool	non_tautological_cube (std::vector< int > cube)
void	fatal_message_start ()
void	fatal_message_end ()
void	fatal (const char *fmt,...)
double	absolute_real_time ()
double	absolute_process_time ()
uint64_t	maximum_resident_set_size ()
uint64_t	current_resident_set_size ()
bool	parse_int_str (const char *val_str, int &val)
bool	has_suffix (const char *str, const char *suffix)
bool	has_prefix (const char *str, const char *prefix)
bool	is_color_option (const char *arg)
bool	is_no_color_option (const char *arg)
uint64_t	hash_string (const char *str)
const char *	version ()
const char *	copyright ()
const char *	authors ()
const char *	affiliations ()
const char *	signature ()
const char *	identifier ()
const char *	compiler ()
const char *	date ()
const char *	flags ()
vivify_ref	create_ref (Internal *internal, Clause *c)
std::vector< vivify_ref > &	current_refs_schedule (Vivifier &vivifier)
std::vector< Clause * > &	current_schedule (Vivifier &vivifier)
void	set_vivifier_mode (Vivifier &vivifier, Vivify_Mode tier)
bool	ite_flags_no_then_clauses (int8_t flag)
bool	ite_flags_no_else_clauses (int8_t flag)
bool	ite_flags_neg_cond_lhs (int8_t flag)
bool	ite_flags_cond_lhs (int8_t flag)
void	shrink_occs (Occs &os)
void	erase_occs (Occs &os)
void	remove_occs (Occs &os, Clause *c)
template<class I, class Rank>
void	rsort (I first, I last, Rank rank)
double	relative (double a, double b)
double	percent (double a, double b)
int	sign (int lit)
unsigned	bign (int lit)
bool	is_power_of_two (unsigned n)
bool	contained (int64_t c, int64_t l, int64_t u)
bool	aligned (size_t n, size_t alignment)
size_t	align (size_t n, size_t alignment)
bool	parity (unsigned a)
template<class T>
void	erase_vector (std::vector< T > &v)
template<class T>
void	shrink_vector (std::vector< T > &v)
template<class T>
void	clear_n (T *base, size_t n)
void	remove_watch (Watches &ws, Clause *clause)
void	update_watch_size (Watches &ws, int blit, Clause *conflict)

Variables
Terminal	tout (stdout)
Terminal	terr (stderr)
const unsigned	invalid_heap_position = UINT_MAX

Typedef Documentation

Bins

typedef vector<Bin> CaDiCaL::Bins

Definition at line 19 of file bins.hpp.

BlockSchedule

typedef heap<block_more_occs_size> CaDiCaL::BlockSchedule

Definition at line 20 of file block.hpp.

CheckerWatcher

typedef vector<CheckerWatch> CaDiCaL::CheckerWatcher

Definition at line 50 of file checker.hpp.

const_literal_iterator

typedef const int* CaDiCaL::const_literal_iterator

Definition at line 18 of file clause.hpp.

const_occs_iterator

typedef Occs::const_iterator CaDiCaL::const_occs_iterator

Definition at line 36 of file occs.hpp.

const_watch_iterator

typedef Watches::const_iterator CaDiCaL::const_watch_iterator

Definition at line 48 of file watch.hpp.

ElimSchedule

typedef heap<elim_more> CaDiCaL::ElimSchedule

Definition at line 20 of file elim.hpp.

FactorSchedule

typedef heap<factor_occs_size> CaDiCaL::FactorSchedule

Definition at line 33 of file factor.hpp.

GOccs

typedef vector<Gate *> CaDiCaL::GOccs

Definition at line 264 of file congruence.hpp.

Links

typedef std::vector<Link> CaDiCaL::Links

Definition at line 21 of file queue.hpp.

lit_equivalences

typedef std::vector<lit_equivalence> CaDiCaL::lit_equivalences

Definition at line 131 of file congruence.hpp.

lit_implications

typedef std::vector<lit_implication> CaDiCaL::lit_implications

Definition at line 130 of file congruence.hpp.

literal_iterator

typedef int* CaDiCaL::literal_iterator

Definition at line 17 of file clause.hpp.

LRAT_ID

typedef int64_t CaDiCaL::LRAT_ID

Definition at line 26 of file congruence.hpp.

Occs

typedef vector<Clause *> CaDiCaL::Occs

Definition at line 18 of file occs.hpp.

occs_iterator

typedef Occs::iterator CaDiCaL::occs_iterator

Definition at line 35 of file occs.hpp.

ScoreSchedule

typedef heap<score_smaller> CaDiCaL::ScoreSchedule

Definition at line 16 of file score.hpp.

watch_iterator

typedef Watches::iterator CaDiCaL::watch_iterator

Definition at line 47 of file watch.hpp.

Watches

typedef vector<Watch> CaDiCaL::Watches

Definition at line 45 of file watch.hpp.

Enumeration Type Documentation

ConclusionType

enum CaDiCaL::ConclusionType

Enumerator
CONFLICT
ASSUMPTIONS
CONSTRAINT

Definition at line 15 of file tracer.hpp.

{ CONFLICT = 1, ASSUMPTIONS = 2, CONSTRAINT = 4 };

Gate_Type

enum class CaDiCaL::Gate_Type

strong

Enumerator
And_Gate
XOr_Gate
ITE_Gate

Definition at line 76 of file congruence.hpp.

{ And_Gate, XOr_Gate, ITE_Gate };

GateType

enum CaDiCaL::GateType

Enumerator
NO
EQUI
AND
ITE
XOR
DEF

Definition at line 31 of file elim.hpp.

{ NO = 0, EQUI = 1, AND = 2, ITE = 3, XOR = 4, DEF = 5 };

Special_ITE_GATE

enum CaDiCaL::Special_ITE_GATE

Enumerator
NORMAL
NO_PLUS_THEN
NO_NEG_THEN
NO_THEN
NO_PLUS_ELSE
NO_NEG_ELSE
NO_ELSE
COND_LHS
UCOND_LHS

Definition at line 176 of file congruence.hpp.

                      {
  NORMAL = 0,
  NO_PLUS_THEN = (1 << 0),
  NO_NEG_THEN = (1 << 1),
  NO_THEN = NO_PLUS_THEN + NO_NEG_THEN,
  NO_PLUS_ELSE = (1 << 2),
  NO_NEG_ELSE = (1 << 3),
  NO_ELSE = NO_PLUS_ELSE + NO_NEG_ELSE,
  COND_LHS = NO_NEG_THEN + NO_PLUS_ELSE,
  UCOND_LHS = NO_PLUS_THEN + NO_NEG_ELSE,
};

State

enum CaDiCaL::State

Enumerator
INITIALIZING
CONFIGURING
STEADY
ADDING
SOLVING
SATISFIED
UNSATISFIED
DELETING
INCONCLUSIVE
READY
VALID
INVALID

Definition at line 186 of file cadical.hpp.

           {
  INITIALIZING = 1,   // during initialization (invalid)
  CONFIGURING = 2,    // configure options (with 'set')
  STEADY = 4,         // ready to call 'solve'
  ADDING = 8,         // adding clause literals (zero missing)
  SOLVING = 16,       // while solving (within 'solve')
  SATISFIED = 32,     // satisfiable allows 'val'
  UNSATISFIED = 64,   // unsatisfiable allows 'failed'
  DELETING = 128,     // during and after deletion (invalid)
  INCONCLUSIVE = 256, // unknown allows 'implied'
 
  // These combined states are used to check contracts.
 
  READY = CONFIGURING | STEADY | SATISFIED | UNSATISFIED | INCONCLUSIVE,
  VALID = READY | ADDING,
  INVALID = INITIALIZING | DELETING
};

Status

enum CaDiCaL::Status

Enumerator
SATISFIABLE
UNSATISFIABLE
UNKNOWN

Definition at line 28 of file cadical.hpp.

            {
  SATISFIABLE = 10,
  UNSATISFIABLE = 20,
  UNKNOWN = 0,
};

Vivify_Mode

enum class CaDiCaL::Vivify_Mode

strong

Enumerator
TIER1
TIER2
TIER3
IRREDUNDANT

Definition at line 18 of file vivify.hpp.

{ TIER1, TIER2, TIER3, IRREDUNDANT };

Function Documentation

absolute_process_time()

double CaDiCaL::absolute_process_time

(

)

Definition at line 89 of file cadical_resources.cpp.

                                {
  double res;
  struct rusage u;
  if (getrusage (RUSAGE_SELF, &u))
    return 0;
  res = u.ru_utime.tv_sec + 1e-6 * u.ru_utime.tv_usec;  // user time
  res += u.ru_stime.tv_sec + 1e-6 * u.ru_stime.tv_usec; // + system time
  return res;
}

Here is the caller graph for this function:

absolute_real_time()

double CaDiCaL::absolute_real_time

(

)

Definition at line 78 of file cadical_resources.cpp.

                             {
  struct timeval tv;
  if (gettimeofday (&tv, 0))
    return 0;
  return 1e-6 * tv.tv_usec + tv.tv_sec;
}

Here is the caller graph for this function:

affiliations()

const char * CaDiCaL::affiliations

(

)

Definition at line 104 of file cadical_version.cpp.

{ return AFFILIATIONS; }

align()

size_t CaDiCaL::align ( size_t n, size_t alignment )

inline

Definition at line 59 of file util.hpp.

                                                 {
  size_t res = n;
  CADICAL_assert (is_power_of_two (alignment));
  const size_t mask = alignment - 1;
  if (res & mask)
    res = (res | mask) + 1;
  CADICAL_assert (aligned (res, alignment));
  return res;
}

Here is the call graph for this function:

Here is the caller graph for this function:

aligned()

bool CaDiCaL::aligned ( size_t n, size_t alignment )

inline

Definition at line 53 of file util.hpp.

                                                 {
  CADICAL_assert (is_power_of_two (alignment));
  const size_t mask = alignment - 1;
  return !(n & mask);
}

Here is the call graph for this function:

Here is the caller graph for this function:

authors()

const char * CaDiCaL::authors

(

)

Definition at line 103 of file cadical_version.cpp.

{ return AUTHORS; }

bign()

unsigned CaDiCaL::bign ( int lit )

inline

Definition at line 23 of file util.hpp.

{ return 1 + (lit < 0); }

Here is the caller graph for this function:

check_correct_ite_flags()

void CaDiCaL::check_correct_ite_flags

(

const Gate *const

g

)

Definition at line 60 of file cadical_congruence.cpp.

                                                   {
#ifndef CADICAL_NDEBUG
  const int8_t f = g->degenerated_ite;
  const int lhs = g->lhs;
  const int cond = g->rhs [0];
  const int then_lit = g->rhs[1];
  const int else_lit = g->rhs[2];
  CADICAL_assert (g->pos_lhs_ids.size () == 4);
  if (g->pos_lhs_ids[0].clause == nullptr)
    CADICAL_assert ((f & Special_ITE_GATE::NO_PLUS_THEN));
  if (g->pos_lhs_ids[1].clause == nullptr)
    CADICAL_assert (f & Special_ITE_GATE::NO_NEG_THEN);
  if (g->pos_lhs_ids[2].clause == nullptr)
    CADICAL_assert (f & Special_ITE_GATE::NO_PLUS_ELSE);
  if (g->pos_lhs_ids[3].clause == nullptr)
    CADICAL_assert (f & Special_ITE_GATE::NO_NEG_ELSE);
  if (lhs == cond) {
    CADICAL_assert (f & Special_ITE_GATE::NO_NEG_THEN);
    CADICAL_assert (f & Special_ITE_GATE::NO_PLUS_ELSE);
  }
  if (lhs == -cond) {
    CADICAL_assert (f & Special_ITE_GATE::NO_PLUS_THEN);
    CADICAL_assert (f & Special_ITE_GATE::NO_NEG_ELSE);
  }
  if (lhs == then_lit) {
    CADICAL_assert (f & Special_ITE_GATE::NO_PLUS_THEN);
    CADICAL_assert (f & Special_ITE_GATE::NO_NEG_THEN);
  }
  if (lhs == else_lit) {
    CADICAL_assert (f & Special_ITE_GATE::NO_PLUS_ELSE);
    CADICAL_assert (f & Special_ITE_GATE::NO_NEG_ELSE);
  }
  CADICAL_assert (lhs != -then_lit);
  CADICAL_assert (lhs != -else_lit);
  CADICAL_assert (cond != then_lit);
  CADICAL_assert (cond != else_lit);
  CADICAL_assert (cond != -then_lit);
  CADICAL_assert (cond != -else_lit);
#else
  (void)g;
#endif
}

Here is the caller graph for this function:

check_ite_lits_normalized()

void CaDiCaL::check_ite_lits_normalized

(

const std::vector< int > &

lits

)

Definition at line 6867 of file cadical_congruence.cpp.

                                                            {
  CADICAL_assert (lits[0] > 0);
  CADICAL_assert (lits[1] > 0);
  CADICAL_assert (lits[0] != lits[1]);
  CADICAL_assert (lits[0] != lits[2]);
  CADICAL_assert (lits[1] != lits[2]);
  CADICAL_assert (lits[0] != -lits[1]);
  CADICAL_assert (lits[0] != -lits[2]);
  CADICAL_assert (lits[1] != -lits[2]);
#ifdef CADICAL_NDEBUG
  (void) lits;
#endif
}

clear_n()

template<class T>

void CaDiCaL::clear_n ( T * base, size_t n )

inline

Definition at line 149 of file util.hpp.

                                                           {
  memset (base, 0, sizeof (T) * n);
}

Here is the call graph for this function:

Here is the caller graph for this function:

compiler()

const char * CaDiCaL::compiler

(

)

Definition at line 107 of file cadical_version.cpp.

{ return COMPILER; }

Here is the caller graph for this function:

contained()

bool CaDiCaL::contained ( int64_t c, int64_t l, int64_t u )

inline

Definition at line 49 of file util.hpp.

                                                        {
  return l <= c && c <= u;
}

Here is the caller graph for this function:

copyright()

const char * CaDiCaL::copyright

(

)

Definition at line 102 of file cadical_version.cpp.

{ return COPYRIGHT; }

create_ref()

vivify_ref CaDiCaL::create_ref	(	Internal *	internal,
		Clause *	c )

Definition at line 1328 of file cadical_vivify.cpp.

                                                      {
  LOG (c, "creating vivify_refs of clause");
  vivify_ref ref;
  ref.clause = c;
  ref.size = c->size;
  for (int i = 0; i < COUNTREF_COUNTS; ++i)
    ref.count[i] = 0;
  ref.vivify = c->vivify;
  int lits[COUNTREF_COUNTS] = {0};
  for (int i = 0; i != std::min (COUNTREF_COUNTS, c->size); ++i) {
    int best = 0;
    unsigned best_count = 0;
    for (auto lit : *c) {
      LOG ("to find best number of occurrences for literal %d, looking at "
           "literal %d",
           i, lit);
      for (int j = 0; j != i; ++j) {
        LOG ("comparing %d with literal %d", lit, lits[j]);
        if (lits[j] == lit)
          goto CONTINUE_WITH_NEXT_LITERAL;
      }
      {
        const int64_t lit_count = internal->noccs (lit);
        CADICAL_assert (lit_count);
        LOG ("checking literal %d with %zd occurrences", lit, lit_count);
        if (lit_count <= best_count)
          continue;
        best_count = lit_count;
        best = lit;
      }
    CONTINUE_WITH_NEXT_LITERAL:;
    }
    CADICAL_assert (best);
    CADICAL_assert (best_count);
    CADICAL_assert (best_count < UINT32_MAX);
    ref.count[i] =
        ((uint64_t) best_count << 32) + (uint64_t) internal->vlit (best);
    LOG ("final count at position %d is %d - %d: %lu", i, best, best_count,
         ref.count[i]);
    lits[i] = best;
  }
  return ref;
}

Here is the call graph for this function:

Here is the caller graph for this function:

current_refs_schedule()

std::vector< vivify_ref > & CaDiCaL::current_refs_schedule ( Vivifier & vivifier )

inline

Definition at line 1489 of file cadical_vivify.cpp.

                                                                         {
  switch (vivifier.tier) {
  case Vivify_Mode::TIER1:
    return vivifier.refs_schedule_tier1;
    break;
  case Vivify_Mode::TIER2:
    return vivifier.refs_schedule_tier2;
    break;
  case Vivify_Mode::TIER3:
    return vivifier.refs_schedule_tier3;
    break;
  default:
    return vivifier.refs_schedule_irred;
    break;
  }
#ifdef WIN32
  __assume(false);
#else
  __builtin_unreachable ();
#endif
}

Here is the caller graph for this function:

current_resident_set_size()

uint64_t CaDiCaL::current_resident_set_size

(

)

Definition at line 147 of file cadical_resources.cpp.

                                      {
  char path[64];
  snprintf (path, sizeof path, "/proc/%" PRId64 "/statm",
            (int64_t) getpid ());
  FILE *file = fopen (path, "r");
  if (!file)
    return 0;
  uint64_t dummy, rss;
  int scanned = fscanf (file, "%" PRIu64 " %" PRIu64 "", &dummy, &rss);
  fclose (file);
  return scanned == 2 ? rss * sysconf (_SC_PAGESIZE) : 0;
}

current_schedule()

std::vector< Clause * > & CaDiCaL::current_schedule ( Vivifier & vivifier )

inline

Definition at line 1511 of file cadical_vivify.cpp.

                                                                  {
  switch (vivifier.tier) {
  case Vivify_Mode::TIER1:
    return vivifier.schedule_tier1;
    break;
  case Vivify_Mode::TIER2:
    return vivifier.schedule_tier2;
    break;
  case Vivify_Mode::TIER3:
    return vivifier.schedule_tier3;
    break;
  default:
    return vivifier.schedule_irred;
    break;
  }
#ifdef WIN32
  __assume(false);
#else
  __builtin_unreachable ();
#endif
}

Here is the caller graph for this function:

date()

const char * CaDiCaL::date

(

)

Definition at line 108 of file cadical_version.cpp.

{ return DATE; }

Here is the caller graph for this function:

erase_bins()

void CaDiCaL::erase_bins ( Bins & bs )

inline

Definition at line 22 of file bins.hpp.

{ erase_vector (bs); }

Here is the call graph for this function:

erase_occs()

void CaDiCaL::erase_occs ( Occs & os )

inline

Definition at line 21 of file occs.hpp.

{ erase_vector (os); }

Here is the call graph for this function:

Here is the caller graph for this function:

erase_vector()

template<class T>

void CaDiCaL::erase_vector

(

std::vector< T > &

v

)

Definition at line 90 of file util.hpp.

                                                       {
  if (v.capacity ()) {
    std::vector<T> ().swap (v);
  }
  CADICAL_assert (!v.capacity ()); // not guaranteed though
}

Here is the caller graph for this function:

fatal()

void CaDiCaL::fatal	(	const char *	fmt,
			... )

Definition at line 206 of file cadical_message.cpp.

                                  {
  fatal_message_start ();
  va_list ap;
  va_start (ap, fmt);
  vfprintf (stderr, fmt, ap);
  va_end (ap);
  fatal_message_end ();
  abort ();
}

Here is the call graph for this function:

fatal_message_end()

void CaDiCaL::fatal_message_end

(

)

Definition at line 200 of file cadical_message.cpp.

                          {
  fputc ('\n', stderr);
  fflush (stderr);
  abort ();
}

Here is the call graph for this function:

Here is the caller graph for this function:

fatal_message_start()

void CaDiCaL::fatal_message_start

(

)

Definition at line 190 of file cadical_message.cpp.

                            {
  fflush (stdout);
  terr.bold ();
  fputs ("cadical: ", stderr);
  terr.red (1);
  fputs ("fatal error:", stderr);
  terr.normal ();
  fputc (' ', stderr);
}

Here is the caller graph for this function:

flags()

const char * CaDiCaL::flags

(

)

Definition at line 109 of file cadical_version.cpp.

{ return FLAGS; }

gate_contains()

bool CaDiCaL::gate_contains	(	Gate *	g,
		int	lit )

Definition at line 127 of file cadical_congruence.cpp.

                                      {
  return find (begin (g->rhs), end (g->rhs), lit) != end (g->rhs);
}

Here is the caller graph for this function:

has_prefix()

bool CaDiCaL::has_prefix	(	const char *	str,
		const char *	prefix )

Definition at line 82 of file cadical_util.cpp.

                                                      {
  for (const char *p = str, *q = prefix; *q; q++, p++)
    if (*q != *p)
      return false;
  return true;
}

has_suffix()

bool CaDiCaL::has_suffix	(	const char *	str,
		const char *	suffix )

Definition at line 77 of file cadical_util.cpp.

                                                      {
  size_t k = strlen (str), l = strlen (suffix);
  return k > l && !strcmp (str + k - l, suffix);
}

Here is the call graph for this function:

Here is the caller graph for this function:

hash_string()

uint64_t CaDiCaL::hash_string

(

const char *

str

)

Definition at line 119 of file cadical_util.cpp.

                                       {
  const unsigned size = sizeof primes / sizeof *primes;
  uint64_t res = 0;
  unsigned char ch;
  unsigned i = 0;
  for (const char *p = str; (ch = *p); p++) {
    res += ch;
    res *= primes[i++];
    if (i == size)
      i = 0;
  }
  return res;
}

identifier()

const char * CaDiCaL::identifier

(

)

Definition at line 106 of file cadical_version.cpp.

{ return IDENTIFIER; }

Here is the caller graph for this function:

inc_lits()

void CaDiCaL::inc_lits

(

vector< int > &

lits

)

Definition at line 3407 of file cadical_congruence.cpp.

                                  {
  bool carry = true;
  for (size_t i = 0; i < lits.size () && carry; ++i) {
    int lit = lits[i];
    carry = (lit < 0);
    lits[i] = -lit;
  }
}

Here is the caller graph for this function:

is_color_option()

bool CaDiCaL::is_color_option

(

const char *

arg

)

Definition at line 91 of file cadical_util.cpp.

                                       {
  return !strcmp (arg, "--color") || !strcmp (arg, "--colors") ||
         !strcmp (arg, "--colour") || !strcmp (arg, "--colours") ||
         !strcmp (arg, "--color=1") || !strcmp (arg, "--colors=1") ||
         !strcmp (arg, "--colour=1") || !strcmp (arg, "--colours=1") ||
         !strcmp (arg, "--color=true") || !strcmp (arg, "--colors=true") ||
         !strcmp (arg, "--colour=true") || !strcmp (arg, "--colours=true");
}

Here is the call graph for this function:

is_no_color_option()

bool CaDiCaL::is_no_color_option

(

const char *

arg

)

Definition at line 100 of file cadical_util.cpp.

                                          {
  return !strcmp (arg, "--no-color") || !strcmp (arg, "--no-colors") ||
         !strcmp (arg, "--no-colour") || !strcmp (arg, "--no-colours") ||
         !strcmp (arg, "--color=0") || !strcmp (arg, "--colors=0") ||
         !strcmp (arg, "--colour=0") || !strcmp (arg, "--colours=0") ||
         !strcmp (arg, "--color=false") ||
         !strcmp (arg, "--colors=false") ||
         !strcmp (arg, "--colour=false") ||
         !strcmp (arg, "--colours=false");
}

Here is the call graph for this function:

is_power_of_two()

bool CaDiCaL::is_power_of_two ( unsigned n )

inline

Definition at line 47 of file util.hpp.

{ return n && !(n & (n - 1)); }

Here is the caller graph for this function:

ite_flags_cond_lhs()

bool CaDiCaL::ite_flags_cond_lhs ( int8_t flag )

inline

Definition at line 200 of file congruence.hpp.

                                             {
  return (flag & COND_LHS) == COND_LHS;
}

Here is the caller graph for this function:

ite_flags_neg_cond_lhs()

bool CaDiCaL::ite_flags_neg_cond_lhs ( int8_t flag )

inline

Definition at line 196 of file congruence.hpp.

                                                 {
  return (flag & UCOND_LHS) == UCOND_LHS;
}

Here is the caller graph for this function:

ite_flags_no_else_clauses()

bool CaDiCaL::ite_flags_no_else_clauses ( int8_t flag )

inline

Definition at line 192 of file congruence.hpp.

                                                    {
  return (flag & NO_ELSE) == NO_ELSE;
}

Here is the caller graph for this function:

ite_flags_no_then_clauses()

bool CaDiCaL::ite_flags_no_then_clauses ( int8_t flag )

inline

Definition at line 188 of file congruence.hpp.

                                                    {
  return (flag & NO_THEN) == NO_THEN;
}

Here is the caller graph for this function:

less_litpair()

bool CaDiCaL::less_litpair	(	lit_equivalence	p,
		lit_equivalence	q )

Definition at line 7054 of file cadical_congruence.cpp.

                                                         {
  const int a = p.first;
  const int b = q.first;
  if (a < b)
    return true;
  if (b > a)
    return false;
  const int c = p.second;
  const int d = q.second;
  return (c < d);
}

maximum_resident_set_size()

uint64_t CaDiCaL::maximum_resident_set_size

(

)

Definition at line 133 of file cadical_resources.cpp.

                                      {
  struct rusage u;
  if (getrusage (RUSAGE_SELF, &u))
    return 0;
  return ((uint64_t) u.ru_maxrss) << 10;
}

Here is the caller graph for this function:

non_tautological_cube()

bool CaDiCaL::non_tautological_cube

(

std::vector< int >

cube

)

Definition at line 253 of file cadical_lookahead.cpp.

                                                 {
  std::sort (begin (cube), end (cube), clause_lit_less_than ());
 
  for (size_t i = 0, j = 1; j < cube.size (); ++i, ++j)
    if (cube[i] == cube[j])
      return false;
    else if (cube[i] == -cube[j])
      return false;
    else if (cube[i] == 0)
      return false;
 
  return true;
}

Here is the caller graph for this function:

parity()

bool CaDiCaL::parity ( unsigned a )

inline

Definition at line 71 of file util.hpp.

                                {
  CADICAL_assert (sizeof a == 4);
  unsigned tmp = a;
  tmp ^= (tmp >> 16);
  tmp ^= (tmp >> 8);
  tmp ^= (tmp >> 4);
  tmp ^= (tmp >> 2);
  tmp ^= (tmp >> 1);
  return tmp & 1;
}

Here is the caller graph for this function:

parity_lits()

bool CaDiCaL::parity_lits

(

const vector< int > &

lits

)

Definition at line 3400 of file cadical_congruence.cpp.

                                           {
  unsigned res = 0;
  for (auto lit : lits)
    res ^= (lit < 0);
  return res;
}

Here is the caller graph for this function:

parse_int_str()

bool CaDiCaL::parse_int_str	(	const char *	val_str,
		int &	val )

Definition at line 11 of file cadical_util.cpp.

                                                   {
  if (!strcmp (val_str, "true"))
    val = 1;
  else if (!strcmp (val_str, "false"))
    val = 0;
  else {
    const char *p = val_str;
    int sign;
 
    if (*p == '-')
      sign = -1, p++;
    else
      sign = 1;
 
    int ch;
    if (!isdigit ((ch = *p++)))
      return false;
 
    const int64_t bound = -(int64_t) INT_MIN;
    int64_t mantissa = ch - '0';
 
    while (isdigit (ch = *p++)) {
      if (bound / 10 < mantissa)
        mantissa = bound;
      else
        mantissa *= 10;
      const int digit = ch - '0';
      if (bound - digit < mantissa)
        mantissa = bound;
      else
        mantissa += digit;
    }
 
    int exponent = 0;
    if (ch == 'e') {
      while (isdigit ((ch = *p++)))
        exponent = exponent ? 10 : ch - '0';
      if (ch)
        return false;
    } else if (ch)
      return false;
 
    CADICAL_assert (exponent <= 10);
    int64_t val64 = mantissa;
    for (int i = 0; i < exponent; i++)
      val64 *= 10;
 
    if (sign < 0) {
      val64 = -val64;
      if (val64 < INT_MIN)
        val64 = INT_MIN;
    } else {
      if (val64 > INT_MAX)
        val64 = INT_MAX;
    }
 
    CADICAL_assert (INT_MIN <= val64);
    CADICAL_assert (val64 <= INT_MAX);
 
    val = val64;
  }
  return true;
}

Here is the call graph for this function:

Here is the caller graph for this function:

percent()

double CaDiCaL::percent ( double a, double b )

inline

Definition at line 21 of file util.hpp.

{ return relative (100 * a, b); }

Here is the call graph for this function:

Here is the caller graph for this function:

relative()

double CaDiCaL::relative ( double a, double b )

inline

Definition at line 20 of file util.hpp.

{ return b ? a / b : 0; }

Here is the caller graph for this function:

remove_occs()

void CaDiCaL::remove_occs ( Occs & os, Clause * c )

inline

Definition at line 23 of file occs.hpp.

                                              {
  const auto end = os.end ();
  auto i = os.begin ();
  for (auto j = i; j != end; j++) {
    const Clause *d = *i++ = *j;
    if (c == d)
      i--;
  }
  CADICAL_assert (i + 1 == end);
  os.resize (i - os.begin ());
}

Here is the caller graph for this function:

remove_watch()

void CaDiCaL::remove_watch ( Watches & ws, Clause * clause )

inline

Definition at line 50 of file watch.hpp.

                                                       {
  const auto end = ws.end ();
  auto i = ws.begin ();
  for (auto j = i; j != end; j++) {
    const Watch &w = *i++ = *j;
    if (w.clause == clause)
      i--;
  }
  CADICAL_assert (i + 1 == end);
  ws.resize (i - ws.begin ());
}

Here is the caller graph for this function:

rsort()

template<class I, class Rank>

void CaDiCaL::rsort	(	I	first,
		I	last,
		Rank	rank )

Definition at line 45 of file radix.hpp.

                                                                       {
  typedef typename iterator_traits<I>::value_type T;
  typedef typename Rank::Type R;
 
  CADICAL_assert (first <= last);
  const size_t n = last - first;
  if (n <= 1)
    return;
 
  const size_t l = 8;        // Radix 8, thus byte-wise.
  const size_t w = (1 << l); // So many buckets.
 
  const unsigned mask = w - 1; // Fast mod 'w'.
 
// Uncomment the following define for large values of 'w' in order to keep
// the large bucket array 'count' on the heap instead of the stack.
//
// #define CADICAL_RADIX_BUCKETS_ON_THE_HEAP
//
#ifdef CADICAL_RADIX_BUCKETS_ON_THE_HEAP
  size_t *count = new size_t[w]; // Put buckets on the heap.
#else
  size_t count[w]; // Put buckets on the stack.
#endif
 
  I a = first, b = last, c = a;
  bool initialized = false;
  std::vector<T> v;
 
  R upper = 0, lower = ~upper;
  R shifted = mask;
  bool bounded = false;
 
  R masked_lower = 0, masked_upper = mask;
 
  for (size_t i = 0; i < 8 * sizeof (rank (*first));
       i += l, shifted <<= l) {
 
    if (bounded && (lower & shifted) == (upper & shifted))
      continue;
 
    memset (count + masked_lower, 0,
            (masked_upper - masked_lower + 1) * sizeof *count);
 
    const I end = c + n;
    bool sorted = true;
    R last = 0;
 
    for (I p = c; p != end; p++) {
      const auto r = rank (*p);
      if (!bounded)
        lower &= r, upper |= r;
      const auto s = r >> i;
      const auto m = s & mask;
      if (sorted && last > m)
        sorted = false;
      else
        last = m;
      count[m]++;
    }
 
    masked_lower = (lower >> i) & mask;
    masked_upper = (upper >> i) & mask;
 
    if (!bounded) {
      bounded = true;
      if ((lower & shifted) == (upper & shifted))
        continue;
    }
 
    if (sorted)
      continue;
 
    size_t pos = 0;
    for (R j = masked_lower; j <= masked_upper; j++) {
      const size_t delta = count[j];
      count[j] = pos;
      pos += delta;
    }
 
    if (!initialized) {
      CADICAL_assert (&*c == &*a); // MS VC++
      v.resize (n);
      b = v.begin ();
      initialized = true;
    }
 
    I d = (&*c == &*a) ? b : a; // MS VC++
 
    for (I p = c; p != end; p++) {
      const auto r = rank (*p);
      const auto s = r >> i;
      const auto m = s & mask;
      d[count[m]++] = *p;
    }
    c = d;
  }
 
  if (c == b) {
    for (size_t i = 0; i < n; i++)
      a[i] = b[i];
  }
 
#ifdef CADICAL_RADIX_BUCKETS_ON_THE_HEAP
  delete[] count;
#endif
 
#ifndef CADICAL_NDEBUG
  for (I p = first; p + 1 != last; p++)
    CADICAL_assert (rank (p[0]) <= rank (p[1]));
#endif
}

Here is the call graph for this function:

Here is the caller graph for this function:

set_vivifier_mode()

void CaDiCaL::set_vivifier_mode	(	Vivifier &	vivifier,
		Vivify_Mode	tier )

Definition at line 1772 of file cadical_vivify.cpp.

                                                              {
  vivifier.tier = tier;
  switch (tier) {
  case Vivify_Mode::TIER1:
    vivifier.tag = 'u';
    break;
  case Vivify_Mode::TIER2:
    vivifier.tag = 'v';
    break;
  case Vivify_Mode::TIER3:
    vivifier.tag = 'w';
    break;
  default:
    CADICAL_assert (tier == Vivify_Mode::IRREDUNDANT);
    vivifier.tag = 'x';
    break;
  }
}

Here is the caller graph for this function:

shrink_bins()

void CaDiCaL::shrink_bins ( Bins & bs )

inline

Definition at line 21 of file bins.hpp.

{ shrink_vector (bs); }

Here is the call graph for this function:

shrink_occs()

void CaDiCaL::shrink_occs ( Occs & os )

inline

Definition at line 20 of file occs.hpp.

{ shrink_vector (os); }

Here is the call graph for this function:

Here is the caller graph for this function:

shrink_vector()

template<class T>

void CaDiCaL::shrink_vector

(

std::vector< T > &

v

)

Definition at line 101 of file util.hpp.

                                                        {
  if (v.capacity () > v.size ()) {
    std::vector<T> (v).swap (v);
  }
  CADICAL_assert (v.capacity () == v.size ()); // not guaranteed though
}

Here is the caller graph for this function:

sign()

int CaDiCaL::sign ( int lit )

inline

Definition at line 22 of file util.hpp.

{ return (lit > 0) - (lit < 0); }

Here is the caller graph for this function:

signature()

const char * CaDiCaL::signature

(

)

Definition at line 105 of file cadical_version.cpp.

{ return "cadical-" VERSION SHORTIDSTR; }

Here is the caller graph for this function:

string_of_gate()

std::string CaDiCaL::string_of_gate

(

Gate_Type

t

)

Definition at line 4823 of file cadical_congruence.cpp.

                                       {
  switch (t) {
  case Gate_Type::And_Gate:
    return "And";
  case Gate_Type::XOr_Gate:
    return "XOr";
  case Gate_Type::ITE_Gate:
    return "ITE";
  default:
    return "buggy";
  }
}

update_ite_flags()

void CaDiCaL::update_ite_flags

(

Gate *

g

)

Definition at line 28 of file cadical_congruence.cpp.

                                {
  int8_t f = g->degenerated_ite;
  const int lhs = g->lhs;
  const int cond = g->rhs [0];
  const int then_lit = g->rhs[1];
  const int else_lit = g->rhs[2];
 
  if (lhs == cond) {
    f |= Special_ITE_GATE::NO_NEG_THEN;
    f |= Special_ITE_GATE::NO_PLUS_ELSE;
  }
  if (lhs == -cond) {
    f |= Special_ITE_GATE::NO_PLUS_THEN;
    f |= Special_ITE_GATE::NO_NEG_ELSE;
  }
  if (lhs == then_lit) {
    f |= Special_ITE_GATE::NO_PLUS_THEN;
    f |= Special_ITE_GATE::NO_NEG_THEN;
  }
  if (lhs == else_lit) {
    f |= Special_ITE_GATE::NO_PLUS_ELSE;
    f |= Special_ITE_GATE::NO_NEG_ELSE;
  }
  g->degenerated_ite = f;
  CADICAL_assert (lhs != -then_lit);
  CADICAL_assert (lhs != -else_lit);
  CADICAL_assert (cond != then_lit);
  CADICAL_assert (cond != else_lit);
  CADICAL_assert (cond != -then_lit);
  CADICAL_assert (cond != -else_lit);
}

Here is the caller graph for this function:

update_watch_size()

void CaDiCaL::update_watch_size ( Watches & ws, int blit, Clause * conflict )

inline

Definition at line 63 of file watch.hpp.

                                                                        {
  bool found = false;
  const int size = conflict->size;
  for (Watch &w : ws) {
    if (w.clause == conflict)
      w.size = size, w.blit = blit, found = true;
    CADICAL_assert (w.clause->garbage || w.size == 2 || w.clause->size != 2);
  }
  CADICAL_assert (found), (void) found;
}

Here is the caller graph for this function:

version()

const char * CaDiCaL::version

(

)

Definition at line 101 of file cadical_version.cpp.

{ return VERSION; }

Here is the caller graph for this function:

Variable Documentation

invalid_heap_position

const unsigned CaDiCaL::invalid_heap_position = UINT_MAX

Definition at line 26 of file heap.hpp.

terr

Terminal CaDiCaL::terr

(

stderr

)

Definition at line 98 of file terminal.hpp.

tout

Terminal CaDiCaL::tout

(

stdout

)

Definition at line 97 of file terminal.hpp.