Skip to content

A
abc
Commit f14ee271 by Alan Mishchenko
Options

Reordering if-statements in the xsat solver.

parent a226496b
Showing with 3 additions and 5 deletions
src/sat/xsat/xsatSolver.c
...@@ -680,12 +680,10 @@ unsigned xSAT_SolverPropagate( xSAT_Solver_t* s ) ...@@ -680,12 +680,10 @@ unsigned xSAT_SolverPropagate( xSAT_Solver_t* s )
nProp++; nProp++;
for ( i = begin; i < end; i++ ) for ( i = begin; i < end; i++ )
{ {
if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( i->Blocker ) ) == xSAT_LitSign( xSAT_NegLit( i->Blocker ) ) ) if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( i->Blocker ) ) == VarX )
{
return i->CRef;
}
else if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( i->Blocker ) ) == VarX )
xSAT_SolverEnqueue( s, i->Blocker, i->CRef ); xSAT_SolverEnqueue( s, i->Blocker, i->CRef );
else if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( i->Blocker ) ) == xSAT_LitSign( xSAT_NegLit( i->Blocker ) ) )
return i->CRef;
} }
ws = xSAT_VecWatchListEntry( s->vWatches, p ); ws = xSAT_VecWatchListEntry( s->vWatches, p );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment