weaken.c File Reference

#include "weaken.h"
#include "inline.h"

Include dependency graph for weaken.c:

Go to the source code of this file.

Macros
#define	LOGPUSHED(SIZE)

Functions
void	kissat_weaken_clause (kissat *solver, unsigned lit, clause *c)
void	kissat_weaken_binary (kissat *solver, unsigned lit, unsigned other)
void	kissat_weaken_unit (kissat *solver, unsigned lit)

Macro Definition Documentation

LOGPUSHED

#define LOGPUSHED

(

SIZE

)

Value:

  do { \
    LOGEXT ((SIZE), END_STACK (solver->extend) - (SIZE), \
            "pushed size %zu witness labelled clause at", \
            (size_t) (SIZE)); \
  } while (0)

Definition at line 31 of file weaken.c.

#define LOGPUSHED(SIZE) \
  do { \
    LOGEXT ((SIZE), END_STACK (solver->extend) - (SIZE), \
            "pushed size %zu witness labelled clause at", \
            (size_t) (SIZE)); \
  } while (0)

Function Documentation

kissat_weaken_binary()

void kissat_weaken_binary	(	kissat *	solver,
		unsigned	lit,
		unsigned	other )

Definition at line 48 of file weaken.c.

                                                                         {
  INC (weakened);
  LOGBINARY (lit, other, "blocking on %s and weakening", LOGLIT (lit));
  push_witness_literal (solver, lit);
  push_clause_literal (solver, other);
  LOGPUSHED (2);
}

kissat_weaken_clause()

void kissat_weaken_clause	(	kissat *	solver,
		unsigned	lit,
		clause *	c )

Definition at line 38 of file weaken.c.

                                                                    {
  INC (weakened);
  LOGCLS (c, "blocking on %s and weakening", LOGLIT (lit));
  push_witness_literal (solver, lit);
  for (all_literals_in_clause (other, c))
    if (lit != other)
      push_clause_literal (solver, other);
  LOGPUSHED (c->size);
}

kissat_weaken_unit()

void kissat_weaken_unit	(	kissat *	solver,
		unsigned	lit )

Definition at line 56 of file weaken.c.

                                                       {
  INC (weakened);
  LOG ("blocking and weakening unit %s", LOGLIT (lit));
  push_witness_literal (solver, lit);
  LOGEXT (1, END_STACK (solver->extend) - 1,
          "pushed witness labelled unit clause at");
}