Lines Matching refs:stats
331 s->stats.learnts--;
332 s->stats.learnts_literals -= clause_size(c);
334 s->stats.clauses--;
335 s->stats.clauses_literals -= clause_size(c);
482 s->stats.learnts++;
483 s->stats.learnts_literals += veci_size(cls);
644 s->stats.max_literals += veci_size(learnt);
646 s->stats.tot_literals += j;
701 s->stats.propagations++;
763 s->stats.inspects += j - (clause**)vecp_begin(ws);
813 s->stats.starts++;
828 s->stats.conflicts++; conflictC++;
863 s->stats.decisions++;
937 s->stats.starts = 0;
938 s->stats.decisions = 0;
939 s->stats.propagations = 0;
940 s->stats.inspects = 0;
941 s->stats.conflicts = 0;
942 s->stats.clauses = 0;
943 s->stats.clauses_literals = 0;
944 s->stats.learnts = 0;
945 s->stats.learnts_literals = 0;
946 s->stats.max_literals = 0;
947 s->stats.tot_literals = 0;
1119 s->stats.clauses++;
1120 s->stats.clauses_literals += j - begin;
1156 // (shouldn't depend on 'stats' really, but it will do for now)
1157 s->simpdb_props = (int)(s->stats.clauses_literals + s->stats.learnts_literals);
1197 double Ratio = (s->stats.learnts == 0)? 0.0 :
1198 s->stats.learnts_literals / (double)s->stats.learnts;
1202 (double)s->stats.conflicts,
1203 (double)s->stats.clauses,
1204 (double)s->stats.clauses_literals,
1206 (double)s->stats.learnts,
1207 (double)s->stats.learnts_literals,
1238 return (int)s->stats.conflicts;