weaken.h File Reference

#include "global.h"

Include dependency graph for weaken.h:

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

Go to the source code of this file.

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

Function Documentation

kissat_weaken_binary()

void kissat_weaken_binary	(	struct 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	(	struct kissat *	solver,
		unsigned	lit,
		struct 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	(	struct 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");
}