Skip to content

Commit

Permalink
Merge pull request #61 from kasimebrahim/glob-unify
Browse files Browse the repository at this point in the history
Glob unify
  • Loading branch information
ngeiswei committed Feb 12, 2020
2 parents 9b5c57e + 4ebc23b commit 9fb6fee
Show file tree
Hide file tree
Showing 4 changed files with 690 additions and 37 deletions.
110 changes: 73 additions & 37 deletions opencog/unify/Unify.cc
Original file line number Diff line number Diff line change
Expand Up @@ -624,13 +624,7 @@ Unify::SolutionSet Unify::unify(const Handle& lh, const Handle& rh,
if (lt != rt)
return SolutionSet();

// At this point they are both links of the same type, check that
// they have the same arity
Arity lh_arity(lh->get_arity());
Arity rh_arity(rh->get_arity());
if (lh_arity != rh_arity)
return SolutionSet();

// At this point they are both links of the same type.
if (rh->is_unordered_link())
return unordered_unify(lh->getOutgoingSet(), rh->getOutgoingSet(), lc, rc);
else
Expand All @@ -641,47 +635,82 @@ Unify::SolutionSet Unify::unordered_unify(const HandleSeq& lhs,
const HandleSeq& rhs,
Context lc, Context rc) const
{
Arity lhs_arity(lhs.size());
Arity rhs_arity(rhs.size());
OC_ASSERT(lhs_arity == rhs_arity);

// Base case
if (lhs_arity == 0)
return SolutionSet(true);

// Recursive case
SolutionSet sol;
for (Arity i = 0; i < lhs_arity; ++i) {
auto head_sol = unify(lhs[i], rhs[0], lc, rc);
if (head_sol.is_satisfiable()) {
HandleSeq lhs_tail(cp_erase(lhs, i));
HandleSeq rhs_tail(cp_erase(rhs, 0));
auto tail_sol = unordered_unify(lhs_tail, rhs_tail, lc, rc);
// Union merge satisfiable permutations
sol.insert(join(head_sol, tail_sol));
}
}
SolutionSet sol(false);

HandleSeq perm(rhs);
do {
sol.insert(ordered_unify(lhs, perm, lc, rc));
} while (std::next_permutation(perm.begin(), perm.end()));

return sol;
}

Unify::SolutionSet Unify::ordered_unify(const HandleSeq& lhs,
const HandleSeq& rhs,
Context lc, Context rc) const
{
Arity lhs_arity(lhs.size());
Arity rhs_arity(rhs.size());
OC_ASSERT(lhs_arity == rhs_arity);
SolutionSet sol(false);

SolutionSet sol(true);
for (Arity i = 0; i < lhs_arity; ++i) {
auto rs = unify(lhs[i], rhs[i], lc, rc);
sol = join(sol, rs);
if (not sol.is_satisfiable()) // Stop if unification has failed
break;
if (lhs.empty() and rhs.empty()) return SolutionSet(true);

#define is_lh_glob lhs[0]->get_type() == GLOB_NODE
#define is_rh_glob rhs[0]->get_type() == GLOB_NODE

if (!lhs.empty() and !rhs.empty() and !(is_lh_glob) and !(is_rh_glob)){
const auto head_sol = unify(lhs[0], rhs[0], lc, rc);
const auto tail_sol = ordered_unify(tail(lhs), tail(rhs), lc, rc);
return join(head_sol, tail_sol);
}

// If lhs[0] we need to try to unify for every possible number
// of arguments the glob can contain.
if (!lhs.empty() and is_lh_glob)
ordered_unify_glob(lhs, rhs, sol, lc, rc);

// The flip flag is to prevent redundant partitions.
// i:e for globs X and U with the same type restriction
// {{{X, U}, U}} and {{{X, U}, X}} are equivalent.
if (!rhs.empty() and is_rh_glob)
ordered_unify_glob(rhs, lhs, sol, rc, lc, true);

#undef is_lh_glob
#undef is_rh_glob

return sol;
}

void Unify::ordered_unify_glob(const HandleSeq &lhs,
const HandleSeq &rhs,
Unify::SolutionSet &sol,
Context lc, Context rc, bool flip) const
{
const auto inter = _variables.get_interval(lhs[0]);
for (size_t i = inter.first;
(i <= inter.second and i <= rhs.size()); i++) {
const Handle r_h =
i == 1 ?
*rhs.begin() :
createLink(HandleSeq(rhs.begin(), rhs.begin() + i), LIST_LINK);
auto head_sol = flip ?
unify(r_h, lhs[0], rc, lc) :
unify(lhs[0], r_h, lc, rc);
auto tail_sol = flip ?
ordered_unify(tail(rhs, i), tail(lhs), rc, lc) :
ordered_unify(tail(lhs), tail(rhs, i), lc, rc);
sol.insert(join(tail_sol, head_sol));
}
}

HandleSeq Unify::tail(const HandleSeq &seq) const
{
return seq.empty() ? seq : HandleSeq(std::next(seq.begin()), seq.end());
}

HandleSeq Unify::tail(const HandleSeq &seq, const size_t offset) const
{
return seq.size() < offset ? seq : HandleSeq(seq.begin() + offset, seq.end());
}

Unify::SolutionSet Unify::pairwise_unify(const std::set<CHandlePair>& pchs) const
{
SolutionSet sol(true);
Expand Down Expand Up @@ -1073,7 +1102,8 @@ bool Unify::inherit(const Handle& lh, const Handle& rh,
// If both are free variables and declared then look at their types
// (only simple types are considered for now).
if (is_free_declared_variable(lc, lh) and is_free_declared_variable(rc, rh))
return inherit(get_union_type(lh), get_union_type(rh));
return inherit(get_union_type(lh), get_union_type(rh)) and
inherit(_variables.get_interval(lh), _variables.get_interval(rh));

// If only rh is a free and declared variable then check whether lh
// type inherits from it (using Variables::is_type).
Expand Down Expand Up @@ -1104,6 +1134,12 @@ bool Unify::inherit(const TypeSet& lhs, const TypeSet& rhs) const
return true;
}

bool Unify::inherit(const std::pair<double, double> &lgm,
const std::pair<double, double> &rgm) const
{
return rgm.first <= lgm.first and rgm.second >= lgm.second;
}

bool Unify::is_declared_variable(const Handle& h) const
{
return _variables.is_in_varset(h);
Expand Down
34 changes: 34 additions & 0 deletions opencog/unify/Unify.h
Original file line number Diff line number Diff line change
Expand Up @@ -770,6 +770,12 @@ class Unify
*/
bool inherit(const TypeSet& lhs, const TypeSet& rhs) const;

/**
* Return true if lgm is in rgm.
*/
bool inherit(const std::pair<double, double> &lgm,
const std::pair<double, double> &rgm) const;

/**
* Return true iff h (or ch) is a variable that is declared in
* _variables.
Expand Down Expand Up @@ -808,6 +814,34 @@ class Unify
return res;
return fixpoint(fun, res);
}

HandleSeq tail(const HandleSeq &seq) const;

HandleSeq tail(const HandleSeq &seq, const size_t offset) const;

/**
* Unify lhs and rhs where at least lhs contains a glob.
*
* For every possible allowed interval of the glob in lhs
* three operations will be undergone:
*
* 1/ pick that many elements from rhs and unify with glob as head_sol.
* Example: lhs = X[2, 3]Y[0, inf], rhs = ABC
* 2 is the first allowed interval for X
* head_sol = unify(X, AB) = {{X, List(A, B)}, List(A, B)}
*
* 2/ remove glob from lhs and unified atoms from rhs. Then recurse over
* the the remaining as tail_sol.
* Example: ordered_unify(Y[0, inf], C)
*
* 3/ join the head_sol and tail_sol into a complite solution and insert
* it tosolutions.
*/
void ordered_unify_glob(const HandleSeq &lhs, const HandleSeq &rhs,
SolutionSet &sol,
Context lhs_context=Context(),
Context rhs_context=Context(),
bool flip=false) const;
};

bool unifiable(const Handle& lhs, const Handle& rhs,
Expand Down
1 change: 1 addition & 0 deletions tests/unify/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -8,3 +8,4 @@ IF (HAVE_GUILE)
ENDIF (HAVE_GUILE)

ADD_CXXTEST(UnifyUTest)
ADD_CXXTEST(UnifyGlobUTest)
Loading

0 comments on commit 9fb6fee

Please sign in to comment.