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/CAKgW%3D6L-GQhE8PUtmYubTq0-mvk9OE9Nta8JQUxJ-WbeZh0SjQ%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
