From bf4f464cec8b6515d9e5131d43847ef9b2fd21d1 Mon Sep 17 00:00:00 2001 From: Richard Qin Date: Sat, 4 Apr 2026 05:21:26 +0800 Subject: style: reformat codebase with consistent indentation --- src/infer/resolution.cc | 12 +++---- src/infer/substitution.cc | 1 + src/infer/unification.cc | 90 +++++++++++++++++++++++------------------------ 3 files changed, 51 insertions(+), 52 deletions(-) (limited to 'src/infer') diff --git a/src/infer/resolution.cc b/src/infer/resolution.cc index 3c82460..f072b8e 100644 --- a/src/infer/resolution.cc +++ b/src/infer/resolution.cc @@ -17,6 +17,7 @@ */ #include "atp/infer/resolution.h" + #include "atp/core/clause.h" #include "atp/core/symbol_table.h" #include "atp/core/term.h" @@ -34,8 +35,7 @@ namespace atp { namespace { /// Recursively collect all variable TermIds appearing in a term. -void collectVariables(TermId term, const TermBank& bank, - std::unordered_map& seen) { +void collectVariables(TermId term, const TermBank& bank, std::unordered_map& seen) { if (bank.isVariable(term)) { seen[term] = true; return; @@ -84,9 +84,8 @@ Clause renameVariables(const Clause& c, TermBank& bank, SymbolTable& symbols, return renamed; } -std::optional resolve(TermBank& bank, const Clause& c1, size_t lit_idx1, - const Clause& c2, size_t lit_idx2, - const UnificationConfig& uconfig) { +std::optional resolve(TermBank& bank, const Clause& c1, size_t lit_idx1, const Clause& c2, + size_t lit_idx2, const UnificationConfig& uconfig) { // Must have opposite polarity if (c1.literals[lit_idx1].is_positive == c2.literals[lit_idx2].is_positive) { return std::nullopt; @@ -142,8 +141,7 @@ std::vector allResolvents(TermBank& bank, const Clause& c1, const Clause return results; } -std::vector factor(TermBank& bank, const Clause& c, - const UnificationConfig& uconfig) { +std::vector factor(TermBank& bank, const Clause& c, const UnificationConfig& uconfig) { std::vector results; for (size_t i = 0; i < c.literals.size(); ++i) { for (size_t j = i + 1; j < c.literals.size(); ++j) { diff --git a/src/infer/substitution.cc b/src/infer/substitution.cc index c570676..a7ce617 100644 --- a/src/infer/substitution.cc +++ b/src/infer/substitution.cc @@ -17,6 +17,7 @@ */ #include "atp/infer/substitution.h" + #include "atp/core/term.h" #include "atp/core/term_bank.h" #include "atp/core/types.h" diff --git a/src/infer/unification.cc b/src/infer/unification.cc index be8a025..66e1af6 100644 --- a/src/infer/unification.cc +++ b/src/infer/unification.cc @@ -16,72 +16,72 @@ * along with this program. If not, see . */ - #include "atp/infer/unification.h" + #include "atp/core/types.h" #include "atp/infer/substitution.h" namespace atp { - bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst, +bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst, const UnificationConfig& config) { - t1 = subst.resolve(t1, bank); - t2 = subst.resolve(t2, bank); + t1 = subst.resolve(t1, bank); + t2 = subst.resolve(t2, bank); - if (t1 == t2) { - return true; - } + if (t1 == t2) { + return true; + } - if (bank.isVariable(t1)) { - if (config.enable_occurs_check && subst.occursIn(t1, t2, bank)) { - return false; - } - subst.bind(t1, t2); - return true; + if (bank.isVariable(t1)) { + if (config.enable_occurs_check && subst.occursIn(t1, t2, bank)) { + return false; } + subst.bind(t1, t2); + return true; + } - if (bank.isVariable(t2)) { - if (config.enable_occurs_check && subst.occursIn(t2, t1, bank)) { - return false; - } - subst.bind(t2, t1); - return true; + if (bank.isVariable(t2)) { + if (config.enable_occurs_check && subst.occursIn(t2, t1, bank)) { + return false; } + subst.bind(t2, t1); + return true; + } + + const Term& term1 = bank.getTerm(t1); + const Term& term2 = bank.getTerm(t2); - const Term& term1 = bank.getTerm(t1); - const Term& term2 = bank.getTerm(t2); + if (term1.symbol_id != term2.symbol_id || term1.arity() != term2.arity()) { + return false; + } - if (term1.symbol_id != term2.symbol_id || term1.arity() != term2.arity()) { + for (size_t i = 0; i < term1.arity(); ++i) { + if (!unify(bank, term1.args[i], term2.args[i], subst, config)) { return false; } + } - for (size_t i = 0; i < term1.arity(); ++i) { - if (!unify(bank, term1.args[i], term2.args[i], subst, config)) { - return false; - } - } + return true; +} - return true; +TermId applySubstitution(const Substitution& subst, TermId term, TermBank& bank) { + term = subst.resolve(term, bank); + if (bank.isVariable(term)) { + return term; } - TermId applySubstitution(const Substitution& subst, TermId term, TermBank& bank) { - term = subst.resolve(term, bank); - if (bank.isVariable(term)) { - return term; - } - - // IMPORTANT: Copy args and symbol_id BEFORE recursing. - // Recursive calls may call bank.makeTerm() → realloc terms_ → invalidate refs. - const Term& t = bank.getTerm(term); - SymbolId sym = t.symbol_id; - std::vector old_args(t.args); // copy! + // IMPORTANT: Copy args and symbol_id BEFORE recursing. + // Recursive calls may call bank.makeTerm() → realloc terms_ → invalidate refs. + const Term& t = bank.getTerm(term); + SymbolId sym = t.symbol_id; + std::vector old_args(t.args); // copy! - std::vector new_args; - new_args.reserve(old_args.size()); - for (TermId arg : old_args) { - new_args.push_back(applySubstitution(subst, arg, bank)); - } - return bank.makeTerm(sym, new_args); + std::vector new_args; + new_args.reserve(old_args.size()); + for (TermId arg : old_args) { + new_args.push_back(applySubstitution(subst, arg, bank)); } + return bank.makeTerm(sym, new_args); +} } // namespace atp \ No newline at end of file -- cgit v1.2.3