Stream: t-compiler/wg-polonius

Topic: Datalog and incremental SMT solving


Albin Stjerna (Aug 11 2020 at 17:47, on Zulip):

This might be relevant to the Chalk integration?

lqd (Aug 11 2020 at 20:55, on Zulip):

is that a poster ? the complete Formulog paper seemed bigger when I saw it a couple days ago

lqd (Aug 11 2020 at 20:56, on Zulip):

but I think SMT solvers seem unlikely to land in rustc :)

lqd (Aug 11 2020 at 20:58, on Zulip):

but just reading the refinement type checker as one of the examples in the paper had me make this face: :heart_eyes:

Albin Stjerna (Aug 13 2020 at 12:14, on Zulip):

I didn't read it yet, but perhaps I should :)

Albin Stjerna (Aug 13 2020 at 12:14, on Zulip):

I have...a large stack of papers to read, to say the least

RalfJ (Aug 14 2020 at 09:36, on Zulip):

Albin Stjerna said:

I have...a large stack of papers to read, to say the least

I know that feeling. my "papers to read" folder has a subfolder "more relevant than others" and even that subfolder has too many papers in it...

bjorn3 (Aug 14 2020 at 16:48, on Zulip):

I have a lot of papers on my phone that I read while traveling to and from university.

Vytautas Astrauskas (Aug 16 2020 at 15:35, on Zulip):

bjorn3 said:

I have a lot of papers on my phone that I read while traveling to and from university.

Unfortunately, the trip from my bed to my desk is too short to read even a sentence…

bjorn3 (Aug 16 2020 at 16:02, on Zulip):

Since the pandemic I haven't read much papers myself either.

Albin Stjerna (Aug 18 2020 at 12:05, on Zulip):

I...bike to university and don't think it would be a good idea to read while I do so

Albin Stjerna (Aug 18 2020 at 12:05, on Zulip):

Also, it takes three minutes

namibj (Aug 19 2020 at 00:45, on Zulip):

@Albin Stjerna said:

I didn't read it yet, but perhaps I should :)

Well, the last message of yours in here made me read it, it's thankfully quite short at 2.5 pages not counting references.

TL;DR: If you have a directed graph where each node has an SMT preposition φ attached to it, and want to efficiently find a path through the graph where the conjunction of the traversed node's SMT prepositions remains SAT, you just introduce one boolean variable x per graph node, rewrite the node's contribution to the SMT input to the implication x => φ, and then just ask the solver with check-sat-assuming (setting all those boolean variables based on whether the respective node is part of the path we're currently considering). They call this tactic CSA.

This lets the solver cache a lot, without really caring about the order in which we explore paths, and gives a speedup in 79 of 105 total experiments (over non-incremental baseline), being surpassed by a simple stack-based backtrace (named PP; using the assertion stack with push and pop) in 7 experiments.
In 2 of the 7, CSA did not improve over baseline, while PP did. In the other 5 experiments, both improved on baseline, but PP did a better job.
For symbolic execution, incremental was always better, and 12 of 18 cases were won by CSA.
For refinement-types type-checking, CSA won for all 3 input programs (improving over baseline and delivering the best improvements).
The random graph tests went mostly-good, with about half of the cases where incremental solving did not deliver an improvement used a logic combining linear integer arithmetic (_not_ bit vector logic) with arrays.

Albin Stjerna (Aug 19 2020 at 09:19, on Zulip):

Wow, doing my work for me, thanks!

lqd (Sep 01 2020 at 23:08, on Zulip):

this was also cute https://github.com/ekzhang/crepe

Albin Stjerna (Dec 02 2020 at 13:41, on Zulip):

lqd said:

this was also cute https://github.com/ekzhang/crepe

Wow yes!

Last update: Jun 20 2021 at 00:00UTC