doyougnu / VSmt

Variational Satisfiability Solver
3 stars 0 forks source link

Use Continuation Passing Style #3

Open doyougnu opened 4 years ago

doyougnu commented 4 years ago

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.

doyougnu commented 4 years ago

zipper for arithmetic expressions added in a892f0ebb84cf5467a5e279bb59d1f095da20fd4 and produces sound results.