Home
last modified time | relevance | path

Searched refs:nbReducedClauses (Results 1 – 6 of 6) sorted by relevance

/dports/math/glucose/glucose-syrup-4.1/simp/
H A DMain.cc88 printf("c nb reduced Clauses : %" PRIu64"\n",solver.stats[nbReducedClauses]); in printStats()
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/glucose/
H A DSolver.h187 …int64_t nbRemovedClauses,nbReducedClauses,nbDL2,nbBin,nbUn,nbReduceDB,solves, starts, decisions, r… variable
H A DGlucose.cpp127 , nbRemovedClauses(0),nbReducedClauses(0), nbDL2(0),nbBin(0),nbUn(0) , nbReduceDB(0) in Solver()
453 nbReducedClauses++; in minimisationWithBinaryResolution()
H A DAbcGlucose.cpp589 printf("c nb reduced Clauses : %-12d\n", (int)s.nbReducedClauses); in glucose_print_stats()
/dports/math/glucose/glucose-syrup-4.1/core/
H A DSolver.h76 nbReducedClauses, enumerator
H A DSolver.cc638 stats[nbReducedClauses]++; in minimisationWithBinaryResolution()