analyze.h File Reference

#include <stdbool.h>
#include "global.h"

Include dependency graph for analyze.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions
int	kissat_analyze (struct kissat *, struct clause *)
void	kissat_reset_only_analyzed_literals (struct kissat *)

Function Documentation

kissat_analyze()

int kissat_analyze	(	struct kissat *	solver,
		struct clause *	conflict )

Definition at line 529 of file analyze.c.

                                                      {
  if (solver->inconsistent) {
    KISSAT_assert (!solver->level);
    return 20;
  }
 
  START (analyze);
  if (!solver->probing) {
    update_trail_average (solver);
    update_decision_rate_average (solver);
#ifndef KISSAT_QUIET
    UPDATE_AVERAGE (level, solver->level);
#endif
  }
  int res;
  do {
    LOGCLS (conflict, "analyzing conflict %" PRIu64, CONFLICTS);
    unsigned conflict_level;
    if (one_literal_on_conflict_level (solver, conflict, &conflict_level))
      res = 1;
    else if (!conflict_level)
      res = -1;
    else if (conflict_level == 1) {
      analyze_failed_literal (solver, conflict);
      res = 1;
    } else if ((conflict =
                    kissat_deduce_first_uip_clause (solver, conflict))) {
      reset_analysis_but_not_analyzed_literals (solver);
      INC (conflicts);
      if (CONFLICTS > solver->limits.glue.conflicts)
        update_tier_limits (solver);
      res = 0; // And continue with new conflict analysis.
    } else {
      if (GET_OPTION (minimize)) {
        sort_deduced_clause (solver);
        kissat_minimize_clause (solver);
        if (GET_OPTION (shrink))
          kissat_shrink_clause (solver);
      }
      analyze_reason_side_literals (solver);
      kissat_learn_clause (solver);
      reset_analysis_but_not_analyzed_literals (solver);
      res = 1;
    }
    if (!EMPTY_STACK (solver->analyzed)) {
      if (!solver->probing && GET_OPTION (bump))
        kissat_bump_analyzed (solver);
      kissat_reset_only_analyzed_literals (solver);
    }
  } while (!res);
  STOP (analyze);
  return res > 0 ? 0 : 20;
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_reset_only_analyzed_literals()

void kissat_reset_only_analyzed_literals

(

struct kissat *

solver

)

Definition at line 328 of file analyze.c.

                                                          {
  LOG ("reset %zu analyzed variables", SIZE_STACK (solver->analyzed));
  assigned *assigned = solver->assigned;
  for (all_stack (unsigned, idx, solver->analyzed)) {
    KISSAT_assert (idx < VARS);
    struct assigned *a = assigned + idx;
    KISSAT_assert (!a->poisoned);
    KISSAT_assert (!a->removable);
    KISSAT_assert (!a->shrinkable);
    a->analyzed = false;
  }
  CLEAR_STACK (solver->analyzed);
}

Here is the caller graph for this function: