Refactor code tree search structs; change flat term to lazily expandi…

…ng version in term code trees
vprover · Apr 10, 2024 · a336557 · a336557
1 parent 5a168f8
commit a336557
Show file tree

Hide file tree

Showing 9 changed files with 309 additions and 258 deletions.
diff --git a/Indexing/ClauseCodeTree.cpp b/Indexing/ClauseCodeTree.cpp
@@ -74,6 +74,7 @@ void ClauseCodeTree::insert(Clause* cl)
   cctx.init();
 
   for(unsigned i=0;i<clen;i++) {
+    cctx.nextLit();
     compileTerm(lits[i], code, cctx, true);
   }
   code.push(CodeOp::getSuccess(cl));
@@ -185,7 +186,7 @@ void ClauseCodeTree::matchCode(CodeStack& code, CodeOp* startOp, size_t& matched
       if(treeOp->isSearchStruct()) {
 	SearchStruct* ss=treeOp->getSearchStruct();
 	CodeOp** toPtr;
-	if(ss->getTargetOpPtr(code[i], toPtr) && *toPtr) {
+	if(ss->getTargetOpPtr<false>(code[i], toPtr) && *toPtr) {
 	  treeOp=*toPtr;
 	  continue;
 	}