The previous implementation used a buffer of fixed size causing too long clauses to silently be cut off (https://github.com/QuMuLab/dsharp/issues/15). This implementation is based on sharpSAT's, going over literals using >> and ifstream.ignore.
I tested it against the long clause file of https://github.com/QuMuLab/dsharp/issues/15 and it gave the correct model count, nbVars and nbClauses. Also tested exp-testing/bmc-ibm-2.cnf, exp-testing/logistics.a.cnf and a 2bitmax_6.cnf file I had from some benchmarks, and confirmed the model counts, nbVars and nbClauses are still correct. I purposely changed p cnf 252 766 to p cnf 252 and it crashed and warned correctly.
Changes the way the CNF file is parsed.
The previous implementation used a buffer of fixed size causing too long clauses to silently be cut off (https://github.com/QuMuLab/dsharp/issues/15). This implementation is based on sharpSAT's, going over literals using
>>andifstream.ignore.I tested it against the long clause file of https://github.com/QuMuLab/dsharp/issues/15 and it gave the correct model count, nbVars and nbClauses. Also tested exp-testing/bmc-ibm-2.cnf, exp-testing/logistics.a.cnf and a 2bitmax_6.cnf file I had from some benchmarks, and confirmed the model counts, nbVars and nbClauses are still correct. I purposely changed
p cnf 252 766top cnf 252and it crashed and warned correctly.