Petar Vukmirovic
2020-04-29 16:50:49 (GMT)
As discussed with Simon, to make simplification a bit stronger in Zip,
I wanted to collect all positive ground equalities both in passive and in active set,
and sue them for
- Tautology checking -- if any ground positive literal is implied by this equational theory, then the clause is tautology
- Literal cutting -- if any negative ground literal can be resolved using this eq. theory, then the literal can be removed
This would be performed both when clause is picked for processing, but also moved from unprocessed to passive set
(right now for this second part, clauses are not rewritten, so ground rewriting cannot achieve the same effect)
Algorithm that I would use for this is Congruence closure.
Petar Vukmirovic
2020-04-29 16:51:24 (GMT)
But I have one problem (@Simon Cruanes ):
Right now, CC as implemented in Zip, does not allow for proof generation, that is, it does not support Explain operation
Petar Vukmirovic
2020-04-29 16:52:8 (GMT)
I have found this ( image.png in the paper
Proof-Producing Congruence Closure
Robert Nieuwenhuis and Albert Oliveras
Simon Cruanes
2020-04-29 16:52:9 (GMT)
yes, it's a lot more naive than the one you can find in sidekick. Writing a good CC is a bit of work.
Petar Vukmirovic
2020-04-29 16:52:28 (GMT)
Is this what you use for proof generation
Simon Cruanes
2020-04-29 16:53:1 (GMT)
the one in sidekick (which, btw, is a small library of its own) does provide backtracking and explanations.
And yes, it's used to produce conflicts, following that paper (except, without the currying bits — just kept the proof forest part)
Simon Cruanes
2020-04-29 16:53:23 (GMT)
If you read the code you'll find reroot functions and all the other bells and whistles :)
Petar Vukmirovic
2020-04-29 16:54:11 (GMT)
But it is very easy to modify your simple CC in Zip if I understood the idea of this paper properly:
Petar Vukmirovic
2020-04-29 16:54:32 (GMT)
I just need to annotate each merge operation with the unit equation responsible for the merge
Petar Vukmirovic
2020-04-29 16:54:46 (GMT)
And keep the non-path-compressed pointers?
Simon Cruanes
2020-04-29 16:54:47 (GMT)
It's not that easy, there's some work to do :p
But I shouldn't push sidekick too much, Zipper is also your project now.
Petar Vukmirovic
2020-04-29 16:55:38 (GMT)
I mean I am happy to just reuse Sidekick's CC algo if it is easy to integrate
Simon Cruanes
2020-04-29 16:55:50 (GMT)
Petar Vukmirovic said:
I just need to annotate each merge operation with the unit equation responsible for the merge
you also need to maintain proof forests, and add explanations for congruence operations. And then for explanations you need stuff like finding a path between a and b when the explanation for a ~ b is needed.
I urge you to at least _read_ the code of sidekick-cc.
Simon Cruanes
2020-04-29 16:56:24 (GMT)
Petar Vukmirovic said:
I mean I am happy to just reuse Sidekick's CC algo if it is easy to integrate
you can copy paste it into zipper, if it makes things simpler :)
Petar Vukmirovic
2020-04-29 17:36:3 (GMT)
Aaaahhh... I get it now.. when you do congurence check and if it suceeds the explanation is dependent on the explanations already there in CC
for the arguments
Petar Vukmirovic
2020-04-29 17:36:9 (GMT)
That is why you need the tree
Petar Vukmirovic
2020-04-29 17:36:13 (GMT)
Right?
Simon Cruanes
2020-04-29 17:49:37 (GMT)
Hum, you need the tree to remember why you merged classes, for the day you need to explain why a=b. Classes can be merged either directly by asserting t=u (merges [t] and [u]) or because t=u implies f(t) = f(u)`.
Typically you need explanation to justify propagation of booleans in the SAT solver (in CDCL(T), eager propagation) or to make a small conflict.
Petar Vukmirovic
2020-04-29 17:51:21 (GMT)
Of course... I was just trying to undesrtyand why the idea of simply annotating each merge with an equation it stems from is not enough
Petar Vukmirovic
2020-04-29 17:52:33 (GMT)
And the reason is that not every merge is external (bc you insterted new equation), but there are also internal merges (consequence of calling merge after checking congurence of nodes) which depend on the equations already in the structure
Petar Vukmirovic
2020-04-29 17:52:50 (GMT)
And thus, simple annotation of the merge with an equation is not enough
Petar Vukmirovic
2020-04-29 17:56:38 (GMT)
But I will first implement this wihout proof generation
Petar Vukmirovic
2020-04-29 17:57:7 (GMT)
and then see if it works nicely, and if not then forget about it :slight_smile:
Petar Vukmirovic
2020-04-29 17:57:23 (GMT)
if it does, I will augment Zip's CC to support proof generation
Simon Cruanes
2020-04-29 18:38:56 (GMT)
I still have hopes to get sidekick in there to get Avatar-light modulo UF :)
Or at least to proof check efficiently.
And dolmen, on which @Guillaume Bury works a lot and which would give us cleaner THF and smt2 parsers…
Guillaume Bury
2020-04-29 18:56:12 (GMT)
I can only be supportive of including dolmen ! I'm working on it quite a lot currently as @Simon Cruanes says, so any issue or feature request will be resolved quickly, ^^
Petar Vukmirovic
2020-04-29 18:58:29 (GMT)
I will take a look :slight_smile: Thank you guys :slight_smile:
Simon Cruanes
2020-04-29 19:48:7 (GMT)
Also I encourage tooling geeks to give a try to dolmenls which does syntax and typechecking of smt2, zf, tptp problems directly in your editor, real time :)