clause.c File Reference

#include "allocate.h"
#include "collect.h"
#include "inline.h"
#include <string.h>

Include dependency graph for clause.c:

Go to the source code of this file.

Functions
void	kissat_connect_referenced (kissat *solver, reference ref)
void	kissat_connect_clause (kissat *solver, clause *c)
void	kissat_new_binary_clause (kissat *solver, unsigned first, unsigned second)
void	kissat_new_unwatched_binary_clause (kissat *solver, unsigned first, unsigned second)
reference	kissat_new_original_clause (kissat *solver)
reference	kissat_new_irredundant_clause (kissat *solver)
reference	kissat_new_redundant_clause (kissat *solver, unsigned glue)
void	kissat_mark_clause_as_garbage (kissat *solver, clause *c)
clause *	kissat_delete_clause (kissat *solver, clause *c)
void	kissat_delete_binary (kissat *solver, unsigned a, unsigned b)

Function Documentation

kissat_connect_clause()

void kissat_connect_clause	(	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	(	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	(	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	(	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	(	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	(	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

(

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

(

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	(	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	(	kissat *	solver,
		unsigned	first,
		unsigned	second )

Definition at line 127 of file clause.c.

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