deduce.c File Reference

#include "deduce.h"
#include "inline.h"
#include "promote.h"
#include "strengthen.h"

Include dependency graph for deduce.c:

Go to the source code of this file.

Functions
bool	kissat_recompute_and_promote (kissat *solver, clause *c)
clause *	kissat_deduce_first_uip_clause (kissat *solver, clause *conflict)

Function Documentation

kissat_deduce_first_uip_clause()

clause * kissat_deduce_first_uip_clause	(	kissat *	solver,
		clause *	conflict )

Definition at line 72 of file deduce.c.

                                                                          {
  START (deduce);
  KISSAT_assert (EMPTY_STACK (solver->analyzed));
  KISSAT_assert (EMPTY_STACK (solver->levels));
  KISSAT_assert (EMPTY_STACK (solver->clause));
#if defined(LOGGING) || !defined(KISSAT_NDEBUG)
  CLEAR_STACK (solver->resolvent);
#endif
  if (conflict->size > 2)
    mark_clause_as_used (solver, conflict);
  PUSH_STACK (solver->clause, INVALID_LIT);
  solver->antecedent_size = 0;
  solver->resolvent_size = 0;
  unsigned unresolved_on_current_level = 0, conflict_size = 0;
  assigned *all_assigned = solver->assigned;
  frame *frames = BEGIN_STACK (solver->frames);
  for (all_literals_in_clause (lit, conflict)) {
    KISSAT_assert (VALUE (lit) < 0);
    if (LEVEL (lit))
      conflict_size++;
    if (analyze_literal (solver, all_assigned, frames, lit))
      unresolved_on_current_level++;
  }
  KISSAT_assert (unresolved_on_current_level > 1);
  LOG ("starting with %u unresolved literals on current decision level",
       unresolved_on_current_level);
  KISSAT_assert (solver->antecedent_size == solver->resolvent_size);
  LOGRES2 ("initial");
  const bool otfs = GET_OPTION (otfs);
  unsigned const *t = END_ARRAY (solver->trail);
  unsigned uip = INVALID_LIT;
  unsigned resolved = 0;
  assigned *a = 0;
  for (;;) {
    do {
      KISSAT_assert (t > BEGIN_ARRAY (solver->trail));
      uip = *--t;
      a = ASSIGNED (uip);
    } while (!a->analyzed || a->level != solver->level);
    if (unresolved_on_current_level == 1)
      break;
    KISSAT_assert (a->reason != DECISION_REASON);
    KISSAT_assert (a->level == solver->level);
    solver->antecedent_size = 1;
    resolved++;
    if (a->binary) {
      const unsigned other = a->reason;
      LOGBINARY (uip, other, "resolving %s reason", LOGLIT (uip));
      if (analyze_literal (solver, all_assigned, frames, other))
        unresolved_on_current_level++;
    } else {
      const reference ref = a->reason;
      LOGREF (ref, "resolving %s reason", LOGLIT (uip));
      clause *reason = kissat_dereference_clause (solver, ref);
      for (all_literals_in_clause (lit, reason))
        if (lit != uip &&
            analyze_literal (solver, all_assigned, frames, lit))
          unresolved_on_current_level++;
      mark_clause_as_used (solver, reason);
    }
    KISSAT_assert (unresolved_on_current_level > 0);
    unresolved_on_current_level--;
    LOG ("after resolving %s there are %u literals left "
         "on current decision level",
         LOGLIT (uip), unresolved_on_current_level);
    KISSAT_assert (solver->resolvent_size > 0);
    solver->resolvent_size--;
#if defined(LOGGING) || !defined(KISSAT_NDEBUG)
    LOG2 ("actual antecedent size %u", solver->antecedent_size);
    REMOVE_STACK (unsigned, solver->resolvent, NOT (uip));
    KISSAT_assert (SIZE_STACK (solver->resolvent) == solver->resolvent_size);
    LOGRES2 ("new");
#endif
    if (otfs && solver->antecedent_size > 2 &&
        solver->resolvent_size < solver->antecedent_size) {
      KISSAT_assert (!a->binary);
      KISSAT_assert (solver->antecedent_size && solver->resolvent_size + 1);
      clause *reason = kissat_dereference_clause (solver, a->reason);
      KISSAT_assert (!reason->garbage);
      clause *res = kissat_on_the_fly_strengthen (solver, reason, uip);
      if (resolved == 1 && solver->resolvent_size < conflict_size) {
        KISSAT_assert (!conflict->garbage);
        KISSAT_assert (conflict_size > 2);
        kissat_on_the_fly_subsume (solver, res, conflict);
      }
      STOP (deduce);
      return res;
    }
  }
  KISSAT_assert (uip != INVALID_LIT);
  LOG ("first unique implication point %s (1st UIP)", LOGLIT (uip));
  KISSAT_assert (PEEK_STACK (solver->clause, 0) == INVALID_LIT);
  POKE_STACK (solver->clause, 0, NOT (uip));
  LOGTMP ("deduced not yet minimized 1st UIP");
  if (!solver->probing)
    ADD (literals_deduced, SIZE_STACK (solver->clause));
  STOP (deduce);
  return 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_recompute_and_promote()

bool kissat_recompute_and_promote	(	kissat *	solver,
		clause *	c )

Definition at line 31 of file deduce.c.

                                                              {
  KISSAT_assert (c->redundant);
  const unsigned old_glue = c->glue;
  const unsigned new_glue = kissat_recompute_glue (solver, c, old_glue);
  if (new_glue >= old_glue)
    return false;
  kissat_promote_clause (solver, c, new_glue);
  return true;
}

Here is the call graph for this function: