Id *decisionmap = solv->decisionmap;
Id *watches = solv->watches + pool->nsolvables;
+ if (solv->pool->verbose > 3)
+ printf ("----- propagate -----\n");
+
while (solv->propagate_index < solv->decisionq.count)
{
/* negate because our watches trigger if literal goes FALSE */
}
}
}
+ if (solv->pool->verbose > 3)
+ printf ("----- propagate end-----\n");
+
return 0; /* all is well */
}
makewatches(solv);
if (pool->verbose) printf("initial decisions: %d\n", solv->decisionq.count);
+ if (pool->verbose > 3)
+ printdecisions (solv);
/* start SAT algorithm */
level = 1;
if (level == 1)
{
- if (pool->verbose) printf("propagating (%d %d)...\n", solv->propagate_index, solv->decisionq.count);
+ if (pool->verbose) printf("propagating (propagate_index: %d; size decisionq: %d)...\n", solv->propagate_index, solv->decisionq.count);
if ((r = propagate(solv, level)) != 0)
{
if (analyze_unsolvable(solv, r, disablerules))