#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 "allocate.h"
#include "error.h"
#include "internal.h"
#include "terminate.h"

Include dependency graph for kitten.c:

Classes
struct	kink

struct	katch

struct	klause

struct	kimits

struct	kitten

Macros
#define	KITTEN_TICKS (solver->statistics_.kitten_ticks)

#define	INVALID UINT_MAX

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

#define	CORE_FLAG (1u)

#define	LEARNED_FLAG (2u)

#define	KITTEN_BLIT

#define	solver (kitten->kissat)

#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	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 katch	katch

Functions
typedef	STACK (unsigned)

kitten *	kitten_embedded (struct kissat *kissat)

void	kitten_track_antecedents (kitten *kitten)

void	kitten_randomize_phases (kitten *kitten)

void	kitten_flip_phases (kitten *kitten)

void	kitten_no_ticks_limit (kitten *kitten)

void	kitten_set_ticks_limit (kitten *kitten, uint64_t delta)

void	kitten_shuffle_clauses (kitten *kitten)

unsigned	new_learned_klause (kitten *kitten)

void	kitten_clear (kitten *kitten)

void	kitten_release (kitten *kitten)

void	completely_backtrack_to_root_level (kitten *kitten)

void	kitten_assume (kitten *kitten, unsigned elit)

void	kitten_clause_with_id_and_exception (kitten kitten, unsigned id, size_t size, const unsigned elits, unsigned except)

void	kitten_clause (kitten kitten, size_t size, unsigned elits)

void	kitten_unit (kitten *kitten, unsigned lit)

void	kitten_binary (kitten *kitten, unsigned a, unsigned b)

int	kitten_solve (kitten *kitten)

int	kitten_status (kitten *kitten)

unsigned	kitten_compute_clausal_core (kitten kitten, uint64_t learned_ptr)

void	kitten_traverse_core_ids (kitten kitten, void state, void(traverse)(void , unsigned))

void	kitten_traverse_core_clauses (kitten kitten, void state, void(traverse)(void , bool, size_t, const unsigned *))

void	kitten_shrink_to_clausal_core (kitten *kitten)

signed char	kitten_value (kitten *kitten, unsigned elit)

signed char	kitten_fixed (kitten *kitten, unsigned elit)

bool	kitten_flip_literal (kitten *kitten, unsigned elit)

bool	kitten_failed (kitten *kitten, unsigned elit)

Macro Definition Documentation

◆ all_antecedents

#define all_antecedents	(		REF,
			C )

Value:

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

Definition at line 346 of file kitten.c.

#define all_antecedents(REF, C) \
  unsigned REF, *REF##_PTR = antecedents_func (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 = kitten->lits; \
  KIT != KIT_##END; \
  KIT++

Definition at line 331 of file kitten.c.

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

◆ all_klauses

#define all_klauses ( C )

Value:

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

Definition at line 314 of file kitten.c.

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

◆ all_learned_klauses

#define all_learned_klauses ( C )

Value:

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

Definition at line 325 of file kitten.c.

#define all_learned_klauses(C) \
  klause *C = begin_learned_klauses (kitten), \
         *end_##C = end_klauses (kitten); \
  (C) != end_##C; \
  (C) = next_klause (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 340 of file 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 (kitten), \
         *end_##C = end_original_klauses (kitten); \
  (C) != end_##C; \
  (C) = next_klause (kitten, C)

Definition at line 319 of file kitten.c.

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

◆ BEGIN_KLAUSE

#define BEGIN_KLAUSE ( C )

Value:

(C)->lits

Definition at line 336 of file kitten.c.

◆ CORE_FLAG

#define CORE_FLAG (1u)

Definition at line 130 of file kitten.c.

◆ END_KLAUSE

#define END_KLAUSE ( C )

Value:

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

Definition at line 338 of file kitten.c.

◆ INVALID

#define INVALID UINT_MAX

Definition at line 127 of file kitten.c.

◆ INVALID_API_USAGE

#define INVALID_API_USAGE ( ... )

Value:

invalid_api_usage (__func__, __VA_ARGS__)

Definition at line 626 of file kitten.c.

◆ KATCHES

#define KATCHES ( KIT )

Value:

(kitten->watches[KISSAT_assert ((KIT) < kitten->lits), (KIT)])

KISSAT_assert

#define KISSAT_assert(ignore)

Definition global.h:13

kitten::watches

katches * watches

Definition kitten.c:256

Definition at line 312 of file kitten.c.

◆ KITTEN_BLIT

#define KITTEN_BLIT

Definition at line 155 of file kitten.c.

◆ KITTEN_TICKS

#define KITTEN_TICKS (solver->statistics_.kitten_ticks)

Definition at line 119 of file kitten.c.

◆ LEARNED_FLAG

#define LEARNED_FLAG (2u)

Definition at line 131 of file kitten.c.

◆ LOG

#define LOG ( ... )

Value:

do { \

} while (0)

Definition at line 422 of file kitten.c.

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

◆ MAX_VARS

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

Definition at line 128 of file kitten.c.

◆ REQUIRE_INITIALIZED

#define REQUIRE_INITIALIZED ( )

Value:

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

Definition at line 628 of file kitten.c.

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

◆ REQUIRE_STATUS

#define REQUIRE_STATUS ( EXPECTED )

Value:

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

Definition at line 634 of file kitten.c.

#define REQUIRE_STATUS(EXPECTED) \
  do { \
    REQUIRE_INITIALIZED (); \
    if (kitten->status != (EXPECTED)) \
      INVALID_API_USAGE ("invalid status '%s' (expected '%s')", \
                         status_to_string (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); \
    if (BYTES) \
      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 546 of file 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); \
    if (BYTES) \
      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); \
    if (BYTES) \
      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 559 of file kitten.c.

#define RESIZE2(T, P)                            \
  do { \
    void *OLD_PTR = (P); \
    CALLOC (T, (P), new_size);                    \
    const size_t BYTES = old_lits * sizeof *(P); \
    if (BYTES) \
      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 425 of file kitten.c.

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

◆ solver

#define solver (kitten->kissat)

Definition at line 211 of file kitten.c.

◆ UPDATE_STATUS

#define UPDATE_STATUS ( STATUS )

Value:

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

Definition at line 643 of file kitten.c.

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

Typedef Documentation

◆ katch

typedef struct katch katch

Definition at line 138 of file kitten.c.

Function Documentation

◆ completely_backtrack_to_root_level()

void completely_backtrack_to_root_level ( kitten * kitten )

Definition at line 1260 of file kitten.c.

                                                         {
  check_queue (kitten);
  LOG ("completely backtracking to level 0");
  value *values = kitten->values;
  unsigneds *trail = &kitten->trail;
#ifndef KISSAT_NDEBUG
  kar *vars = kitten->vars;
#endif
  for (all_stack (unsigned, lit, *trail)) {
    KISSAT_assert (vars[lit / 2].level);
    unassign (kitten, values, lit);
  }
  CLEAR_STACK (*trail);
  kitten->propagated = 0;
  kitten->level = 0;
  check_queue (kitten);
}

Here is the caller graph for this function:

◆ kitten_assume()

void kitten_assume	(	kitten *	kitten,
		unsigned	elit )

Definition at line 1763 of file kitten.c.

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

◆ kitten_binary()

void kitten_binary	(	kitten *	kitten,
		unsigned	a,
		unsigned	b )

Definition at line 1809 of file kitten.c.

                                                            {
  unsigned clause[2] = {a, b};
  kitten_clause (kitten, 2, clause);
}

Here is the call graph for this function:

◆ kitten_clause()

void kitten_clause	(	kitten *	kitten,
		size_t	size,
		unsigned *	elits )

Definition at line 1800 of file kitten.c.

                                                                  {
  kitten_clause_with_id_and_exception (kitten, INVALID, size, elits,
                                       INVALID);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ kitten_clause_with_id_and_exception()

void kitten_clause_with_id_and_exception	(	kitten *	kitten,
		unsigned	id,
		size_t	size,
		const unsigned *	elits,
		unsigned	except )

Definition at line 1772 of file kitten.c.

                                                           {
  REQUIRE_INITIALIZED ();
  if (kitten->status)
    reset_incremental (kitten);
  KISSAT_assert (EMPTY_STACK (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 (kitten, elit);
    KISSAT_assert (ilit < kitten->lits);
    const unsigned iidx = ilit / 2;
    if (kitten->marks[iidx])
      INVALID_API_USAGE ("variable '%u' of literal '%u' occurs twice",
                         elit / 2, elit);
    kitten->marks[iidx] = true;
    PUSH_STACK (kitten->klause, ilit);
  }
  for (unsigned *p = kitten->klause.begin; p != kitten->klause.end; p++)
    kitten->marks[*p / 2] = false;
  new_original_klause (kitten, id);
  CLEAR_STACK (kitten->klause);
}

Here is the caller graph for this function:

◆ kitten_clear()

void kitten_clear ( kitten * kitten )

Definition at line 986 of file kitten.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ kitten_compute_clausal_core()

unsigned kitten_compute_clausal_core	(	kitten *	kitten,
		uint64_t *	learned_ptr )

Definition at line 1872 of file kitten.c.

                                                             {
  REQUIRE_STATUS (20);
 
  if (!kitten->antecedents)
    INVALID_API_USAGE ("antecedents not tracked");
 
  LOG ("computing clausal core");
 
  unsigneds *resolved = &kitten->resolved;
  KISSAT_assert (EMPTY_STACK (*resolved));
 
  unsigned original = 0;
  uint64_t learned = 0;
 
  unsigned reason_ref = kitten->inconsistent;
 
  if (reason_ref == INVALID) {
    KISSAT_assert (!EMPTY_STACK (kitten->assumptions));
    reason_ref = 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);
#ifdef STAND_ALONE_KITTEN
  kitten->statistics.original = original;
  kitten->statistics.learned = 0;
#endif
  UPDATE_STATUS (21);
 
  return original;
 
  
    }
  }
 
  PUSH_STACK (*resolved, reason_ref);
  unsigneds *core = &kitten->core;
  KISSAT_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 (kitten, d_ref);
      KISSAT_assert (!is_core_klause (d));
      set_core_klause (d);
      if (is_learned_klause (d))
        learned++;
      else
        original++;
    } else {
      klause *c = dereference_klause (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 (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);
#ifdef STAND_ALONE_KITTEN
  kitten->statistics.original = original;
  kitten->statistics.learned = 0;
#endif
  UPDATE_STATUS (21);
 
  return original;
}

Here is the caller graph for this function:

◆ kitten_embedded()

kitten * kitten_embedded ( struct kissat * kissat )

Definition at line 664 of file kitten.c.

                                                {
  if (!kissat)
    INVALID_API_USAGE ("'kissat' argument zero");
 
  kitten *kitten;
  struct kitten dummy;
  dummy.kissat = kissat;
  kitten = &dummy;
  CALLOC (struct kitten, kitten, 1);
  kitten->kissat = kissat;
  initialize_kitten (kitten);
  return kitten;
}

◆ kitten_failed()

bool kitten_failed	(	kitten *	kitten,
		unsigned	elit )

Definition at line 2137 of file kitten.c.

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

◆ kitten_fixed()

signed char kitten_fixed	(	kitten *	kitten,
		unsigned	elit )

Definition at line 2107 of file kitten.c.

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

◆ kitten_flip_literal()

bool kitten_flip_literal	(	kitten *	kitten,
		unsigned	elit )

Definition at line 2125 of file kitten.c.

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

◆ kitten_flip_phases()

void kitten_flip_phases ( kitten * kitten )

Definition at line 722 of file kitten.c.

                                         {
  REQUIRE_INITIALIZED ();
 
  LOG ("flipping phases");
 
  unsigned char *phases = kitten->phases;
  const unsigned vars = 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;
}

◆ kitten_no_ticks_limit()

void kitten_no_ticks_limit ( kitten * kitten )

Definition at line 743 of file kitten.c.

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

◆ kitten_randomize_phases()

void kitten_randomize_phases ( kitten * kitten )

Definition at line 690 of file kitten.c.

                                              {
  REQUIRE_INITIALIZED ();
 
  LOG ("randomizing phases");
 
  unsigned char *phases = kitten->phases;
  const unsigned vars = kitten->size / 2;
 
  uint64_t random = kissat_next_random64 (&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 (&kitten->generator);
    i += 64;
  }
 
  unsigned shift = 0;
  while (i != vars)
    phases[i++] = (random >> shift++) & 1;
}

Here is the call graph for this function:

◆ kitten_release()

void kitten_release ( kitten * kitten )

Definition at line 1028 of file kitten.c.

                                     {
  RELEASE_STACK (kitten->analyzed);
  RELEASE_STACK (kitten->assumptions);
  RELEASE_STACK (kitten->core);
  RELEASE_STACK (kitten->eclause);
  RELEASE_STACK (kitten->export_);
  RELEASE_STACK (kitten->klause);
  RELEASE_STACK (kitten->klauses);
  RELEASE_STACK (kitten->resolved);
  RELEASE_STACK (kitten->trail);
  RELEASE_STACK (kitten->units);
 
  for (size_t lit = 0; lit < kitten->size; lit++)
    RELEASE_STACK (kitten->watches[lit]);
 
#ifndef STAND_ALONE_KITTEN
  const size_t lits = kitten->size;
  const unsigned vars = lits / 2;
#endif
  DEALLOC (kitten->marks, vars);
  DEALLOC (kitten->phases, vars);
  DEALLOC (kitten->values, lits);
  DEALLOC (kitten->failed, lits);
  DEALLOC (kitten->vars, vars);
  DEALLOC (kitten->links, vars);
  DEALLOC (kitten->watches, lits);
  DEALLOC (kitten->import, kitten->esize);
#ifdef STAND_ALONE_KITTEN
  free (kitten);
#else
  kissat_free (kitten->kissat, kitten, sizeof *kitten);
#endif
}

Here is the call graph for this function:

◆ kitten_set_ticks_limit()

void kitten_set_ticks_limit	(	kitten *	kitten,
		uint64_t	delta )

Definition at line 749 of file 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);
  }
 
  kitten->limits.ticks = limit;
}

Here is the caller graph for this function:

◆ kitten_shrink_to_clausal_core()

void kitten_shrink_to_clausal_core ( kitten * kitten )

Definition at line 2022 of file kitten.c.

                                                    {
  REQUIRE_STATUS (21);
 
  LOG ("shrinking formula to core of original clauses");
 
  CLEAR_STACK (kitten->trail);
 
  kitten->unassigned = kitten->lits / 2;
  kitten->propagated = 0;
  kitten->level = 0;
 
  update_search (kitten, kitten->queue.last);
 
  memset (kitten->values, 0, kitten->lits);
 
  for (all_kits (lit))
    CLEAR_STACK (KATCHES (lit));
 
  KISSAT_assert (kitten->inconsistent != INVALID);
  klause *inconsistent = dereference_klause (kitten, kitten->inconsistent);
  if (is_learned_klause (inconsistent) || inconsistent->size) {
    ROG (kitten->inconsistent, "resetting inconsistent");
    kitten->inconsistent = INVALID;
  } else
    ROG (kitten->inconsistent, "keeping inconsistent");
 
  CLEAR_STACK (kitten->units);
 
  klause *begin = begin_klauses (kitten), *q = begin;
  klause const *const end = end_original_klauses (kitten);
#ifdef LOGGING
  unsigned original = 0;
#endif
  for (klause *c = begin, *next; c != end; c = next) {
    next = next_klause (kitten, c);
    KISSAT_assert (!is_learned_klause (c));
    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 (!kitten->inconsistent)
        kitten->inconsistent = dst;
    } else if (size == 1)
      PUSH_STACK (kitten->units, dst);
    else {
      watch_klause (kitten, c->lits[0], c, dst);
      watch_klause (kitten, c->lits[1], c, 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 (kitten->klauses, (unsigned *) q);
  kitten->end_original_ref = SIZE_STACK (kitten->klauses);
  LOG ("end of original clauses at %zu", kitten->end_original_ref);
  LOG ("%u original clauses left", original);
 
  CLEAR_STACK (kitten->core);
 
  UPDATE_STATUS (0);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ kitten_shuffle_clauses()

void kitten_shuffle_clauses ( kitten * kitten )

Definition at line 825 of file kitten.c.

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

Here is the caller graph for this function:

◆ kitten_solve()

int kitten_solve ( kitten * kitten )

Definition at line 1818 of file kitten.c.

                                  {
  REQUIRE_INITIALIZED ();
  if (kitten->status)
    reset_incremental (kitten);
  else if (kitten->level)
    completely_backtrack_to_root_level (kitten);
 
  LOG ("starting solving under %zu assumptions",
       SIZE_STACK (kitten->assumptions));
 
  INC (kitten_solved);
 
  int res = propagate_units (kitten);
  while (!res) {
    const unsigned conflict = propagate (kitten);
    if (conflict != INVALID) {
      if (kitten->level)
        analyze (kitten, conflict);
      else {
        inconsistent (kitten, conflict);
        res = 20;
      }
    } else
#ifdef STAND_ALONE_KITTEN
        if (time_limit_hit) {
      time_limit_hit = false;
      break;
    } else
#endif
      res = decide (kitten);
  }
 
  if (res < 0)
    res = 0;
 
  if (!res && !EMPTY_STACK (kitten->assumptions))
    reset_assumptions (kitten);
 
  UPDATE_STATUS (res);
 
  if (res == 10)
    INC (kitten_sat);
  else if (res == 20)
    INC (kitten_unsat);
  else
    INC (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:

◆ kitten_status()

int kitten_status ( kitten * kitten )

Definition at line 1870 of file kitten.c.

1870{ return kitten->status; }

◆ kitten_track_antecedents()

void kitten_track_antecedents ( kitten * kitten )

Definition at line 680 of file kitten.c.

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

Here is the caller graph for this function:

◆ kitten_traverse_core_clauses()

void kitten_traverse_core_clauses	(	kitten *	kitten,
		void *	state,
		void(*	traverse )(void , bool, size_t, const unsigned ) )

Definition at line 1989 of file kitten.c.

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

Here is the caller graph for this function:

◆ kitten_traverse_core_ids()

void kitten_traverse_core_ids	(	kitten *	kitten,
		void *	state,
		void(*	traverse )(void *, unsigned) )

Definition at line 1964 of file kitten.c.

                                                                    {
  REQUIRE_STATUS (21);
 
  LOG ("traversing core of original clauses");
 
  unsigned traversed = 0;
 
  for (all_original_klauses (c)) {
    KISSAT_assert (!is_learned_klause (c));
    if (is_learned_klause (c))
      continue;
    if (!is_core_klause (c))
      continue;
    ROG (reference_klause (kitten, c), "traversing");
    traverse (state, c->aux);
    traversed++;
  }
 
  LOG ("traversed %u original core clauses", traversed);
  (void) traversed;
 
  KISSAT_assert (kitten->status == 21);
}

Here is the caller graph for this function:

◆ kitten_unit()

void kitten_unit	(	kitten *	kitten,
		unsigned	lit )

Definition at line 1805 of file kitten.c.

                                                {
  kitten_clause (kitten, 1, &lit);
}

Here is the call graph for this function:

◆ kitten_value()

signed char kitten_value	(	kitten *	kitten,
		unsigned	elit )

Definition at line 2095 of file kitten.c.

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

◆ new_learned_klause()

unsigned new_learned_klause ( kitten * kitten )

Definition at line 962 of file kitten.c.

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

◆ STACK()

typedef STACK ( unsigned )

Definition at line 139 of file kitten.c.

           {
  unsigned level;
  unsigned reason;
};

Classes

Macros

Typedefs

Functions

Macro Definition Documentation

◆ all_antecedents

◆ all_kits

◆ all_klauses

◆ all_learned_klauses

◆ all_literals_in_klause

◆ all_original_klauses

◆ BEGIN_KLAUSE

◆ CORE_FLAG

◆ END_KLAUSE

◆ INVALID

◆ INVALID_API_USAGE

◆ KATCHES

◆ KITTEN_BLIT

◆ KITTEN_TICKS

◆ LEARNED_FLAG

◆ LOG

◆ MAX_VARS

◆ REQUIRE_INITIALIZED

◆ REQUIRE_STATUS

◆ RESIZE1

◆ RESIZE2

◆ ROG

◆ solver

◆ UPDATE_STATUS

Typedef Documentation

◆ katch

Function Documentation

◆ completely_backtrack_to_root_level()

◆ kitten_assume()

◆ kitten_binary()

◆ kitten_clause()

◆ kitten_clause_with_id_and_exception()

◆ kitten_clear()

◆ kitten_compute_clausal_core()

◆ kitten_embedded()

◆ kitten_failed()

◆ kitten_fixed()

◆ kitten_flip_literal()

◆ kitten_flip_phases()

◆ kitten_no_ticks_limit()

◆ kitten_randomize_phases()

◆ kitten_release()

◆ kitten_set_ticks_limit()

◆ kitten_shrink_to_clausal_core()

◆ kitten_shuffle_clauses()

◆ kitten_solve()

◆ kitten_status()

◆ kitten_track_antecedents()

◆ kitten_traverse_core_clauses()

◆ kitten_traverse_core_ids()

◆ kitten_unit()

◆ kitten_value()

◆ new_learned_klause()

◆ STACK()