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 --- include/atp/infer/resolution.h | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) (limited to 'include/atp/infer/resolution.h') diff --git a/include/atp/infer/resolution.h b/include/atp/infer/resolution.h index df9cab3..6e2954d 100644 --- a/include/atp/infer/resolution.h +++ b/include/atp/infer/resolution.h @@ -16,7 +16,6 @@ * along with this program. If not, see . */ - #pragma once /// @file resolution.h @@ -24,32 +23,28 @@ #include "atp/core/clause.h" #include "atp/core/term_bank.h" +#include "atp/infer/unification.h" #include #include -#include "atp/infer/unification.h" - 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(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 = {}); /// Generate all possible resolvents between two clauses. std::vector allResolvents(TermBank& bank, const Clause& c1, const Clause& c2, const UnificationConfig& uconfig = {}); /// Attempt factoring on a single clause (merge two unifiable literals). -std::vector factor(TermBank& bank, const Clause& c, - const UnificationConfig& uconfig = {}); +std::vector factor(TermBank& bank, const Clause& c, const UnificationConfig& uconfig = {}); /// 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