substitute.c File Reference

#include "substitute.h"
#include "allocate.h"
#include "backtrack.h"
#include "inline.h"
#include "print.h"
#include "proprobe.h"
#include "report.h"
#include "terminate.h"
#include "trail.h"
#include "weaken.h"
#include <string.h>

Include dependency graph for substitute.c:

Go to the source code of this file.

Functions
void	kissat_substitute (kissat *solver, bool complete)

Function Documentation

kissat_substitute()

void kissat_substitute	(	kissat *	solver,
		bool	complete )

Definition at line 606 of file substitute.c.

                                                       {
  if (solver->inconsistent)
    return;
  KISSAT_assert (solver->probing);
  KISSAT_assert (solver->watching);
  KISSAT_assert (!solver->level);
  LOG ("assuming not all large clauses watched after binary clauses");
  solver->large_clauses_watched_after_binary_clauses = false;
  if (!GET_OPTION (substitute))
    return;
  if (TERMINATED (substitute_terminated_1))
    return;
  substitute_rounds (solver, complete);
}