feat: implement saturation-based resolution loop in Prover class

1 files changed, 8 insertions, 3 deletions

diff --git a/include/atp/infer/resolution.h b/include/atp/infer/resolution.h
index c31ff0e..df9cab3 100644
--- a/include/atp/infer/resolution.h
+++ b/include/atp/infer/resolution.h
@@ -28,18 +28,23 @@
 #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 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);
+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);
+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.