Code tree subsumption #605
Conversation
…ype in front of equality arguments in both flatterm/codetree -- initial implementation
|
Debug tests were run, so far no assrtion violations. Correctness checks have been performed with the current SAT subsumption, showing that there is (i) no unsoundness, but (ii) code tree subsumption cannot detect set-based subsumption resolution, only multiset-based.
Surely it can - we did it ages ago. The only difference is the
interpretation of the instruction in charge of setting the literal in
the query clause. For multisets, you iterate through previously
untried literals. For sets, you iterate through all literals.
A
|
|
This looks awesome. Thank you, @mezpusz . Even before checking the code change in full, I suggest we make |
Thanks, it's good to know that it should work. Then perhaps a subsequent PR could fix this, I'm not sure at this point where this should happen in the current code. |
I agree, and big thanks to whoever implemented this in the first place. 🙂 Additionally, since the SAT subsumption cross-check on top is relatively cheap after we have found an instance, maybe we could add that as a permanent debug check to make sure no bugs creep in. |
|
Just to make it clear: set subsumption is super incomplete. Set subsumption
can be used for subsumption resolution because it always resolves away a
literal, so it creates a strictly smaller clause.
A
…On Wed, 18 Sept 2024 at 13:51, Márton Hajdu ***@***.***> wrote:
***@***.**** commented on this pull request.
------------------------------
In Shell/ConditionalRedundancyHandler.cpp
<#605 (comment)>:
> for (const auto& t : ts) {
if (t.isVar()) {
- unsigned var=t.var();
- unsigned* varNumPtr;
- if (cctx.varMap.getValuePtr(var,varNumPtr)) {
- *varNumPtr=cctx.nextVarNum++;
- code.push(CodeOp::getTermOp(ASSIGN_VAR, *varNumPtr));
- } else {
- code.push(CodeOp::getTermOp(CHECK_VAR, *varNumPtr));
- }
- }
- else {
- ASS(t.isTerm());
- compileTerm(t.term(), code, cctx, false);
+ compiler.handleVar(t.var());
+ continue;
https://github.com/vprover/vampire/pull/605/files/4288d86b61ab4c0d837740e63aa68595625dd317#diff-27f226e0d1aa0fbd306b419b284352bf6030973f67de4bda4123b7f045bcce26R728
—
Reply to this email directly, view it on GitHub
<#605 (comment)>, or
unsubscribe
<https://github.com/notifications/unsubscribe-auth/ABVY4BKNVQ6NCOSEUYEY3LTZXFSLDAVCNFSM6AAAAABONCYNASVHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMZDGMJSGQ2TKMBZGE>
.
You are receiving this because you commented.Message ID:
***@***.***>
|
|
In #265 I removed a dead file called |
Thanks, that's a good suggestion! I have checked the code, fortunately it looks very similar, apart from (i) setting the age of the result for some reason and (ii) doing something with |
|
Agreed. Whatever |
Revival of code tree subsumption. The following fixes were necessary:
LIT_ENDwas not set properly in the code tree forILStructobjects.FlatTermandCodeStackto avoid unsoundness in the two-variable equality case. Some refactors were necessary to do this cleanly.Debug tests were run, so far no assrtion violations. Correctness checks have been performed with the current SAT subsumption, showing that there is (i) no unsoundness, but (ii) code tree subsumption cannot detect set-based subsumption resolution, only multiset-based.
The final experimental data:
In parentheses the number of uniques are shown of master to codetree, regression to codetree and codetree to master, respectively.