Skip to content

Commit 1ab4809

Browse files
committed
minisat: use lbool namespace
1 parent e262edc commit 1ab4809

File tree

1 file changed

+5
-5
lines changed

1 file changed

+5
-5
lines changed

src/solvers/sat/satcheck_minisat2.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -53,9 +53,9 @@ tvt satcheck_minisat2_baset<T>::l_get(literalt a) const
5353

5454
using Minisat::lbool;
5555

56-
if(solver->model[a.var_no()]==l_True)
56+
if(solver->model[a.var_no()]==Minisat::l_True)
5757
result=tvt(true);
58-
else if(solver->model[a.var_no()]==l_False)
58+
else if(solver->model[a.var_no()]==Minisat::l_False)
5959
result=tvt(false);
6060
else
6161
return tvt::unknown();
@@ -234,19 +234,19 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
234234
}
235235

236236
lbool solver_result=
237-
solver->solve(solver_assumptions) ? l_True : l_False;
237+
solver->solve(solver_assumptions) ? Minisat::l_True : Minisat::l_False;
238238

239239
#endif
240240

241-
if(solver_result==l_True)
241+
if(solver_result==Minisat::l_True)
242242
{
243243
messaget::status() <<
244244
"SAT checker: instance is SATISFIABLE" << eom;
245245
CHECK_RETURN(solver->model.size()>0);
246246
status=statust::SAT;
247247
return resultt::P_SATISFIABLE;
248248
}
249-
else if(solver_result==l_False)
249+
else if(solver_result==Minisat::l_False)
250250
{
251251
messaget::status() <<
252252
"SAT checker: instance is UNSATISFIABLE" << eom;

0 commit comments

Comments
 (0)