mirror of https://github.com/YosysHQ/abc.git
fixed some warnings in bsat2
This commit is contained in:
parent
bfbec71211
commit
d87b1cd543
|
|
@ -45,10 +45,12 @@ int Minisat::parseOptions(int& argc, char** argv, bool strict)
|
|||
}
|
||||
|
||||
if (!parsed_ok)
|
||||
{
|
||||
if (strict && match(argv[i], "-"))
|
||||
{ fprintf(stderr, "ERROR! Unknown flag \"%s\". Use '--%shelp' for help.\n", argv[i], Option::getHelpPrefixString()); return 0; } // exit(0);
|
||||
else
|
||||
argv[j++] = argv[i];
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -62,7 +62,7 @@ class Option
|
|||
struct OptionLt {
|
||||
bool operator()(const Option* x, const Option* y) {
|
||||
int test1 = strcmp(x->category, y->category);
|
||||
return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0;
|
||||
return test1 < 0 || ( test1 == 0 && strcmp(x->type_name, y->type_name) < 0 );
|
||||
}
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -230,10 +230,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& ou
|
|||
if (var(qs[i]) != v){
|
||||
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:;
|
||||
|
|
@ -264,10 +266,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
|
|||
if (var(__qs[i]) != v){
|
||||
for (int j = 0; j < ps.size(); j++)
|
||||
if (var(__ps[j]) == var(__qs[i]))
|
||||
{
|
||||
if (__ps[j] == ~__qs[i])
|
||||
return false;
|
||||
else
|
||||
goto next;
|
||||
}
|
||||
size++;
|
||||
}
|
||||
next:;
|
||||
|
|
|
|||
|
|
@ -211,7 +211,7 @@ void Solver::cancelUntil(int level) {
|
|||
for (int c = trail.size()-1; c >= trail_lim[level]; c--){
|
||||
Var x = var(trail[c]);
|
||||
assigns [x] = l_Undef;
|
||||
if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last())
|
||||
if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last()))
|
||||
polarity[x] = sign(trail[c]);
|
||||
insertVarOrder(x); }
|
||||
qhead = trail_lim[level];
|
||||
|
|
@ -659,7 +659,7 @@ lbool Solver::search(int nof_conflicts)
|
|||
|
||||
}else{
|
||||
// NO CONFLICT
|
||||
if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){
|
||||
if ( (nof_conflicts >= 0 && conflictC >= nof_conflicts) || !withinBudget()){
|
||||
// Reached bound on number of conflicts:
|
||||
progress_estimate = progressEstimate();
|
||||
cancelUntil(0);
|
||||
|
|
|
|||
|
|
@ -93,7 +93,6 @@ public:
|
|||
void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
|
||||
};
|
||||
|
||||
|
||||
template<class T>
|
||||
void vec<T>::capacity(int min_cap) {
|
||||
if (cap >= min_cap) return;
|
||||
|
|
|
|||
Loading…
Reference in New Issue