Searched refs:nbReducedClauses (Results 1 – 6 of 6) sorted by relevance
/dports/math/glucose/glucose-syrup-4.1/simp/ |
H A D | Main.cc | 88 printf("c nb reduced Clauses : %" PRIu64"\n",solver.stats[nbReducedClauses]); in printStats()
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/glucose/ |
H A D | Solver.h | 187 …int64_t nbRemovedClauses,nbReducedClauses,nbDL2,nbBin,nbUn,nbReduceDB,solves, starts, decisions, r… variable
|
H A D | Glucose.cpp | 127 , nbRemovedClauses(0),nbReducedClauses(0), nbDL2(0),nbBin(0),nbUn(0) , nbReduceDB(0) in Solver() 453 nbReducedClauses++; in minimisationWithBinaryResolution()
|
H A D | AbcGlucose.cpp | 589 printf("c nb reduced Clauses : %-12d\n", (int)s.nbReducedClauses); in glucose_print_stats()
|
/dports/math/glucose/glucose-syrup-4.1/core/ |
H A D | Solver.h | 76 nbReducedClauses, enumerator
|
H A D | Solver.cc | 638 stats[nbReducedClauses]++; in minimisationWithBinaryResolution()
|