You have to bisect the facts. There's an open issue to do this automatically https://github.com/sympy/sympy/issues/8029.
I played with it and I believe the facts CheckOneByOneMatrix(Q.diagonal)) and CheckEmptyMatrix(Q.zero)) are wrong. These compile to Equivalent(Q.diagonal(A), A.shape == (1, 1)) and Equivalent(Q.zero(A), A.shape == (0, 0)). But Equivalent is incorrect here. It should just be reverse implication. Diagonal matrices are not necessarily 1x1, and zero matrices are not necessarily empty. I'm assuming you modeled these after CheckIsPrime. Direct equivalence handler classes like this should only be used to show the system that an assumption is equivalent to some computation on an object (e.g., Q.prime is equivalent to the isprime() function). No doubt some better naming, and perhaps some refactoring could make this clearer. Something like EmptyMatrix would need to be a predicate, not a handler. Something like (MatrixExpr, CheckEmptyMatrix(Q.EmptyMatrix)) would be a correct fact. Finally, your fact Implies(Q.diagonal, Q.symmetric)) is unnecessary (it's already in the known_facts in ask.py), and Implies(Q.zero & Q.square, Q.diagonal)) should go in ask.py, since it's a completely free fact (it's true regardless of what expression you apply it to). I also want to note that I'm a little worried about the use of Q.zero to refer to zero matrices. That could lead to problems down the road, since Q.zero means "real and zero" in the assumptions. However, just looking at the existing known_facts, I see a lot of inconsistencies and confusion of numbers and matrices (and operators) in the new assumptions, so as long as things work, we can probably punt this to another day. Aaron Meurer On Wed, Dec 14, 2016 at 11:56 PM, Andrey Torba <[email protected]> wrote: > How can I resolve "Inconsistent assumptions"? Any techniques how to find > what exactly is inconsistent? > > File "sympy/assumptions/satask.py", line 44, in satask > raise ValueError("Inconsistent assumptions") > ValueError: Inconsistent assumptions > > I know what rules cause inconsistency, but I can't understand why > > Example: > > class CheckSquareMatrix(UnevaluatedOnFree): > def apply(self): > r, c = self.expr.shape > return Equivalent(self.args[0], r == c) > > class CheckEmptyMatrix(UnevaluatedOnFree): > def apply(self): > return Equivalent(self.args[0], self.expr.shape == (0, 0)) > > class CheckOneByOneMatrix(UnevaluatedOnFree): > def apply(self): > return Equivalent(self.args[0], self.expr.shape == (1, 1)) > > (MatrixExpr, CheckSquareMatrix(Q.square)), > (MatrixExpr, CheckOneByOneMatrix(Q.diagonal)), > (MatrixExpr, CheckEmptyMatrix(Q.zero)), > (MatrixExpr, Implies(Q.zero & Q.square, Q.diagonal)), > (MatrixExpr, Implies(Q.diagonal, Q.symmetric)), > (ZeroMatrix, Q.zero), > (Identity, Q.diagonal), > > > > > On Wednesday, December 14, 2016 at 1:59:10 PM UTC-8, Aaron Meurer wrote: >> >> And a final thought, empty square and 1x1 matrices have multiple >> trivial facts. So probably having EmptySquareMatrix and OneByOneMatrix >> classes would be useful. I don't know if my Shape idea would be used >> other than for them. This is basically your original idea, except I >> think it would be useful to separate them out, since some more things >> are true about empty matrices than 1x1 matrices (just glancing at the >> existing facts, integer_elements and real_elements both apply, and if >> we ever add some kind of Q.elements(fact) meta-predicate for matrices, >> that would also apply by vacuous truth). >> >> Aaron Meurer >> >> On Wed, Dec 14, 2016 at 4:47 PM, Aaron Meurer <[email protected]> wrote: >> > Actually, using Eq for tuples seems problematic as well. Maybe just >> > something like ShapeEq((1, 1)), so the fact would be >> > >> > Implies(ShapeEq((1, 1)) | ShapeEq((0, 0)), Q.diagonal) >> > >> > That's just one idea. There's lots of ways you can equivalently write >> > the same thing. The goal is to make abstractions that make the facts >> > as readable as possible. >> > >> > Aaron Meurer >> > >> > On Wed, Dec 14, 2016 at 4:42 PM, Aaron Meurer <[email protected]> wrote: >> >> That looks good, although I might try to go for something more general. >> >> Maybe we just need a Shape class that we can combine with Eq, like >> >> Eq(Shape, >> >> (1, 1)) where Shape(A) evaluates as the shape of A. It wouldn't really >> >> be a >> >> predicate, though, so maybe some more thought is needed here. >> >> >> >> Aaron Meurer >> >> >> >> On Wed, Dec 14, 2016 at 4:35 PM Andrey Torba <[email protected]> >> >> wrote: >> >>> >> >>> Aaron, what should be done in order to add new sat handlers? >> >>> >> >>> I'm thinking where to start from? sympy/assumptions/sathandlers.py: >> >>> >> >>> class IsEmptyOr1x1(UnevaluatedOnFree): >> >>> >> >>> def apply(self): >> >>> return Equivalent(self.args[0], self.expr.shape == (0, 0) or >> >>> self.expr.shape == (1, 1)) >> >>> >> >>> >> >>> for klass, fact in [ >> >>> ... >> >>> (MatrixExpr, IsEmptyOr1x1(Q.diagonal)), >> >>> (MatrixExpr, Implies(Q.diagonal, Q.symmetric)), >> >>> ... >> >>> ] >> >>> >> >>> >> >>> On Monday, December 12, 2016 at 4:04:57 PM UTC-8, Aaron Meurer wrote: >> >>>> >> >>>> This is a downside of the handlers system. The deductions aren't made >> >>>> >> >>>> >> >>>> based on facts that the handlers return. This is one of the main >> >>>> >> >>>> >> >>>> deficiencies that the satask/sathandlers system tries to fix. I don't >> >>>> >> >>>> >> >>>> know if there's an easy fix to make it work in the handlers system. >> >>>> >> >>>> >> >>>> You could also manually modify the SymmetricHandler class to check >> >>>> for >> >>>> >> >>>> >> >>>> diagonal (this is obviously annoying, because it blatantly duplicates >> >>>> >> >>>> >> >>>> the general fact in get_known_facts >> >>>> >> >>>> >> >>>> >> >>>> >> >>>> https://github.com/sympy/sympy/blob/5827cafb1e1840915b3e7c9f62cd0d58fff9fc48/sympy/assumptions/ask.py#L1517). >> >>>> >> >>>> >> >>>> >> >>>> >> >>>> >> >>>> The better way to fix it is to implement it in the sathandlers >> >>>> system. >> >>>> >> >>>> >> >>>> No matrix stuff is implemented there yet, so it may require some >> >>>> >> >>>> >> >>>> ground work. >> >>>> >> >>>> >> >>>> >> >>>> >> >>>> >> >>>> Aaron Meurer >> >>>> >> >>>> >> >>>> >> >>>> >> >>>> >> >>>> On Mon, Dec 12, 2016 at 6:57 PM, Andrey Torba <[email protected]> >> >>>> wrote: >> >>>> >> >>>> >> >>>> > Hi, >> >>>> >> >>>> >> >>>> > >> >>>> >> >>>> >> >>>> > I'm working on the pull request. >> >>>> >> >>>> >> >>>> > >> >>>> >> >>>> >> >>>> > A 1x1 matrix is always diagonal. Diagonal implies symmetric. I have >> >>>> > fixed >> >>>> >> >>>> >> >>>> > AskDiagonalHandler such that this assertion pass: >> >>>> >> >>>> >> >>>> > >> >>>> >> >>>> >> >>>> > V1 = MatrixSymbol('V1', 2, 1) >> >>>> >> >>>> >> >>>> > V2 = MatrixSymbol('V2', 2, 1) >> >>>> >> >>>> >> >>>> > expr = V1.T*(V1 + V2) >> >>>> >> >>>> >> >>>> > assert ask(Q.diagonal(expr)) is True >> >>>> >> >>>> >> >>>> > >> >>>> >> >>>> >> >>>> > Now I assume that inference module will deduce that this expression >> >>>> > is >> >>>> > also >> >>>> >> >>>> >> >>>> > symmetric (since the expression is diagonal): >> >>>> >> >>>> >> >>>> > >> >>>> >> >>>> >> >>>> > assert ask(Q.symmetric(expr)) is True # it is >> >>>> > None! >> >>>> >> >>>> >> >>>> > >> >>>> >> >>>> >> >>>> > It returns None. Is anything missing? Can you show an example where >> >>>> > this >> >>>> >> >>>> >> >>>> > kind of inference works well? >> >>>> >> >>>> >> >>>> > >> >>>> >> >>>> >> >>>> > -Andrey >> >>>> >> >>>> >> >>>> > >> >>>> >> >>>> >> >>>> > -- >> >>>> >> >>>> >> >>>> > You received this message because you are subscribed to the Google >> >>>> > Groups >> >>>> >> >>>> >> >>>> > "sympy" group. >> >>>> >> >>>> >> >>>> > To unsubscribe from this group and stop receiving emails from it, >> >>>> > send >> >>>> > an >> >>>> >> >>>> >> >>>> > email to [email protected]. >> >>>> >> >>>> >> >>>> > To post to this group, send email to [email protected]. >> >>>> >> >>>> >> >>>> > Visit this group at https://groups.google.com/group/sympy. >> >>>> >> >>>> >> >>>> > To view this discussion on the web visit >> >>>> >> >>>> >> >>>> > >> >>>> > >> >>>> > https://groups.google.com/d/msgid/sympy/d84286f8-9a6f-469b-ac95-4a3c8b21cda2%40googlegroups.com. >> >>>> >> >>>> >> >>>> > For more options, visit https://groups.google.com/d/optout. >> >>>> >> >>>> >> >>> >> >>> >> >>> >> >>> >> >>> >> >>> >> >>> >> >>> >> >>> -- >> >>> >> >>> >> >>> You received this message because you are subscribed to the Google >> >>> Groups >> >>> "sympy" group. >> >>> >> >>> >> >>> To unsubscribe from this group and stop receiving emails from it, send >> >>> an >> >>> email to [email protected]. >> >>> >> >>> >> >>> To post to this group, send email to [email protected]. >> >>> >> >>> >> >>> Visit this group at https://groups.google.com/group/sympy. >> >>> >> >>> >> >>> To view this discussion on the web visit >> >>> >> >>> https://groups.google.com/d/msgid/sympy/1e2b221a-2b4a-48f5-b1dc-44ff6ab0db28%40googlegroups.com. >> >>> >> >>> >> >>> For more options, visit https://groups.google.com/d/optout. >> >>> >> >>> >> >> > > -- > You received this message because you are subscribed to the Google Groups > "sympy" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To post to this group, send email to [email protected]. > Visit this group at https://groups.google.com/group/sympy. > To view this discussion on the web visit > https://groups.google.com/d/msgid/sympy/0ea41a27-64fb-4dfb-8ad0-bed1472c7b81%40googlegroups.com. > > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "sympy" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/sympy. To view this discussion on the web visit https://groups.google.com/d/msgid/sympy/CAKgW%3D6Ltv7U3GHinjjykav5dAP0%3DJzrnXTcb0cGE8xOreQX5OQ%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
