kitten.h File Reference

#include <stdbool.h>
#include <stdint.h>
#include <stdlib.h>
#include "global.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 kitten	kitten

Functions
kitten *	kitten_init (void)
void	kitten_clear (kitten *)
void	kitten_release (kitten *)
void	kitten_track_antecedents (kitten *)
void	kitten_shuffle_clauses (kitten *)
void	kitten_flip_phases (kitten *)
void	kitten_randomize_phases (kitten *)
void	kitten_assume (kitten *, unsigned lit)
void	kitten_clause (kitten *, size_t size, unsigned *)
void	kitten_unit (kitten *, unsigned)
void	kitten_binary (kitten *, unsigned, unsigned)
void	kitten_clause_with_id_and_exception (kitten *, unsigned id, size_t size, const unsigned *, unsigned except)
void	kitten_no_ticks_limit (kitten *)
void	kitten_set_ticks_limit (kitten *, uint64_t)
int	kitten_solve (kitten *)
int	kitten_status (kitten *)
signed char	kitten_value (kitten *, unsigned)
signed char	kitten_fixed (kitten *, unsigned)
bool	kitten_failed (kitten *, unsigned)
bool	kitten_flip_literal (kitten *, unsigned)
unsigned	kitten_compute_clausal_core (kitten *, uint64_t *learned)
void	kitten_shrink_to_clausal_core (kitten *)
void	kitten_traverse_core_ids (kitten *, void *state, void(*traverse)(void *state, unsigned id))
void	kitten_traverse_core_clauses (kitten *, void *state, void(*traverse)(void *state, bool learned, size_t, const unsigned *))
kitten *	kitten_embedded (struct kissat *)

Typedef Documentation

kitten

typedef typedefABC_NAMESPACE_HEADER_START struct kitten kitten

Definition at line 11 of file kitten.h.

Function Documentation

kitten_assume()

void kitten_assume	(	kitten *	kitten,
		unsigned	lit )

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 )

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_init()

kitten * kitten_init

(

void

)

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.

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

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