luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Compiler warnings.

This commit is contained in:
Alan Mishchenko 2017-09-07 19:54:12 -07:00
parent 7ce7e9ec31
commit 8a11c911ab
3 changed files with 18 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
src/sat/glucose/Glucose.cpp
View File

@ -92,8 +92,8 @@ Solver::Solver() :
SolverType(0)
, pCnfFunc(NULL)
, nCallConfl(1000)
, verbEveryConflicts(10000)
, terminate_search_early(false)
, verbEveryConflicts(10000)
, pstop(NULL)
, nRuntimeLimit(0)
@ -1188,16 +1188,16 @@ double Solver::progressEstimate() const
void Solver::printIncrementalStats() {
printf("c---------- Glucose Stats -------------------------\n");
printf("c restarts : %lld\n", starts);
printf("c nb ReduceDB : %lld\n", nbReduceDB);
printf("c nb removed Clauses : %lld\n", nbRemovedClauses);
printf("c nb learnts DL2 : %lld\n", nbDL2);
printf("c nb learnts size 2 : %lld\n", nbBin);
printf("c nb learnts size 1 : %lld\n", nbUn);
printf("c restarts : %ld\n", starts);
printf("c nb ReduceDB : %ld\n", nbReduceDB);
printf("c nb removed Clauses : %ld\n", nbRemovedClauses);
printf("c nb learnts DL2 : %ld\n", nbDL2);
printf("c nb learnts size 2 : %ld\n", nbBin);
printf("c nb learnts size 1 : %ld\n", nbUn);
printf("c conflicts : %lld\n", conflicts);
printf("c decisions : %lld\n", decisions);
printf("c propagations : %lld\n", propagations);
printf("c conflicts : %ld\n", conflicts);
printf("c decisions : %ld\n", decisions);
printf("c propagations : %ld\n", propagations);
printf("c SAT Calls : %d in %g seconds\n", nbSatCalls, totalTime4Sat);
printf("c UNSAT Calls : %d in %g seconds\n", nbUnsatCalls, totalTime4Unsat);

3
src/sat/glucose/Options.cpp
View File

@ -42,11 +42,12 @@ void Gluco::parseOptions(int& argc, char** argv, bool strict)
// fprintf(stderr, "checking %d: %s against flag <%s> (%s)\n", i, argv[i], Option::getOptionList()[k]->name, parsed_ok ? "ok" : "skip");
}
if (!parsed_ok)
if (!parsed_ok) {
if (strict && match(argv[i], "-"))
fprintf(stderr, "ERROR! Unknown flag \"%s\". Use '--%shelp' for help.\n", argv[i], Option::getHelpPrefixString()), exit(1);
else
argv[j++] = argv[i];
}
}
}

10
src/sat/glucose/SimpSolver.cpp
View File

@ -241,15 +241,16 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& ou
const Clause& ps = ps_smallest ? _qs : _ps;
const Clause& qs = ps_smallest ? _ps : _qs;
int i;
int i, j;
for (i = 0; i < qs.size(); i++){
if (var(qs[i]) != v){
for (int j = 0; j < ps.size(); j++)
if (var(ps[j]) == var(qs[i]))
for (j = 0; j < ps.size(); j++)
if (var(ps[j]) == var(qs[i])) {
if (ps[j] == ~qs[i])
return false;
else
goto next;
}
out_clause.push(qs[i]);
}
next:;
@ -279,11 +280,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
for (int i = 0; i < qs.size(); i++){
if (var(__qs[i]) != v){
for (int j = 0; j < ps.size(); j++)
if (var(__ps[j]) == var(__qs[i]))
if (var(__ps[j]) == var(__qs[i])) {
if (__ps[j] == ~__qs[i])
return false;
else
goto next;
}
size++;
}
next:;