diff options
Diffstat (limited to 'src/infer')
| -rw-r--r-- | src/infer/resolution.cc | 12 | ||||
| -rw-r--r-- | src/infer/substitution.cc | 1 | ||||
| -rw-r--r-- | src/infer/unification.cc | 90 |
3 files changed, 51 insertions, 52 deletions
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<TermId, bool>& seen) { +void collectVariables(TermId term, const TermBank& bank, std::unordered_map<TermId, bool>& 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<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) { // 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<Clause> allResolvents(TermBank& bank, const Clause& c1, const Clause return results; } -std::vector<Clause> factor(TermBank& bank, const Clause& c, - const UnificationConfig& uconfig) { +std::vector<Clause> factor(TermBank& bank, const Clause& c, const UnificationConfig& uconfig) { std::vector<Clause> 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 <https://www.gnu.org/licenses/>. */ - #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<TermId> 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<TermId> old_args(t.args); // copy! - std::vector<TermId> 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<TermId> 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 |