aboutsummaryrefslogtreecommitdiff
path: root/include/atp/infer
diff options
context:
space:
mode:
authorRichard Qin <richard.qin.x@gmail.com>2026-04-04 05:21:26 +0800
committerRichard Qin <richard.qin.x@gmail.com>2026-04-04 05:21:26 +0800
commitbf4f464cec8b6515d9e5131d43847ef9b2fd21d1 (patch)
tree8cff611e6dab7473c3bb601e58658fa44f0fd86f /include/atp/infer
parent6fac8eb886f1e60a5a075c48a5f7648bb537f74e (diff)
downloadratp-bf4f464cec8b6515d9e5131d43847ef9b2fd21d1.tar.gz
ratp-bf4f464cec8b6515d9e5131d43847ef9b2fd21d1.tar.xz
style: reformat codebase with consistent indentation
Diffstat (limited to 'include/atp/infer')
-rw-r--r--include/atp/infer/resolution.h13
-rw-r--r--include/atp/infer/unification.h1
2 files changed, 4 insertions, 10 deletions
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 <https://www.gnu.org/licenses/>.
*/
-
#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 <optional>
#include <vector>
-#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<Clause> resolve(TermBank& bank, const Clause& c1, size_t lit_idx1,
- const Clause& c2, size_t lit_idx2,
- const UnificationConfig& uconfig = {});
+std::optional<Clause> 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<Clause> allResolvents(TermBank& bank, const Clause& c1, const Clause& c2,
const UnificationConfig& uconfig = {});
/// Attempt factoring on a single clause (merge two unifiable literals).
-std::vector<Clause> factor(TermBank& bank, const Clause& c,
- const UnificationConfig& uconfig = {});
+std::vector<Clause> 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
diff --git a/include/atp/infer/unification.h b/include/atp/infer/unification.h
index f2ea180..9a4b6cc 100644
--- a/include/atp/infer/unification.h
+++ b/include/atp/infer/unification.h
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*/
-
#pragma once
/// @file unification.h