definition.c File Reference

#include "definition.h"
#include "allocate.h"
#include "gates.h"
#include "inline.h"
#include "kitten.h"
#include "print.h"

Include dependency graph for definition.c:

Go to the source code of this file.

Classes
struct	definition_extractor

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct definition_extractor	definition_extractor

Functions
bool	kissat_find_definition (kissat *solver, unsigned lit)

Typedef Documentation

definition_extractor

typedef typedefABC_NAMESPACE_IMPL_START struct definition_extractor definition_extractor

Definition at line 10 of file definition.c.

Function Documentation

kissat_find_definition()

bool kissat_find_definition	(	kissat *	solver,
		unsigned	lit )

Definition at line 93 of file definition.c.

                                                           {
  if (!GET_OPTION (definitions))
    return false;
  START (definition);
  struct kitten *kitten = solver->kitten;
  KISSAT_assert (kitten);
  kitten_clear (kitten);
  const unsigned not_lit = NOT (lit);
  definition_extractor extractor;
  extractor.lit = lit;
  extractor.solver = solver;
  extractor.watches[0] = &WATCHES (lit);
  extractor.watches[1] = &WATCHES (not_lit);
  kitten_track_antecedents (kitten);
  unsigned exported = 0;
#if !defined(KISSAT_QUIET) || !defined(KISSAT_NDEBUG)
  size_t occs[2] = {0, 0};
#endif
  for (unsigned sign = 0; sign < 2; sign++) {
    const unsigned except = sign ? not_lit : lit;
    for (all_binary_large_watches (watch, *extractor.watches[sign])) {
      if (watch.type.binary) {
        const unsigned other = watch.binary.lit;
        kitten_clause_with_id_and_exception (kitten, exported, 1, &other,
                                             INVALID_LIT);
      } else {
        const reference ref = watch.large.ref;
        clause *c = kissat_dereference_clause (solver, ref);
        kitten_clause_with_id_and_exception (kitten, exported, c->size,
                                             c->lits, except);
      }
#if !defined(KISSAT_QUIET) || !defined(KISSAT_NDEBUG)
      occs[sign]++;
#endif
      exported++;
    }
  }
  bool res = false;
  LOG ("exported %u = %zu + %zu environment clauses to sub-solver",
       exported, occs[0], occs[1]);
  INC (definitions_checked);
  const size_t limit = GET_OPTION (definitionticks);
  kitten_set_ticks_limit (kitten, limit);
  int status = kitten_solve (kitten);
  if (status == 20) {
    LOG ("sub-solver result UNSAT shows definition exists");
    uint64_t learned;
    unsigned reduced = kitten_compute_clausal_core (kitten, &learned);
    LOG ("1st sub-solver core of size %u original clauses out of %u",
         reduced, exported);
    for (int i = 2; i <= GET_OPTION (definitioncores); i++) {
      kitten_shrink_to_clausal_core (kitten);
      kitten_shuffle_clauses (kitten);
      kitten_set_ticks_limit (kitten, 10 * limit);
      int tmp = kitten_solve (kitten);
      KISSAT_assert (!tmp || tmp == 20);
      if (!tmp) {
        LOG ("aborting core extraction");
        goto ABORT;
      }
#ifndef KISSAT_NDEBUG
      unsigned previous = reduced;
#endif
      reduced = kitten_compute_clausal_core (kitten, &learned);
      LOG ("%s sub-solver core of size %u original clauses out of %u",
           FORMAT_ORDINAL (i), reduced, exported);
      KISSAT_assert (reduced <= previous);
#if defined(KISSAT_QUIET) && defined(KISSAT_NDEBUG)
      (void) reduced;
#endif
    }
    INC (definitions_extracted);
    kitten_traverse_core_ids (kitten, &extractor, traverse_definition_core);
    size_t size[2];
    size[0] = SIZE_STACK (solver->gates[0]);
    size[1] = SIZE_STACK (solver->gates[1]);
#if !defined(KISSAT_QUIET) || !defined(KISSAT_NDEBUG)
    KISSAT_assert (reduced == size[0] + size[1]);
#ifdef METRICS
    kissat_extremely_verbose (
        solver,
        "definition extracted[%" PRIu64 "] "
        "size %u = %zu + %zu clauses %.0f%% "
        "of %u = %zu + %zu (checked %" PRIu64 ")",
        solver->statistics.definitions_extracted, reduced, size[0], size[1],
        kissat_percent (reduced, exported), exported, occs[0], occs[1],
        solver->statistics.definitions_checked);
#else
    kissat_extremely_verbose (solver,
                              "definition extracted with core "
                              "size %u = %zu + %zu clauses %.0f%% "
                              "of %u = %zu + %zu",
                              reduced, size[0], size[1],
                              kissat_percent (reduced, exported), exported,
                              occs[0], occs[1]);
#endif
#endif
    unsigned unit = INVALID_LIT;
    if (!size[0]) {
      unit = not_lit;
      KISSAT_assert (size[1]);
    } else if (!size[1])
      unit = lit;
 
    if (unit != INVALID_LIT) {
      INC (definition_units);
 
      kissat_extremely_verbose (solver, "one sided core "
                                        "definition extraction yields "
                                        "failed literal");
#if !defined(KISSAT_NDEBUG) || !defined(KISSAT_NPROOFS)
      if (false
#ifndef KISSAT_NDEBUG
          || GET_OPTION (check) > 1
#endif
#ifndef KISSAT_NPROOFS
          || solver->proof
#endif
      ) {
        lemma_extractor extractor;
        extractor.solver = solver;
        extractor.unit = unit;
        extractor.lemmas = 0;
        kitten_traverse_core_clauses (kitten, &extractor,
                                      traverse_one_sided_core_lemma);
      } else
#endif
        kissat_learned_unit (solver, unit);
    }
    solver->gate_eliminated = GATE_ELIMINATED (definitions);
    solver->resolve_gate = true;
    res = true;
  } else {
  ABORT:
    LOG ("sub-solver failed to show that definition exists");
  }
  CLEAR_STACK (solver->analyzed);
  STOP (definition);
  return res;
}

Here is the call graph for this function:

Here is the caller graph for this function: