ask returns True instead of raising inconsistent assumptions exception

[TiloRC]

from sympy import ask, Q
from sympy.abc import x, y
ask(Q.positive(x), Q.positive(x) & Q.positive(y) & ~Q.positive(y)) # returns True instead of raising exception

The problem happens at lines 471 , 472 (of ask.py):

 # extract the relevant facts from assumptions with respect to args
 local_facts = _extract_all_facts(assump_cnf, args)

here we lose all of the predicate that don't have x as their argument.

Originally, I had thought this error had originated from satask, but it correctly rasies an exception here:

from sympy.assumptions.satask import satask
satask(Q.positive(x), Q.positive(x) & Q.positive(y) & ~Q.positive(y)) # correctly raises inconsistent assumptions exception

However, with a little modification satask has the same bug:

satask(Q.positive(x), Q.positive(x) & Q.positive(y) & Q.zero(y)) # returns True instead of raising exception

The problem is due the get_all_relevant_facts function which only thinks facts relating to the variables in the proposition are relevant. Facts about expressions like y which don't appear in the predicate are ignored.

Edit: here's a modified case where satask correctly raises the exception:

satask(Q.positive(x) & Q.positive(y), Q.positive(x) & Q.positive(y) & Q.zero(y)) # correctly raises exception

[TiloRC]

@ShubhamKJha, @JSS95, @asmeurer can you shed some light on the purpose of this code from the extract_predargs function? Getting rid of it fixes this bug, but slows down satask a lot. For the purposes of this function, why should arguments from the proposition be treated differently than arguments from the assumptions?

sympy/sympy/assumptions/satask.py

Lines 146 to 154 in a76b02f

	while tmp_keys != set():
	tmp = set()
	for l in lkeys:
	syms = find_symbols(l)
	if (syms & req_keys) != set():
	tmp |= syms
	tmp_keys = tmp - req_keys
	req_keys |= tmp_keys
	keys |= {l for l in lkeys if find_symbols(l) & req_keys != set()}

[TiloRC]

My impression of it is that it's a way to reduce the number of clauses given to the sat solver to speed things up? However, as this bug demonstrates that's problematic for some edge cases.

[asmeurer]

It looks like it was a performance optimization #17144. But we need to make sure that whatever optimizations we make are correct. It's better to have correct but slow code than to have code that is fast but gives wrong answers sometimes.