Lines Matching refs:resolve
94 if (proof != NULL) proof->resolve(unit_id[var(qs[i])], var(qs[i]));
287 if (proof != NULL) proof->resolve(unit_id[var(q)], var(q));
301 proof->resolve(sconfl ? (confl->id())*(-1) : confl->id(), var(p));
351 proof->resolve(sreason[v] ? -1*(c.id()) : c.id(), v); //HA: -id if v&1 in c
354 proof->resolve(unit_id[var(c[k])], var(c[k]));
428 if (proof != NULL) proof->resolve(unit_id[x], x);
442 proof->resolve(sreason[x] ? -1*(c.id()) : c.id(), x);
447 if (proof != NULL) proof->resolve(unit_id[var(c[j])], var(c[j]));
541 proof->resolve(unit_id[var(c[k])], var(c[k]));
549 proof->resolve((unit_id[var(first)]>=0)? -id: id, var(first)); //HA: sign