#include "global.h"
#include "kitten.h"
#include "random.h"
#include "stack.h"
#include <assert.h>
#include <inttypes.h>
#include <limits.h>
#include <stdarg.h>
#include <stdbool.h>
#include <stdint.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>

Include dependency graph for cadical_kitten.c:

Classes
struct	kink

struct	klause

struct	statistics

struct	kimits

struct	cadical_kitten

Macros
#define	CALLOC(T, P, N)

#define	DEALLOC(P, N)

#define	ENLARGE_STACK(S)

#define	INC(NAME)

#define	ADD(NAME, DELTA)

#define	KITTEN_TICKS (cadical_kitten->statistics.cadical_kitten_ticks)

#define	INVALID UINT_MAX

#define	MAX_VARS ((1u << 31) - 1)

#define	CORE_FLAG (1u)

#define	LEARNED_FLAG (2u)

#define	KATCHES(KIT)

#define	all_klauses(C)

#define	all_original_klauses(C)

#define	all_learned_klauses(C)

#define	all_kits(KIT)

#define	BEGIN_KLAUSE(C)

#define	END_KLAUSE(C)

#define	all_literals_in_klause(KIT, C)

#define	all_antecedents(REF, C)

#define	LOG(...)

#define	ROG(...)

#define	LOGLITS(...)

#define	RESIZE1(T, P)

#define	RESIZE2(T, P)

#define	INVALID_API_USAGE(...)

#define	REQUIRE_INITIALIZED()

#define	REQUIRE_STATUS(EXPECTED)

#define	UPDATE_STATUS(STATUS)

Typedefs
typedef struct kar	kar

typedef struct kink	kink

typedef struct klause	klause

typedef struct statistics	statistics

typedef struct kimits	kimits

Functions
typedef	STACK (unsigned)

cadical_kitten *	cadical_kitten_init (void)

void	cadical_kitten_track_antecedents (cadical_kitten *cadical_kitten)

void	cadical_kitten_randomize_phases (cadical_kitten *cadical_kitten)

void	cadical_kitten_flip_phases (cadical_kitten *cadical_kitten)

void	cadical_kitten_no_ticks_limit (cadical_kitten *cadical_kitten)

uint64_t	cadical_kitten_current_ticks (cadical_kitten *cadical_kitten)

void	cadical_kitten_set_ticks_limit (cadical_kitten *cadical_kitten, uint64_t delta)

void	cadical_kitten_no_terminator (cadical_kitten *cadical_kitten)

void	cadical_kitten_set_terminator (cadical_kitten cadical_kitten, void data, int(terminator)(void ))

void	cadical_kitten_shuffle_clauses (cadical_kitten *cadical_kitten)

unsigned	cadical_new_learned_klause (cadical_kitten *cadical_kitten)

void	cadical_kitten_clear (cadical_kitten *cadical_kitten)

void	cadical_kitten_release (cadical_kitten *cadical_kitten)

void	cadical_completely_backtrack_to_root_level (cadical_kitten *cadical_kitten)

void	cadical_kitten_assume (cadical_kitten *cadical_kitten, unsigned elit)

void	cadical_kitten_assume_signed (cadical_kitten *cadical_kitten, int elit)

void	cadical_kitten_clause_with_id_and_exception (cadical_kitten cadical_kitten, unsigned id, size_t size, const unsigned elits, unsigned except)

void	citten_clause_with_id_and_exception (cadical_kitten cadical_kitten, unsigned id, size_t size, const int elits, unsigned except)

void	citten_clause_with_id_and_equivalence (cadical_kitten cadical_kitten, unsigned id, size_t size, const int elits, unsigned lit, unsigned other)

void	cadical_kitten_clause (cadical_kitten cadical_kitten, size_t size, unsigned elits)

void	citten_clause_with_id (cadical_kitten cadical_kitten, unsigned id, size_t size, int elits)

void	cadical_kitten_unit (cadical_kitten *cadical_kitten, unsigned lit)

void	cadical_kitten_binary (cadical_kitten *cadical_kitten, unsigned a, unsigned b)

int	cadical_kitten_solve (cadical_kitten *cadical_kitten)

int	cadical_kitten_status (cadical_kitten *cadical_kitten)

unsigned	cadical_kitten_compute_clausal_core (cadical_kitten cadical_kitten, uint64_t learned_ptr)

void	cadical_kitten_traverse_core_ids (cadical_kitten cadical_kitten, void state, void(traverse)(void , unsigned))

void	cadical_kitten_traverse_core_clauses (cadical_kitten cadical_kitten, void state, void(traverse)(void , bool, size_t, const unsigned *))

void	cadical_kitten_traverse_core_clauses_with_id (cadical_kitten cadical_kitten, void state, void(traverse)(void state, unsigned, bool learned, size_t, const unsigned *))

void	cadical_kitten_trace_core (cadical_kitten cadical_kitten, void state, void(trace)(void , unsigned, unsigned, bool, size_t, const unsigned , size_t, const unsigned ))

void	cadical_kitten_shrink_to_clausal_core (cadical_kitten *cadical_kitten)

signed char	cadical_kitten_signed_value (cadical_kitten *cadical_kitten, int selit)

signed char	cadical_kitten_value (cadical_kitten *cadical_kitten, unsigned elit)

signed char	cadical_kitten_fixed (cadical_kitten *cadical_kitten, unsigned elit)

signed char	cadical_kitten_fixed_signed (cadical_kitten *cadical_kitten, int elit)

bool	cadical_kitten_flip_literal (cadical_kitten *cadical_kitten, unsigned elit)

bool	cadical_kitten_flip_signed_literal (cadical_kitten *cadical_kitten, int elit)

bool	cadical_kitten_failed (cadical_kitten *cadical_kitten, unsigned elit)

void	cadical_kitten_add_prime_implicant (cadical_kitten cadical_kitten, void state, int side, void(add_implicant)(void , int, size_t, const unsigned *))

int	cadical_kitten_compute_prime_implicant (cadical_kitten cadical_kitten, void state, bool(ignore)(void , unsigned))

int	cadical_kitten_flip_and_implicant_for_signed_literal (cadical_kitten *cadical_kitten, int elit)

Variables
ABC_NAMESPACE_IMPL_START typedef signed char	value

Macro Definition Documentation

◆ ADD

#define ADD	(		NAME,
			DELTA )

Value:

  do { \
    statistics *statistics = &cadical_kitten->statistics; \
    CADICAL_assert (statistics->NAME <= UINT64_MAX - (DELTA)); \
    statistics->NAME += (DELTA); \
  } while (0)

Definition at line 69 of file cadical_kitten.c.

#define ADD(NAME, DELTA) \
  do { \
    statistics *statistics = &cadical_kitten->statistics; \
    CADICAL_assert (statistics->NAME <= UINT64_MAX - (DELTA)); \
    statistics->NAME += (DELTA); \
  } while (0)

◆ all_antecedents

#define all_antecedents	(		REF,
			C )

Value:

  unsigned REF, *REF##_PTR = antecedents (C), \
                *REF##_END = REF##_PTR + (C)->aux; \
  REF##_PTR != REF##_END && ((REF = *REF##_PTR), true); \
  ++REF##_PTR

Definition at line 266 of file cadical_kitten.c.

#define all_antecedents(REF, C) \
  unsigned REF, *REF##_PTR = antecedents (C), \
                *REF##_END = REF##_PTR + (C)->aux; \
  REF##_PTR != REF##_END && ((REF = *REF##_PTR), true); \
  ++REF##_PTR

◆ all_kits

#define all_kits ( KIT )

Value:

  size_t KIT = 0, KIT_##END = cadical_kitten->lits; \
  KIT != KIT_##END; \
  KIT++

Definition at line 251 of file cadical_kitten.c.

#define all_kits(KIT) \
  size_t KIT = 0, KIT_##END = cadical_kitten->lits; \
  KIT != KIT_##END; \
  KIT++

◆ all_klauses

#define all_klauses ( C )

Value:

  klause *C = begin_klauses (cadical_kitten), *end_##C = end_klauses (cadical_kitten); \
  (C) != end_##C; \
  (C) = next_klause (cadical_kitten, C)

Definition at line 234 of file cadical_kitten.c.

#define all_klauses(C) \
  klause *C = begin_klauses (cadical_kitten), *end_##C = end_klauses (cadical_kitten); \
  (C) != end_##C; \
  (C) = next_klause (cadical_kitten, C)

◆ all_learned_klauses

#define all_learned_klauses ( C )

Value:

  klause *C = begin_learned_klauses (cadical_kitten), \
         *end_##C = end_klauses (cadical_kitten); \
  (C) != end_##C; \
  (C) = next_klause (cadical_kitten, C)

Definition at line 245 of file cadical_kitten.c.

#define all_learned_klauses(C) \
  klause *C = begin_learned_klauses (cadical_kitten), \
         *end_##C = end_klauses (cadical_kitten); \
  (C) != end_##C; \
  (C) = next_klause (cadical_kitten, C)

◆ all_literals_in_klause

#define all_literals_in_klause	(		KIT,
			C )

Value:

  unsigned KIT, *KIT##_PTR = BEGIN_KLAUSE (C), \
                *KIT##_END = END_KLAUSE (C); \
  KIT##_PTR != KIT##_END && ((KIT = *KIT##_PTR), true); \
  ++KIT##_PTR

Definition at line 260 of file cadical_kitten.c.

#define all_literals_in_klause(KIT, C) \
  unsigned KIT, *KIT##_PTR = BEGIN_KLAUSE (C), \
                *KIT##_END = END_KLAUSE (C); \
  KIT##_PTR != KIT##_END && ((KIT = *KIT##_PTR), true); \
  ++KIT##_PTR

◆ all_original_klauses

#define all_original_klauses ( C )

Value:

  klause *C = begin_klauses (cadical_kitten), \
         *end_##C = end_original_klauses (cadical_kitten); \
  (C) != end_##C; \
  (C) = next_klause (cadical_kitten, C)

Definition at line 239 of file cadical_kitten.c.

#define all_original_klauses(C) \
  klause *C = begin_klauses (cadical_kitten), \
         *end_##C = end_original_klauses (cadical_kitten); \
  (C) != end_##C; \
  (C) = next_klause (cadical_kitten, C)

◆ BEGIN_KLAUSE

#define BEGIN_KLAUSE ( C )

Value:

(C)->lits

Definition at line 256 of file cadical_kitten.c.

◆ CALLOC

#define CALLOC	(	T,
		P,
		N )

Value:

  do { \
    (P) = (T*)cadical_kitten_calloc (N, sizeof *(P));   \
  } while (0)

Definition at line 38 of file cadical_kitten.c.

#define CALLOC(T, P, N)                          \
  do { \
    (P) = (T*)cadical_kitten_calloc (N, sizeof *(P));   \
  } while (0)

◆ CORE_FLAG

#define CORE_FLAG (1u)

Definition at line 81 of file cadical_kitten.c.

◆ DEALLOC

#define DEALLOC	(		P,
			N )

Value:

free (P)

free

VOID_HACK free()

Definition at line 42 of file cadical_kitten.c.

◆ END_KLAUSE

#define END_KLAUSE ( C )

Value:

(BEGIN_KLAUSE (C) + (C)->size)

Definition at line 258 of file cadical_kitten.c.

◆ ENLARGE_STACK

#define ENLARGE_STACK ( S )

Value:

  do { \
    CADICAL_assert (FULL_STACK (S)); \
    const size_t SIZE = SIZE_STACK (S); \
    const size_t OLD_CAPACITY = CAPACITY_STACK (S); \
    const size_t NEW_CAPACITY = OLD_CAPACITY ? 2 * OLD_CAPACITY : 1; \
    const size_t BYTES = NEW_CAPACITY * sizeof *(S).begin; \
    (S).begin = (unsigned*)realloc ((S).begin, BYTES);              \
    if (!(S).begin) \
      die ("out of memory reallocating '%zu' bytes", BYTES); \
    (S).allocated = (S).begin + NEW_CAPACITY; \
    (S).end = (S).begin + SIZE; \
  } while (0)

Definition at line 46 of file cadical_kitten.c.

#define ENLARGE_STACK(S) \
  do { \
    CADICAL_assert (FULL_STACK (S)); \
    const size_t SIZE = SIZE_STACK (S); \
    const size_t OLD_CAPACITY = CAPACITY_STACK (S); \
    const size_t NEW_CAPACITY = OLD_CAPACITY ? 2 * OLD_CAPACITY : 1; \
    const size_t BYTES = NEW_CAPACITY * sizeof *(S).begin; \
    (S).begin = (unsigned*)realloc ((S).begin, BYTES);              \
    if (!(S).begin) \
      die ("out of memory reallocating '%zu' bytes", BYTES); \
    (S).allocated = (S).begin + NEW_CAPACITY; \
    (S).end = (S).begin + SIZE; \
  } while (0)

◆ INC

#define INC ( NAME )

Value:

  do { \
    statistics *statistics = &cadical_kitten->statistics; \
    CADICAL_assert (statistics->NAME < UINT64_MAX); \
    statistics->NAME++; \
  } while (0)

Definition at line 62 of file cadical_kitten.c.

#define INC(NAME) \
  do { \
    statistics *statistics = &cadical_kitten->statistics; \
    CADICAL_assert (statistics->NAME < UINT64_MAX); \
    statistics->NAME++; \
  } while (0)

◆ INVALID

#define INVALID UINT_MAX

Definition at line 78 of file cadical_kitten.c.

◆ INVALID_API_USAGE

#define INVALID_API_USAGE ( ... )

Value:

invalid_api_usage (__func__, __VA_ARGS__)

Definition at line 579 of file cadical_kitten.c.

◆ KATCHES

#define KATCHES ( KIT )

Value:

(cadical_kitten->watches[CADICAL_assert ((KIT) < cadical_kitten->lits), (KIT)])

CADICAL_assert

#define CADICAL_assert(ignore)

Definition global.h:14

cadical_kitten::watches

katches * watches

Definition cadical_kitten.c:178

Definition at line 232 of file cadical_kitten.c.

◆ KITTEN_TICKS

#define KITTEN_TICKS (cadical_kitten->statistics.cadical_kitten_ticks)

Definition at line 76 of file cadical_kitten.c.

◆ LEARNED_FLAG

#define LEARNED_FLAG (2u)

Definition at line 82 of file cadical_kitten.c.

◆ LOG

#define LOG ( ... )

Value:

do { \

} while (0)

Definition at line 368 of file cadical_kitten.c.

#define LOG(...) \
  do { \
  } while (0)

◆ LOGLITS

#define LOGLITS ( ... )

Value:

do { \

} while (0)

Definition at line 374 of file cadical_kitten.c.

#define LOGLITS(...) \
  do { \
  } while (0)

◆ MAX_VARS

#define MAX_VARS ((1u << 31) - 1)

Definition at line 79 of file cadical_kitten.c.

◆ REQUIRE_INITIALIZED

#define REQUIRE_INITIALIZED ( )

Value:

  do { \
    if (!cadical_kitten) \
      INVALID_API_USAGE ("solver argument zero"); \
  } while (0)

Definition at line 581 of file cadical_kitten.c.

#define REQUIRE_INITIALIZED() \
  do { \
    if (!cadical_kitten) \
      INVALID_API_USAGE ("solver argument zero"); \
  } while (0)

◆ REQUIRE_STATUS

#define REQUIRE_STATUS ( EXPECTED )

Value:

  do { \
    REQUIRE_INITIALIZED (); \
    if (cadical_kitten->status != (EXPECTED)) \
      INVALID_API_USAGE ("invalid status '%s' (expected '%s')", \
                         status_to_string (cadical_kitten->status), \
                         status_to_string (EXPECTED)); \
  } while (0)

Definition at line 587 of file cadical_kitten.c.

#define REQUIRE_STATUS(EXPECTED) \
  do { \
    REQUIRE_INITIALIZED (); \
    if (cadical_kitten->status != (EXPECTED)) \
      INVALID_API_USAGE ("invalid status '%s' (expected '%s')", \
                         status_to_string (cadical_kitten->status), \
                         status_to_string (EXPECTED)); \
  } while (0)

◆ RESIZE1

#define RESIZE1	(		T,
			P )

Value:

  do { \
    void *OLD_PTR = (P); \
    CALLOC (T, (P), new_size / 2);                \
    const size_t BYTES = old_vars * sizeof *(P); \
    memcpy ((P), OLD_PTR, BYTES); \
    void *NEW_PTR = (P); \
    (P) = (T*)OLD_PTR;           \
    DEALLOC ((P), old_size / 2); \
    (P) = (T*)NEW_PTR;            \
  } while (0)

Definition at line 495 of file cadical_kitten.c.

#define RESIZE1(T, P)                            \
  do { \
    void *OLD_PTR = (P); \
    CALLOC (T, (P), new_size / 2);                \
    const size_t BYTES = old_vars * sizeof *(P); \
    memcpy ((P), OLD_PTR, BYTES); \
    void *NEW_PTR = (P); \
    (P) = (T*)OLD_PTR;           \
    DEALLOC ((P), old_size / 2); \
    (P) = (T*)NEW_PTR;            \
  } while (0)

◆ RESIZE2

#define RESIZE2	(		T,
			P )

Value:

  do { \
    void *OLD_PTR = (P); \
    CALLOC (T, (P), new_size);                    \
    const size_t BYTES = old_lits * sizeof *(P); \
    memcpy ((P), OLD_PTR, BYTES); \
    void *NEW_PTR = (P); \
    (P) = (T*)OLD_PTR;       \
    DEALLOC ((P), old_size); \
    (P) = (T*)NEW_PTR;       \
  } while (0)

Definition at line 507 of file cadical_kitten.c.

#define RESIZE2(T, P)                            \
  do { \
    void *OLD_PTR = (P); \
    CALLOC (T, (P), new_size);                    \
    const size_t BYTES = old_lits * sizeof *(P); \
    memcpy ((P), OLD_PTR, BYTES); \
    void *NEW_PTR = (P); \
    (P) = (T*)OLD_PTR;       \
    DEALLOC ((P), old_size); \
    (P) = (T*)NEW_PTR;       \
  } while (0)

◆ ROG

#define ROG ( ... )

Value:

do { \

} while (0)

Definition at line 371 of file cadical_kitten.c.

#define ROG(...) \
  do { \
  } while (0)

◆ UPDATE_STATUS

#define UPDATE_STATUS ( STATUS )

Value:

  do { \
    if (cadical_kitten->status != (STATUS)) \
      LOG ("updating status from '%s' to '%s'", \
           status_to_string (cadical_kitten->status), status_to_string (STATUS)); \
    else \
      LOG ("keeping status at '%s'", status_to_string (STATUS)); \
    cadical_kitten->status = (STATUS); \
  } while (0)

Definition at line 596 of file cadical_kitten.c.

#define UPDATE_STATUS(STATUS) \
  do { \
    if (cadical_kitten->status != (STATUS)) \
      LOG ("updating status from '%s' to '%s'", \
           status_to_string (cadical_kitten->status), status_to_string (STATUS)); \
    else \
      LOG ("keeping status at '%s'", status_to_string (STATUS)); \
    cadical_kitten->status = (STATUS); \
  } while (0)

Typedef Documentation

◆ kar

typedef struct kar kar

Definition at line 86 of file cadical_kitten.c.

◆ kimits

typedef struct kimits kimits

Definition at line 129 of file cadical_kitten.c.

◆ kink

typedef struct kink kink

Definition at line 87 of file cadical_kitten.c.

◆ klause

typedef struct klause klause

Definition at line 88 of file cadical_kitten.c.

◆ statistics

typedef struct statistics statistics

Definition at line 112 of file cadical_kitten.c.

Function Documentation

◆ cadical_completely_backtrack_to_root_level()

void cadical_completely_backtrack_to_root_level ( cadical_kitten * cadical_kitten )

Definition at line 1149 of file cadical_kitten.c.

                                                                                 {
  check_queue (cadical_kitten);
  LOG ("completely backtracking to level 0");
  value *values = cadical_kitten->values;
  unsigneds *trail = &cadical_kitten->trail;
  unsigneds *units = &cadical_kitten->units;
#ifndef CADICAL_NDEBUG
  kar *vars = cadical_kitten->vars;
#endif
  for (all_stack (unsigned, lit, *trail)) {
    CADICAL_assert (vars[lit / 2].level);
    unassign (cadical_kitten, values, lit);
  }
  CLEAR_STACK (*trail);
  for (all_stack (unsigned, ref, *units)) {
    klause *c = dereference_klause (cadical_kitten, ref);
    CADICAL_assert (c->size == 1);
    const unsigned unit = c->lits[0];
    const value value = values[unit];
    if (value <= 0)
      continue;
    unassign (cadical_kitten, values, unit);
  }
  cadical_kitten->propagated = 0;
  cadical_kitten->level = 0;
  check_queue (cadical_kitten);
}

Here is the caller graph for this function:

◆ cadical_kitten_add_prime_implicant()

void cadical_kitten_add_prime_implicant	(	cadical_kitten *	cadical_kitten,
		void *	state,
		int	side,
		void(*	add_implicant )(void , int, size_t, const unsigned ) )

Definition at line 2350 of file cadical_kitten.c.

                                                                           {
  REQUIRE_STATUS (11);
  // might be possible in some edge cases
  unsigneds *prime = &cadical_kitten->prime[side];
  unsigneds *prime2 = &cadical_kitten->prime[!side];
  CADICAL_assert (!EMPTY_STACK (*prime) || !EMPTY_STACK (*prime2));
  CLEAR_STACK (*prime2);
 
  for (all_stack (unsigned, lit, *prime)) {
    const unsigned not_lit = lit ^ 1;
    const unsigned elit = export_literal (cadical_kitten, not_lit);
    PUSH_STACK (*prime2, elit);
  }
 
  // adds a clause which will reset cadical_kitten status and backtrack
  add_implicant (state, side, SIZE_STACK (*prime2), BEGIN_STACK (*prime2));
  CLEAR_STACK (*prime);
  CLEAR_STACK (*prime2);
}

◆ cadical_kitten_assume()

void cadical_kitten_assume	(	cadical_kitten *	cadical_kitten,
		unsigned	elit )

Definition at line 1732 of file cadical_kitten.c.

                                                                           {
  REQUIRE_INITIALIZED ();
  if (cadical_kitten->status)
    reset_incremental (cadical_kitten);
  const unsigned ilit = import_literal (cadical_kitten, elit);
  LOG ("registering assumption %u", ilit);
  PUSH_STACK (cadical_kitten->assumptions, ilit);
}

Here is the caller graph for this function:

◆ cadical_kitten_assume_signed()

void cadical_kitten_assume_signed	(	cadical_kitten *	cadical_kitten,
		int	elit )

Definition at line 1741 of file cadical_kitten.c.

                                                                             {
  unsigned kelit = int2u (elit);
  cadical_kitten_assume (cadical_kitten, kelit);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ cadical_kitten_binary()

void cadical_kitten_binary	(	cadical_kitten *	cadical_kitten,
		unsigned	a,
		unsigned	b )

Definition at line 1848 of file cadical_kitten.c.

                                                                                    {
  unsigned clause[2] = {a, b};
  cadical_kitten_clause (cadical_kitten, 2, clause);
}

Here is the call graph for this function:

◆ cadical_kitten_clause()

void cadical_kitten_clause	(	cadical_kitten *	cadical_kitten,
		size_t	size,
		unsigned *	elits )

Definition at line 1834 of file cadical_kitten.c.

                                                                                          {
  cadical_kitten_clause_with_id_and_exception (cadical_kitten, INVALID, size, elits,
                                       INVALID);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ cadical_kitten_clause_with_id_and_exception()

void cadical_kitten_clause_with_id_and_exception	(	cadical_kitten *	cadical_kitten,
		unsigned	id,
		size_t	size,
		const unsigned *	elits,
		unsigned	except )

Definition at line 1746 of file cadical_kitten.c.

                                                           {
  REQUIRE_INITIALIZED ();
  if (cadical_kitten->status)
    reset_incremental (cadical_kitten);
  CADICAL_assert (EMPTY_STACK (cadical_kitten->klause));
  const unsigned *const end = elits + size;
  for (const unsigned *p = elits; p != end; p++) {
    const unsigned elit = *p;
    if (elit == except)
      continue;
    const unsigned ilit = import_literal (cadical_kitten, elit);
    CADICAL_assert (ilit < cadical_kitten->lits);
    const unsigned iidx = ilit / 2;
    if (cadical_kitten->marks[iidx])
      INVALID_API_USAGE ("variable '%u' of literal '%u' occurs twice",
                         elit / 2, elit);
    cadical_kitten->marks[iidx] = true;
    PUSH_STACK (cadical_kitten->klause, ilit);
  }
  for (unsigned *p = cadical_kitten->klause.begin; p != cadical_kitten->klause.end; p++)
    cadical_kitten->marks[*p / 2] = false;
  new_original_klause (cadical_kitten, id);
  CLEAR_STACK (cadical_kitten->klause);
}

Here is the caller graph for this function:

◆ cadical_kitten_clear()

void cadical_kitten_clear ( cadical_kitten * cadical_kitten )

Definition at line 899 of file cadical_kitten.c.

                                                           {
  LOG ("clear cadical_kitten of size %zu", cadical_kitten->size);
 
  CADICAL_assert (EMPTY_STACK (cadical_kitten->analyzed));
  CADICAL_assert (EMPTY_STACK (cadical_kitten->eclause));
  CADICAL_assert (EMPTY_STACK (cadical_kitten->resolved));
 
  CLEAR_STACK (cadical_kitten->assumptions);
  CLEAR_STACK (cadical_kitten->core);
  CLEAR_STACK (cadical_kitten->klause);
  CLEAR_STACK (cadical_kitten->klauses);
  CLEAR_STACK (cadical_kitten->trail);
  CLEAR_STACK (cadical_kitten->units);
  CLEAR_STACK (cadical_kitten->clause);
  CLEAR_STACK (cadical_kitten->prime[0]);
  CLEAR_STACK (cadical_kitten->prime[1]);
 
  for (all_kits (kit))
    CLEAR_STACK (KATCHES (kit));
 
  while (!EMPTY_STACK (cadical_kitten->export_))
    cadical_kitten->import[POP_STACK (cadical_kitten->export_)] = 0;
 
  const size_t lits = cadical_kitten->size;
  const unsigned vars = lits / 2;
 
#ifndef CADICAL_NDEBUG
  for (unsigned i = 0; i < vars; i++)
    CADICAL_assert (!cadical_kitten->marks[i]);
#endif
 
  memset (cadical_kitten->phases, 0, vars);
  memset (cadical_kitten->values, 0, lits);
  memset (cadical_kitten->failed, 0, lits);
  memset (cadical_kitten->vars, 0, vars);
 
  clear_cadical_kitten (cadical_kitten);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ cadical_kitten_compute_clausal_core()

unsigned cadical_kitten_compute_clausal_core	(	cadical_kitten *	cadical_kitten,
		uint64_t *	learned_ptr )

Definition at line 1907 of file cadical_kitten.c.

                                                             {
  REQUIRE_STATUS (20);
 
  if (!cadical_kitten->antecedents)
    INVALID_API_USAGE ("antecedents not tracked");
 
  LOG ("computing clausal core");
 
  unsigneds *resolved = &cadical_kitten->resolved;
  CADICAL_assert (EMPTY_STACK (*resolved));
 
  unsigned original = 0;
  uint64_t learned = 0;
 
  unsigned reason_ref = cadical_kitten->inconsistent;
 
  if (reason_ref == INVALID) {
    CADICAL_assert (!EMPTY_STACK (cadical_kitten->assumptions));
    reason_ref = cadical_kitten->failing;
    if (reason_ref == INVALID) {
      LOG ("assumptions mutually inconsistent");
      //goto DONE;
        if (learned_ptr)
          *learned_ptr = learned;
        
        LOG ("clausal core of %u original clauses", original);
        LOG ("clausal core of %" PRIu64 " learned clauses", learned);
        cadical_kitten->statistics.original = original;
        cadical_kitten->statistics.learned = 0;
        UPDATE_STATUS (21);
        
        return original;
    }
  }
 
  PUSH_STACK (*resolved, reason_ref);
  unsigneds *core = &cadical_kitten->core;
  CADICAL_assert (EMPTY_STACK (*core));
 
  while (!EMPTY_STACK (*resolved)) {
    const unsigned c_ref = POP_STACK (*resolved);
    if (c_ref == INVALID) {
      const unsigned d_ref = POP_STACK (*resolved);
      ROG (d_ref, "core[%zu]", SIZE_STACK (*core));
      PUSH_STACK (*core, d_ref);
      klause *d = dereference_klause (cadical_kitten, d_ref);
      CADICAL_assert (!is_core_klause (d));
      set_core_klause (d);
      if (is_learned_klause (d))
        learned++;
      else
        original++;
    } else {
      klause *c = dereference_klause (cadical_kitten, c_ref);
      if (is_core_klause (c))
        continue;
      PUSH_STACK (*resolved, c_ref);
      PUSH_STACK (*resolved, INVALID);
      ROG (c_ref, "analyzing antecedent core");
      if (!is_learned_klause (c))
        continue;
      for (all_antecedents (d_ref, c)) {
        klause *d = dereference_klause (cadical_kitten, d_ref);
        if (!is_core_klause (d))
          PUSH_STACK (*resolved, d_ref);
      }
    }
  }
 
  //DONE:
 
  if (learned_ptr)
    *learned_ptr = learned;
 
  LOG ("clausal core of %u original clauses", original);
  LOG ("clausal core of %" PRIu64 " learned clauses", learned);
  cadical_kitten->statistics.original = original;
  cadical_kitten->statistics.learned = 0;
  UPDATE_STATUS (21);
 
  return original;
}

Here is the caller graph for this function:

◆ cadical_kitten_compute_prime_implicant()

int cadical_kitten_compute_prime_implicant	(	cadical_kitten *	cadical_kitten,
		void *	state,
		bool(*	ignore )(void *, unsigned) )

Definition at line 2376 of file cadical_kitten.c.

                                                                       {
  REQUIRE_STATUS (10);
 
  value *values = cadical_kitten->values;
  kar *vars = cadical_kitten->vars;
  unsigneds unassigned;
  INIT_STACK (unassigned);
  bool limit_hit = 0;
  CADICAL_assert (EMPTY_STACK (cadical_kitten->prime[0]) && EMPTY_STACK (cadical_kitten->prime[1]));
  for (int i = 0; i < 2; i++) {
    const bool ignoring = i;
    for (all_stack (unsigned, lit, cadical_kitten->trail)) {
      if (KITTEN_TICKS >= cadical_kitten->limits.ticks) {
        LOG ("ticks limit %" PRIu64 " hit after %" PRIu64 " ticks",
             cadical_kitten->limits.ticks, KITTEN_TICKS);
        limit_hit = 1;
        break;
      }
      CADICAL_assert (values[lit] > 0);
      const unsigned idx = lit / 2;
      const unsigned ref = vars[idx].reason;
      CADICAL_assert (vars[idx].level);
      klause *c = 0;
      if (ref != INVALID)
        c = dereference_klause (cadical_kitten, ref);
      if (ref == INVALID || is_learned_klause (c) ||
          ignore (state, c->aux) == ignoring) {
        LOG ("non-prime candidate var %d", idx);
        if (prime_propagate (cadical_kitten, idx, state, ignoring, ignore)) {
          values[lit] = 0;
          values[lit ^ 1] = 0;
          PUSH_STACK (unassigned, lit);
        } else
          CADICAL_assert (values[lit] > 0);
      }
    }
    unsigneds *prime = &cadical_kitten->prime[i];
    // push on prime implicant stack.
    for (all_kits (lit)) {
      if (values[lit] > 0)
        PUSH_STACK (*prime, lit);
    }
    // reassign all literals on
    for (all_stack (unsigned, lit, unassigned)) {
      CADICAL_assert (!values[lit]);
      values[lit] = 1;
      values[lit ^ 1] = -1;
    }
    CLEAR_STACK (unassigned);
  }
  RELEASE_STACK (unassigned);
 
  if (limit_hit) {
    CLEAR_STACK (cadical_kitten->prime[0]);
    CLEAR_STACK (cadical_kitten->prime[1]);
    return -1;
  }
  // the only case when one of the prime implicants is allowed to be empty
  // is if ignore returns always true or always false.
  CADICAL_assert (!EMPTY_STACK (cadical_kitten->prime[0]) ||
          !EMPTY_STACK (cadical_kitten->prime[1]));
  UPDATE_STATUS (11);
 
  int res = SIZE_STACK (cadical_kitten->prime[0]) > SIZE_STACK (cadical_kitten->prime[1]);
  return res;
}

◆ cadical_kitten_current_ticks()

uint64_t cadical_kitten_current_ticks ( cadical_kitten * cadical_kitten )

Definition at line 686 of file cadical_kitten.c.

                                                                       {
  REQUIRE_INITIALIZED ();
  const uint64_t current = KITTEN_TICKS;
  return current;
}

Here is the caller graph for this function:

◆ cadical_kitten_failed()

bool cadical_kitten_failed	(	cadical_kitten *	cadical_kitten,
		unsigned	elit )

Definition at line 2275 of file cadical_kitten.c.

                                                                           {
  REQUIRE_STATUS (20);
  const unsigned eidx = elit / 2;
  if (eidx >= cadical_kitten->evars)
    return false;
  unsigned iidx = cadical_kitten->import[eidx];
  if (!iidx)
    return false;
  const unsigned ilit = 2 * (iidx - 1) + (elit & 1);
  return cadical_kitten->failed[ilit];
}

◆ cadical_kitten_fixed()

signed char cadical_kitten_fixed	(	cadical_kitten *	cadical_kitten,
		unsigned	elit )

Definition at line 2232 of file cadical_kitten.c.

                                                                                 {
  const unsigned eidx = elit / 2;
  if (eidx >= cadical_kitten->evars)
    return 0;
  unsigned iidx = cadical_kitten->import[eidx];
  if (!iidx)
    return 0;
  iidx--;
  const unsigned ilit = 2 * iidx + (elit & 1);
  signed char res = cadical_kitten->values[ilit];
  if (!res)
    return 0;
  kar *v = cadical_kitten->vars + iidx;
  if (v->level)
    return 0;
  return res;
}

Here is the caller graph for this function:

◆ cadical_kitten_fixed_signed()

signed char cadical_kitten_fixed_signed	(	cadical_kitten *	cadical_kitten,
		int	elit )

Definition at line 2250 of file cadical_kitten.c.

                                                                                   {
  unsigned kelit = int2u (elit);
  return cadical_kitten_fixed (cadical_kitten, kelit);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ cadical_kitten_flip_and_implicant_for_signed_literal()

int cadical_kitten_flip_and_implicant_for_signed_literal	(	cadical_kitten *	cadical_kitten,
		int	elit )

Definition at line 2595 of file cadical_kitten.c.

                                                            {
  REQUIRE_STATUS (10);
  unsigned kelit = int2u (elit);
  if (!cadical_kitten_flip_literal (cadical_kitten, kelit)) {
    return -2;
  }
  const unsigned eidx = kelit / 2;
  unsigned iidx = cadical_kitten->import[eidx];
  CADICAL_assert (iidx);
  const unsigned ilit = 2 * (iidx - 1) + (kelit & 1);
  return compute_prime_implicant_for (cadical_kitten, ilit);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ cadical_kitten_flip_literal()

bool cadical_kitten_flip_literal	(	cadical_kitten *	cadical_kitten,
		unsigned	elit )

Definition at line 2255 of file cadical_kitten.c.

                                                                                 {
  REQUIRE_STATUS (10);
  const unsigned eidx = elit / 2;
  if (eidx >= cadical_kitten->evars)
    return false;
  unsigned iidx = cadical_kitten->import[eidx];
  if (!iidx)
    return false;
  const unsigned ilit = 2 * (iidx - 1) + (elit & 1);
  if (cadical_kitten_fixed (cadical_kitten, elit))
    return false;
  return flip_literal (cadical_kitten, ilit);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ cadical_kitten_flip_phases()

void cadical_kitten_flip_phases ( cadical_kitten * cadical_kitten )

Definition at line 659 of file cadical_kitten.c.

                                                                 {
  REQUIRE_INITIALIZED ();
 
  LOG ("flipping phases");
 
  unsigned char *phases = cadical_kitten->phases;
  const unsigned vars = cadical_kitten->size / 2;
 
  unsigned i = 0;
  const unsigned rest = vars & ~7u;
 
  while (i != rest) {
    uint64_t *p = (uint64_t *) (phases + i);
    *p ^= 0x0101010101010101;
    i += 8;
  }
 
  while (i != vars)
    phases[i++] ^= 1;
}

◆ cadical_kitten_flip_signed_literal()

bool cadical_kitten_flip_signed_literal	(	cadical_kitten *	cadical_kitten,
		int	elit )

Definition at line 2269 of file cadical_kitten.c.

                                                                                   {
  REQUIRE_STATUS (10);
  unsigned kelit = int2u (elit);
  return cadical_kitten_flip_literal (cadical_kitten, kelit);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ cadical_kitten_init()

cadical_kitten * cadical_kitten_init ( void )

Definition at line 606 of file cadical_kitten.c.

                                           {
  cadical_kitten *cadical_kitten;
  CALLOC (struct cadical_kitten, cadical_kitten, 1);
  initialize_cadical_kitten (cadical_kitten);
  return cadical_kitten;
}

Here is the caller graph for this function:

◆ cadical_kitten_no_terminator()

void cadical_kitten_no_terminator ( cadical_kitten * cadical_kitten )

Definition at line 707 of file cadical_kitten.c.

                                                                   {
  REQUIRE_INITIALIZED ();
  LOG ("removing terminator");
  cadical_kitten->terminator = 0;
  cadical_kitten->terminator_data = 0;
}

◆ cadical_kitten_no_ticks_limit()

void cadical_kitten_no_ticks_limit ( cadical_kitten * cadical_kitten )

Definition at line 680 of file cadical_kitten.c.

                                                                    {
  REQUIRE_INITIALIZED ();
  LOG ("forcing no ticks limit");
  cadical_kitten->limits.ticks = UINT64_MAX;
}

◆ cadical_kitten_randomize_phases()

void cadical_kitten_randomize_phases ( cadical_kitten * cadical_kitten )

Definition at line 627 of file cadical_kitten.c.

                                                                      {
  REQUIRE_INITIALIZED ();
 
  LOG ("randomizing phases");
 
  unsigned char *phases = cadical_kitten->phases;
  const unsigned vars = cadical_kitten->size / 2;
 
  uint64_t random = kissat_next_random64 (&cadical_kitten->generator);
 
  unsigned i = 0;
  const unsigned rest = vars & ~63u;
 
  while (i != rest) {
    uint64_t *p = (uint64_t *) (phases + i);
    p[0] = (random >> 0) & 0x0101010101010101;
    p[1] = (random >> 1) & 0x0101010101010101;
    p[2] = (random >> 2) & 0x0101010101010101;
    p[3] = (random >> 3) & 0x0101010101010101;
    p[4] = (random >> 4) & 0x0101010101010101;
    p[5] = (random >> 5) & 0x0101010101010101;
    p[6] = (random >> 6) & 0x0101010101010101;
    p[7] = (random >> 7) & 0x0101010101010101;
    random = kissat_next_random64 (&cadical_kitten->generator);
    i += 64;
  }
 
  unsigned shift = 0;
  while (i != vars)
    phases[i++] = (random >> shift++) & 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ cadical_kitten_release()

void cadical_kitten_release ( cadical_kitten * cadical_kitten )

Definition at line 938 of file cadical_kitten.c.

                                                             {
  RELEASE_STACK (cadical_kitten->analyzed);
  RELEASE_STACK (cadical_kitten->assumptions);
  RELEASE_STACK (cadical_kitten->core);
  RELEASE_STACK (cadical_kitten->eclause);
  RELEASE_STACK (cadical_kitten->export_);
  RELEASE_STACK (cadical_kitten->klause);
  RELEASE_STACK (cadical_kitten->klauses);
  RELEASE_STACK (cadical_kitten->resolved);
  RELEASE_STACK (cadical_kitten->trail);
  RELEASE_STACK (cadical_kitten->units);
  RELEASE_STACK (cadical_kitten->clause);
  RELEASE_STACK (cadical_kitten->prime[0]);
  RELEASE_STACK (cadical_kitten->prime[1]);
 
  for (size_t lit = 0; lit < cadical_kitten->size; lit++)
    RELEASE_STACK (cadical_kitten->watches[lit]);
 
  const size_t lits = cadical_kitten->size;
  const unsigned vars = lits / 2;
  DEALLOC (cadical_kitten->marks, vars);
  DEALLOC (cadical_kitten->phases, vars);
  DEALLOC (cadical_kitten->values, lits);
  DEALLOC (cadical_kitten->failed, lits);
  DEALLOC (cadical_kitten->vars, vars);
  DEALLOC (cadical_kitten->links, vars);
  DEALLOC (cadical_kitten->watches, lits);
  DEALLOC (cadical_kitten->import, cadical_kitten->esize);
  (void) vars;
 
  free (cadical_kitten);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ cadical_kitten_set_terminator()

void cadical_kitten_set_terminator	(	cadical_kitten *	cadical_kitten,
		void *	data,
		int(*	terminator )(void *) )

Definition at line 714 of file cadical_kitten.c.

                                                        {
  REQUIRE_INITIALIZED ();
  LOG ("setting terminator");
  cadical_kitten->terminator = terminator;
  cadical_kitten->terminator_data = data;
}

Here is the caller graph for this function:

◆ cadical_kitten_set_ticks_limit()

void cadical_kitten_set_ticks_limit	(	cadical_kitten *	cadical_kitten,
		uint64_t	delta )

Definition at line 692 of file cadical_kitten.c.

                                                                                     {
  REQUIRE_INITIALIZED ();
  const uint64_t current = KITTEN_TICKS;
  uint64_t limit;
  if (UINT64_MAX - delta <= current) {
    LOG ("forcing unlimited ticks limit");
    limit = UINT64_MAX;
  } else {
    limit = current + delta;
    LOG ("new limit of %" PRIu64 " ticks after %" PRIu64, limit, delta);
  }
 
  cadical_kitten->limits.ticks = limit;
}

Here is the caller graph for this function:

◆ cadical_kitten_shrink_to_clausal_core()

void cadical_kitten_shrink_to_clausal_core ( cadical_kitten * cadical_kitten )

Definition at line 2133 of file cadical_kitten.c.

                                                                            {
  REQUIRE_STATUS (21);
 
  LOG ("shrinking formula to core of original clauses");
 
  CLEAR_STACK (cadical_kitten->trail);
 
  cadical_kitten->unassigned = cadical_kitten->lits / 2;
  cadical_kitten->propagated = 0;
  cadical_kitten->level = 0;
 
  update_search (cadical_kitten, cadical_kitten->queue.last);
 
  memset (cadical_kitten->values, 0, cadical_kitten->lits);
 
  for (all_kits (lit))
    CLEAR_STACK (KATCHES (lit));
 
  CADICAL_assert (cadical_kitten->inconsistent != INVALID);
  klause *inconsistent = dereference_klause (cadical_kitten, cadical_kitten->inconsistent);
  if (is_learned_klause (inconsistent) || inconsistent->size) {
    ROG (cadical_kitten->inconsistent, "resetting inconsistent");
    cadical_kitten->inconsistent = INVALID;
  } else
    ROG (cadical_kitten->inconsistent, "keeping inconsistent");
 
  CLEAR_STACK (cadical_kitten->units);
 
  klause *begin = begin_klauses (cadical_kitten), *q = begin;
  klause const *const end = end_original_klauses (cadical_kitten);
#ifdef LOGGING
  unsigned original = 0;
#endif
  for (klause *c = begin, *next; c != end; c = next) {
    next = next_klause (cadical_kitten, c);
    // CADICAL_assert (!is_learned_klause (c)); not necessarily true
    if (is_learned_klause (c))
      continue;
    if (!is_core_klause (c))
      continue;
    unset_core_klause (c);
    const unsigned dst = (unsigned *) q - (unsigned *) begin;
    const unsigned size = c->size;
    if (!size) {
      if (cadical_kitten->inconsistent != INVALID)
        cadical_kitten->inconsistent = dst;
    } else if (size == 1) {
      PUSH_STACK (cadical_kitten->units, dst);
      ROG (dst, "keeping");
    } else {
      watch_klause (cadical_kitten, c->lits[0], dst);
      watch_klause (cadical_kitten, c->lits[1], dst);
    }
    if (c == q)
      q = next;
    else {
      const size_t bytes = (char *) next - (char *) c;
      memmove (q, c, bytes);
      q = (klause *) ((char *) q + bytes);
    }
#ifdef LOGGING
    original++;
#endif
  }
  SET_END_OF_STACK (cadical_kitten->klauses, (unsigned *) q);
  cadical_kitten->end_original_ref = SIZE_STACK (cadical_kitten->klauses);
  LOG ("end of original clauses at %zu", cadical_kitten->end_original_ref);
  LOG ("%u original clauses left", original);
 
  CLEAR_STACK (cadical_kitten->core);
 
  UPDATE_STATUS (0);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ cadical_kitten_shuffle_clauses()

void cadical_kitten_shuffle_clauses ( cadical_kitten * cadical_kitten )

Definition at line 764 of file cadical_kitten.c.

                                                                     {
  REQUIRE_STATUS (0);
  shuffle_queue (cadical_kitten);
  shuffle_katches (cadical_kitten);
  shuffle_units (cadical_kitten);
}

Here is the caller graph for this function:

◆ cadical_kitten_signed_value()

signed char cadical_kitten_signed_value	(	cadical_kitten *	cadical_kitten,
		int	selit )

Definition at line 2207 of file cadical_kitten.c.

                                                                                    {
  REQUIRE_STATUS (10);
  const unsigned elit = int2u (selit);
  const unsigned eidx = elit / 2;
  if (eidx >= cadical_kitten->evars)
    return 0;
  unsigned iidx = cadical_kitten->import[eidx];
  if (!iidx)
    return 0;
  const unsigned ilit = 2 * (iidx - 1) + (elit & 1);
  return cadical_kitten->values[ilit];
}

Here is the caller graph for this function:

◆ cadical_kitten_solve()

int cadical_kitten_solve ( cadical_kitten * cadical_kitten )

Definition at line 1853 of file cadical_kitten.c.

                                                          {
  REQUIRE_INITIALIZED ();
  if (cadical_kitten->status)
    reset_incremental (cadical_kitten);
  else // if (cadical_kitten->level)
    cadical_completely_backtrack_to_root_level (cadical_kitten);
 
  LOG ("starting solving under %zu assumptions",
       SIZE_STACK (cadical_kitten->assumptions));
 
  INC (cadical_kitten_solved);
 
  int res = propagate_units (cadical_kitten);
  while (!res) {
    const unsigned conflict = propagate (cadical_kitten);
    if (cadical_kitten->terminator &&
        cadical_kitten->terminator (cadical_kitten->terminator_data)) {
      LOG ("terminator requested termination");
      res = -1;
      break;
    }
    if (conflict != INVALID) {
      if (cadical_kitten->level)
        analyze (cadical_kitten, conflict);
      else {
        inconsistent (cadical_kitten, conflict);
        res = 20;
      }
    } else
      res = decide (cadical_kitten);
  }
 
  if (res < 0)
    res = 0;
 
  if (!res && !EMPTY_STACK (cadical_kitten->assumptions))
    reset_assumptions (cadical_kitten);
 
  UPDATE_STATUS (res);
 
  if (res == 10)
    INC (cadical_kitten_sat);
  else if (res == 20)
    INC (cadical_kitten_unsat);
  else
    INC (cadical_kitten_unknown);
 
  LOG ("finished solving with result %d", res);
 
  return res;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ cadical_kitten_status()

int cadical_kitten_status ( cadical_kitten * cadical_kitten )

Definition at line 1905 of file cadical_kitten.c.

1905{ return cadical_kitten->status; }

Here is the caller graph for this function:

◆ cadical_kitten_trace_core()

void cadical_kitten_trace_core	(	cadical_kitten *	cadical_kitten,
		void *	state,
		void(*	trace )(void , unsigned, unsigned, bool, size_t, const unsigned , size_t, const unsigned *) )

Definition at line 2085 of file cadical_kitten.c.

                                                          {
  REQUIRE_STATUS (21);
 
  LOG ("tracing clausal core");
 
  unsigned traced = 0;
 
  for (all_stack (unsigned, c_ref, cadical_kitten->core)) {
    klause *c = dereference_klause (cadical_kitten, c_ref);
    CADICAL_assert (is_core_klause (c));
    const bool learned = is_learned_klause (c);
    unsigneds *eclause = &cadical_kitten->eclause;
    CADICAL_assert (EMPTY_STACK (*eclause));
    for (all_literals_in_klause (ilit, c)) {
      const unsigned elit = export_literal (cadical_kitten, ilit);
      PUSH_STACK (*eclause, elit);
    }
    const size_t size = SIZE_STACK (*eclause);
    const unsigned *elits = eclause->begin;
 
    unsigneds *resolved = &cadical_kitten->resolved;
    CADICAL_assert (EMPTY_STACK (*resolved));
    if (learned) {
      for (all_antecedents (ref, c)) {
        PUSH_STACK (*resolved, ref);
      }
    }
    const size_t rsize = SIZE_STACK (*resolved);
    const unsigned *rids = resolved->begin;
 
    unsigned cid = reference_klause (cadical_kitten, c);
    unsigned ctag = learned ? 0 : c->aux;
    ROG (cid, "tracing");
    trace (state, cid, ctag, learned, size, elits, rsize, rids);
    CLEAR_STACK (*eclause);
    CLEAR_STACK (*resolved);
    traced++;
  }
 
  LOG ("traced %u core clauses", traced);
  (void) traced;
 
  CADICAL_assert (cadical_kitten->status == 21);
}

Here is the caller graph for this function:

◆ cadical_kitten_track_antecedents()

void cadical_kitten_track_antecedents ( cadical_kitten * cadical_kitten )

Definition at line 617 of file cadical_kitten.c.

                                                                       {
  REQUIRE_STATUS (0);
 
  if (cadical_kitten->learned)
    INVALID_API_USAGE ("can not start tracking antecedents after learning");
 
  LOG ("enabling antecedents tracking");
  cadical_kitten->antecedents = true;
}

Here is the caller graph for this function:

◆ cadical_kitten_traverse_core_clauses()

void cadical_kitten_traverse_core_clauses	(	cadical_kitten *	cadical_kitten,
		void *	state,
		void(*	traverse )(void , bool, size_t, const unsigned ) )

Definition at line 2017 of file cadical_kitten.c.

                                                                        {
  REQUIRE_STATUS (21);
 
  LOG ("traversing clausal core");
 
  unsigned traversed = 0;
 
  for (all_stack (unsigned, c_ref, cadical_kitten->core)) {
    klause *c = dereference_klause (cadical_kitten, c_ref);
    CADICAL_assert (is_core_klause (c));
    const bool learned = is_learned_klause (c);
    unsigneds *eclause = &cadical_kitten->eclause;
    CADICAL_assert (EMPTY_STACK (*eclause));
    for (all_literals_in_klause (ilit, c)) {
      const unsigned elit = export_literal (cadical_kitten, ilit);
      PUSH_STACK (*eclause, elit);
    }
    const size_t size = SIZE_STACK (*eclause);
    const unsigned *elits = eclause->begin;
    ROG (reference_klause (cadical_kitten, c), "traversing");
    traverse (state, learned, size, elits);
    CLEAR_STACK (*eclause);
    traversed++;
  }
 
  LOG ("traversed %u core clauses", traversed);
  (void) traversed;
 
  CADICAL_assert (cadical_kitten->status == 21);
}

Here is the caller graph for this function:

◆ cadical_kitten_traverse_core_clauses_with_id()

void cadical_kitten_traverse_core_clauses_with_id	(	cadical_kitten *	cadical_kitten,
		void *	state,
		void(*	traverse )(void state, unsigned, bool learned, size_t, const unsigned ) )

Definition at line 2050 of file cadical_kitten.c.

                                         {
  REQUIRE_STATUS (21);
 
  LOG ("traversing clausal core");
 
  unsigned traversed = 0;
 
  for (all_stack (unsigned, c_ref, cadical_kitten->core)) {
    klause *c = dereference_klause (cadical_kitten, c_ref);
    CADICAL_assert (is_core_klause (c));
    const bool learned = is_learned_klause (c);
    unsigneds *eclause = &cadical_kitten->eclause;
    CADICAL_assert (EMPTY_STACK (*eclause));
    for (all_literals_in_klause (ilit, c)) {
      const unsigned elit = export_literal (cadical_kitten, ilit);
      PUSH_STACK (*eclause, elit);
    }
    const size_t size = SIZE_STACK (*eclause);
    const unsigned *elits = eclause->begin;
    ROG (reference_klause (cadical_kitten, c), "traversing");
    unsigned ctag = learned ? 0 : c->aux;
    traverse (state, ctag, learned, size, elits);
    CLEAR_STACK (*eclause);
    traversed++;
  }
 
  LOG ("traversed %u core clauses", traversed);
  (void) traversed;
 
  CADICAL_assert (cadical_kitten->status == 21);
}

Here is the caller graph for this function:

◆ cadical_kitten_traverse_core_ids()

void cadical_kitten_traverse_core_ids	(	cadical_kitten *	cadical_kitten,
		void *	state,
		void(*	traverse )(void *, unsigned) )

Definition at line 1991 of file cadical_kitten.c.

                                                                    {
  REQUIRE_STATUS (21);
 
  LOG ("traversing core of original clauses");
 
  unsigned traversed = 0;
 
  for (all_original_klauses (c)) {
    // only happens for 'true' incremental calls, i.e. if add happens after
    // solve
    if (is_learned_klause (c))
      continue;
    if (!is_core_klause (c))
      continue;
    ROG (reference_klause (cadical_kitten, c), "traversing");
    traverse (state, c->aux);
    traversed++;
  }
 
  LOG ("traversed %u original core clauses", traversed);
  (void) traversed;
 
  CADICAL_assert (cadical_kitten->status == 21);
}

Here is the caller graph for this function:

◆ cadical_kitten_unit()

void cadical_kitten_unit	(	cadical_kitten *	cadical_kitten,
		unsigned	lit )

Definition at line 1844 of file cadical_kitten.c.

                                                                        {
  cadical_kitten_clause (cadical_kitten, 1, &lit);
}

Here is the call graph for this function:

◆ cadical_kitten_value()

signed char cadical_kitten_value	(	cadical_kitten *	cadical_kitten,
		unsigned	elit )

Definition at line 2220 of file cadical_kitten.c.

                                                                                 {
  REQUIRE_STATUS (10);
  const unsigned eidx = elit / 2;
  if (eidx >= cadical_kitten->evars)
    return 0;
  unsigned iidx = cadical_kitten->import[eidx];
  if (!iidx)
    return 0;
  const unsigned ilit = 2 * (iidx - 1) + (elit & 1);
  return cadical_kitten->values[ilit];
}

◆ cadical_new_learned_klause()

unsigned cadical_new_learned_klause ( cadical_kitten * cadical_kitten )

Definition at line 877 of file cadical_kitten.c.

                                                                     {
  unsigned res = new_reference (cadical_kitten);
  unsigneds *klauses = &cadical_kitten->klauses;
  const size_t size = SIZE_STACK (cadical_kitten->klause);
  CADICAL_assert (size <= UINT_MAX);
  const size_t aux =
      cadical_kitten->antecedents ? SIZE_STACK (cadical_kitten->resolved) : 0;
  CADICAL_assert (aux <= UINT_MAX);
  PUSH_STACK (*klauses, (unsigned) aux);
  PUSH_STACK (*klauses, (unsigned) size);
  PUSH_STACK (*klauses, LEARNED_FLAG);
  for (all_stack (unsigned, lit, cadical_kitten->klause))
    PUSH_STACK (*klauses, lit);
  if (aux)
    for (all_stack (unsigned, ref, cadical_kitten->resolved))
      PUSH_STACK (*klauses, ref);
  connect_new_klause (cadical_kitten, res);
  cadical_kitten->learned = true;
  cadical_kitten->statistics.learned++;
  return res;
}

◆ citten_clause_with_id()

void citten_clause_with_id	(	cadical_kitten *	cadical_kitten,
		unsigned	id,
		size_t	size,
		int *	elits )

Definition at line 1839 of file cadical_kitten.c.

                                        {
  citten_clause_with_id_and_exception (cadical_kitten, id, size, elits, INVALID);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ citten_clause_with_id_and_equivalence()

void citten_clause_with_id_and_equivalence	(	cadical_kitten *	cadical_kitten,
		unsigned	id,
		size_t	size,
		const int *	elits,
		unsigned	lit,
		unsigned	other )

Definition at line 1801 of file cadical_kitten.c.

                                                                          {
  REQUIRE_INITIALIZED ();
  if (cadical_kitten->status)
    reset_incremental (cadical_kitten);
  CADICAL_assert (EMPTY_STACK (cadical_kitten->klause));
  bool sat = false;
  const int *const end = elits + size;
  for (const int *p = elits; p != end; p++) {
    const unsigned elit = int2u (*p); // this is the conversion
    if (elit == (lit ^ 1u) || elit == (other ^ 1u))
      continue;
    if (elit == lit || elit == other) {
      sat = true;
      break;
    }
    const unsigned ilit = import_literal (cadical_kitten, elit);
    CADICAL_assert (ilit < cadical_kitten->lits);
    const unsigned iidx = ilit / 2;
    if (cadical_kitten->marks[iidx])
      INVALID_API_USAGE ("variable '%u' of literal '%u' occurs twice",
                         elit / 2, elit);
    cadical_kitten->marks[iidx] = true;
    PUSH_STACK (cadical_kitten->klause, ilit);
  }
  for (unsigned *p = cadical_kitten->klause.begin; p != cadical_kitten->klause.end; p++)
    cadical_kitten->marks[*p / 2] = false;
  if (!sat)
    new_original_klause (cadical_kitten, id);
  CLEAR_STACK (cadical_kitten->klause);
}

◆ citten_clause_with_id_and_exception()

void citten_clause_with_id_and_exception	(	cadical_kitten *	cadical_kitten,
		unsigned	id,
		size_t	size,
		const int *	elits,
		unsigned	except )

Definition at line 1774 of file cadical_kitten.c.

                                                           {
  REQUIRE_INITIALIZED ();
  if (cadical_kitten->status)
    reset_incremental (cadical_kitten);
  CADICAL_assert (EMPTY_STACK (cadical_kitten->klause));
  const int *const end = elits + size;
  for (const int *p = elits; p != end; p++) {
    const unsigned elit = int2u (*p); // this is the conversion
    if (elit == except)
      continue;
    const unsigned ilit = import_literal (cadical_kitten, elit);
    CADICAL_assert (ilit < cadical_kitten->lits);
    const unsigned iidx = ilit / 2;
    if (cadical_kitten->marks[iidx])
      INVALID_API_USAGE ("variable '%u' of literal '%u' occurs twice",
                         elit / 2, elit);
    cadical_kitten->marks[iidx] = true;
    PUSH_STACK (cadical_kitten->klause, ilit);
  }
  for (unsigned *p = cadical_kitten->klause.begin; p != cadical_kitten->klause.end; p++)
    cadical_kitten->marks[*p / 2] = false;
  new_original_klause (cadical_kitten, id);
  CLEAR_STACK (cadical_kitten->klause);
}

Here is the caller graph for this function:

◆ STACK()

typedef STACK ( unsigned )

Definition at line 89 of file cadical_kitten.c.

           {
  unsigned level;
  unsigned reason;
};

Variable Documentation

◆ value

ABC_NAMESPACE_IMPL_START typedef signed char value

Definition at line 19 of file cadical_kitten.c.

Classes

Macros

Typedefs

Functions

Variables

Macro Definition Documentation

◆ ADD

◆ all_antecedents

◆ all_kits

◆ all_klauses

◆ all_learned_klauses

◆ all_literals_in_klause

◆ all_original_klauses

◆ BEGIN_KLAUSE

◆ CALLOC

◆ CORE_FLAG

◆ DEALLOC

◆ END_KLAUSE

◆ ENLARGE_STACK

◆ INC

◆ INVALID

◆ INVALID_API_USAGE

◆ KATCHES

◆ KITTEN_TICKS

◆ LEARNED_FLAG

◆ LOG

◆ LOGLITS

◆ MAX_VARS

◆ REQUIRE_INITIALIZED

◆ REQUIRE_STATUS

◆ RESIZE1

◆ RESIZE2

◆ ROG

◆ UPDATE_STATUS

Typedef Documentation

◆ kar

◆ kimits

◆ kink

◆ klause

◆ statistics

Function Documentation

◆ cadical_completely_backtrack_to_root_level()

◆ cadical_kitten_add_prime_implicant()

◆ cadical_kitten_assume()

◆ cadical_kitten_assume_signed()

◆ cadical_kitten_binary()

◆ cadical_kitten_clause()

◆ cadical_kitten_clause_with_id_and_exception()

◆ cadical_kitten_clear()

◆ cadical_kitten_compute_clausal_core()

◆ cadical_kitten_compute_prime_implicant()

◆ cadical_kitten_current_ticks()

◆ cadical_kitten_failed()

◆ cadical_kitten_fixed()

◆ cadical_kitten_fixed_signed()

◆ cadical_kitten_flip_and_implicant_for_signed_literal()

◆ cadical_kitten_flip_literal()

◆ cadical_kitten_flip_phases()

◆ cadical_kitten_flip_signed_literal()

◆ cadical_kitten_init()

◆ cadical_kitten_no_terminator()

◆ cadical_kitten_no_ticks_limit()

◆ cadical_kitten_randomize_phases()

◆ cadical_kitten_release()

◆ cadical_kitten_set_terminator()

◆ cadical_kitten_set_ticks_limit()

◆ cadical_kitten_shrink_to_clausal_core()

◆ cadical_kitten_shuffle_clauses()

◆ cadical_kitten_signed_value()

◆ cadical_kitten_solve()

◆ cadical_kitten_status()

◆ cadical_kitten_trace_core()

◆ cadical_kitten_track_antecedents()

◆ cadical_kitten_traverse_core_clauses()

◆ cadical_kitten_traverse_core_clauses_with_id()

◆ cadical_kitten_traverse_core_ids()

◆ cadical_kitten_unit()

◆ cadical_kitten_value()

◆ cadical_new_learned_klause()

◆ citten_clause_with_id()