Found while answering #996, and deliberately left out of #1126 because it is a solver change
rather than a domain-versus-set one. Measured on master at b30a4923, .NET 10, default settings.
not has no arm in the statement solver, so every negation answers "no solutions"
"not (x = 1)".ToEntity().Solve("x") -> { }
"not (x > 1)".ToEntity().Solve("x") -> { }
"not (x in RR)".ToEntity().Solve("x") -> { }
The empty set is a positive claim — no x satisfies this — and each of these has solutions.
not (x = 1) holds at every value but 1.
Cause
StatementSolver.Solve (SolveStatement.cs) has arms for Equalsf, Andf, Orf, Impliesf,
the four comparisons, Inf, Providedf and Piecewise. There is no Notf arm, so a negation
falls to _ => Set.Empty.
This is the defect #1036 fixed for equations — an equation nothing settled was answered with the
empty set rather than with itself — left unfixed for negation.
What the answer should be
The same shape #1126 gives an implication: { x : not a } names the set without naming a universe,
and a complement written that way is right whatever x ranges over.
Notf(var operand) => new ConditionalSet(x, expr),
with the rewrites that can do better than that — not (x = a) where the equation is solvable,
not (x > a) as x <= a — going in front of it if they are wanted. The point of the issue is that
the fallback must not be Empty.
Worth checking at the same time whether Solve of a bare Boolean should be Empty either:
"A implies true".ToEntity().Solve("A") is { A : not A } because Solve(True, A) is Empty,
where every A satisfies it.
Found while answering #996, and deliberately left out of #1126 because it is a solver change
rather than a domain-versus-set one. Measured on
masteratb30a4923, .NET 10, default settings.nothas no arm in the statement solver, so every negation answers "no solutions"The empty set is a positive claim — no x satisfies this — and each of these has solutions.
not (x = 1)holds at every value but 1.Cause
StatementSolver.Solve(SolveStatement.cs) has arms forEqualsf,Andf,Orf,Impliesf,the four comparisons,
Inf,ProvidedfandPiecewise. There is noNotfarm, so a negationfalls to
_ => Set.Empty.This is the defect #1036 fixed for equations — an equation nothing settled was answered with the
empty set rather than with itself — left unfixed for negation.
What the answer should be
The same shape #1126 gives an implication:
{ x : not a }names the set without naming a universe,and a complement written that way is right whatever
xranges over.with the rewrites that can do better than that —
not (x = a)where the equation is solvable,not (x > a)asx <= a— going in front of it if they are wanted. The point of the issue is thatthe fallback must not be
Empty.Worth checking at the same time whether
Solveof a bareBooleanshould beEmptyeither:"A implies true".ToEntity().Solve("A")is{ A : not A }becauseSolve(True, A)isEmpty,where every
Asatisfies it.