the idea here is to avoid lots of pack and unpacking of these values. The average case has is way more lookups then generations, so when we lookup we don’t want any extra actions
Issue: #7
- Note taken on [2020-11-12 Thu 18:16]
With the parallel version of vsmt we have to season the solver with the variational core. This means that we actually computenIL’s wherenis the number of threads. This is likely a small price to pay for the parallelism but could certainly be reduced. SBVsSymbolicTis a reader monad overIObut sbv doesn’t export theReaderTtype class instance, so in the main thread we can season, then grab the state withT.symbolicEnvbut then there is no way for me to calllocalover the thread instances and thus no way to replace the thread states with the seasoned state. Hence, we are forced recompute the state for each thread with a call withtoIL.
Not enough time left in phd for this
- Note taken on [2020-11-12 Thu 14:32]
Megaparsec is great but can have memory blow up if the parser isn’t exactly right, Early only parses context free grammars but you never have backtracking so it can be much much faster
- Note taken on [2020-12-03 Thu 20:01]
Right now I have an additional O(n) pass before generating the variational core - Note taken on [2020-12-03 Thu 20:00]
We need to know the number of unique dimensions to know the maximum possible variants, this allows the solver to shut down
If we find a statement like:
(assert (== x 2))
then do we perform propagation for x -> 2?
- Note taken on [2020-12-22 Tue 12:53]
We ran into a severe architectural issue with the async version of vsmt. The problem boils down to have to copy the base solver state for each alternative. sbv currently doesn’t have a way to do that so I added a freeze un-freeze strategy from the vector package, but the z3 state still messed up. There are two paths forward: 1. get sbv to return all the constants and asserstions to recreate the solver state, this is what is recommended by z3 devs and 2: use configurations to maintain the correct context for each thread. This last strategy is very brute force-y and essentially admits defeat. - Note taken on [2020-12-03 Thu 21:47]
I tried to toggle debugging in the type system. It didn’t work because the channels are hard coded over the solver monad. If you try to paramterize it then we have problems with the has typeclass which now must be parameterized over the input to state. This looks like living with the redundancy is the easiest win for the remainder of the phd - Note taken on [2020-09-19 Sat 04:47]
Massive changes to the internal model of the solver today. Most importantly I was liberated of several assumptions I had made from vsat. In vsat I moved all unary operators (justNot) into either symbolic terms or into choices. This worked well because there were never any edge cases where I would not be able to move a negation via a distributive property. In vsmt this is not the case, you may have aNotover and inequality that has complicated arithmetic in it and thus you cannot distribute theNot. Hence I combined the zipper I made yesterday to include boolean contexts. This greatly simplified the code base and made it much easier to reason about. I have check vsmt’s soundness up to ~700 random tests with propositions that only hold boolean terms. For a mix of arithmetic and boolean terms there are several problems: first is the quickcheck is creating propositions that aren’t satisfiable themselves and so the solver concludes unsat and the test fails, secondly I’ve had to filter out a lot of floats because they explode the search space and thus acheck-satcall takes too much time. I’ve limited the solver to 15 seconds per check sat in the meantime. All things considered I’m very confident in the soundness of the solver now, i’m sure there are edge cases lurking in the arithmetic but these are likely too expensive to nail down and probably also exist inz3andsbv. - Note taken on [2020-09-15 Tue 15:59]
I noticed that evaluate’, the form of evaluate that works on arithmetics had typeIL' -> IL'. This is strange because it is pure! Then I noticed thatevaluate'was identical toaccumulate'which makes sense because accumulation is pure symbolic evaluation. Hence I removedevaluate'in favor ofaccumulate'which is more accurate about the effects that are occurring - Note taken on [2020-09-15 Tue 02:36]
Fixed the result accumulation. I employed a Maybe to wrap around the Variant Context. There needs to be hygiene work next, the code doesn’t read well and neither do the types. Which means that now I have a working implementation some refactoring is in order - Note taken on [2020-09-14 Mon 18:36]
Solver core is working for up to two choices now. However, the result module is not accumulating results properly. There are several problems:- mappend is erasing previous results
- We fundamentally need a way to demarcate between variables which are local to the assertion stack and those which are not
- the
itebuilding is not occurring the linked list of return values
- Note taken on [2020-11-10 Tue 13:50]
Quite easy actually, we spin up a second thread and use channels to send over a dimension asking the solver to check if the dimension is true in current context and then return the result
- Note taken on [2021-03-24 Wed 12:32]
Tried to use StableNames to memoize accumulation. This is a no-go, the references in the sat solver are lost with stable names and the memoization is too expensive without StableNames to use on ASTs
- Note taken on [2021-03-24 Wed 12:33]
I tried IORef’s vs STM and found no difference between then for this workload. Going to stick with STM which has a better interface
- Note taken on [2021-03-24 Wed 12:34]
Newtype wrapper for only booleans is done - Note taken on [2020-09-19 Sat 14:39]
soundness is setup and working but we need newtype wrappers instead of predicates, see #4
link: http://hackage.haskell.org/package/text-metrics-0.3.0/docs/Data-Text-Metrics.html