propinitially.c File Reference

#include "propinitially.h"
#include "analyze.h"
#include "fastassign.h"
#include "print.h"
#include "trail.h"
#include "proplit.h"

Include dependency graph for propinitially.c:

Go to the source code of this file.

Macros
#define	PROPAGATE_LITERAL   initially_propagate_literal
#define	PROPAGATION_TYPE   "initially"

Functions
bool	kissat_initially_propagate (kissat *solver)

Macro Definition Documentation

PROPAGATE_LITERAL

#define PROPAGATE_LITERAL   initially_propagate_literal

Definition at line 9 of file propinitially.c.

PROPAGATION_TYPE

#define PROPAGATION_TYPE   "initially"

Definition at line 10 of file propinitially.c.

Function Documentation

kissat_initially_propagate()

bool kissat_initially_propagate

(

kissat *

solver

)

Definition at line 36 of file propinitially.c.

                                                 {
  KISSAT_assert (!solver->probing);
  KISSAT_assert (solver->watching);
  KISSAT_assert (!solver->inconsistent);
 
  START (propagate);
 
  solver->ticks = 0;
  const unsigned *saved_propagate = solver->propagate;
  clause *conflict = initially_propagate (solver);
  update_initial_propagation_statistics (solver, saved_propagate);
  kissat_update_conflicts_and_trail (solver, conflict, true);
  if (conflict) {
    int res = kissat_analyze (solver, conflict);
    KISSAT_assert (solver->inconsistent);
    KISSAT_assert (res == 20);
    (void) res;
  }
 
  STOP (propagate);
 
  return !conflict;
}

Here is the call graph for this function:

Here is the caller graph for this function: