Yices : ever thought of a great idea, implemented it and then found you still couldn't beat another solver because they thought of it first? It was Yices that thought of it first.
-
Thanks! I've been thinking of making arrays go away for one task that I'm modelling. Unfortunately, there's another task where I can't imagine how to do it without arrays (for those into that sort of thing, modelling the x86 instructions PEXT or PDEP and generating a const mask).
-
-
One thing I have on my todo list is playing with the following: PEXT is a bwd butterfly circuit with pre-and-mask, PDEP a fwd butterfly circuit with post-and-mask. But those butterflies are more powerful than PEXT/PDEP.
-
So maybe I can find an efficient way of constraint those butterfly control signals to only implement permutations that correlate to PEXT/PDEP. (This idea is based on the insights from http://palms.ee.princeton.edu/PALMSopen/hilewitz06FastBitCompression.pdf ….)
- Show replies
New conversation -
-
-
OK, so the butterfly idea is way ahead of mine. For PEXT/bext, I was imagining (pls don't laugh, I am SMT noob) that we'd generate an array with constraints dictating strictly ascending bits (obvs in the range of 0..bitwidth-1) and shift/extract the bits.
-
I think that's a perfectly fine way of encoding PEXT if it's fast enough. I wouldn't use an array for that though. Simply use 32/64 individual variables. (Array abstraction only makes sense if you don't access all 2^N elements, otherwise just using 2^N individual vars is better.)
End of conversation
New conversation -
-
-
If there is a copy of the notes going past I can have a look if that would help. The cost trade-off between hardware and SMT are different in subtle ways.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.