propbeyond.c File Reference

#include "propbeyond.h"
#include "fastassign.h"
#include "trail.h"
#include "proplit.h"

Include dependency graph for propbeyond.c:

Go to the source code of this file.

Macros
#define	PROPAGATE_LITERAL   propagate_literal_beyond_conflicts
#define	CONTINUE_PROPAGATING_AFTER_CONFLICT
#define	PROPAGATION_TYPE   "beyond conflict"

Functions
void	kissat_propagate_beyond_conflicts (kissat *solver)

Macro Definition Documentation

CONTINUE_PROPAGATING_AFTER_CONFLICT

#define CONTINUE_PROPAGATING_AFTER_CONFLICT

Definition at line 8 of file propbeyond.c.

PROPAGATE_LITERAL

#define PROPAGATE_LITERAL   propagate_literal_beyond_conflicts

Definition at line 7 of file propbeyond.c.

PROPAGATION_TYPE

#define PROPAGATION_TYPE   "beyond conflict"

Definition at line 9 of file propbeyond.c.

Function Documentation

kissat_propagate_beyond_conflicts()

void kissat_propagate_beyond_conflicts

(

kissat *

solver

)

Definition at line 36 of file propbeyond.c.

                                                        {
  KISSAT_assert (!solver->probing);
  KISSAT_assert (solver->watching);
  KISSAT_assert (solver->warming);
  KISSAT_assert (!solver->inconsistent);
 
  START (propagate);
 
  solver->ticks = 0;
  const unsigned *saved_propagate = solver->propagate;
  propagate_literals_beyond_conflicts (solver);
  update_beyond_propagation_statistics (solver, saved_propagate);
 
  STOP (propagate);
}

Here is the caller graph for this function: