From 3c1582035a2acf1b2406e62eccacb1d07429de15 Mon Sep 17 00:00:00 2001 From: Richard Qin Date: Sat, 4 Apr 2026 02:33:26 +0800 Subject: feat: implement variable renaming and update resolution logic to prevent variable collisions --- include/atp/infer/resolution.h | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) (limited to 'include/atp') diff --git a/include/atp/infer/resolution.h b/include/atp/infer/resolution.h index 2d73b06..c31ff0e 100644 --- a/include/atp/infer/resolution.h +++ b/include/atp/infer/resolution.h @@ -32,13 +32,19 @@ namespace atp { /// Attempt binary resolution between two clauses on the specified literal indices. /// @return The resolvent clause if resolution succeeds, std::nullopt otherwise. -std::optional resolve(const TermBank& bank, const Clause& c1, size_t lit_idx1, +std::optional resolve(TermBank& bank, const Clause& c1, size_t lit_idx1, const Clause& c2, size_t lit_idx2); /// Generate all possible resolvents between two clauses. -std::vector allResolvents(const TermBank& bank, const Clause& c1, const Clause& c2); +std::vector allResolvents(TermBank& bank, const Clause& c1, const Clause& c2); /// Attempt factoring on a single clause (merge two unifiable literals). -std::vector factor(const TermBank& bank, const Clause& c); +std::vector factor(TermBank& bank, const Clause& c); + +/// Rename all variables in a clause to fresh ones, avoiding conflicts +/// with variables already in the bank. +Clause renameVariables(const Clause& c, TermBank& bank, SymbolTable& symbols, + uint32_t& next_var_id); + } // namespace atp -- cgit v1.2.3