watch.h File Reference

#include "keatures.h"
#include "reference.h"
#include "stack.h"
#include "vector.h"
#include <stdbool.h>
#include "global.h"

Include dependency graph for watch.h:

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

Go to the source code of this file.

Classes
struct	binary_tagged_literal
struct	binary_tagged_reference
union	watch
struct	litwatch
struct	litpair
struct	litriple

Macros
#define	EMPTY_WATCHES(W)
#define	SIZE_WATCHES(W)
#define	PUSH_WATCHES(W, E)
#define	LAST_WATCH_POINTER(WS)
#define	BEGIN_WATCHES(WS)
#define	END_WATCHES(WS)
#define	BEGIN_CONST_WATCHES(WS)
#define	END_CONST_WATCHES(WS)
#define	RELEASE_WATCHES(WS)
#define	SET_END_OF_WATCHES(WS, P)
#define	REMOVE_WATCHES(W, E)
#define	WATCHES(LIT)
#define	all_binary_blocking_watch_ref(WATCH, REF, WATCHES)
#define	all_binary_blocking_watches(WATCH, WATCHES)
#define	all_binary_large_watches(WATCH, WATCHES)

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START union watch	watch
typedef struct binary_tagged_literal	watch_type
typedef struct binary_tagged_literal	binary_watch
typedef struct binary_tagged_literal	blocking_watch
typedef struct binary_tagged_reference	large_watch
typedef vector	watches
typedef struct litwatch	litwatch
typedef struct litpair	litpair
typedef struct litriple	litriple

Functions
typedef	STACK (litwatch) litwatches
typedef	STACK (litpair) litpairs
typedef	STACK (litriple) litriples
void	kissat_remove_binary_watch (struct kissat *, watches *, unsigned)
void	kissat_remove_blocking_watch (struct kissat *, watches *, reference)
void	kissat_substitute_large_watch (struct kissat *, watches *, watch src, watch dst)
void	kissat_flush_all_connected (struct kissat *)
void	kissat_flush_large_watches (struct kissat *)
void	kissat_watch_large_clauses (struct kissat *)
void	kissat_flush_large_connected (struct kissat *)
void	kissat_connect_irredundant_large_clauses (struct kissat *)

Macro Definition Documentation

all_binary_blocking_watch_ref

#define all_binary_blocking_watch_ref	(		WATCH,
			REF,
			WATCHES )

Value:

  watch WATCH, \
      *WATCH##_PTR = (KISSAT_assert (solver->watching), BEGIN_WATCHES (WATCHES)), \
      *const WATCH##_END = END_WATCHES (WATCHES); \
  WATCH##_PTR != WATCH##_END && \
      ((WATCH = *WATCH##_PTR), \
       (REF = WATCH.type.binary ? INVALID_REF : WATCH##_PTR[1].large.ref), \
       true); \
  WATCH##_PTR += 1u + !WATCH.type.binary

Definition at line 141 of file watch.h.

#define all_binary_blocking_watch_ref(WATCH, REF, WATCHES) \
  watch WATCH, \
      *WATCH##_PTR = (KISSAT_assert (solver->watching), BEGIN_WATCHES (WATCHES)), \
      *const WATCH##_END = END_WATCHES (WATCHES); \
  WATCH##_PTR != WATCH##_END && \
      ((WATCH = *WATCH##_PTR), \
       (REF = WATCH.type.binary ? INVALID_REF : WATCH##_PTR[1].large.ref), \
       true); \
  WATCH##_PTR += 1u + !WATCH.type.binary

all_binary_blocking_watches

#define all_binary_blocking_watches	(		WATCH,
			WATCHES )

Value:

  watch WATCH, \
      *WATCH##_PTR = (KISSAT_assert (solver->watching), BEGIN_WATCHES (WATCHES)), \
      *const WATCH##_END = END_WATCHES (WATCHES); \
  WATCH##_PTR != WATCH##_END && ((WATCH = *WATCH##_PTR), true); \
  WATCH##_PTR += 1u + !WATCH.type.binary

Definition at line 151 of file watch.h.

#define all_binary_blocking_watches(WATCH, WATCHES) \
  watch WATCH, \
      *WATCH##_PTR = (KISSAT_assert (solver->watching), BEGIN_WATCHES (WATCHES)), \
      *const WATCH##_END = END_WATCHES (WATCHES); \
  WATCH##_PTR != WATCH##_END && ((WATCH = *WATCH##_PTR), true); \
  WATCH##_PTR += 1u + !WATCH.type.binary

all_binary_large_watches

#define all_binary_large_watches	(		WATCH,
			WATCHES )

Value:

  watch WATCH, \
      *WATCH##_PTR = \
          (KISSAT_assert (!solver->watching), BEGIN_WATCHES (WATCHES)), \
      *const WATCH##_END = END_WATCHES (WATCHES); \
  WATCH##_PTR != WATCH##_END && ((WATCH = *WATCH##_PTR), true); \
  ++WATCH##_PTR

Definition at line 158 of file watch.h.

#define all_binary_large_watches(WATCH, WATCHES) \
  watch WATCH, \
      *WATCH##_PTR = \
          (KISSAT_assert (!solver->watching), BEGIN_WATCHES (WATCHES)), \
      *const WATCH##_END = END_WATCHES (WATCHES); \
  WATCH##_PTR != WATCH##_END && ((WATCH = *WATCH##_PTR), true); \
  ++WATCH##_PTR

BEGIN_CONST_WATCHES

#define BEGIN_CONST_WATCHES

(

WS

)

Value:

  ((union watch *) kissat_begin_const_vector (solver, &(WS)))

Definition at line 120 of file watch.h.

#define BEGIN_CONST_WATCHES(WS) \
  ((union watch *) kissat_begin_const_vector (solver, &(WS)))

BEGIN_WATCHES

#define BEGIN_WATCHES

(

WS

)

Value:

  ((union watch *) kissat_begin_vector (solver, &(WS)))

Definition at line 115 of file watch.h.

#define BEGIN_WATCHES(WS) \
  ((union watch *) kissat_begin_vector (solver, &(WS)))

EMPTY_WATCHES

#define EMPTY_WATCHES

(

W

)

Value:

kissat_empty_vector (&W)

Definition at line 103 of file watch.h.

END_CONST_WATCHES

#define END_CONST_WATCHES

(

WS

)

Value:

  ((union watch *) kissat_end_const_vector (solver, &(WS)))

Definition at line 123 of file watch.h.

#define END_CONST_WATCHES(WS) \
  ((union watch *) kissat_end_const_vector (solver, &(WS)))

END_WATCHES

#define END_WATCHES

(

WS

)

Value:

((union watch *) kissat_end_vector (solver, &(WS)))

Definition at line 118 of file watch.h.

LAST_WATCH_POINTER

#define LAST_WATCH_POINTER

(

WS

)

Value:

  (watch *) kissat_last_vector_pointer (solver, &WS)

Definition at line 112 of file watch.h.

#define LAST_WATCH_POINTER(WS) \
  (watch *) kissat_last_vector_pointer (solver, &WS)

PUSH_WATCHES

#define PUSH_WATCHES	(		W,
			E )

Value:

  do { \
    KISSAT_assert (sizeof (E) == sizeof (unsigned)); \
    kissat_push_vectors (solver, &(W), (E).raw); \
  } while (0)

Definition at line 106 of file watch.h.

#define PUSH_WATCHES(W, E) \
  do { \
    KISSAT_assert (sizeof (E) == sizeof (unsigned)); \
    kissat_push_vectors (solver, &(W), (E).raw); \
  } while (0)

RELEASE_WATCHES

#define RELEASE_WATCHES

(

WS

)

Value:

kissat_release_vector (solver, &(WS))

Definition at line 126 of file watch.h.

REMOVE_WATCHES

#define REMOVE_WATCHES	(		W,
			E )

Value:

  kissat_remove_from_vector (solver, &(W), (E).raw)

Definition at line 134 of file watch.h.

#define REMOVE_WATCHES(W, E) \
  kissat_remove_from_vector (solver, &(W), (E).raw)

SET_END_OF_WATCHES

#define SET_END_OF_WATCHES	(		WS,
			P )

Value:

  do { \
    size_t SIZE = (unsigned *) (P) - kissat_begin_vector (solver, &WS); \
    kissat_resize_vector (solver, &WS, SIZE); \
  } while (0)

Definition at line 128 of file watch.h.

#define SET_END_OF_WATCHES(WS, P) \
  do { \
    size_t SIZE = (unsigned *) (P) - kissat_begin_vector (solver, &WS); \
    kissat_resize_vector (solver, &WS, SIZE); \
  } while (0)

SIZE_WATCHES

#define SIZE_WATCHES

(

W

)

Value:

kissat_size_vector (&W)

Definition at line 104 of file watch.h.

WATCHES

#define WATCHES

(

LIT

)

Value:

(solver->watches[KISSAT_assert ((LIT) < LITS), (LIT)])

Definition at line 137 of file watch.h.

Typedef Documentation

binary_watch

typedef struct binary_tagged_literal binary_watch

Definition at line 17 of file watch.h.

blocking_watch

typedef struct binary_tagged_literal blocking_watch

Definition at line 18 of file watch.h.

large_watch

typedef struct binary_tagged_reference large_watch

Definition at line 19 of file watch.h.

litpair

typedef struct litpair litpair

Definition at line 52 of file watch.h.

litriple

typedef struct litriple litriple

Definition at line 53 of file watch.h.

litwatch

typedef struct litwatch litwatch

Definition at line 51 of file watch.h.

watch

typedef typedefABC_NAMESPACE_HEADER_START union watch watch

Definition at line 14 of file watch.h.

watch_type

typedef struct binary_tagged_literal watch_type

Definition at line 16 of file watch.h.

watches

typedef vector watches

Definition at line 49 of file watch.h.

Function Documentation

kissat_connect_irredundant_large_clauses()

void kissat_connect_irredundant_large_clauses

(

struct kissat *

solver

)

Definition at line 171 of file watch.c.

                                                               {
  KISSAT_assert (!solver->watching);
  LOG ("connecting all large irredundant clauses");
 
  clause *last_irredundant = kissat_last_irredundant_clause (solver);
 
  const value *const values = solver->values;
  watches *all_watches = solver->watches;
  ward *const arena = BEGIN_STACK (solver->arena);
 
  for (all_clauses (c)) {
    if (last_irredundant && c > last_irredundant)
      break;
    if (c->redundant)
      continue;
    if (c->garbage)
      continue;
    bool satisfied = false;
    KISSAT_assert (!solver->level);
    for (all_literals_in_clause (lit, c)) {
      const value value = values[lit];
      if (value <= 0)
        continue;
      satisfied = true;
      break;
    }
    if (satisfied) {
      kissat_mark_clause_as_garbage (solver, c);
      continue;
    }
    const reference ref = (ward *) c - arena;
    kissat_inlined_connect_clause (solver, all_watches, c, ref);
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_flush_all_connected()

void kissat_flush_all_connected

(

struct kissat *

solver

)

Definition at line 104 of file watch.c.

                                                 {
  KISSAT_assert (!solver->watching);
  LOG ("flush all connected binaries and clauses");
  watches *all_watches = solver->watches;
  for (all_literals (lit))
    RELEASE_WATCHES (all_watches[lit]);
}

kissat_flush_large_connected()

void kissat_flush_large_connected

(

struct kissat *

solver

)

Definition at line 206 of file watch.c.

                                                   {
  KISSAT_assert (!solver->watching);
  LOG ("flushing large connected clause references");
  size_t flushed = 0;
  for (all_literals (lit)) {
    watches *watches = &WATCHES (lit);
    watch *begin = BEGIN_WATCHES (*watches), *q = begin;
    const watch *const end_watches = END_WATCHES (*watches), *p = q;
    while (p != end_watches) {
      const watch head = *p++;
      if (head.type.binary)
        *q++ = head;
      else
        flushed++;
    }
    SET_END_OF_WATCHES (*watches, q);
  }
  LOG ("flushed %zu large clause references", flushed);
  (void) flushed;
}

Here is the caller graph for this function:

kissat_flush_large_watches()

void kissat_flush_large_watches

(

struct kissat *

solver

)

Definition at line 112 of file watch.c.

                                                 {
  KISSAT_assert (solver->watching);
  LOG ("flush large clause watches");
  watches *all_watches = solver->watches;
  signed char *marks = solver->marks;
  for (all_literals (lit)) {
    watches *lit_watches = all_watches + lit;
    watch *begin = BEGIN_WATCHES (*lit_watches), *q = begin;
    const watch *const end = END_WATCHES (*lit_watches), *p = q;
    while (p != end) {
      const watch watch = *q++ = *p++;
      if (!watch.type.binary)
        p++, q--;
      else {
        const unsigned other = watch.binary.lit;
        if (marks[other]) {
          if (lit < other) {
            LOGBINARY (lit, other, "flushing duplicated");
            kissat_delete_binary (solver, lit, other);
          }
          q--;
        } else
          marks[other] = 1;
      }
    }
    SET_END_OF_WATCHES (*lit_watches, q);
    for (p = begin; p != q; p++) {
      KISSAT_assert (p->type.binary);
      marks[p->binary.lit] = 0;
    }
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_remove_binary_watch()

void kissat_remove_binary_watch	(	struct kissat *	solver,
		watches *	watches,
		unsigned	lit )

Definition at line 8 of file watch.c.

                                               {
  watch *const begin = BEGIN_WATCHES (*watches);
  watch *const end = END_WATCHES (*watches);
  watch *q = begin;
  watch const *p = q;
#ifndef KISSAT_NDEBUG
  bool found = false;
#endif
  while (p != end) {
    const watch watch = *q++ = *p++;
    if (!watch.type.binary) {
      *q++ = *p++;
      continue;
    }
    const unsigned other = watch.binary.lit;
    if (other != lit)
      continue;
#ifndef KISSAT_NDEBUG
    KISSAT_assert (!found);
    found = true;
#endif
    q--;
  }
  KISSAT_assert (found);
#ifdef KISSAT_COMPACT
  watches->size -= 1;
#else
  KISSAT_assert (begin + 1 <= end);
  watches->end -= 1;
#endif
  const watch empty = {.raw = INVALID_VECTOR_ELEMENT};
  end[-1] = empty;
  KISSAT_assert (solver->vectors.usable < MAX_SECTOR - 1);
  solver->vectors.usable += 1;
  kissat_check_vectors (solver);
}

kissat_remove_blocking_watch()

void kissat_remove_blocking_watch	(	struct kissat *	solver,
		watches *	watches,
		reference	ref )

Definition at line 46 of file watch.c.

                                                  {
  KISSAT_assert (solver->watching);
  watch *const begin = BEGIN_WATCHES (*watches);
  watch *const end = END_WATCHES (*watches);
  watch *q = begin;
  watch const *p = q;
#ifndef KISSAT_NDEBUG
  bool found = false;
#endif
  while (p != end) {
    const watch head = *q++ = *p++;
    if (head.type.binary)
      continue;
    const watch tail = *q++ = *p++;
    if (tail.raw != ref)
      continue;
#ifndef KISSAT_NDEBUG
    KISSAT_assert (!found);
    found = true;
#endif
    q -= 2;
  }
  KISSAT_assert (found);
#ifdef KISSAT_COMPACT
  watches->size -= 2;
#else
  KISSAT_assert (begin + 2 <= end);
  watches->end -= 2;
#endif
  const watch empty = {.raw = INVALID_VECTOR_ELEMENT};
  end[-2] = end[-1] = empty;
  KISSAT_assert (solver->vectors.usable < MAX_SECTOR - 2);
  solver->vectors.usable += 2;
  kissat_check_vectors (solver);
}

kissat_substitute_large_watch()

void kissat_substitute_large_watch	(	struct kissat *	solver,
		watches *	watches,
		watch	src,
		watch	dst )

Definition at line 83 of file watch.c.

                                                          {
  KISSAT_assert (!solver->watching);
  watch *const begin = BEGIN_WATCHES (*watches);
  const watch *const end = END_WATCHES (*watches);
#ifndef KISSAT_NDEBUG
  bool found = false;
#endif
  for (watch *p = begin; p != end; p++) {
    const watch head = *p;
    if (head.raw != src.raw)
      continue;
#ifndef KISSAT_NDEBUG
    found = true;
#endif
    *p = dst;
    break;
  }
  KISSAT_assert (found);
}

kissat_watch_large_clauses()

void kissat_watch_large_clauses

(

struct kissat *

solver

)

Definition at line 145 of file watch.c.

                                                 {
  LOG ("watching all large clauses");
  KISSAT_assert (solver->watching);
 
  const value *const values = solver->values;
  const assigned *const assigned = solver->assigned;
  watches *watches = solver->watches;
  ward *const arena = BEGIN_STACK (solver->arena);
 
  for (all_clauses (c)) {
    if (c->garbage)
      continue;
 
    unsigned *lits = c->lits;
    kissat_sort_literals (solver, values, assigned, c->size, lits);
    c->searched = 2;
 
    const reference ref = (ward *) c - arena;
    const unsigned l0 = lits[0];
    const unsigned l1 = lits[1];
 
    kissat_push_blocking_watch (solver, watches + l0, l1, ref);
    kissat_push_blocking_watch (solver, watches + l1, l0, ref);
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

STACK() [1/3]

typedef STACK

(

litpair

)

STACK() [2/3]

typedef STACK

(

litriple

)

STACK() [3/3]

typedef STACK

(

litwatch

)