CaDiCaL::Stats Struct Reference

#include <stats.hpp>

Collaboration diagram for CaDiCaL::Stats:

Public Member Functions
	Stats ()
void	print (Internal *)

Public Attributes
Internal *	internal
int64_t	vars = 0
int64_t	conflicts = 0
int64_t	decisions = 0
struct {
int64_t   cover = 0
int64_t   instantiate = 0
int64_t   probe = 0
int64_t   search = 0
int64_t   transred = 0
int64_t   vivify = 0
int64_t   walk = 0
}	propagations
struct {
int64_t   search [2] = {0}
int64_t   factor = 0
int64_t   probe = 0
int64_t   sweep = 0
int64_t   ternary = 0
int64_t   vivify = 0
}	ticks
struct {
int64_t   ext_cb = 0
int64_t   eprop_call = 0
int64_t   eprop_prop = 0
int64_t   eprop_conf
int64_t   eprop_expl
int64_t   elearn_call
int64_t   elearned
int64_t   elearn_prop
int64_t   elearn_conf
int64_t   echeck_call = 0
}	ext_prop
int64_t	condassinit = 0
int64_t	condassirem = 0
int64_t	condassrem = 0
int64_t	condassvars = 0
int64_t	condautinit = 0
int64_t	condautrem = 0
int64_t	condcands = 0
int64_t	condcondinit = 0
int64_t	condcondrem
int64_t	conditioned = 0
int64_t	conditionings = 0
int64_t	condprops = 0
struct {
int64_t   block = 0
int64_t   elim = 0
int64_t   subsume = 0
int64_t   ternary = 0
int64_t   factor = 0
}	mark
struct {
int64_t   total = 0
int64_t   redundant = 0
int64_t   irredundant = 0
}	current
struct {
int64_t   total = 0
int64_t   redundant = 0
int64_t   irredundant = 0
}	added
struct {
double   process = 0
double   real = 0
}	time
struct {
int64_t   count = 0
int64_t   asymmetric = 0
int64_t   blocked = 0
int64_t   total = 0
}	cover
struct {
int64_t   tried = 0
int64_t   succeeded = 0
struct {
int64_t   one = 0
int64_t   zero = 0
}   constant
struct {
int64_t   one = 0
int64_t   zero = 0
}   forward
struct {
int64_t   one = 0
int64_t   zero = 0
}   backward
struct {
int64_t   positive = 0
int64_t   negative = 0
}   horn
}	lucky
struct {
int64_t   total = 0
int64_t   best = 0
int64_t   flipped = 0
int64_t   inverted = 0
int64_t   original = 0
int64_t   random = 0
int64_t   walk = 0
}	rephased
struct {
int64_t   count = 0
int64_t   broken = 0
int64_t   flips = 0
int64_t   minimum = 0
}	walk
struct {
int64_t   count = 0
int64_t   learned = 0
int64_t   hyper = 0
}	flush
int64_t	compacts = 0
int64_t	shuffled = 0
int64_t	restarts = 0
int64_t	restartlevels = 0
int64_t	restartstable = 0
int64_t	stabphases = 0
int64_t	stabconflicts
int64_t	rescored = 0
int64_t	reused = 0
int64_t	reusedlevels = 0
int64_t	reusedstable = 0
int64_t	sections = 0
int64_t	chrono = 0
int64_t	backtracks = 0
int64_t	improvedglue = 0
int64_t	promoted1 = 0
int64_t	promoted2 = 0
int64_t	bumped = 0
int64_t	recomputed = 0
int64_t	searched = 0
int64_t	reductions = 0
int64_t	reduced = 0
int64_t	reduced_sqrt = 0
int64_t	reduced_prct = 0
int64_t	collected = 0
int64_t	collections = 0
int64_t	hbrs = 0
int64_t	hbrsizes = 0
int64_t	hbreds = 0
int64_t	hbrsubs = 0
int64_t	instried = 0
int64_t	instantiated = 0
int64_t	instrounds = 0
int64_t	subsumed = 0
int64_t	deduplicated = 0
int64_t	deduplications = 0
int64_t	strengthened = 0
int64_t	eliminated_equi
int64_t	eliminated_and = 0
int64_t	eliminated_ite = 0
int64_t	eliminated_xor = 0
int64_t	eliminated_def
int64_t	definitions_checked = 0
int64_t	definitions_extracted = 0
int64_t	definition_units = 0
int64_t	definition_ticks = 0
int64_t	factored = 0
int64_t	factor_added = 0
int64_t	variables_extension = 0
int64_t	variables_original = 0
int64_t	literals_factored = 0
int64_t	clauses_unfactored = 0
int64_t	literals_unfactored = 0
int64_t	elimotfstr
int64_t	subirr = 0
int64_t	subred = 0
int64_t	subtried = 0
int64_t	subchecks = 0
int64_t	subchecks2 = 0
int64_t	elimotfsub
int64_t	subsumerounds = 0
int64_t	subsumephases = 0
int64_t	eagertried = 0
int64_t	eagersub
int64_t	elimres = 0
int64_t	elimrestried = 0
int64_t	elimfastrounds = 0
int64_t	elimrounds = 0
int64_t	elimphases = 0
int64_t	elimfastphases = 0
int64_t	elimcompleted = 0
int64_t	elimtried = 0
int64_t	elimsubst = 0
int64_t	elimgates = 0
int64_t	elimequivs = 0
int64_t	elimands = 0
int64_t	elimites = 0
int64_t	elimxors = 0
int64_t	elimbwsub = 0
int64_t	elimbwstr = 0
int64_t	ternres = 0
int64_t	htrs = 0
int64_t	htrs2 = 0
int64_t	htrs3 = 0
int64_t	decompositions = 0
int64_t	vivifications = 0
int64_t	vivifychecks = 0
int64_t	vivifydecs = 0
int64_t	vivifyreused = 0
int64_t	vivifysched = 0
int64_t	vivifysubs = 0
int64_t	vivifysubred = 0
int64_t	vivifysubirr = 0
int64_t	vivifystrs = 0
int64_t	vivifystrirr = 0
int64_t	vivifystred1 = 0
int64_t	vivifystred2 = 0
int64_t	vivifystred3 = 0
int64_t	vivifyunits = 0
int64_t	vivifyimplied = 0
int64_t	vivifyinst = 0
int64_t	vivifydemote = 0
int64_t	transreds = 0
int64_t	transitive = 0
struct {
int64_t   literals = 0
int64_t   clauses = 0
}	learned
int64_t	minimized = 0
int64_t	shrunken = 0
int64_t	minishrunken = 0
int64_t	irrlits = 0
struct {
int64_t   bytes = 0
int64_t   clauses = 0
int64_t   literals = 0
}	garbage
int64_t	sweep_units = 0
int64_t	sweep_flip_backbone = 0
int64_t	sweep_fixed_backbone = 0
int64_t	sweep_flipped_backbone = 0
int64_t	sweep_solved_backbone = 0
int64_t	sweep_sat_backbone = 0
int64_t	sweep_unsat_backbone = 0
int64_t	sweep_unknown_backbone = 0
int64_t	sweep_flip_equivalences = 0
int64_t	sweep_flipped_equivalences = 0
int64_t	sweep_sat_equivalences = 0
int64_t	sweep_unsat_equivalences = 0
int64_t	sweep_unknown_equivalences = 0
int64_t	sweep_solved_equivalences = 0
int64_t	sweep_equivalences = 0
int64_t	sweep_variables = 0
int64_t	sweep_completed = 0
int64_t	sweep_solved = 0
int64_t	sweep_sat = 0
int64_t	sweep_unsat = 0
int64_t	sweep_depth = 0
int64_t	sweep_environment = 0
int64_t	sweep_clauses = 0
int64_t	units = 0
int64_t	binaries = 0
int64_t	inprobingphases = 0
int64_t	probingrounds = 0
int64_t	inprobesuccess = 0
int64_t	probed = 0
int64_t	failed = 0
int64_t	hyperunary = 0
int64_t	probefailed = 0
int64_t	transredunits = 0
int64_t	blockings = 0
int64_t	blockres = 0
int64_t	blockcands = 0
int64_t	blockpured = 0
int64_t	blockpurelits = 0
int64_t	extensions = 0
int64_t	extended = 0
int64_t	weakened = 0
int64_t	weakenedlen = 0
int64_t	restorations = 0
int64_t	restored = 0
int64_t	reactivated = 0
int64_t	restoredlits = 0
int64_t	preprocessings = 0
int64_t	ilbtriggers = 0
int64_t	ilbsuccess = 0
int64_t	levelsreused = 0
int64_t	literalsreused = 0
int64_t	assumptionsreused = 0
int64_t	tierecomputed = 0
struct {
int64_t   fixed = 0
int64_t   eliminated = 0
int64_t   fasteliminated = 0
int64_t   substituted = 0
int64_t   pure = 0
}	all
struct {
int64_t   fixed = 0
int64_t   eliminated = 0
int64_t   fasteliminated = 0
int64_t   substituted = 0
int64_t   pure = 0
}	now
struct {
int64_t   strengthened = 0
int64_t   subsumed = 0
}	otfs
int64_t	unused = 0
int64_t	active = 0
int64_t	inactive = 0
std::vector< uint64_t >	bump_used = {0, 0}
std::vector< std::vector< uint64_t > >	used
struct {
int64_t   gates = 0
int64_t   ands = 0
int64_t   ites = 0
int64_t   xors = 0
int64_t   units = 0
int64_t   congruent = 0
int64_t   rounds = 0
int64_t   unary_and = 0
int64_t   unaries = 0
int64_t   rewritten_ands = 0
int64_t   simplified = 0
int64_t   simplified_ands = 0
int64_t   simplified_xors = 0
int64_t   simplified_ites = 0
int64_t   subsumed = 0
int64_t   trivial_ite = 0
int64_t   unary_ites = 0
}	congruence

Detailed Description

Definition at line 16 of file stats.hpp.

Constructor & Destructor Documentation

Stats()

CaDiCaL::Stats::Stats

(

)

Definition at line 13 of file cadical_stats.cpp.

              {
  time.real = absolute_real_time ();
  time.process = absolute_process_time ();
  walk.minimum = LONG_MAX;
  used.resize (2);
  used[0].resize (127);
  used[1].resize (127);
}

Here is the call graph for this function:

Here is the caller graph for this function:

Member Function Documentation

print()

void CaDiCaL::Stats::print

(

Internal *

internal

)

Definition at line 33 of file cadical_stats.cpp.

                                     {
 
#ifdef CADICAL_QUIET
  (void) internal;
#else
 
  Stats &stats = internal->stats;
 
  int all = internal->opts.verbose > 0 || internal->opts.stats;
#ifdef LOGGING
  if (internal->opts.log)
    all = true;
#endif // ifdef LOGGING
 
  if (internal->opts.profile)
    internal->print_profile ();
 
  double t = internal->solve_time ();
 
  int64_t propagations = 0;
  propagations += stats.propagations.cover;
  propagations += stats.propagations.probe;
  propagations += stats.propagations.search;
  propagations += stats.propagations.transred;
  propagations += stats.propagations.vivify;
  propagations += stats.propagations.walk;
 
  int64_t vivified = stats.vivifysubs + stats.vivifystrs;
  int64_t searchticks = stats.ticks.search[0] + stats.ticks.search[1];
  int64_t inprobeticks = stats.ticks.vivify + stats.ticks.probe +
                         stats.ticks.factor + stats.ticks.ternary +
                         stats.ticks.sweep;
  int64_t totalticks = searchticks + inprobeticks;
 
  size_t extendbytes = internal->external->extension.size ();
  extendbytes *= sizeof (int);
 
  SECTION ("statistics");
 
  if (all || stats.blocked) {
    PRT ("blocked:         %15" PRId64
         "   %10.2f %%  of irredundant clauses",
         stats.blocked, percent (stats.blocked, stats.added.irredundant));
    PRT ("  blockings:     %15" PRId64 "   %10.2f    internal",
         stats.blockings, relative (stats.conflicts, stats.blockings));
    PRT ("  candidates:    %15" PRId64 "   %10.2f    per blocking ",
         stats.blockcands, relative (stats.blockcands, stats.blockings));
    PRT ("  blockres:      %15" PRId64 "   %10.2f    per candidate",
         stats.blockres, relative (stats.blockres, stats.blockcands));
    PRT ("  pure:          %15" PRId64 "   %10.2f %%  of all variables",
         stats.all.pure, percent (stats.all.pure, stats.vars));
    PRT ("  pureclauses:   %15" PRId64 "   %10.2f    per pure literal",
         stats.blockpured, relative (stats.blockpured, stats.all.pure));
  }
  if (all || stats.chrono)
    PRT ("chronological:   %15" PRId64 "   %10.2f %%  of conflicts",
         stats.chrono, percent (stats.chrono, stats.conflicts));
  if (all)
    PRT ("compacts:        %15" PRId64 "   %10.2f    interval",
         stats.compacts, relative (stats.conflicts, stats.compacts));
  if (all || stats.conflicts) {
    PRT ("conflicts:       %15" PRId64 "   %10.2f    per second",
         stats.conflicts, relative (stats.conflicts, t));
    PRT ("  backtracked:   %15" PRId64 "   %10.2f %%  of conflicts",
         stats.backtracks, percent (stats.backtracks, stats.conflicts));
  }
  if (all || stats.conditioned) {
    PRT ("conditioned:     %15" PRId64
         "   %10.2f %%  of irredundant clauses",
         stats.conditioned,
         percent (stats.conditioned, stats.added.irredundant));
    PRT ("  conditionings: %15" PRId64 "   %10.2f    interval",
         stats.conditionings,
         relative (stats.conflicts, stats.conditionings));
    PRT ("  condcands:     %15" PRId64 "   %10.2f    candidate clauses",
         stats.condcands, relative (stats.condcands, stats.conditionings));
    PRT ("  condassinit:   %17.1f  %9.2f %%  initial assigned",
         relative (stats.condassinit, stats.conditionings),
         percent (stats.condassinit, stats.condassvars));
    PRT ("  condcondinit:  %17.1f  %9.2f %%  initial condition",
         relative (stats.condcondinit, stats.conditionings),
         percent (stats.condcondinit, stats.condassinit));
    PRT ("  condautinit:   %17.1f  %9.2f %%  initial autarky",
         relative (stats.condautinit, stats.conditionings),
         percent (stats.condautinit, stats.condassinit));
    PRT ("  condassrem:    %17.1f  %9.2f %%  final assigned",
         relative (stats.condassrem, stats.conditioned),
         percent (stats.condassrem, stats.condassirem));
    PRT ("  condcondrem:   %19.3f  %7.2f %%  final conditional",
         relative (stats.condcondrem, stats.conditioned),
         percent (stats.condcondrem, stats.condassrem));
    PRT ("  condautrem:    %19.3f  %7.2f %%  final autarky",
         relative (stats.condautrem, stats.conditioned),
         percent (stats.condautrem, stats.condassrem));
    PRT ("  condprops:     %15" PRId64 "   %10.2f    per candidate",
         stats.condprops, relative (stats.condprops, stats.condcands));
  }
  if (all || stats.cover.total) {
    PRT ("covered:         %15" PRId64
         "   %10.2f %%  of irredundant clauses",
         stats.cover.total,
         percent (stats.cover.total, stats.added.irredundant));
    PRT ("  coverings:     %15" PRId64 "   %10.2f    interval",
         stats.cover.count, relative (stats.conflicts, stats.cover.count));
    PRT ("  asymmetric:    %15" PRId64 "   %10.2f %%  of covered clauses",
         stats.cover.asymmetric,
         percent (stats.cover.asymmetric, stats.cover.total));
    PRT ("  blocked:       %15" PRId64 "   %10.2f %%  of covered clauses",
         stats.cover.blocked,
         percent (stats.cover.blocked, stats.cover.total));
  }
  if (all || stats.decisions) {
    PRT ("decisions:       %15" PRId64 "   %10.2f    per second",
         stats.decisions, relative (stats.decisions, t));
    PRT ("  searched:      %15" PRId64 "   %10.2f    per decision",
         stats.searched, relative (stats.searched, stats.decisions));
  }
  if (all || stats.all.eliminated) {
    PRT ("eliminated:      %15" PRId64 "   %10.2f %%  of all variables",
         stats.all.eliminated, percent (stats.all.eliminated, stats.vars));
    PRT ("  fastelim:      %15" PRId64 "   %10.2f %%  of eliminated",
         stats.all.fasteliminated,
         percent (stats.all.fasteliminated, stats.all.eliminated));
    PRT ("  elimphases:    %15" PRId64 "   %10.2f    interval",
         stats.elimphases, relative (stats.conflicts, stats.elimphases));
    PRT ("  elimrounds:    %15" PRId64 "   %10.2f    per phase",
         stats.elimrounds, relative (stats.elimrounds, stats.elimphases));
    PRT ("  elimtried:     %15" PRId64 "   %10.2f %%  eliminated",
         stats.elimtried, percent (stats.all.eliminated, stats.elimtried));
    PRT ("  elimgates:     %15" PRId64 "   %10.2f %%  gates per tried",
         stats.elimgates, percent (stats.elimgates, stats.elimtried));
    PRT ("  elimequivs:    %15" PRId64 "   %10.2f %%  equivalence gates",
         stats.elimequivs, percent (stats.elimequivs, stats.elimgates));
    PRT ("  elimands:      %15" PRId64 "   %10.2f %%  and gates",
         stats.elimands, percent (stats.elimands, stats.elimgates));
    PRT ("  elimites:      %15" PRId64 "   %10.2f %%  if-then-else gates",
         stats.elimites, percent (stats.elimites, stats.elimgates));
    PRT ("  elimxors:      %15" PRId64 "   %10.2f %%  xor gates",
         stats.elimxors, percent (stats.elimxors, stats.elimgates));
    PRT ("  elimdefs:      %15" PRId64 "   %10.2f %%  definitions",
         stats.definitions_extracted,
         percent (stats.definitions_extracted, stats.elimgates));
    PRT ("  elimsubst:     %15" PRId64 "   %10.2f %%  substituted",
         stats.elimsubst, percent (stats.elimsubst, stats.all.eliminated));
    PRT ("  elimsubstequi: %15" PRId64 "   %10.2f %%  equivalence gates",
         stats.eliminated_equi,
         percent (stats.eliminated_equi, stats.elimsubst));
    PRT ("  elimsubstands: %15" PRId64 "   %10.2f %%  and gates",
         stats.eliminated_and,
         percent (stats.eliminated_and, stats.elimsubst));
    PRT ("  elimsubstites: %15" PRId64 "   %10.2f %%  if-then-else gates",
         stats.eliminated_ite,
         percent (stats.eliminated_ite, stats.elimsubst));
    PRT ("  elimsubstxors: %15" PRId64 "   %10.2f %%  xor gates",
         stats.eliminated_xor,
         percent (stats.eliminated_xor, stats.elimsubst));
    PRT ("  elimsubstdefs: %15" PRId64 "   %10.2f %%  definitions",
         stats.eliminated_def,
         percent (stats.eliminated_def, stats.elimsubst));
    PRT ("  elimres:       %15" PRId64 "   %10.2f    per eliminated",
         stats.elimres, relative (stats.elimres, stats.all.eliminated));
    PRT ("  elimrestried:  %15" PRId64 "   %10.2f %%  per resolution",
         stats.elimrestried, percent (stats.elimrestried, stats.elimres));
    PRT ("  def checked:   %15" PRId64 "   %10.2f    per phase",
         stats.definitions_checked,
         relative (stats.definitions_checked, stats.elimphases));
    PRT ("  def extracted: %15" PRId64 "   %10.2f %%  per checked",
         stats.definitions_extracted,
         percent (stats.definitions_extracted, stats.definitions_checked));
    PRT ("  def units:     %15" PRId64 "   %10.2f %%  per checked",
         stats.definition_units,
         percent (stats.definition_units, stats.definitions_checked));
  }
  if (all || stats.ext_prop.ext_cb) {
    PRT ("ext.prop. calls: %15" PRId64 "   %10.2f %%  of queries",
         stats.ext_prop.eprop_call,
         percent (stats.ext_prop.eprop_call, stats.ext_prop.ext_cb));
    PRT ("  propagating:   %15" PRId64 "   %10.2f %%  per eprop-call",
         stats.ext_prop.eprop_prop,
         percent (stats.ext_prop.eprop_prop, stats.ext_prop.eprop_call));
    PRT ("  explained:     %15" PRId64 "   %10.2f %%  per eprop-call",
         stats.ext_prop.eprop_expl,
         percent (stats.ext_prop.eprop_expl, stats.ext_prop.eprop_call));
    PRT ("  falsified:     %15" PRId64 "   %10.2f %%  per eprop-call",
         stats.ext_prop.eprop_conf,
         percent (stats.ext_prop.eprop_conf, stats.ext_prop.eprop_call));
    PRT ("ext.clause calls:%15" PRId64 "   %10.2f %%  of queries",
         stats.ext_prop.elearn_call,
         percent (stats.ext_prop.elearn_call, stats.ext_prop.ext_cb));
    PRT ("  learned:       %15" PRId64 "   %10.2f %%  per called",
         stats.ext_prop.elearned,
         percent (stats.ext_prop.elearned, stats.ext_prop.elearn_call));
    PRT ("  conflicting:   %15" PRId64 "   %10.2f %%  per learned",
         stats.ext_prop.elearn_conf,
         percent (stats.ext_prop.elearn_conf, stats.ext_prop.elearned));
    PRT ("  propagating:   %15" PRId64 "   %10.2f %%  per learned",
         stats.ext_prop.elearn_prop,
         percent (stats.ext_prop.elearn_prop, stats.ext_prop.elearned));
    PRT ("ext.final check: %15" PRId64 "   %10.2f %%  of queries",
         stats.ext_prop.echeck_call,
         percent (stats.ext_prop.echeck_call, stats.ext_prop.ext_cb));
  }
  if (all || stats.factored) {
    PRT ("factored:        %15" PRId64 "   %10.2f %%  of variables",
         stats.factored, percent (stats.factored, internal->max_var));
    PRT ("  factor:        %15" PRId64 "   %10.2f    conflict interval",
         stats.factor, relative (stats.conflicts, stats.factor));
    PRT ("  cls factored:  %15" PRId64 "   %10.2f    per factored",
         stats.factor_added, relative (stats.factor_added, factored));
    PRT ("  lits factored: %15" PRId64 "   %10.2f    per factored",
         stats.literals_factored,
         relative (stats.literals_factored, factored));
    PRT ("  cls unfactored:%15" PRId64 "   %10.2f    per factored",
         stats.clauses_unfactored,
         relative (stats.clauses_unfactored, factored));
    PRT ("  lits unfactored:%14" PRId64 "   %10.2f    per factored",
         stats.literals_unfactored,
         relative (stats.literals_unfactored, factored));
  }
  if (all || stats.all.fixed) {
    PRT ("fixed:           %15" PRId64 "   %10.2f %%  of all variables",
         stats.all.fixed, percent (stats.all.fixed, stats.vars));
    PRT ("  failed:        %15" PRId64 "   %10.2f %%  of all variables",
         stats.failed, percent (stats.failed, stats.vars));
    PRT ("  probefailed:   %15" PRId64 "   %10.2f %%  per failed",
         stats.probefailed, percent (stats.probefailed, stats.failed));
    PRT ("  transredunits: %15" PRId64 "   %10.2f %%  per failed",
         stats.transredunits, percent (stats.transredunits, stats.failed));
    PRT ("  inprobephases: %15" PRId64 "   %10.2f    interval",
         stats.inprobingphases,
         relative (stats.conflicts, stats.inprobingphases));
    PRT ("  inprobesuccess:%15" PRId64 "   %10.2f %%  phases",
         stats.inprobesuccess,
         percent (stats.inprobesuccess, stats.inprobingphases));
    PRT ("  probingrounds: %15" PRId64 "   %10.2f    per phase",
         stats.probingrounds,
         relative (stats.probingrounds, stats.inprobingphases));
    PRT ("  probed:        %15" PRId64 "   %10.2f    per failed",
         stats.probed, relative (stats.probed, stats.failed));
    PRT ("  hbrs:          %15" PRId64 "   %10.2f    per probed",
         stats.hbrs, relative (stats.hbrs, stats.probed));
    PRT ("  hbrsizes:      %15" PRId64 "   %10.2f    per hbr",
         stats.hbrsizes, relative (stats.hbrsizes, stats.hbrs));
    PRT ("  hbreds:        %15" PRId64 "   %10.2f %%  per hbr",
         stats.hbreds, percent (stats.hbreds, stats.hbrs));
    PRT ("  hbrsubs:       %15" PRId64 "   %10.2f %%  per hbr",
         stats.hbrsubs, percent (stats.hbrsubs, stats.hbrs));
  }
  PRT ("  units:         %15" PRId64 "   %10.2f    interval", stats.units,
       relative (stats.conflicts, stats.units));
  PRT ("  binaries:      %15" PRId64 "   %10.2f    interval",
       stats.binaries, relative (stats.conflicts, stats.binaries));
  if (all || stats.flush.learned) {
    PRT ("flushed:         %15" PRId64 "   %10.2f %%  per conflict",
         stats.flush.learned,
         percent (stats.flush.learned, stats.conflicts));
    PRT ("  hyper:         %15" PRId64 "   %10.2f %%  per conflict",
         stats.flush.hyper, relative (stats.flush.hyper, stats.conflicts));
    PRT ("  flushings:     %15" PRId64 "   %10.2f    interval",
         stats.flush.count, relative (stats.conflicts, stats.flush.count));
  }
  if (all || stats.instantiated) {
    PRT ("instantiated:    %15" PRId64 "   %10.2f %%  of tried",
         stats.instantiated, percent (stats.instantiated, stats.instried));
    PRT ("  instrounds:    %15" PRId64 "   %10.2f %%  of elimrounds",
         stats.instrounds, percent (stats.instrounds, stats.elimrounds));
  }
  if (all || stats.conflicts) {
    PRT ("learned:         %15" PRId64 "   %10.2f %%  per conflict",
         stats.learned.clauses,
         percent (stats.learned.clauses, stats.conflicts));
    PRT ("@ bumped:        %15" PRId64 "   %10.2f    per learned",
         stats.bumped, relative (stats.bumped, stats.learned.clauses));
    PRT ("  recomputed:    %15" PRId64 "   %10.2f %%  per learned",
         stats.recomputed,
         percent (stats.recomputed, stats.learned.clauses));
    PRT ("  promoted1:     %15" PRId64 "   %10.2f %%  per learned",
         stats.promoted1, percent (stats.promoted1, stats.learned.clauses));
    PRT ("  promoted2:     %15" PRId64 "   %10.2f %%  per learned",
         stats.promoted2, percent (stats.promoted2, stats.learned.clauses));
    PRT ("  improvedglue:  %15" PRId64 "   %10.2f %%  per learned",
         stats.improvedglue,
         percent (stats.improvedglue, stats.learned.clauses));
  }
  if (all || stats.lucky.succeeded) {
    PRT ("lucky:           %15" PRId64 "   %10.2f %%  of tried",
         stats.lucky.succeeded,
         percent (stats.lucky.succeeded, stats.lucky.tried));
    PRT ("  constantzero   %15" PRId64 "   %10.2f %%  of tried",
         stats.lucky.constant.zero,
         percent (stats.lucky.constant.zero, stats.lucky.tried));
    PRT ("  constantone    %15" PRId64 "   %10.2f %%  of tried",
         stats.lucky.constant.one,
         percent (stats.lucky.constant.one, stats.lucky.tried));
    PRT ("  backwardone    %15" PRId64 "   %10.2f %%  of tried",
         stats.lucky.backward.one,
         percent (stats.lucky.backward.one, stats.lucky.tried));
    PRT ("  backwardzero   %15" PRId64 "   %10.2f %%  of tried",
         stats.lucky.backward.zero,
         percent (stats.lucky.backward.zero, stats.lucky.tried));
    PRT ("  forwardone     %15" PRId64 "   %10.2f %%  of tried",
         stats.lucky.forward.one,
         percent (stats.lucky.forward.one, stats.lucky.tried));
    PRT ("  forwardzero    %15" PRId64 "   %10.2f %%  of tried",
         stats.lucky.forward.zero,
         percent (stats.lucky.forward.zero, stats.lucky.tried));
    PRT ("  positivehorn   %15" PRId64 "   %10.2f %%  of tried",
         stats.lucky.horn.positive,
         percent (stats.lucky.horn.positive, stats.lucky.tried));
    PRT ("  negativehorn   %15" PRId64 "   %10.2f %%  of tried",
         stats.lucky.horn.negative,
         percent (stats.lucky.horn.negative, stats.lucky.tried));
  }
  PRT ("  extendbytes:   %15zd   %10.2f    bytes and MB", extendbytes,
       extendbytes / (double) (1l << 20));
  if (all || stats.learned.clauses)
    PRT ("learned_lits:    %15" PRId64 "   %10.2f %%  learned literals",
         stats.learned.literals,
         percent (stats.learned.literals, stats.learned.literals));
  PRT ("minimized:       %15" PRId64 "   %10.2f %%  learned literals",
       stats.minimized, percent (stats.minimized, stats.learned.literals));
  PRT ("shrunken:        %15" PRId64 "   %10.2f %%  learned literals",
       stats.shrunken, percent (stats.shrunken, stats.learned.literals));
  PRT ("minishrunken:    %15" PRId64 "   %10.2f %%  learned literals",
       stats.minishrunken,
       percent (stats.minishrunken, stats.learned.literals));
 
  if (all || stats.conflicts) {
    PRT ("otfs:            %15" PRId64 "   %10.2f %%  of conflict",
         stats.otfs.subsumed + stats.otfs.strengthened,
         percent (stats.otfs.subsumed + stats.otfs.strengthened,
                  stats.conflicts));
    PRT ("  subsumed       %15" PRId64 "   %10.2f %%  of conflict",
         stats.otfs.subsumed,
         percent (stats.otfs.subsumed, stats.conflicts));
    PRT ("  strengthened   %15" PRId64 "   %10.2f %%  of conflict",
         stats.otfs.strengthened,
         percent (stats.otfs.strengthened, stats.conflicts));
  }
 
  PRT ("propagations:    %15" PRId64 "   %10.2f M  per second",
       propagations, relative (propagations / 1e6, t));
  PRT ("  coverprops:    %15" PRId64 "   %10.2f %%  of propagations",
       stats.propagations.cover,
       percent (stats.propagations.cover, propagations));
  PRT ("  probeprops:    %15" PRId64 "   %10.2f %%  of propagations",
       stats.propagations.probe,
       percent (stats.propagations.probe, propagations));
  PRT ("  searchprops:   %15" PRId64 "   %10.2f %%  of propagations",
       stats.propagations.search,
       percent (stats.propagations.search, propagations));
  PRT ("  transredprops: %15" PRId64 "   %10.2f %%  of propagations",
       stats.propagations.transred,
       percent (stats.propagations.transred, propagations));
  PRT ("  vivifyprops:   %15" PRId64 "   %10.2f %%  of propagations",
       stats.propagations.vivify,
       percent (stats.propagations.vivify, propagations));
  PRT ("  walkprops:     %15" PRId64 "   %10.2f %%  of propagations",
       stats.propagations.walk,
       percent (stats.propagations.walk, propagations));
  if (all || stats.reactivated) {
    PRT ("reactivated:     %15" PRId64 "   %10.2f %%  of all variables",
         stats.reactivated, percent (stats.reactivated, stats.vars));
  }
  if (all || stats.reduced) {
    PRT ("reduced:         %15" PRId64 "   %10.2f %%  per conflict",
         stats.reduced, percent (stats.reduced, stats.conflicts));
    PRT ("  reductions:    %15" PRId64 "   %10.2f    interval",
         stats.reductions, relative (stats.conflicts, stats.reductions));
    PRT ("  sqrt scheme:   %15" PRId64 "   %10.2f %%  reductions",
         stats.reduced_sqrt,
         relative (stats.reduced_sqrt, stats.reductions));
    PRT ("  prct scheme:   %15" PRId64 "   %10.2f %%  reductions",
         stats.reduced_prct,
         relative (stats.reduced_prct, stats.reductions));
    PRT ("  collections:   %15" PRId64 "   %10.2f    interval",
         stats.collections, relative (stats.conflicts, stats.collections));
  }
  if (all || stats.rephased.total) {
    PRT ("rephased:        %15" PRId64 "   %10.2f    interval",
         stats.rephased.total,
         relative (stats.conflicts, stats.rephased.total));
    PRT ("  rephasedbest:  %15" PRId64 "   %10.2f %%  rephased best",
         stats.rephased.best,
         percent (stats.rephased.best, stats.rephased.total));
    PRT ("  rephasedflip:  %15" PRId64 "   %10.2f %%  rephased flipping",
         stats.rephased.flipped,
         percent (stats.rephased.flipped, stats.rephased.total));
    PRT ("  rephasedinv:   %15" PRId64 "   %10.2f %%  rephased inverted",
         stats.rephased.inverted,
         percent (stats.rephased.inverted, stats.rephased.total));
    PRT ("  rephasedorig:  %15" PRId64 "   %10.2f %%  rephased original",
         stats.rephased.original,
         percent (stats.rephased.original, stats.rephased.total));
    PRT ("  rephasedrand:  %15" PRId64 "   %10.2f %%  rephased random",
         stats.rephased.random,
         percent (stats.rephased.random, stats.rephased.total));
    PRT ("  rephasedwalk:  %15" PRId64 "   %10.2f %%  rephased walk",
         stats.rephased.walk,
         percent (stats.rephased.walk, stats.rephased.total));
  }
  if (all)
    PRT ("rescored:        %15" PRId64 "   %10.2f    interval",
         stats.rescored, relative (stats.conflicts, stats.rescored));
  if (all || stats.restarts) {
    PRT ("restarts:        %15" PRId64 "   %10.2f    interval",
         stats.restarts, relative (stats.conflicts, stats.restarts));
    PRT ("  reused:        %15" PRId64 "   %10.2f %%  per restart",
         stats.reused, percent (stats.reused, stats.restarts));
    PRT ("  reusedlevels:  %15" PRId64 "   %10.2f %%  per restart levels",
         stats.reusedlevels,
         percent (stats.reusedlevels, stats.restartlevels));
  }
  if (all || stats.restored) {
    PRT ("restored:        %15" PRId64 "   %10.2f %%  per weakened",
         stats.restored, percent (stats.restored, stats.weakened));
    PRT ("  restorations:  %15" PRId64 "   %10.2f %%  per extension",
         stats.restorations,
         percent (stats.restorations, stats.extensions));
    PRT ("  literals:      %15" PRId64 "   %10.2f    per restored clause",
         stats.restoredlits, relative (stats.restoredlits, stats.restored));
  }
  if (all || stats.stabphases) {
    PRT ("stabilizing:     %15" PRId64 "   %10.2f %%  of conflicts",
         stats.stabphases, percent (stats.stabconflicts, stats.conflicts));
    PRT ("  restartstab:   %15" PRId64 "   %10.2f %%  of all restarts",
         stats.restartstable,
         percent (stats.restartstable, stats.restarts));
    PRT ("  reusedstab:    %15" PRId64 "   %10.2f %%  per stable restarts",
         stats.reusedstable,
         percent (stats.reusedstable, stats.restartstable));
  }
  if (all || stats.all.substituted) {
    PRT ("substituted:     %15" PRId64 "   %10.2f %%  of all variables",
         stats.all.substituted,
         percent (stats.all.substituted, stats.vars));
    PRT ("  decompositions:%15" PRId64 "   %10.2f    per phase",
         stats.decompositions,
         relative (stats.decompositions, stats.inprobingphases));
  }
  if (all || stats.sweep_equivalences) {
    PRT ("sweep equivs:    %15" PRId64 "   %10.2f %%  of swept variables",
         stats.sweep_equivalences,
         percent (stats.sweep_equivalences, stats.sweep_variables));
    PRT ("  sweepings:     %15" PRId64 "   %10.2f    vars per sweeping",
         stats.sweep, relative (stats.sweep_variables, stats.sweep));
    PRT ("  swept vars:    %15" PRId64 "   %10.2f %%  of all variables",
         stats.sweep_variables,
         percent (stats.sweep_variables, stats.vars));
    PRT ("  sweep units:   %15" PRId64 "   %10.2f %%  of all variables",
         stats.sweep_units, percent (stats.sweep_units, stats.vars));
    PRT ("  solved:        %15" PRId64 "   %10.2f    per swept variable",
         stats.sweep_solved,
         relative (stats.sweep_solved, stats.sweep_variables));
    PRT ("  sat:           %15" PRId64 "   %10.2f %%  solved",
         stats.sweep_sat, percent (stats.sweep_sat, stats.sweep_solved));
    PRT ("  unsat:         %15" PRId64 "   %10.2f %%  solved",
         stats.sweep_unsat,
         percent (stats.sweep_unsat, stats.sweep_solved));
    PRT ("  backbone solved:%14" PRId64 "   %10.2f %%  solved",
         stats.sweep_solved_backbone,
         percent (stats.sweep_solved_backbone, stats.sweep_solved));
    PRT ("    sat:         %15" PRId64 "   %10.2f %%  backbone solved",
         stats.sweep_sat_backbone,
         percent (stats.sweep_sat_backbone, stats.sweep_solved_backbone));
    PRT ("    unsat:       %15" PRId64 "   %10.2f %%  backbone solved",
         stats.sweep_unsat_backbone,
         percent (stats.sweep_unsat_backbone, stats.sweep_solved_backbone));
    PRT ("    unknown:     %15" PRId64 "   %10.2f %%  backbone solved",
         stats.sweep_unknown_backbone,
         percent (stats.sweep_unknown_backbone,
                  stats.sweep_solved_backbone));
    PRT ("    fixed:       %15" PRId64 "   %10.2f   per swept variable",
         stats.sweep_fixed_backbone,
         relative (stats.sweep_fixed_backbone, stats.sweep_variables));
    PRT ("    flip:        %15" PRId64 "   %10.2f   per swept variable",
         stats.sweep_flip_backbone,
         relative (stats.sweep_flip_backbone, stats.sweep_variables));
    PRT ("    flipped:     %15" PRId64 "   %10.2f %%  of backbone flip",
         stats.sweep_flipped_backbone,
         percent (stats.sweep_flipped_backbone, stats.sweep_flip_backbone));
    PRT ("  equiv solved:  %15" PRId64 "   %10.2f %%  solved",
         stats.sweep_solved_equivalences,
         percent (stats.sweep_solved_equivalences, stats.sweep_solved));
    PRT ("    sat:         %15" PRId64 "   %10.2f %%  equiv solved",
         stats.sweep_sat_equivalences,
         percent (stats.sweep_sat_equivalences,
                  stats.sweep_solved_equivalences));
    PRT ("    unsat:       %15" PRId64 "   %10.2f %%  equiv solved",
         stats.sweep_unsat_equivalences,
         percent (stats.sweep_unsat_equivalences,
                  stats.sweep_solved_equivalences));
    PRT ("    unknown:     %15" PRId64 "   %10.2f %%  equiv solved",
         stats.sweep_unknown_equivalences,
         percent (stats.sweep_unknown_equivalences,
                  stats.sweep_solved_equivalences));
    PRT ("    flip:        %15" PRId64 "   %10.2f    per swept variable",
         stats.sweep_flip_equivalences,
         relative (stats.sweep_flip_equivalences, stats.sweep_variables));
    PRT ("    flipped:     %15" PRId64 "   %10.2f %%  of equiv flip",
         stats.sweep_flipped_equivalences,
         percent (stats.sweep_flipped_equivalences,
                  stats.sweep_flip_equivalences));
    PRT ("  depth:         %15" PRId64 "   %10.2f    per swept variable",
         stats.sweep_depth,
         relative (stats.sweep_depth, stats.sweep_variables));
    PRT ("  environment:   %15" PRId64 "   %10.2f    per swept variable",
         stats.sweep_environment,
         relative (stats.sweep_environment, stats.sweep_variables));
    PRT ("  clauses:       %15" PRId64 "   %10.2f    per swept variable",
         stats.sweep_clauses,
         relative (stats.sweep_clauses, stats.sweep_variables));
    PRT ("  completed:     %15" PRId64 "   %10.2f    sweeps to complete",
         stats.sweep_completed,
         relative (stats.sweep, stats.sweep_completed));
  }
  if (all || stats.subsumed) {
    PRT ("subsumed:        %15" PRId64 "   %10.2f %%  of all clauses",
         stats.subsumed, percent (stats.subsumed, stats.added.total));
    PRT ("  subsumephases: %15" PRId64 "   %10.2f    interval",
         stats.subsumephases,
         relative (stats.conflicts, stats.subsumephases));
    PRT ("  subsumerounds: %15" PRId64 "   %10.2f    per phase",
         stats.subsumerounds,
         relative (stats.subsumerounds, stats.subsumephases));
    PRT ("  deduplicated:  %15" PRId64 "   %10.2f %%  per subsumed",
         stats.deduplicated, percent (stats.deduplicated, stats.subsumed));
    PRT ("  transreds:     %15" PRId64 "   %10.2f    interval",
         stats.transreds, relative (stats.conflicts, stats.transreds));
    PRT ("  transitive:    %15" PRId64 "   %10.2f %%  per subsumed",
         stats.transitive, percent (stats.transitive, stats.subsumed));
    PRT ("  subirr:        %15" PRId64 "   %10.2f %%  of subsumed",
         stats.subirr, percent (stats.subirr, stats.subsumed));
    PRT ("  subred:        %15" PRId64 "   %10.2f %%  of subsumed",
         stats.subred, percent (stats.subred, stats.subsumed));
    PRT ("  subtried:      %15" PRId64 "   %10.2f    tried per subsumed",
         stats.subtried, relative (stats.subtried, stats.subsumed));
    PRT ("  subchecks:     %15" PRId64 "   %10.2f    per tried",
         stats.subchecks, relative (stats.subchecks, stats.subtried));
    PRT ("  subchecks2:    %15" PRId64 "   %10.2f %%  per subcheck",
         stats.subchecks2, percent (stats.subchecks2, stats.subchecks));
    PRT ("  elimotfsub:    %15" PRId64 "   %10.2f %%  of subsumed",
         stats.elimotfsub, percent (stats.elimotfsub, stats.subsumed));
    PRT ("  elimbwsub:     %15" PRId64 "   %10.2f %%  of subsumed",
         stats.elimbwsub, percent (stats.elimbwsub, stats.subsumed));
    PRT ("  eagersub:      %15" PRId64 "   %10.2f %%  of subsumed",
         stats.eagersub, percent (stats.eagersub, stats.subsumed));
    PRT ("  eagertried:    %15" PRId64 "   %10.2f    tried per eagersub",
         stats.eagertried, relative (stats.eagertried, stats.eagersub));
  }
  if (all || stats.strengthened) {
    PRT ("strengthened:    %15" PRId64 "   %10.2f %%  of all clauses",
         stats.strengthened,
         percent (stats.strengthened, stats.added.total));
    PRT ("  elimotfstr:    %15" PRId64 "   %10.2f %%  of strengthened",
         stats.elimotfstr, percent (stats.elimotfstr, stats.strengthened));
    PRT ("  elimbwstr:     %15" PRId64 "   %10.2f %%  of strengthened",
         stats.elimbwstr, percent (stats.elimbwstr, stats.strengthened));
  }
  if (all || stats.htrs) {
    PRT ("ternary:         %15" PRId64 "   %10.2f %%  of resolved",
         stats.htrs, percent (stats.htrs, stats.ternres));
    PRT ("  phases:        %15" PRId64 "   %10.2f    interval",
         stats.ternary, relative (stats.conflicts, stats.ternary));
    PRT ("  htr3:          %15" PRId64
         "   %10.2f %%  ternary hyper ternres",
         stats.htrs3, percent (stats.htrs3, stats.htrs));
    PRT ("  htr2:          %15" PRId64 "   %10.2f %%  binary hyper ternres",
         stats.htrs2, percent (stats.htrs2, stats.htrs));
  }
  PRT ("ticks:           %15" PRId64 "   %10.2f    propagation", totalticks,
       relative (totalticks, stats.propagations.search));
  PRT (" searchticks:    %15" PRId64 "   %10.2f %%  totalticks",
       searchticks, percent (searchticks, totalticks));
  PRT ("   stableticks:  %15" PRId64 "   %10.2f %%  searchticks",
       stats.ticks.search[1], percent (stats.ticks.search[1], searchticks));
  PRT ("   unstableticks:%15" PRId64 "   %10.2f %%  searchticks",
       stats.ticks.search[0], percent (stats.ticks.search[0], searchticks));
  PRT (" inprobeticks:   %15" PRId64 "   %10.2f %%  totalticks",
       inprobeticks, percent (inprobeticks, totalticks));
  PRT ("   factorticks:  %15" PRId64 "   %10.2f %%  searchticks",
       stats.ticks.factor, percent (stats.ticks.factor, searchticks));
  PRT ("   probeticks:   %15" PRId64 "   %10.2f %%  searchticks",
       stats.ticks.probe, percent (stats.ticks.probe, searchticks));
  PRT ("   sweepticks:   %15" PRId64 "   %10.2f %%  searchticks",
       stats.ticks.sweep, percent (stats.ticks.sweep, searchticks));
  PRT ("   ternaryticks: %15" PRId64 "   %10.2f %%  searchticks",
       stats.ticks.ternary, percent (stats.ticks.ternary, searchticks));
  PRT ("   vivifyticks:  %15" PRId64 "   %10.2f %%  searchticks",
       stats.ticks.vivify, percent (stats.ticks.vivify, searchticks));
  if (all) {
    PRT ("tier recomputed: %15" PRId64 "   %10.2f    interval",
         stats.tierecomputed,
         relative (stats.conflicts, stats.tierecomputed));
  }
  if (all || stats.ilbtriggers) {
    PRT ("trail reuses:    %15" PRId64 "   %10.2f %%  of incremental calls",
         stats.ilbsuccess, percent (stats.ilbsuccess, stats.ilbtriggers));
    PRT ("  levels:        %15" PRId64 "   %10.2f    per reuse",
         stats.levelsreused,
         relative (stats.levelsreused, stats.ilbsuccess));
    PRT ("  literals:      %15" PRId64 "   %10.2f    per reuse",
         stats.literalsreused,
         relative (stats.literalsreused, stats.ilbsuccess));
    PRT ("  assumptions:   %15" PRId64 "   %10.2f    per reuse",
         stats.assumptionsreused,
         relative (stats.assumptionsreused, stats.ilbsuccess));
  }
  if (all || vivified) {
    PRT ("vivified:        %15" PRId64 "   %10.2f %%  of all clauses",
         vivified, percent (vivified, stats.added.total));
    PRT ("  vivifications: %15" PRId64 "   %10.2f    interval",
         stats.vivifications,
         relative (stats.conflicts, stats.vivifications));
    PRT ("  vivifychecks:  %15" PRId64 "   %10.2f %%  per conflict",
         stats.vivifychecks, percent (stats.vivifychecks, stats.conflicts));
    PRT ("  vivifysched:   %15" PRId64 "   %10.2f %%  checks per scheduled",
         stats.vivifysched,
         percent (stats.vivifychecks, stats.vivifysched));
    PRT ("  vivifyunits:   %15" PRId64 "   %10.2f %%  per vivify check",
         stats.vivifyunits,
         percent (stats.vivifyunits, stats.vivifychecks));
    PRT ("  vivifyinst:    %15" PRId64 "   %10.2f %%  per vivify check",
         stats.vivifyinst, percent (stats.vivifyinst, stats.vivifychecks));
    PRT ("  vivifysubs:    %15" PRId64 "   %10.2f %%  per subsumed",
         stats.vivifysubs, percent (stats.vivifysubs, stats.subsumed));
    PRT ("  vivifysubred:  %15" PRId64 "   %10.2f %%  per subs",
         stats.vivifysubred,
         percent (stats.vivifysubred, stats.vivifysubs));
    PRT ("  vivifysubirr:  %15" PRId64 "   %10.2f %%  per subs",
         stats.vivifysubirr,
         percent (stats.vivifysubirr, stats.vivifysubs));
    PRT ("  vivifystrs:    %15" PRId64 "   %10.2f %%  per strengthened",
         stats.vivifystrs, percent (stats.vivifystrs, stats.strengthened));
    PRT ("  vivifystrirr:  %15" PRId64 "   %10.2f %%  per vivifystrs",
         stats.vivifystrirr,
         percent (stats.vivifystrirr, stats.vivifystrs));
    PRT ("  vivifystred1:  %15" PRId64 "   %10.2f %%  per vivifystrs",
         stats.vivifystred1,
         percent (stats.vivifystred1, stats.vivifystrs));
    PRT ("  vivifystred2:  %15" PRId64 "   %10.2f %%  per viviyfstrs",
         stats.vivifystred2,
         percent (stats.vivifystred2, stats.vivifystrs));
    PRT ("  vivifystred3:  %15" PRId64 "   %10.2f %%  per vivifystrs",
         stats.vivifystred3,
         percent (stats.vivifystred3, stats.vivifystrs));
    PRT ("  vivifydemote:  %15" PRId64 "   %10.2f %%  per vivifystrs",
         stats.vivifydemote,
         percent (stats.vivifydemote, stats.vivifystrs));
    PRT ("  vivifydecs:    %15" PRId64 "   %10.2f    per checks",
         stats.vivifydecs, relative (stats.vivifydecs, stats.vivifychecks));
    PRT ("  vivifyreused:  %15" PRId64 "   %10.2f %%  per decision",
         stats.vivifyreused,
         percent (stats.vivifyreused, stats.vivifydecs));
  }
  if (all || stats.walk.count) {
    PRT ("walked:          %15" PRId64 "   %10.2f    interval",
         stats.walk.count, relative (stats.conflicts, stats.walk.count));
#ifndef CADICAL_QUIET
    if (internal->profiles.walk.value > 0)
      PRT ("  flips:         %15" PRId64 "   %10.2f M  per second",
           stats.walk.flips,
           relative (1e-6 * stats.walk.flips,
                     internal->profiles.walk.value));
    else
#endif
      PRT ("  flips:         %15" PRId64 "   %10.2f    per walk",
           stats.walk.flips, relative (stats.walk.flips, stats.walk.count));
    if (stats.walk.minimum < LONG_MAX)
      PRT ("  minimum:       %15" PRId64 "   %10.2f %%  clauses",
           stats.walk.minimum,
           percent (stats.walk.minimum, stats.added.irredundant));
    PRT ("  broken:        %15" PRId64 "   %10.2f    per flip",
         stats.walk.broken, relative (stats.walk.broken, stats.walk.flips));
  }
  if (all || stats.weakened) {
    PRT ("weakened:        %15" PRId64 "   %10.2f    average size",
         stats.weakened, relative (stats.weakenedlen, stats.weakened));
    PRT ("  extensions:    %15" PRId64 "   %10.2f    interval",
         stats.extensions, relative (stats.conflicts, stats.extensions));
    PRT ("  flipped:       %15" PRId64 "   %10.2f    per weakened",
         stats.extended, relative (stats.extended, stats.weakened));
  }
 
  if (all || stats.congruence.gates) {
    PRT ("congruence:      %15" PRId64 "   %10.2f    interval",
         stats.congruence.rounds,
         relative (stats.conflicts, stats.congruence.rounds));
    PRT ("   units:        %15" PRId64 "   %10.2f    per congruent",
         stats.congruence.units,
         relative (stats.congruence.units, stats.congruence.congruent));
    PRT ("   cong-and:     %15" PRId64 "   %10.2f    per found gates",
         stats.congruence.ands,
         relative (stats.congruence.ands, stats.congruence.gates));
    PRT ("   cong-ite:     %15" PRId64 "   %10.2f    per found gates",
         stats.congruence.ites,
         relative (stats.congruence.ites, stats.congruence.gates));
    PRT ("   cong-xor:     %15" PRId64 "   %10.2f    per found gates",
         stats.congruence.xors,
         relative (stats.congruence.xors, stats.congruence.gates));
    PRT ("   congruent:    %15" PRId64 "   %10.2f    per round",
         stats.congruence.congruent,
         relative (stats.congruence.rounds, stats.congruence.congruent));
    PRT ("   unaries:      %15" PRId64 "   %10.2f    per round",
         stats.congruence.unaries,
         relative (stats.congruence.rounds, stats.congruence.unaries));
    PRT ("   rewri.-ands:  %15" PRId64 "   %10.2f    per round",
         stats.congruence.rewritten_ands,
         relative (stats.congruence.rounds,
                   stats.congruence.rewritten_ands));
    PRT ("   subsumed:     %15" PRId64 "   %10.2f    per round",
         stats.congruence.subsumed,
         relative (stats.congruence.rounds, stats.congruence.subsumed));
  }
 
  LINE ();
  MSG ("%sseconds are measured in %s time for solving%s",
       tout.magenta_code (), internal->opts.realtime ? "real" : "process",
       tout.normal_code ());
 
#endif // ifndef CADICAL_QUIET
}

Here is the call graph for this function:

Member Data Documentation

active

int64_t CaDiCaL::Stats::active = 0

Definition at line 340 of file stats.hpp.

[struct]

struct { ... } CaDiCaL::Stats::added

[struct]

struct { ... } CaDiCaL::Stats::all

ands

int64_t CaDiCaL::Stats::ands = 0

Definition at line 347 of file stats.hpp.

assumptionsreused

int64_t CaDiCaL::Stats::assumptionsreused = 0

Definition at line 323 of file stats.hpp.

asymmetric

int64_t CaDiCaL::Stats::asymmetric = 0

Definition at line 97 of file stats.hpp.

backtracks

int64_t CaDiCaL::Stats::backtracks = 0

Definition at line 150 of file stats.hpp.

[struct]

struct { ... } CaDiCaL::Stats::backward

best

int64_t CaDiCaL::Stats::best = 0

Definition at line 115 of file stats.hpp.

binaries

int64_t CaDiCaL::Stats::binaries = 0

Definition at line 293 of file stats.hpp.

block

int64_t CaDiCaL::Stats::block = 0

Definition at line 78 of file stats.hpp.

blockcands

int64_t CaDiCaL::Stats::blockcands = 0

Definition at line 305 of file stats.hpp.

blocked

int64_t CaDiCaL::Stats::blocked = 0

Definition at line 98 of file stats.hpp.

blockings

int64_t CaDiCaL::Stats::blockings = 0

Definition at line 302 of file stats.hpp.

blockpured

int64_t CaDiCaL::Stats::blockpured = 0

Definition at line 306 of file stats.hpp.

blockpurelits

int64_t CaDiCaL::Stats::blockpurelits = 0

Definition at line 307 of file stats.hpp.

blockres

int64_t CaDiCaL::Stats::blockres = 0

Definition at line 304 of file stats.hpp.

broken

int64_t CaDiCaL::Stats::broken = 0

Definition at line 125 of file stats.hpp.

bump_used

std::vector<uint64_t> CaDiCaL::Stats::bump_used = {0, 0}

Definition at line 342 of file stats.hpp.

{0, 0};

bumped

int64_t CaDiCaL::Stats::bumped = 0

Definition at line 154 of file stats.hpp.

bytes

int64_t CaDiCaL::Stats::bytes = 0

Definition at line 262 of file stats.hpp.

chrono

int64_t CaDiCaL::Stats::chrono = 0

Definition at line 149 of file stats.hpp.

clauses

int64_t CaDiCaL::Stats::clauses = 0

Definition at line 254 of file stats.hpp.

clauses_unfactored

int64_t CaDiCaL::Stats::clauses_unfactored = 0

Definition at line 194 of file stats.hpp.

collected

int64_t CaDiCaL::Stats::collected = 0

Definition at line 161 of file stats.hpp.

collections

int64_t CaDiCaL::Stats::collections = 0

Definition at line 162 of file stats.hpp.

compacts

int64_t CaDiCaL::Stats::compacts = 0

Definition at line 136 of file stats.hpp.

condassinit

int64_t CaDiCaL::Stats::condassinit = 0

Definition at line 63 of file stats.hpp.

condassirem

int64_t CaDiCaL::Stats::condassirem = 0

Definition at line 64 of file stats.hpp.

condassrem

int64_t CaDiCaL::Stats::condassrem = 0

Definition at line 65 of file stats.hpp.

condassvars

int64_t CaDiCaL::Stats::condassvars = 0

Definition at line 66 of file stats.hpp.

condautinit

int64_t CaDiCaL::Stats::condautinit = 0

Definition at line 67 of file stats.hpp.

condautrem

int64_t CaDiCaL::Stats::condautrem = 0

Definition at line 68 of file stats.hpp.

condcands

int64_t CaDiCaL::Stats::condcands = 0

Definition at line 69 of file stats.hpp.

condcondinit

int64_t CaDiCaL::Stats::condcondinit = 0

Definition at line 70 of file stats.hpp.

condcondrem

int64_t CaDiCaL::Stats::condcondrem

Initial value:

=
      0

Definition at line 71 of file stats.hpp.

conditioned

int64_t CaDiCaL::Stats::conditioned = 0

Definition at line 73 of file stats.hpp.

conditionings

int64_t CaDiCaL::Stats::conditionings = 0

Definition at line 74 of file stats.hpp.

condprops

int64_t CaDiCaL::Stats::condprops = 0

Definition at line 75 of file stats.hpp.

conflicts

int64_t CaDiCaL::Stats::conflicts = 0

Definition at line 22 of file stats.hpp.

[struct]

struct { ... } CaDiCaL::Stats::congruence

congruent

int64_t CaDiCaL::Stats::congruent = 0

Definition at line 351 of file stats.hpp.

[struct]

struct { ... } CaDiCaL::Stats::constant

count

int64_t CaDiCaL::Stats::count = 0

Definition at line 96 of file stats.hpp.

cover [1/2]

int64_t CaDiCaL::Stats::cover = 0

Definition at line 26 of file stats.hpp.

[struct] [2/2]

struct { ... } CaDiCaL::Stats::cover

[struct]

struct { ... } CaDiCaL::Stats::current

decisions

int64_t CaDiCaL::Stats::decisions = 0

Definition at line 23 of file stats.hpp.

decompositions

int64_t CaDiCaL::Stats::decompositions = 0

Definition at line 232 of file stats.hpp.

deduplicated

int64_t CaDiCaL::Stats::deduplicated = 0

Definition at line 171 of file stats.hpp.

deduplications

int64_t CaDiCaL::Stats::deduplications = 0

Definition at line 172 of file stats.hpp.

definition_ticks

int64_t CaDiCaL::Stats::definition_ticks = 0

Definition at line 186 of file stats.hpp.

definition_units

int64_t CaDiCaL::Stats::definition_units = 0

Definition at line 185 of file stats.hpp.

definitions_checked

int64_t CaDiCaL::Stats::definitions_checked = 0

Definition at line 183 of file stats.hpp.

definitions_extracted

int64_t CaDiCaL::Stats::definitions_extracted = 0

Definition at line 184 of file stats.hpp.

eagersub

int64_t CaDiCaL::Stats::eagersub

Initial value:

=
      0

Definition at line 209 of file stats.hpp.

eagertried

int64_t CaDiCaL::Stats::eagertried = 0

Definition at line 208 of file stats.hpp.

echeck_call

int64_t CaDiCaL::Stats::echeck_call = 0

Definition at line 60 of file stats.hpp.

elearn_call

int64_t CaDiCaL::Stats::elearn_call

Initial value:

=
        0

Definition at line 52 of file stats.hpp.

elearn_conf

int64_t CaDiCaL::Stats::elearn_conf

Initial value:

=
        0

Definition at line 58 of file stats.hpp.

elearn_prop

int64_t CaDiCaL::Stats::elearn_prop

Initial value:

=
        0

Definition at line 56 of file stats.hpp.

elearned

int64_t CaDiCaL::Stats::elearned

Initial value:

=
        0

Definition at line 54 of file stats.hpp.

elim

int64_t CaDiCaL::Stats::elim = 0

Definition at line 79 of file stats.hpp.

elimands

int64_t CaDiCaL::Stats::elimands = 0

Definition at line 222 of file stats.hpp.

elimbwstr

int64_t CaDiCaL::Stats::elimbwstr = 0

Definition at line 226 of file stats.hpp.

elimbwsub

int64_t CaDiCaL::Stats::elimbwsub = 0

Definition at line 225 of file stats.hpp.

elimcompleted

int64_t CaDiCaL::Stats::elimcompleted = 0

Definition at line 217 of file stats.hpp.

elimequivs

int64_t CaDiCaL::Stats::elimequivs = 0

Definition at line 221 of file stats.hpp.

elimfastphases

int64_t CaDiCaL::Stats::elimfastphases = 0

Definition at line 216 of file stats.hpp.

elimfastrounds

int64_t CaDiCaL::Stats::elimfastrounds = 0

Definition at line 213 of file stats.hpp.

elimgates

int64_t CaDiCaL::Stats::elimgates = 0

Definition at line 220 of file stats.hpp.

eliminated

int64_t CaDiCaL::Stats::eliminated = 0

Definition at line 328 of file stats.hpp.

eliminated_and

int64_t CaDiCaL::Stats::eliminated_and = 0

Definition at line 177 of file stats.hpp.

eliminated_def

int64_t CaDiCaL::Stats::eliminated_def

Initial value:

=
      0

Definition at line 180 of file stats.hpp.

eliminated_equi

int64_t CaDiCaL::Stats::eliminated_equi

Initial value:

=
      0

Definition at line 175 of file stats.hpp.

eliminated_ite

int64_t CaDiCaL::Stats::eliminated_ite = 0

Definition at line 178 of file stats.hpp.

eliminated_xor

int64_t CaDiCaL::Stats::eliminated_xor = 0

Definition at line 179 of file stats.hpp.

elimites

int64_t CaDiCaL::Stats::elimites = 0

Definition at line 223 of file stats.hpp.

elimotfstr

int64_t CaDiCaL::Stats::elimotfstr

Initial value:

=
      0

Definition at line 197 of file stats.hpp.

elimotfsub

int64_t CaDiCaL::Stats::elimotfsub

Initial value:

=
      0

Definition at line 204 of file stats.hpp.

elimphases

int64_t CaDiCaL::Stats::elimphases = 0

Definition at line 215 of file stats.hpp.

elimres

int64_t CaDiCaL::Stats::elimres = 0

Definition at line 211 of file stats.hpp.

elimrestried

int64_t CaDiCaL::Stats::elimrestried = 0

Definition at line 212 of file stats.hpp.

elimrounds

int64_t CaDiCaL::Stats::elimrounds = 0

Definition at line 214 of file stats.hpp.

elimsubst

int64_t CaDiCaL::Stats::elimsubst = 0

Definition at line 219 of file stats.hpp.

elimtried

int64_t CaDiCaL::Stats::elimtried = 0

Definition at line 218 of file stats.hpp.

elimxors

int64_t CaDiCaL::Stats::elimxors = 0

Definition at line 224 of file stats.hpp.

eprop_call

int64_t CaDiCaL::Stats::eprop_call = 0

Definition at line 46 of file stats.hpp.

eprop_conf

int64_t CaDiCaL::Stats::eprop_conf

Initial value:

=
        0

Definition at line 48 of file stats.hpp.

eprop_expl

int64_t CaDiCaL::Stats::eprop_expl

Initial value:

=
        0

Definition at line 50 of file stats.hpp.

eprop_prop

int64_t CaDiCaL::Stats::eprop_prop = 0

Definition at line 47 of file stats.hpp.

ext_cb

int64_t CaDiCaL::Stats::ext_cb = 0

Definition at line 45 of file stats.hpp.

[struct]

struct { ... } CaDiCaL::Stats::ext_prop

extended

int64_t CaDiCaL::Stats::extended = 0

Definition at line 309 of file stats.hpp.

extensions

int64_t CaDiCaL::Stats::extensions = 0

Definition at line 308 of file stats.hpp.

factor

int64_t CaDiCaL::Stats::factor = 0

Definition at line 37 of file stats.hpp.

factor_added

int64_t CaDiCaL::Stats::factor_added = 0

Definition at line 190 of file stats.hpp.

factored

int64_t CaDiCaL::Stats::factored = 0

Definition at line 189 of file stats.hpp.

failed

int64_t CaDiCaL::Stats::failed = 0

Definition at line 298 of file stats.hpp.

fasteliminated

int64_t CaDiCaL::Stats::fasteliminated = 0

Definition at line 329 of file stats.hpp.

fixed

int64_t CaDiCaL::Stats::fixed = 0

Definition at line 327 of file stats.hpp.

flipped

int64_t CaDiCaL::Stats::flipped = 0

Definition at line 116 of file stats.hpp.

flips

int64_t CaDiCaL::Stats::flips = 0

Definition at line 126 of file stats.hpp.

[struct]

struct { ... } CaDiCaL::Stats::flush

[struct]

struct { ... } CaDiCaL::Stats::forward

[struct]

struct { ... } CaDiCaL::Stats::garbage

gates

int64_t CaDiCaL::Stats::gates = 0

Definition at line 346 of file stats.hpp.

hbreds

int64_t CaDiCaL::Stats::hbreds = 0

Definition at line 165 of file stats.hpp.

hbrs

int64_t CaDiCaL::Stats::hbrs = 0

Definition at line 163 of file stats.hpp.

hbrsizes

int64_t CaDiCaL::Stats::hbrsizes = 0

Definition at line 164 of file stats.hpp.

hbrsubs

int64_t CaDiCaL::Stats::hbrsubs = 0

Definition at line 166 of file stats.hpp.

[struct]

struct { ... } CaDiCaL::Stats::horn

htrs

int64_t CaDiCaL::Stats::htrs = 0

Definition at line 229 of file stats.hpp.

htrs2

int64_t CaDiCaL::Stats::htrs2 = 0

Definition at line 230 of file stats.hpp.

htrs3

int64_t CaDiCaL::Stats::htrs3 = 0

Definition at line 231 of file stats.hpp.

hyper

int64_t CaDiCaL::Stats::hyper = 0

Definition at line 133 of file stats.hpp.

hyperunary

int64_t CaDiCaL::Stats::hyperunary = 0

Definition at line 299 of file stats.hpp.

ilbsuccess

int64_t CaDiCaL::Stats::ilbsuccess = 0

Definition at line 320 of file stats.hpp.

ilbtriggers

int64_t CaDiCaL::Stats::ilbtriggers = 0

Definition at line 319 of file stats.hpp.

improvedglue

int64_t CaDiCaL::Stats::improvedglue = 0

Definition at line 151 of file stats.hpp.

inactive

int64_t CaDiCaL::Stats::inactive = 0

Definition at line 341 of file stats.hpp.

inprobesuccess

int64_t CaDiCaL::Stats::inprobesuccess = 0

Definition at line 296 of file stats.hpp.

inprobingphases

int64_t CaDiCaL::Stats::inprobingphases = 0

Definition at line 294 of file stats.hpp.

instantiate

int64_t CaDiCaL::Stats::instantiate = 0

Definition at line 27 of file stats.hpp.

instantiated

int64_t CaDiCaL::Stats::instantiated = 0

Definition at line 168 of file stats.hpp.

instried

int64_t CaDiCaL::Stats::instried = 0

Definition at line 167 of file stats.hpp.

instrounds

int64_t CaDiCaL::Stats::instrounds = 0

Definition at line 169 of file stats.hpp.

internal

Internal* CaDiCaL::Stats::internal

Definition at line 18 of file stats.hpp.

inverted

int64_t CaDiCaL::Stats::inverted = 0

Definition at line 117 of file stats.hpp.

irredundant

int64_t CaDiCaL::Stats::irredundant = 0

Definition at line 88 of file stats.hpp.

irrlits

int64_t CaDiCaL::Stats::irrlits = 0

Definition at line 260 of file stats.hpp.

ites

int64_t CaDiCaL::Stats::ites = 0

Definition at line 348 of file stats.hpp.

learned [1/2]

int64_t CaDiCaL::Stats::learned = 0

Definition at line 132 of file stats.hpp.

[struct] [2/2]

struct { ... } CaDiCaL::Stats::learned

levelsreused

int64_t CaDiCaL::Stats::levelsreused = 0

Definition at line 321 of file stats.hpp.

literals

int64_t CaDiCaL::Stats::literals = 0

Definition at line 253 of file stats.hpp.

literals_factored

int64_t CaDiCaL::Stats::literals_factored = 0

Definition at line 193 of file stats.hpp.

literals_unfactored

int64_t CaDiCaL::Stats::literals_unfactored = 0

Definition at line 195 of file stats.hpp.

literalsreused

int64_t CaDiCaL::Stats::literalsreused = 0

Definition at line 322 of file stats.hpp.

[struct]

struct { ... } CaDiCaL::Stats::lucky

[struct]

struct { ... } CaDiCaL::Stats::mark

minimized

int64_t CaDiCaL::Stats::minimized = 0

Definition at line 256 of file stats.hpp.

minimum

int64_t CaDiCaL::Stats::minimum = 0

Definition at line 127 of file stats.hpp.

minishrunken

int64_t CaDiCaL::Stats::minishrunken = 0

Definition at line 258 of file stats.hpp.

negative

int64_t CaDiCaL::Stats::negative = 0

Definition at line 109 of file stats.hpp.

[struct]

struct { ... } CaDiCaL::Stats::now

one

int64_t CaDiCaL::Stats::one = 0

Definition at line 106 of file stats.hpp.

original

int64_t CaDiCaL::Stats::original = 0

Definition at line 118 of file stats.hpp.

[struct]

struct { ... } CaDiCaL::Stats::otfs

positive

int64_t CaDiCaL::Stats::positive = 0

Definition at line 109 of file stats.hpp.

preprocessings

int64_t CaDiCaL::Stats::preprocessings = 0

Definition at line 317 of file stats.hpp.

probe

int64_t CaDiCaL::Stats::probe = 0

Definition at line 28 of file stats.hpp.

probed

int64_t CaDiCaL::Stats::probed = 0

Definition at line 297 of file stats.hpp.

probefailed

int64_t CaDiCaL::Stats::probefailed = 0

Definition at line 300 of file stats.hpp.

probingrounds

int64_t CaDiCaL::Stats::probingrounds = 0

Definition at line 295 of file stats.hpp.

process

double CaDiCaL::Stats::process = 0

Definition at line 92 of file stats.hpp.

promoted1

int64_t CaDiCaL::Stats::promoted1 = 0

Definition at line 152 of file stats.hpp.

promoted2

int64_t CaDiCaL::Stats::promoted2 = 0

Definition at line 153 of file stats.hpp.

[struct]

struct { ... } CaDiCaL::Stats::propagations

pure

int64_t CaDiCaL::Stats::pure = 0

Definition at line 331 of file stats.hpp.

random

int64_t CaDiCaL::Stats::random = 0

Definition at line 119 of file stats.hpp.

reactivated

int64_t CaDiCaL::Stats::reactivated = 0

Definition at line 314 of file stats.hpp.

real

double CaDiCaL::Stats::real = 0

Definition at line 92 of file stats.hpp.

recomputed

int64_t CaDiCaL::Stats::recomputed = 0

Definition at line 155 of file stats.hpp.

reduced

int64_t CaDiCaL::Stats::reduced = 0

Definition at line 158 of file stats.hpp.

reduced_prct

int64_t CaDiCaL::Stats::reduced_prct = 0

Definition at line 160 of file stats.hpp.

reduced_sqrt

int64_t CaDiCaL::Stats::reduced_sqrt = 0

Definition at line 159 of file stats.hpp.

reductions

int64_t CaDiCaL::Stats::reductions = 0

Definition at line 157 of file stats.hpp.

redundant

int64_t CaDiCaL::Stats::redundant = 0

Definition at line 87 of file stats.hpp.

[struct]

struct { ... } CaDiCaL::Stats::rephased

rescored

int64_t CaDiCaL::Stats::rescored = 0

Definition at line 144 of file stats.hpp.

restartlevels

int64_t CaDiCaL::Stats::restartlevels = 0

Definition at line 139 of file stats.hpp.

restarts

int64_t CaDiCaL::Stats::restarts = 0

Definition at line 138 of file stats.hpp.

restartstable

int64_t CaDiCaL::Stats::restartstable = 0

Definition at line 140 of file stats.hpp.

restorations

int64_t CaDiCaL::Stats::restorations = 0

Definition at line 312 of file stats.hpp.

restored

int64_t CaDiCaL::Stats::restored = 0

Definition at line 313 of file stats.hpp.

restoredlits

int64_t CaDiCaL::Stats::restoredlits = 0

Definition at line 315 of file stats.hpp.

reused

int64_t CaDiCaL::Stats::reused = 0

Definition at line 145 of file stats.hpp.

reusedlevels

int64_t CaDiCaL::Stats::reusedlevels = 0

Definition at line 146 of file stats.hpp.

reusedstable

int64_t CaDiCaL::Stats::reusedstable = 0

Definition at line 147 of file stats.hpp.

rewritten_ands

int64_t CaDiCaL::Stats::rewritten_ands = 0

Definition at line 355 of file stats.hpp.

rounds

int64_t CaDiCaL::Stats::rounds = 0

Definition at line 352 of file stats.hpp.

search

int64_t CaDiCaL::Stats::search[2] = 0

Definition at line 29 of file stats.hpp.

searched

int64_t CaDiCaL::Stats::searched = 0

Definition at line 156 of file stats.hpp.

sections

int64_t CaDiCaL::Stats::sections = 0

Definition at line 148 of file stats.hpp.

shrunken

int64_t CaDiCaL::Stats::shrunken = 0

Definition at line 257 of file stats.hpp.

shuffled

int64_t CaDiCaL::Stats::shuffled = 0

Definition at line 137 of file stats.hpp.

simplified

int64_t CaDiCaL::Stats::simplified = 0

Definition at line 356 of file stats.hpp.

simplified_ands

int64_t CaDiCaL::Stats::simplified_ands = 0

Definition at line 357 of file stats.hpp.

simplified_ites

int64_t CaDiCaL::Stats::simplified_ites = 0

Definition at line 359 of file stats.hpp.

simplified_xors

int64_t CaDiCaL::Stats::simplified_xors = 0

Definition at line 358 of file stats.hpp.

stabconflicts

int64_t CaDiCaL::Stats::stabconflicts

Initial value:

=
      0

Definition at line 142 of file stats.hpp.

stabphases

int64_t CaDiCaL::Stats::stabphases = 0

Definition at line 141 of file stats.hpp.

strengthened

int64_t CaDiCaL::Stats::strengthened = 0

Definition at line 173 of file stats.hpp.

subchecks

int64_t CaDiCaL::Stats::subchecks = 0

Definition at line 202 of file stats.hpp.

subchecks2

int64_t CaDiCaL::Stats::subchecks2 = 0

Definition at line 203 of file stats.hpp.

subirr

int64_t CaDiCaL::Stats::subirr = 0

Definition at line 199 of file stats.hpp.

subred

int64_t CaDiCaL::Stats::subred = 0

Definition at line 200 of file stats.hpp.

substituted

int64_t CaDiCaL::Stats::substituted = 0

Definition at line 330 of file stats.hpp.

subsume

int64_t CaDiCaL::Stats::subsume = 0

Definition at line 80 of file stats.hpp.

subsumed

int64_t CaDiCaL::Stats::subsumed = 0

Definition at line 170 of file stats.hpp.

subsumephases

int64_t CaDiCaL::Stats::subsumephases = 0

Definition at line 207 of file stats.hpp.

subsumerounds

int64_t CaDiCaL::Stats::subsumerounds = 0

Definition at line 206 of file stats.hpp.

subtried

int64_t CaDiCaL::Stats::subtried = 0

Definition at line 201 of file stats.hpp.

succeeded

int64_t CaDiCaL::Stats::succeeded = 0

Definition at line 104 of file stats.hpp.

sweep

int64_t CaDiCaL::Stats::sweep = 0

Definition at line 39 of file stats.hpp.

sweep_clauses

int64_t CaDiCaL::Stats::sweep_clauses = 0

Definition at line 289 of file stats.hpp.

sweep_completed

int64_t CaDiCaL::Stats::sweep_completed = 0

Definition at line 283 of file stats.hpp.

sweep_depth

int64_t CaDiCaL::Stats::sweep_depth = 0

Definition at line 287 of file stats.hpp.

sweep_environment

int64_t CaDiCaL::Stats::sweep_environment = 0

Definition at line 288 of file stats.hpp.

sweep_equivalences

int64_t CaDiCaL::Stats::sweep_equivalences = 0

Definition at line 281 of file stats.hpp.

sweep_fixed_backbone

int64_t CaDiCaL::Stats::sweep_fixed_backbone = 0

Definition at line 269 of file stats.hpp.

sweep_flip_backbone

int64_t CaDiCaL::Stats::sweep_flip_backbone = 0

Definition at line 268 of file stats.hpp.

sweep_flip_equivalences

int64_t CaDiCaL::Stats::sweep_flip_equivalences = 0

Definition at line 275 of file stats.hpp.

sweep_flipped_backbone

int64_t CaDiCaL::Stats::sweep_flipped_backbone = 0

Definition at line 270 of file stats.hpp.

sweep_flipped_equivalences

int64_t CaDiCaL::Stats::sweep_flipped_equivalences = 0

Definition at line 276 of file stats.hpp.

sweep_sat

int64_t CaDiCaL::Stats::sweep_sat = 0

Definition at line 285 of file stats.hpp.

sweep_sat_backbone

int64_t CaDiCaL::Stats::sweep_sat_backbone = 0

Definition at line 272 of file stats.hpp.

sweep_sat_equivalences

int64_t CaDiCaL::Stats::sweep_sat_equivalences = 0

Definition at line 277 of file stats.hpp.

sweep_solved

int64_t CaDiCaL::Stats::sweep_solved = 0

Definition at line 284 of file stats.hpp.

sweep_solved_backbone

int64_t CaDiCaL::Stats::sweep_solved_backbone = 0

Definition at line 271 of file stats.hpp.

sweep_solved_equivalences

int64_t CaDiCaL::Stats::sweep_solved_equivalences = 0

Definition at line 280 of file stats.hpp.

sweep_units

int64_t CaDiCaL::Stats::sweep_units = 0

Definition at line 267 of file stats.hpp.

sweep_unknown_backbone

int64_t CaDiCaL::Stats::sweep_unknown_backbone = 0

Definition at line 274 of file stats.hpp.

sweep_unknown_equivalences

int64_t CaDiCaL::Stats::sweep_unknown_equivalences = 0

Definition at line 279 of file stats.hpp.

sweep_unsat

int64_t CaDiCaL::Stats::sweep_unsat = 0

Definition at line 286 of file stats.hpp.

sweep_unsat_backbone

int64_t CaDiCaL::Stats::sweep_unsat_backbone = 0

Definition at line 273 of file stats.hpp.

sweep_unsat_equivalences

int64_t CaDiCaL::Stats::sweep_unsat_equivalences = 0

Definition at line 278 of file stats.hpp.

sweep_variables

int64_t CaDiCaL::Stats::sweep_variables = 0

Definition at line 282 of file stats.hpp.

ternary

int64_t CaDiCaL::Stats::ternary = 0

Definition at line 40 of file stats.hpp.

ternres

int64_t CaDiCaL::Stats::ternres = 0

Definition at line 228 of file stats.hpp.

[struct]

struct { ... } CaDiCaL::Stats::ticks

tierecomputed

int64_t CaDiCaL::Stats::tierecomputed = 0

Definition at line 324 of file stats.hpp.

[struct]

struct { ... } CaDiCaL::Stats::time

total

int64_t CaDiCaL::Stats::total = 0

Definition at line 86 of file stats.hpp.

transitive

int64_t CaDiCaL::Stats::transitive = 0

Definition at line 251 of file stats.hpp.

transred

int64_t CaDiCaL::Stats::transred = 0

Definition at line 30 of file stats.hpp.

transreds

int64_t CaDiCaL::Stats::transreds = 0

Definition at line 250 of file stats.hpp.

transredunits

int64_t CaDiCaL::Stats::transredunits = 0

Definition at line 301 of file stats.hpp.

tried

int64_t CaDiCaL::Stats::tried = 0

Definition at line 103 of file stats.hpp.

trivial_ite

int64_t CaDiCaL::Stats::trivial_ite = 0

Definition at line 361 of file stats.hpp.

unaries

int64_t CaDiCaL::Stats::unaries = 0

Definition at line 354 of file stats.hpp.

unary_and

int64_t CaDiCaL::Stats::unary_and = 0

Definition at line 353 of file stats.hpp.

unary_ites

int64_t CaDiCaL::Stats::unary_ites = 0

Definition at line 362 of file stats.hpp.

units

int64_t CaDiCaL::Stats::units = 0

Definition at line 292 of file stats.hpp.

unused

int64_t CaDiCaL::Stats::unused = 0

Definition at line 339 of file stats.hpp.

used

std::vector<std::vector<uint64_t> > CaDiCaL::Stats::used

Definition at line 343 of file stats.hpp.

variables_extension

int64_t CaDiCaL::Stats::variables_extension = 0

Definition at line 191 of file stats.hpp.

variables_original

int64_t CaDiCaL::Stats::variables_original = 0

Definition at line 192 of file stats.hpp.

vars

int64_t CaDiCaL::Stats::vars = 0

Definition at line 20 of file stats.hpp.

vivifications

int64_t CaDiCaL::Stats::vivifications = 0

Definition at line 233 of file stats.hpp.

vivify

int64_t CaDiCaL::Stats::vivify = 0

Definition at line 31 of file stats.hpp.

vivifychecks

int64_t CaDiCaL::Stats::vivifychecks = 0

Definition at line 234 of file stats.hpp.

vivifydecs

int64_t CaDiCaL::Stats::vivifydecs = 0

Definition at line 235 of file stats.hpp.

vivifydemote

int64_t CaDiCaL::Stats::vivifydemote = 0

Definition at line 249 of file stats.hpp.

vivifyimplied

int64_t CaDiCaL::Stats::vivifyimplied = 0

Definition at line 247 of file stats.hpp.

vivifyinst

int64_t CaDiCaL::Stats::vivifyinst = 0

Definition at line 248 of file stats.hpp.

vivifyreused

int64_t CaDiCaL::Stats::vivifyreused = 0

Definition at line 236 of file stats.hpp.

vivifysched

int64_t CaDiCaL::Stats::vivifysched = 0

Definition at line 237 of file stats.hpp.

vivifystred1

int64_t CaDiCaL::Stats::vivifystred1 = 0

Definition at line 243 of file stats.hpp.

vivifystred2

int64_t CaDiCaL::Stats::vivifystred2 = 0

Definition at line 244 of file stats.hpp.

vivifystred3

int64_t CaDiCaL::Stats::vivifystred3 = 0

Definition at line 245 of file stats.hpp.

vivifystrirr

int64_t CaDiCaL::Stats::vivifystrirr = 0

Definition at line 242 of file stats.hpp.

vivifystrs

int64_t CaDiCaL::Stats::vivifystrs = 0

Definition at line 241 of file stats.hpp.

vivifysubirr

int64_t CaDiCaL::Stats::vivifysubirr = 0

Definition at line 240 of file stats.hpp.

vivifysubred

int64_t CaDiCaL::Stats::vivifysubred = 0

Definition at line 239 of file stats.hpp.

vivifysubs

int64_t CaDiCaL::Stats::vivifysubs = 0

Definition at line 238 of file stats.hpp.

vivifyunits

int64_t CaDiCaL::Stats::vivifyunits = 0

Definition at line 246 of file stats.hpp.

walk [1/2]

int64_t CaDiCaL::Stats::walk = 0

Definition at line 32 of file stats.hpp.

[struct] [2/2]

struct { ... } CaDiCaL::Stats::walk

weakened

int64_t CaDiCaL::Stats::weakened = 0

Definition at line 310 of file stats.hpp.

weakenedlen

int64_t CaDiCaL::Stats::weakenedlen = 0

Definition at line 311 of file stats.hpp.

xors

int64_t CaDiCaL::Stats::xors = 0

Definition at line 349 of file stats.hpp.

zero

int64_t CaDiCaL::Stats::zero = 0

Definition at line 106 of file stats.hpp.

---

The documentation for this struct was generated from the following files:

• src/sat/cadical/stats.hpp
• src/sat/cadical/cadical_stats.cpp