clause.h File Reference

#include "arena.h"
#include "literal.h"
#include "reference.h"
#include "utilities.h"
#include <stdbool.h>
#include "global.h"

Include dependency graph for clause.h:

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

Go to the source code of this file.

Classes
struct	clause

Macros
#define	LD_MAX_GLUE   19
#define	LD_MAX_USED   5
#define	MAX_GLUE   ((1u << LD_MAX_GLUE) - 1)
#define	MAX_USED   ((1u << LD_MAX_USED) - 1)
#define	SIZE_OF_CLAUSE_HEADER   ((size_t) & ((clause *) 0)->searched)
#define	BEGIN_LITS(C)
#define	END_LITS(C)
#define	all_literals_in_clause(LIT, C)

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct clause	clause

Functions
void	kissat_new_binary_clause (struct kissat *, unsigned, unsigned)
void	kissat_new_unwatched_binary_clause (struct kissat *, unsigned, unsigned)
reference	kissat_new_original_clause (struct kissat *)
reference	kissat_new_irredundant_clause (struct kissat *)
reference	kissat_new_redundant_clause (struct kissat *, unsigned glue)
void	kissat_sort_literals (struct kissat *, unsigned size, unsigned *lits)
void	kissat_connect_clause (struct kissat *, clause *)
void	kissat_connect_referenced (struct kissat *solver, reference)
clause *	kissat_delete_clause (struct kissat *, clause *)
void	kissat_delete_binary (struct kissat *, unsigned, unsigned)
void	kissat_mark_clause_as_garbage (struct kissat *, clause *)

Macro Definition Documentation

all_literals_in_clause

#define all_literals_in_clause	(		LIT,
			C )

Value:

  unsigned LIT, \
      *LIT##_PTR = BEGIN_LITS (C), *const LIT##_END = END_LITS (C); \
  LIT##_PTR != LIT##_END && ((LIT = *LIT##_PTR), true); \
  ++LIT##_PTR

Definition at line 47 of file clause.h.

#define all_literals_in_clause(LIT, C) \
  unsigned LIT, \
      *LIT##_PTR = BEGIN_LITS (C), *const LIT##_END = END_LITS (C); \
  LIT##_PTR != LIT##_END && ((LIT = *LIT##_PTR), true); \
  ++LIT##_PTR

BEGIN_LITS

#define BEGIN_LITS

(

C

)

Value:

((C)->lits)

Definition at line 44 of file clause.h.

END_LITS

#define END_LITS

(

C

)

Value:

(BEGIN_LITS (C) + (C)->size)

Definition at line 45 of file clause.h.

LD_MAX_GLUE

#define LD_MAX_GLUE   19

Definition at line 16 of file clause.h.

LD_MAX_USED

#define LD_MAX_USED   5

Definition at line 17 of file clause.h.

MAX_GLUE

#define MAX_GLUE   ((1u << LD_MAX_GLUE) - 1)

Definition at line 19 of file clause.h.

MAX_USED

#define MAX_USED   ((1u << LD_MAX_USED) - 1)

Definition at line 20 of file clause.h.

SIZE_OF_CLAUSE_HEADER

#define SIZE_OF_CLAUSE_HEADER   ((size_t) & ((clause *) 0)->searched)

Definition at line 42 of file clause.h.

Typedef Documentation

clause

typedef typedefABC_NAMESPACE_HEADER_START struct clause clause

Definition at line 14 of file clause.h.

Function Documentation

kissat_connect_clause()

void kissat_connect_clause	(	struct kissat *	solver,
		clause *	c )

Definition at line 60 of file clause.c.

                                                       {
  watches *all_watches = solver->watches;
  const reference ref = kissat_reference_clause (solver, c);
  kissat_inlined_connect_clause (solver, all_watches, c, ref);
}

kissat_connect_referenced()

void kissat_connect_referenced	(	struct kissat *	solver,
		reference	ref )

Definition at line 54 of file clause.c.

                                                               {
  watches *all_watches = solver->watches;
  clause *c = kissat_dereference_clause (solver, ref);
  kissat_inlined_connect_clause (solver, all_watches, c, ref);
}

kissat_delete_binary()

void kissat_delete_binary	(	struct kissat *	solver,
		unsigned	a,
		unsigned	b )

Definition at line 181 of file clause.c.

                                                                   {
  LOGBINARY (a, b, "delete");
  kissat_mark_removed_literal (solver, a);
  kissat_mark_removed_literal (solver, b);
  REMOVE_CHECKER_BINARY (a, b);
  DELETE_BINARY_FROM_PROOF (a, b);
  dec_clause (solver, false, true);
  INC (clauses_deleted);
}

Here is the caller graph for this function:

kissat_delete_clause()

clause * kissat_delete_clause	(	struct kissat *	solver,
		clause *	c )

Definition at line 171 of file clause.c.

                                                         {
  LOGCLS (c, "delete");
  KISSAT_assert (c->size > 2);
  KISSAT_assert (c->garbage);
  size_t bytes = kissat_actual_bytes_of_clause (c);
  SUB (arena_garbage, bytes);
  INC (clauses_deleted);
  return (clause *) ((char *) c + bytes);
}

kissat_mark_clause_as_garbage()

void kissat_mark_clause_as_garbage	(	struct kissat *	solver,
		clause *	c )

Definition at line 164 of file clause.c.

                                                               {
  KISSAT_assert (!c->garbage);
  mark_clause_as_garbage (solver, c);
  size_t bytes = kissat_actual_bytes_of_clause (c);
  ADD (arena_garbage, bytes);
}

Here is the caller graph for this function:

kissat_new_binary_clause()

void kissat_new_binary_clause	(	struct kissat *	solver,
		unsigned	first,
		unsigned	second )

Definition at line 122 of file clause.c.

                                                {
  (void) new_binary_clause (solver, false, true, first, second);
}

kissat_new_irredundant_clause()

reference kissat_new_irredundant_clause

(

struct kissat *

solver

)

Definition at line 140 of file clause.c.

                                                         {
  const unsigned size = SIZE_STACK (solver->clause);
  unsigned *lits = BEGIN_STACK (solver->clause);
  return new_clause (solver, false, false, 0, size, lits);
}

kissat_new_original_clause()

reference kissat_new_original_clause

(

struct kissat *

solver

)

Definition at line 132 of file clause.c.

                                                      {
  const unsigned size = SIZE_STACK (solver->clause);
  unsigned *lits = BEGIN_STACK (solver->clause);
  kissat_sort_literals (solver, size, lits);
  reference res = new_clause (solver, true, false, 0, size, lits);
  return res;
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_new_redundant_clause()

reference kissat_new_redundant_clause	(	struct kissat *	solver,
		unsigned	glue )

Definition at line 146 of file clause.c.

                                                                      {
  const unsigned size = SIZE_STACK (solver->clause);
  unsigned *lits = BEGIN_STACK (solver->clause);
  return new_clause (solver, false, true, glue, size, lits);
}

kissat_new_unwatched_binary_clause()

void kissat_new_unwatched_binary_clause	(	struct kissat *	solver,
		unsigned	first,
		unsigned	second )

Definition at line 127 of file clause.c.

                                                          {
  (void) new_binary_clause (solver, false, false, first, second);
}

kissat_sort_literals()

void kissat_sort_literals	(	struct kissat *	solver,
		unsigned	size,
		unsigned *	lits )

Definition at line 85 of file sort.c.

                                                         {
#ifndef INLINE_SORT
  const value *const values = solver->values;
  const assigned *const assigned = solver->assigned;
#endif
  value u = move_smallest_literal_to_front (solver, values, assigned, false,
                                            0, size, lits);
  if (size > 2)
    move_smallest_literal_to_front (solver, values, assigned, (u >= 0), 1,
                                    size, lits);
}

Here is the caller graph for this function: