gates.c File Reference

#include "gates.h"
#include "ands.h"
#include "definition.h"
#include "eliminate.h"
#include "equivalences.h"
#include "ifthenelse.h"
#include "inline.h"

Include dependency graph for gates.c:

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START size_t	kissat_mark_binaries (kissat *solver, unsigned lit)
void	kissat_unmark_binaries (kissat *solver, unsigned lit)
bool	kissat_find_gates (kissat *solver, unsigned lit)
void	kissat_get_antecedents (kissat *solver, unsigned lit)

Function Documentation

kissat_find_gates()

bool kissat_find_gates	(	kissat *	solver,
		unsigned	lit )

Definition at line 36 of file gates.c.

                                                      {
  solver->gate_eliminated = 0;
  solver->resolve_gate = false;
  if (!GET_OPTION (extract))
    return false;
  INC (gates_checked);
  const unsigned not_lit = NOT (lit);
  if (EMPTY_WATCHES (WATCHES (not_lit)))
    return false;
  bool res = false;
  if (kissat_find_equivalence_gate (solver, lit))
    res = true;
  else if (kissat_find_and_gate (solver, lit, 0))
    res = true;
  else if (kissat_find_and_gate (solver, not_lit, 1))
    res = true;
  else if (kissat_find_if_then_else_gate (solver, lit, 0))
    res = true;
  else if (kissat_find_if_then_else_gate (solver, not_lit, 1))
    res = true;
  else if (kissat_find_definition (solver, lit))
    res = true;
  if (res)
    INC (gates_extracted);
  return res;
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_get_antecedents()

void kissat_get_antecedents	(	kissat *	solver,
		unsigned	lit )

Definition at line 103 of file gates.c.

                                                           {
  get_antecedents (solver, lit, 0);
  get_antecedents (solver, NOT (lit), 1);
}

Here is the caller graph for this function:

kissat_mark_binaries()

ABC_NAMESPACE_IMPL_START size_t kissat_mark_binaries	(	kissat *	solver,
		unsigned	lit )

Definition at line 11 of file gates.c.

                                                           {
  value *marks = solver->marks;
  size_t res = 0;
  watches *watches = &WATCHES (lit);
  for (all_binary_large_watches (watch, *watches)) {
    if (!watch.type.binary)
      continue;
    const unsigned other = watch.binary.lit;
    KISSAT_assert (!solver->values[other]);
    if (marks[other])
      continue;
    marks[other] = 1;
    res++;
  }
  return res;
}

Here is the caller graph for this function:

kissat_unmark_binaries()

void kissat_unmark_binaries	(	kissat *	solver,
		unsigned	lit )

Definition at line 28 of file gates.c.

                                                           {
  value *marks = solver->marks;
  watches *watches = &WATCHES (lit);
  for (all_binary_large_watches (watch, *watches))
    if (watch.type.binary)
      marks[watch.binary.lit] = 0;
}

Here is the caller graph for this function: