After tinkering around with variational arithmetic I've concluded I need a zipper to handle deeply nested choices. Consider this formula:
deepChoicesLHS :: IO Result
deepChoicesLHS = flip sat Nothing $
(1 - 2 - (3 - c)) .== 23
where c = iChc "AA" (iRef ("Aleft" :: Text)) (iRef "Aright") +
iChc "BB" (iRef "Bleft") (iRef "BRight")
The trick for the booleans was to rotate the AST hence allows plain values to be accumulated/evaluated thereby lifting choices, but for arithmetic this does not work because - is neither commutative or associative, and thus the only way to get to the choice here is to crawl the tree, capturing the context until we find the choice. In Vsat I used a zipper for this before I understood the tree rotations. For VSMT CPS will likely be faster than a zipper and more memory efficient, thus it is desirable. Furthermore, I conjectured and am pretty confident that continuations are the essence of variation and so the fact that CPS sticks out to me is likely an indication of this conjecture.
After tinkering around with variational arithmetic I've concluded I need a zipper to handle deeply nested choices. Consider this formula:
The trick for the booleans was to rotate the AST hence allows plain values to be accumulated/evaluated thereby lifting choices, but for arithmetic this does not work because
-is neither commutative or associative, and thus the only way to get to the choice here is to crawl the tree, capturing the context until we find the choice. In Vsat I used a zipper for this before I understood the tree rotations. For VSMT CPS will likely be faster than a zipper and more memory efficient, thus it is desirable. Furthermore, I conjectured and am pretty confident that continuations are the essence of variation and so the fact that CPS sticks out to me is likely an indication of this conjecture.