Home
last modified time | relevance | path

Searched refs:certifiedUNSAT (Results 1 – 7 of 7) sorted by relevance

/dports/math/glucose/glucose-syrup-4.1/simp/
H A DMain.cc158 S.certifiedUNSAT = opt_certified; in main()
160 if(S.certifiedUNSAT) { in main()
241 if (S.certifiedUNSAT) fprintf(S.certifiedOutput, "0\n"), fclose(S.certifiedOutput); in main()
H A DSimpSolver.cc222 if(!parsing && certifiedUNSAT) { in addClause_()
287 if (certifiedUNSAT) { in strengthenClause()
305 if (certifiedUNSAT) { in strengthenClause()
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/glucose/
H A DGlucose.cpp124 , certifiedUNSAT (opt_certified_) in Solver()
162 if(certifiedUNSAT) { in Solver()
242 if(certifiedUNSAT) { in addClause_()
263 if (flag && (certifiedUNSAT)) { in addClause_()
337 if (certifiedUNSAT) { in removeClause()
1083 if (certifiedUNSAT) { in search()
1212 if(incremental && certifiedUNSAT) { in solve_()
1260 if (certifiedUNSAT){ // Want certified output in solve_()
H A DSimpSolver.cpp152 if(!parsing && certifiedUNSAT) { in addClause_()
208 if (certifiedUNSAT) { in strengthenClause()
218 if (certifiedUNSAT) { in strengthenClause()
H A DSolver.h182 bool certifiedUNSAT; variable
/dports/math/glucose/glucose-syrup-4.1/core/
H A DSolver.cc153 , certifiedUNSAT(false) // Not in the first parallel version in Solver()
237 , certifiedUNSAT(false) // Not in the first parallel version in Solver()
408 if(certifiedUNSAT) { in addClause_()
423 if(flag && (certifiedUNSAT)) { in addClause_()
533 if(certifiedUNSAT) { in removeClause()
1540 if(certifiedUNSAT) { in search()
1738 if(incremental && certifiedUNSAT) { in solve_()
1800 if(certifiedUNSAT) { // Want certified output in solve_()
H A DSolver.h238 bool certifiedUNSAT; variable