search

vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
302 stars 52 forks source link

Code tree subsumption #605

Closed mezpusz closed 2 months ago

mezpusz commented 2 months ago

Revival of code tree subsumption. The following fixes were necessary:

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:

master regression codetree
discount 9981 (47) 9981 (47) 10150 (216)
otter 9720 (42) 9720 (43) 9967 (289)

In parentheses the number of uniques are shown of master to codetree, regression to codetree and codetree to master, respectively.

easychair commented 2 months ago

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

quickbeam123 commented 2 months ago

This looks awesome. Thank you, @mezpusz .

Even before checking the code change in full, I suggest we make -cts on the default.

mezpusz commented 2 months ago

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

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.

mezpusz commented 2 months ago

This looks awesome. Thank you, @mezpusz .

Even before checking the code change in full, I suggest we make -cts on the default.

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.

easychair commented 2 months ago

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 https://github.com/vprover/vampire/pull/605#discussion_r1764914317:

 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 https://github.com/vprover/vampire/pull/605#discussion_r1764914317, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABVY4BKNVQ6NCOSEUYEY3LTZXFSLDAVCNFSM6AAAAABONCYNASVHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMZDGMJSGQ2TKMBZGE . You are receiving this because you commented.Message ID: @.***>

MichaelRawson commented 2 months ago

In #265 I removed a dead file called CTFwSubsAndRes which looks a bit like your CodeTreeForwardSubsumptionAndResolution. I think your new shiny code is probably better but might be worth a look to see if you forgot anything.

mezpusz commented 2 months ago

In #265 I removed a dead file called CTFwSubsAndRes which looks a bit like your CodeTreeForwardSubsumptionAndResolution. I think your new shiny code is probably better but might be worth a look to see if you forgot anything.

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 Clause::_auxData. I believe none of these are necessary anymore, but let me know what you think.

MichaelRawson commented 2 months ago

Agreed. Whatever auxData is I'm happy it's dead, but maybe the age needs to be set: @quickbeam123 is the resident expert, I think.