kitten.h File Reference

#include "global.h"
#include <stdbool.h>
#include <stdint.h>
#include <stdio.h>
#include <stdlib.h>

Include dependency graph for kitten.h:

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

Go to the source code of this file.

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct cadical_kitten	cadical_kitten

Functions
cadical_kitten *	cadical_kitten_init (void)
void	cadical_kitten_clear (cadical_kitten *)
void	cadical_kitten_release (cadical_kitten *)
void	cadical_kitten_track_antecedents (cadical_kitten *)
void	cadical_kitten_shuffle_clauses (cadical_kitten *)
void	cadical_kitten_flip_phases (cadical_kitten *)
void	cadical_kitten_randomize_phases (cadical_kitten *)
void	cadical_kitten_assume (cadical_kitten *, unsigned lit)
void	cadical_kitten_assume_signed (cadical_kitten *, int lit)
void	cadical_kitten_clause (cadical_kitten *, size_t size, unsigned *)
void	citten_clause_with_id (cadical_kitten *, unsigned id, size_t size, int *)
void	cadical_kitten_unit (cadical_kitten *, unsigned)
void	cadical_kitten_binary (cadical_kitten *, unsigned, unsigned)
void	cadical_kitten_clause_with_id_and_exception (cadical_kitten *, unsigned id, size_t size, const unsigned *, unsigned except)
void	citten_clause_with_id_and_exception (cadical_kitten *, unsigned id, size_t size, const int *, unsigned except)
void	citten_clause_with_id_and_equivalence (cadical_kitten *, unsigned id, size_t size, const int *, unsigned, unsigned)
void	cadical_kitten_no_ticks_limit (cadical_kitten *)
void	cadical_kitten_set_ticks_limit (cadical_kitten *, uint64_t)
uint64_t	cadical_kitten_current_ticks (cadical_kitten *)
void	cadical_kitten_no_terminator (cadical_kitten *)
void	cadical_kitten_set_terminator (cadical_kitten *, void *, int(*)(void *))
int	cadical_kitten_solve (cadical_kitten *)
int	cadical_kitten_status (cadical_kitten *)
signed char	cadical_kitten_value (cadical_kitten *, unsigned)
signed char	cadical_kitten_signed_value (cadical_kitten *, int)
signed char	cadical_kitten_fixed (cadical_kitten *, unsigned)
signed char	cadical_kitten_fixed_signed (cadical_kitten *, int)
bool	cadical_kitten_failed (cadical_kitten *, unsigned)
bool	cadical_kitten_flip_literal (cadical_kitten *, unsigned)
bool	cadical_kitten_flip_signed_literal (cadical_kitten *, int)
unsigned	cadical_kitten_compute_clausal_core (cadical_kitten *, uint64_t *learned)
void	cadical_kitten_shrink_to_clausal_core (cadical_kitten *)
void	cadical_kitten_traverse_core_ids (cadical_kitten *, void *state, void(*traverse)(void *state, unsigned id))
void	cadical_kitten_traverse_core_clauses (cadical_kitten *, void *state, void(*traverse)(void *state, bool learned, size_t, const unsigned *))
void	cadical_kitten_traverse_core_clauses_with_id (cadical_kitten *, void *state, void(*traverse)(void *state, unsigned, bool learned, size_t, const unsigned *))
void	cadical_kitten_trace_core (cadical_kitten *, void *state, void(*trace)(void *, unsigned, unsigned, bool, size_t, const unsigned *, size_t, const unsigned *))
int	cadical_kitten_compute_prime_implicant (cadical_kitten *cadical_kitten, void *state, bool(*ignore)(void *, unsigned))
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_flip_and_implicant_for_signed_literal (cadical_kitten *cadical_kitten, int elit)

Typedef Documentation

cadical_kitten

typedef typedefABC_NAMESPACE_HEADER_START struct cadical_kitten cadical_kitten

Definition at line 13 of file kitten.h.

Function Documentation

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	lit )

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	lit )

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 )

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.

{ 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 *state, bool learned, 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 *state, unsigned id) )

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];
}

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: