ifthenelse.c File Reference

#include "ifthenelse.h"
#include "eliminate.h"
#include "gates.h"
#include "inline.h"

Include dependency graph for ifthenelse.c:

Go to the source code of this file.

Functions
bool	kissat_find_if_then_else_gate (kissat *solver, unsigned lit, unsigned negative)

Function Documentation

kissat_find_if_then_else_gate()

bool kissat_find_if_then_else_gate	(	kissat *	solver,
		unsigned	lit,
		unsigned	negative )

Definition at line 97 of file ifthenelse.c.

                                                       {
  if (!GET_OPTION (ifthenelse))
    return false;
  watches *watches = &WATCHES (lit);
  const watch *const begin = BEGIN_WATCHES (*watches);
  const watch *const end = END_WATCHES (*watches);
  if (begin == end)
    return false;
  uint64_t large_clauses = 0;
  for (const watch *p = begin; p != end; p++)
    if (!p->type.binary)
      large_clauses++;
  const uint64_t limit = GET_OPTION (eliminateocclim);
  if (large_clauses * large_clauses > limit)
    return false;
  const watch *const last = end - 1;
  uint64_t steps = 0;
  for (const watch *p1 = begin; steps < limit && p1 != last; p1++) {
    watch w1 = *p1;
    if (w1.type.binary)
      continue;
    unsigned a1, b1, c1;
    if (!get_ternary_clause (solver, p1->large.ref, &a1, &b1, &c1))
      continue;
    if (b1 == lit)
      SWAP (unsigned, a1, b1);
    if (c1 == lit)
      SWAP (unsigned, a1, c1);
    KISSAT_assert (a1 == lit);
    for (const watch *p2 = p1 + 1; steps < limit && p2 != end; p2++) {
      watch w2 = *p2;
      if (w2.type.binary)
        continue;
      unsigned a2, b2, c2;
      if (!get_ternary_clause (solver, p2->large.ref, &a2, &b2, &c2))
        continue;
      if (b2 == lit)
        SWAP (unsigned, a2, b2);
      if (c2 == lit)
        SWAP (unsigned, a2, c2);
      KISSAT_assert (a2 == lit);
      if (STRIP (b1) == STRIP (c2))
        SWAP (unsigned, b2, c2);
      if (STRIP (c1) == STRIP (c2))
        continue;
      const unsigned not_b2 = NOT (b2);
      if (b1 != not_b2)
        continue;
      solver->resolve_gate = false;
      const unsigned not_lit = NOT (lit);
      const unsigned not_c1 = NOT (c1);
      const watch *const p3 =
          find_ternary_clause (solver, &steps, not_lit, b1, not_c1);
      if (!p3)
        continue;
      const unsigned not_c2 = NOT (c2);
      const watch *const p4 =
          find_ternary_clause (solver, &steps, not_lit, b2, not_c2);
      if (!p4)
        continue;
      watch w3 = p3 < p4 ? *p3 : *p4;
      watch w4 = p3 < p4 ? *p4 : *p3;
      LOGWATCH (lit, w1, "1st if-then-else");
      LOGWATCH (lit, w2, "2nd if-then-else");
      LOGWATCH (not_lit, w3, "3rd if-then-else");
      LOGWATCH (not_lit, w4, "4th if-then-else");
      LOG ("found if-then-else gate %s = (%s ? %s : %s)", LOGLIT (lit),
           LOGLIT (NOT (b1)), LOGLIT (not_c1), LOGLIT (not_c2));
      solver->gate_eliminated = GATE_ELIMINATED (if_then_else);
      PUSH_STACK (solver->gates[negative], w1);
      PUSH_STACK (solver->gates[negative], w2);
      PUSH_STACK (solver->gates[!negative], w3);
      PUSH_STACK (solver->gates[!negative], w4);
      INC (if_then_else_extracted);
      return true;
    }
  }
  return false;
}

Here is the caller graph for this function: