Separate generalizing term index and use code trees#848
Open
mezpusz wants to merge 8 commits into
Open
Conversation
…naling termination to the caller
mezpusz
commented
Apr 29, 2026
| auto t = data->key(); | ||
| if (t.isVar()) { | ||
| code.push(CodeOp::getTermOp(ASSIGN_VAR,0)); | ||
| // we match the variable sort separately, but the binding array has to be prepared |
Contributor
Author
There was a problem hiding this comment.
Variable matching change 1.
mezpusz
commented
Apr 29, 2026
|
|
||
| ASS(Base::op->isSuccess()); | ||
| return Base::op->template getSuccessResult<Data>(); | ||
| while ((Base::_matched=Base::execute())) { |
Contributor
Author
There was a problem hiding this comment.
Variable matching change 2.
mezpusz
commented
Apr 29, 2026
| return Term::getVariableIterator(untyped()); | ||
| } | ||
|
|
||
| bool containsAllVariablesOf(TypedTermList other) const { |
Contributor
Author
There was a problem hiding this comment.
Variable matching change 3.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR is a first step towards making code trees the default for matching (generalizing) indices. This will help us focus on code trees for matching in the future, e.g. extending it to HOL.
Most of the PR contains just removing interface code so that code trees can be more directly used as generalizing term indices.
One missing feature from term code trees was the handling of sorts of indexed variables. An ad-hoc fix was used in forward demodulation but this was not even used in the critical case where the variable has a non-ground sort, as those equations were not added to the demodulation LHS index due to another small bug. In any case, handling inside the code tree is more natural (IMO), but it could be later updated to share also the variable sorts in a separate code tree, such that sort matching would be also efficient.
I also switched all places where we used substitution trees for getting generalizations to use code trees. In particular, in induction, ALASCA demodulation and obtaining Skolems in CNF on the fly.
Regression results are shown below:
ALASCA SMTLIB+TPTP:
run 0 unsat: 44428 (0) sat: 135 (0) cputime: 48261.48 s instructions: 185056392 Mi memory: 996109.45 MB
run 1 unsat: 44428 (0) sat: 135 (0) cputime: 48617.18 s instructions: 185033849 Mi memory: 995655.16 MB
(Two problems flipped from timeout to error, I checked these locally and the error happens with a bigger timeout on master.)
FOL Discount TPTP:
run 0 unsat: 9208 (0) sat: 1042 (0) cputime: 56855.80 s instructions: 222732554 Mi memory: 1462215.63 MB
run 1 unsat: 9208 (0) sat: 1042 (0) cputime: 57448.59 s instructions: 222738803 Mi memory: 1462395.81 MB
FOL Otter TPTP:
run 0 unsat: 9321 (2) sat: 1025 (1) cputime: 61948.36 s instructions: 222706049 Mi memory: 1694946.39 MB
run 1 unsat: 9322 (3) sat: 1024 (0) cputime: 62511.80 s instructions: 222690853 Mi memory: 1695844.64 MB
(I will check the diff here more closely, most likely noise.)
HOL Discount TPTP:
run 0 unsat: 2112 (0) sat: 1 (0) cputime: 8822.22 s instructions: 43898419 Mi memory: 113978.75 MB
run 1 unsat: 2112 (0) sat: 1 (0) cputime: 8812.26 s instructions: 43899663 Mi memory: 113938.23 MB
HOL Otter TPTP:
run 0 unsat: 2073 (0) sat: 1 (0) cputime: 9278.63 s instructions: 44823797 Mi memory: 136652.94 MB
run 1 unsat: 2073 (0) sat: 1 (0) cputime: 9291.50 s instructions: 44824137 Mi memory: 136576.49 MB
Induction:
run 0 unsat: 973 (3) sat: 0 (0) cputime: 11091.90 s instructions: 45481819 Mi memory: 673205.01 MB
run 1 unsat: 973 (3) sat: 0 (0) cputime: 11088.78 s instructions: 45482307 Mi memory: 672135.89 MB
(Diff to be checked here too.)
Synthesis:
run 0 unsat: 438 (0) sat: 0 (0) cputime: 1226.62 s instructions: 5234739 Mi memory: 52817.96 MB
run 1 unsat: 438 (0) sat: 0 (0) cputime: 1227.77 s instructions: 5234630 Mi memory: 52778.30 MB