resolve.c File Reference

#include "resolve.h"
#include "eliminate.h"
#include "gates.h"
#include "inline.h"
#include "print.h"
#include <inttypes.h>
#include <string.h>

Include dependency graph for resolve.c:

Go to the source code of this file.

Functions
bool	kissat_generate_resolvents (kissat *solver, unsigned idx, unsigned *lit_ptr)

Function Documentation

kissat_generate_resolvents()

bool kissat_generate_resolvents	(	kissat *	solver,
		unsigned	idx,
		unsigned *	lit_ptr )

Definition at line 266 of file resolve.c.

                                                    {
  unsigned lit = LIT (idx);
  unsigned not_lit = NOT (lit);
 
  bool update = false;
  bool pure = false;
  uint64_t limit;
 
  {
    unsigned pos_count = occurrences_literal (solver, lit, &update);
    unsigned neg_count = occurrences_literal (solver, not_lit, &update);
 
    if (pos_count > neg_count) {
      SWAP (unsigned, lit, not_lit);
      SWAP (size_t, pos_count, neg_count);
    }
 
    const unsigned occlim = GET_OPTION (eliminateocclim);
    limit = pos_count + (uint64_t) neg_count;
 
    if (pos_count && limit > occlim) {
      LOG ("no elimination of variable %u "
           "since it has %" PRIu64 " > %u occurrences",
           idx, limit, occlim);
      return false;
    }
 
    if (pos_count) {
      const uint64_t bound = solver->bounds.eliminate.additional_clauses;
      limit += bound;
      LOG ("trying to eliminate %s "
           "limit %" PRIu64 " bound %" PRIu64,
           LOGVAR (idx), limit, bound);
    } else {
      LOG ("eliminating pure literal %s thus its variable %u", LOGLIT (lit),
           idx);
      pure = true;
    }
  }
 
  *lit_ptr = lit;
 
  INC (eliminate_attempted);
  if (pure)
    return true;
 
  const bool gates = !pure && kissat_find_gates (solver, lit);
 
  statches *const gates0 = &solver->gates[0];
  statches *const gates1 = &solver->gates[1];
 
  if (solver->values[lit]) {
    kissat_extremely_verbose (solver, "definition produced unit");
    CLEAR_STACK (*gates0);
    CLEAR_STACK (*gates1);
    return false;
  }
 
  bool failed = false;
  uint64_t resolved = 0;
 
  kissat_get_antecedents (solver, lit);
  statches *const antecedents0 = &solver->antecedents[0];
  statches *const antecedents1 = &solver->antecedents[1];
 
  if (gates) {
    LOG ("resolving gates[0] against antecedents[1] clauses");
    if (!generate_resolvents (solver, lit, gates0, antecedents1, &resolved,
                              limit))
      failed = true;
    else {
      LOG ("resolving gates[1] against antecedents[0] clauses");
      if (!generate_resolvents (solver, not_lit, gates1, antecedents0,
                                &resolved, limit)) {
        failed = true;
      } else if (solver->resolve_gate) {
        LOG ("need to resolved gates[0] against gates[1] too");
        if (!generate_resolvents (solver, lit, gates0, gates1, &resolved,
                                  limit))
          failed = true;
      }
    }
  } else {
    LOG ("no gate extracted thus resolving all clauses");
    if (!generate_resolvents (solver, lit, antecedents0, antecedents1,
                              &resolved, limit))
      failed = true;
  }
 
  CLEAR_STACK (*antecedents0);
  CLEAR_STACK (*antecedents1);
 
  if (failed) {
    LOG ("elimination of %s failed", LOGVAR (IDX (lit)));
    CLEAR_STACK (solver->resolvents);
    if (update)
      kissat_update_variable_score (solver, idx);
  }
 
  LOG ("resolved %" PRIu64 " resolvents", resolved);
 
  CLEAR_STACK (*gates0);
  CLEAR_STACK (*gates1);
 
  return !failed;
}

Here is the call graph for this function: