analyze.c File Reference

#include "analyze.h"
#include "backtrack.h"
#include "bump.h"
#include "deduce.h"
#include "inline.h"
#include "learn.h"
#include "minimize.h"
#include "print.h"
#include "rank.h"
#include "shrink.h"
#include "sort.h"
#include "tiers.h"
#include <inttypes.h>

Include dependency graph for analyze.c:

Go to the source code of this file.

Macros
#define	RADIX_SORT_LEVELS_LIMIT   32
#define	RANK_LEVEL(A)
#define	SMALLER_LEVEL(A, B)

Functions
void	kissat_reset_only_analyzed_literals (kissat *solver)
int	kissat_analyze (kissat *solver, clause *conflict)

Macro Definition Documentation

RADIX_SORT_LEVELS_LIMIT

#define RADIX_SORT_LEVELS_LIMIT   32

Definition at line 216 of file analyze.c.

RANK_LEVEL

#define RANK_LEVEL

(

A

)

Value:

(A)

Definition at line 218 of file analyze.c.

SMALLER_LEVEL

#define SMALLER_LEVEL	(		A,
			B )

Value:

(RANK_LEVEL (A) < RANK_LEVEL (B))

Definition at line 219 of file analyze.c.

Function Documentation

kissat_analyze()

int kissat_analyze	(	kissat *	solver,
		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

(

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: