Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
34 commits
Select commit Hold shift + click to select a range
3a2dacb
Use KBO state in KBOComparator instead of computing weight and variab…
mezpusz Jun 26, 2024
7a48a0b
Perform instance redundancy check at the beginning of superposition
mezpusz Jun 26, 2024
2866dde
Add leaf printing functionality to code trees
mezpusz Jul 17, 2024
09e01a0
Templatize InstanceRedundancyHandler (now ConditionalRedundancyHandle…
mezpusz Jul 19, 2024
b402796
Rename InstanceRedundancyHandler files to ConditionalRedundancyHandler
mezpusz Jul 19, 2024
db98d89
Fix ordering constraint check; modify schedules to new option values
mezpusz Jul 19, 2024
3390c94
Implement literal constraints
mezpusz Jul 21, 2024
0d1093d
Merge branch 'master' into optimise-instance-redundancy-handler
mezpusz Jul 21, 2024
08034aa
Merge branch 'master' into optimise-instance-redundancy-handler
mezpusz Jul 22, 2024
be9fd29
Add a somewhat experimental AVATAR extension; do some refactoring
mezpusz Jul 23, 2024
6219018
Check unification of equations initially for each clause
mezpusz Jul 24, 2024
751f6f3
Use secondary ordering check when first is trivial when inserting sup…
mezpusz Jul 24, 2024
7505da1
Refactor CodeTree::Matcher
mezpusz Jul 25, 2024
76494c6
Resurrect code tree subsumption and subsumption resolution
mezpusz Jul 25, 2024
597b5a7
Add some functionality to the branch, variable orders, partial orders…
mezpusz Jul 30, 2024
a2f5902
Merge branch 'master' into optimise-instance-redundancy-handler
mezpusz Jul 31, 2024
b0679bf
Merge branch 'master' into optimise-instance-redundancy-handler
mezpusz Aug 9, 2024
b860664
Add some functionality to variable orderings
mezpusz Sep 9, 2024
77741b2
Merge branch 'master' into optimise-instance-redundancy-handler
mezpusz Sep 13, 2024
ca36015
Merge branch 'master' into optimise-instance-redundancy-handler
mezpusz Sep 21, 2024
0a17561
Merge branch 'master' into optimise-instance-redundancy-handler
mezpusz Feb 1, 2025
d9ea2b4
Remove unused stuff
mezpusz Feb 1, 2025
617806e
Merge branch 'master' into refactor-code-tree-matchers
mezpusz Mar 20, 2025
f704aa3
Remove unnecessary changes
mezpusz Mar 20, 2025
0b1c5cf
Merge branch 'master' into refactor-code-tree-matchers
mezpusz Mar 25, 2025
a66508f
Merge branch 'master' into refactor-code-tree-matchers
mezpusz Apr 7, 2025
c8f095f
Merge branch 'master' into refactor-code-tree-matchers
mezpusz Apr 8, 2025
281b740
Remove todo
mezpusz Apr 8, 2025
446dce5
Merge branch 'master' into refactor-code-tree-matchers
mezpusz Apr 9, 2025
a34988d
Remove remaining diff from original classes
mezpusz Apr 9, 2025
884347e
Hide assertion behind constexpr condition
mezpusz Apr 9, 2025
aedc38d
Merge branch 'master' into refactor-code-tree-matchers
mezpusz Jul 17, 2025
3e79092
Merge branch 'master' into refactor-code-tree-matchers
mezpusz Jan 21, 2026
edf362d
Merge branch 'master' into refactor-code-tree-matchers
mezpusz Jan 24, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 4 additions & 7 deletions Indexing/ClauseCodeTree.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -245,7 +245,7 @@ void ClauseCodeTree::remove(Clause* cl)
}

iteration_restart:
if(!rlm->next()) {
if(!rlm->execute()) {
if(depth==0) {
ASSERTION_VIOLATION;
INVALID_OPERATION("clause to be removed was not found");
Expand Down Expand Up @@ -286,7 +286,7 @@ void ClauseCodeTree::remove(Clause* cl)
void ClauseCodeTree::RemovingLiteralMatcher::init(CodeOp* entry_, LitInfo* linfos_,
size_t linfoCnt_, ClauseCodeTree* tree_, Stack<CodeOp*>* firstsInBlocks_)
{
RemovingMatcher::init(entry_, linfos_, linfoCnt_, tree_, firstsInBlocks_);
Matcher::init(tree_, entry_, linfos_, linfoCnt_, firstsInBlocks_);

ALWAYS(prepareLiteral());
}
Expand Down Expand Up @@ -326,10 +326,7 @@ void ClauseCodeTree::LiteralMatcher::init(CodeTree* tree_, CodeOp* entry_,
{
ASS_G(linfoCnt_,0);

Matcher::init(tree_,entry_);

linfos=linfos_;
linfoCnt=linfoCnt_;
Matcher::init(tree_,entry_,linfos_,linfoCnt_);

_eagerlyMatched=false;
eagerResults.reset();
Expand All @@ -341,7 +338,7 @@ void ClauseCodeTree::LiteralMatcher::init(CodeTree* tree_, CodeOp* entry_,
//(and those must be at the entry point or its alternatives)

_eagerlyMatched=true;
_fresh=false;
fresh=false;
CodeOp* sop=entry;
while(sop) {
if(sop->isSuccess()) {
Expand Down
4 changes: 2 additions & 2 deletions Indexing/ClauseCodeTree.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ class ClauseCodeTree : public CodeTree
bool removeOneOfAlternatives(CodeOp* op, Clause* cl, Stack<CodeOp*>* firstsInBlocks);

struct RemovingLiteralMatcher
: public RemovingMatcher<false>
: public Matcher</*removing*/true,false>
{
void init(CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_,
ClauseCodeTree* tree_, Stack<CodeOp*>* firstsInBlocks_);
Expand All @@ -69,7 +69,7 @@ class ClauseCodeTree : public CodeTree
*
* Here the actual execution of the code of the tree takes place */
struct LiteralMatcher
: public Matcher
: public Matcher</*removing*/false,false>
{
void init(CodeTree* tree, CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, bool seekOnlySuccess=false);
bool next();
Expand Down
Loading