784d7c3 · opencog-ure · pear-git-v3

Changed files (11) +15 -5904

CMakeLists.txt +12 -4

…	…	@@ -92,6 +92,16 @@ ELSE (ATOMSPACE_FOUND)
92	92	MESSAGE(FATAL_ERROR "AtomSpace missing: it is needed!")
93	93	ENDIF (ATOMSPACE_FOUND)
94	94
	95	# Unify
	96	FIND_PACKAGE(Unify CONFIG)
	97	IF (UNIFY_FOUND)
	98	MESSAGE(STATUS "CogUtil version ${UNIFY_VERSION} found.")
	99	ADD_DEFINITIONS(-DHAVE_UNIFY)
	100	SET(HAVE_UNIFY 1)
	101	ELSE (UNIFY_FOUND)
	102	MESSAGE(FATAL_ERROR "Unify missing: it is needed!")
	103	ENDIF (UNIFY_FOUND)
	104
95	105	# add the 'cmake' directory from cogutil to search path
96	106	list(APPEND CMAKE_MODULE_PATH ${COGUTIL_DATA_DIR}/cmake)
97	107	include(OpenCogGccOptions)
…	…	@@ -185,10 +195,9 @@ INCLUDE("${ATOMSPACE_DATA_DIR}/cmake/OpenCogCython.cmake")
185	195	# ==========================================================
186	196	# Decide what to build, based on the packages found.
187	197
188		IF(HAVE_ATOMSPACE AND HAVE_COGUTIL)
	198	IF(HAVE_UNIFY AND HAVE_ATOMSPACE AND HAVE_COGUTIL)
189	199	SET(HAVE_URE 1)
190		SET(HAVE_UNIFY 1)
191		ENDIF(HAVE_ATOMSPACE AND HAVE_COGUTIL)
	200	ENDIF(HAVE_UNIFY AND HAVE_ATOMSPACE AND HAVE_COGUTIL)
192	201
193	202	ADD_SUBDIRECTORY(opencog)
194	203	ADD_SUBDIRECTORY(lib)
…	…	@@ -308,7 +317,6 @@ INCLUDE(CPack)
308	317	# Show a summary of what we found, what we will do.
309	318
310	319	SUMMARY_ADD("URE" "Unified Rule Engine" HAVE_URE)
311		SUMMARY_ADD("Unify" "Syntactic unifer" HAVE_UNIFY)
312	320	SUMMARY_ADD("Python bindings" "Python (cython) bindings" HAVE_CYTHON)
313	321	SUMMARY_ADD("Python tests" "Python bindings nose tests" HAVE_NOSETESTS)
314	322	SUMMARY_ADD("Scheme bindings" "Scheme bindings and shell" HAVE_GUILE)

lib/UREConfig.cmake.in +1 -6

…	…	@@ -3,12 +3,7 @@
3	3	include("@CMAKE_INSTALL_PREFIX@/lib/cmake/URE/URETargets.cmake")
4	4
5	5	set(URE_LIBRARY ure)
6		set(UNIFY_LIBRARY unify)
7
8		set(URE_LIBRARIES
9		ure
10		unify
11		)
	6	set(URE_LIBRARIES ure)
12	7
13	8	set(URE_DATA_DIR "@CMAKE_INSTALL_PREFIX@/share/opencog")
14	9	set(URE_INCLUDE_DIR "@CMAKE_INSTALL_PREFIX@/include/")

opencog/CMakeLists.txt +2 -14

…	…	@@ -1,21 +1,9 @@
1	1	DECLARE_GUILE_CONFIG_TARGET(SCM_CONFIG "opencog ure-config" "URE_TEST")
2	2
3		# The build order used here is loosely in terms of
4		# dependencies: the later parts depend on, or may
5		# someday depend on the earlier parts.
6		#
7		IF (HAVE_UNIFY)
8		ADD_SUBDIRECTORY (unify)
9		ENDIF (HAVE_UNIFY)
10		IF (HAVE_URE)
11		ADD_SUBDIRECTORY (ure)
12		ENDIF (HAVE_URE)
	3	ADD_SUBDIRECTORY (ure)
	4	ADD_SUBDIRECTORY (scm)
13	5
14	6	# Extension language support
15		IF (HAVE_GUILE)
16		ADD_SUBDIRECTORY (scm)
17		ENDIF (HAVE_GUILE)
18
19	7	IF (HAVE_CYTHON)
20	8	ADD_SUBDIRECTORY (cython)
21	9	ENDIF (HAVE_CYTHON)

opencog/unify/CMakeLists.txt +0 -17

…	…	@@ -1,17 +0,0 @@
1		ADD_LIBRARY (unify
2		Unify.cc
3		)
4
5		TARGET_LINK_LIBRARIES(unify
6		${ATOMSPACE_LIBRARIES}
7		${COGUTIL_LIBRARY}
8		)
9
10		INSTALL (TARGETS unify
11		EXPORT URETargets
12		DESTINATION "lib${LIB_DIR_SUFFIX}/opencog")
13
14		INSTALL (FILES
15		Unify.h
16		DESTINATION "include/opencog/unify"
17		)

opencog/unify/README.md +0 -103

…	…	@@ -1,103 +0,0 @@
1		Unifier
2		=======
3
4		The unifier is a component to perform
5		(unification)[https://en.wikipedia.org/wiki/Unification_(computer_science)]
6		between atoms. It is an essential component of the Unified Rule
7		Engine, URE for short, as it allows to check if a given source
8		(resp. target) matches a given premise (resp. conclusion). The reason
9		pattern matching is not enough is because in the URE both sources
10		(resp. targets) and premises (resp. conclusions) may contain
11		variables, while in the pattern matcher only the patterns contain
12		variables, not the groundings (or if they do these are interpreted as
13		constants).
14
15		At its core what the unifier does is finding assignements to each
16		variables in the terms that would render them equal by substitution.
17
18		For instance given the following 2 terms
19
20		```scheme
21		(Inheritance
22		(Concept "A")
23		(Variable "$Y"))
24		```
25
26		and
27
28		```scheme
29		(Inheritance
30		(Variable "$X")
31		(Concept "B"))
32		```
33
34		the unifier would return the following assignment as a solution:
35
36		```
37		{ (Variable "$X") -> (Concept "A"),
38		(Variable "$Y") -> (Concept "B") }
39		```
40
41		meaning that if `$X` is subtituted by `A` and `$Y` is substituted by
42		`B`, the 2 terms are equal.
43
44		Sometimes assignments may map variables to other variables, or to
45		subhypergraphs containing variables, etc, but the ideas remain the
46		same.
47
48		Status
49		------
50
51		The unifier is virtually complete and can handle most situations,
52		including cyclic dependencies and typed variables. It is reasonably
53		efficient, though, due to the inherent cost of unification, could
54		welcome some optimizations. Beyond that its main limit is the lack of
55		deep type support.
56
57		Usage
58		-----
59
60		For the moment only a C++ API is available. The entry point is the
61		functor class `Unify` that is contructed with 2 terms as follows
62
63		```c++
64		Unify unify(t1, t2, t1_vardecl, t2_vardecl)
65		```
66
67		where `t1` and `t2` are Handles, and `t1_vardecl` and `t2_vardecl` are
68		optional variable declarations to specify their types.
69
70		Then it can be called via its `operator()`
71
72		```c++
73		Unify::SolutionSet ss = unify();
74		```
75
76		where `Unify::SolutionSet` is a class representing a mapping between
77		variables appearing in both terms and their most abstract values
78		(values in a broad sense as such may be variables, or subhypegraphs
79		containing themselves variables).
80
81		The `Unify` class contains also convenient methods to carry out
82		substitutions on the terms and given their unification solutions,
83		which is heavily used by the URE.
84
85		Examples can be found in `tests/unify/UnifyUTest.cxxtest` containing
86		dozens of tests, ranging from very simple to quite complex.
87
88		TODO
89		----
90
91		* Support deep types
92		* Support GlobNode
93		* Add Scheme bindings
94		* Implement memoization at the subcall level. Indeed the unifier is
95		stateless, and is writen in a functional way relying on recursivity,
96		thus is likely an excellent candidate for subcall memoization.
97		Queries sharing subhypergraphs, which is common in the URE context,
98		would likely benefit from such optimization.
99
100		Author
101		------
102
103		Nil Geisweiller

opencog/unify/Unify.cc +0 -1381

…	…	@@ -1,1381 +0,0 @@
1		/**
2		* Unify.cc
3		*
4		* Utilities for unifying atoms.
5		*
6		* Copyright (C) 2016 OpenCog Foundation
7		* All Rights Reserved
8		* Author: Nil Geisweiller
9		*
10		* This program is free software; you can redistribute it and/or modify
11		* it under the terms of the GNU Affero General Public License v3 as
12		* published by the Free Software Foundation and including the exceptions
13		* at http://opencog.org/wiki/Licenses
14		*
15		* This program is distributed in the hope that it will be useful,
16		* but WITHOUT ANY WARRANTY; without even the implied warranty of
17		* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
18		* GNU General Public License for more details.
19		*
20		* You should have received a copy of the GNU Affero General Public License
21		* along with this program; if not, write to:
22		* Free Software Foundation, Inc.,
23		* 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
24		*/
25
26		#include "Unify.h"
27
28		#include <boost/algorithm/cxx11/any_of.hpp>
29
30		#include <opencog/util/algorithm.h>
31		#include <opencog/util/Logger.h>
32		#include <opencog/atoms/base/Atom.h>
33		#include <opencog/atoms/base/Node.h>
34		#include <opencog/atoms/core/Context.h>
35		#include <opencog/atoms/core/FindUtils.h>
36		#include <opencog/atoms/core/TypeUtils.h>
37		#include <opencog/atoms/core/RewriteLink.h>
38		#include <opencog/atoms/pattern/PatternUtils.h>
39		#include <opencog/atomspace/AtomSpace.h>
40
41		namespace opencog {
42
43		const Unify::Partitions Unify::empty_partitions({});
44
45		const Unify::Partitions Unify::empty_partition_singleton({{}});
46
47		Unify::CHandle::CHandle(const Handle& h, const Context& c)
48		: handle(h), context(c) {}
49
50		bool Unify::CHandle::is_variable() const
51		{
52		return handle->get_type() == VARIABLE_NODE;
53		}
54
55		bool Unify::CHandle::is_free_variable() const
56		{
57		return context.is_free_variable(handle);
58		}
59
60		HandleSet Unify::CHandle::get_free_variables() const
61		{
62		HandleSet free_vars =
63		opencog::get_free_variables(handle, context.quotation);
64		return set_difference(free_vars, context.shadow);
65		}
66
67		Context::VariablesStack::const_iterator
68		Unify::CHandle::find_variables(const Handle& h) const
69		{
70		return std::find_if(context.scope_variables.cbegin(),
71		context.scope_variables.cend(),
72		[&](const Variables& variables) {
73		return variables.varset_contains(h);
74		});
75		}
76
77		bool Unify::CHandle::is_consumable() const
78		{
79		return context.quotation.consumable(handle->get_type());
80		}
81
82		bool Unify::CHandle::is_quoted() const
83		{
84		return context.quotation.is_quoted();
85		}
86
87		bool Unify::CHandle::is_unquoted() const
88		{
89		return context.quotation.is_unquoted();
90		}
91
92		void Unify::CHandle::update()
93		{
94		bool isc = is_consumable();
95		context.update(handle);
96		if (isc)
97		handle = handle->getOutgoingAtom(0);
98		}
99
100		bool Unify::CHandle::is_node_satisfiable(const CHandle& other) const
101		{
102		// If both are variable check whether they could be alpha
103		// equivalent, otherwise merely check for equality
104		if (is_variable() and other.is_variable()) {
105		// Make sure scope variable declarations are stored
106		OC_ASSERT(context.store_scope_variables,
107		"You must store the scope variable declarations "
108		"in order to use this method");
109
110		// Search variable declarations associated to the variables
111		Context::VariablesStack::const_iterator it = find_variables(handle),
112		other_it = other.find_variables(other.handle);
113		OC_ASSERT(it != context.scope_variables.cend(),
114		"Contradicts the assumption that this->handle is not free");
115		OC_ASSERT(other_it != other.context.scope_variables.cend(),
116		"Contradicts the assumption that other.handle is not free");
117
118		// Check that both variable declarations occured at the same level
119		if (std::distance(context.scope_variables.cbegin(), it)
120		!= std::distance(other.context.scope_variables.cbegin(), other_it))
121		return false;
122
123		// Check that the other variable is alpha convertible
124		return it->is_alpha_convertible(handle, other.handle, *other_it, true);
125		} else {
126		return content_eq(handle, other.handle);
127		}
128		}
129
130		bool Unify::CHandle::operator==(const CHandle& ch) const
131		{
132		return content_eq(handle, ch.handle) and (context == ch.context);
133		}
134
135		bool Unify::CHandle::operator<(const CHandle& ch) const
136		{
137		return (handle < ch.handle) or
138		(handle == ch.handle and context < ch.context);
139		}
140
141		Unify::CHandle::operator bool() const
142		{
143		return (bool)handle;
144		}
145
146		Unify::SolutionSet::SolutionSet(bool s)
147		: Partitions(s ? empty_partition_singleton : empty_partitions) {}
148
149		Unify::SolutionSet::SolutionSet(const Unify::Partitions& p)
150		: Partitions(p) {}
151
152		bool Unify::SolutionSet::is_satisfiable() const
153		{
154		return not empty();
155		}
156
157		void Unify::SolutionSet::insert(const SolutionSet& sol)
158		{
159		Partitions::insert(sol.begin(), sol.end());
160		}
161
162		void Unify::SolutionSet::remove_cycles()
163		{
164		// TODO: replace by std::set::erase_if once C++20 is enabled
165		for (auto it = begin(); it != end();) {
166		if (has_cycle(*it)) {
167		it = erase(it);
168		} else {
169		++it;
170		}
171		}
172		}
173
174		Unify::Unify(const Handle& lhs, const Handle& rhs,
175		const Handle& lhs_vardecl, const Handle& rhs_vardecl)
176		{
177		// Set terms to unify
178		_lhs = lhs;
179		_rhs = rhs;
180
181		// Set _variables
182		set_variables(lhs, rhs, lhs_vardecl, rhs_vardecl);
183		}
184
185		Unify::Unify(const Handle& lhs, const Handle& rhs,
186		const Variables& lhs_vars, const Variables& rhs_vars)
187		{
188		// Set terms to unify
189		_lhs = lhs;
190		_rhs = rhs;
191
192		// Set _variables
193		_variables = merge_variables(lhs_vars, rhs_vars);
194		}
195
196		Unify::TypedSubstitutions Unify::typed_substitutions(const SolutionSet& sol,
197		const Handle& pre) const
198		{
199		OC_ASSERT(sol.is_satisfiable());
200
201		TypedSubstitutions result;
202		for (const Partition& partition : sol)
203		result.insert(typed_substitution(partition, pre));
204		return result;
205		}
206
207		Unify::TypedSubstitution Unify::typed_substitution(const Partition& partition,
208		const Handle& pre) const
209		{
210		// Associate the least abstract element to each variable of each
211		// block.
212		HandleCHandleMap var2cval;
213		for (const TypedBlock& block : partition) {
214		CHandle least_abstract = find_least_abstract(block, pre);
215
216		// Build variable mapping
217		for (const CHandle& ch : block.first)
218		if (ch.is_free_variable())
219		var2cval.insert({ch.handle, least_abstract});
220		}
221
222		// Calculate its closure
223		var2cval = substitution_closure(var2cval);
224
225		// Remove ill quotations
226		Variables tmpv(_variables.get_vardecl());
227		for (auto& vcv : var2cval) {
228		bool needless_quotation = true;
229		Handle consumed =
230		RewriteLink::consume_quotations(tmpv, vcv.second.handle,
231		vcv.second.context.quotation,
232		needless_quotation, false);
233		vcv.second = CHandle(consumed, vcv.second.context);
234		}
235
236		// Calculate its variable declaration
237		Handle vardecl = substitution_vardecl(var2cval);
238
239		// Return the typed substitution
240		return {var2cval, vardecl};
241		}
242
243		static Variables gen_univars(const Handle& h, const Handle& vardecl)
244		{
245		if (vardecl)
246		return Variables(vardecl);
247		HandleSet vars = get_free_variables(h);
248		HandleSeq varli(vars.begin(), vars.end());
249		return Variables(varli);
250		}
251
252		void Unify::set_variables(const Handle& lhs, const Handle& rhs,
253		const Handle& lhs_vardecl, const Handle& rhs_vardecl)
254		{
255		// Merge the 2 type declarations
256		Variables lv = gen_univars(lhs, lhs_vardecl);
257		Variables rv = gen_univars(rhs, rhs_vardecl);
258		_variables = merge_variables(lv, rv);
259		}
260
261		Unify::CHandle Unify::find_least_abstract(const TypedBlock& block,
262		const Handle& pre) const
263		{
264		// Get the least abstract element of the block
265		auto blk_it = block.first.begin();
266		CHandle least_abstract = *blk_it;
267		++blk_it;
268		for (; blk_it != block.first.end(); ++blk_it)
269		if (inherit(*blk_it, least_abstract))
270		least_abstract = *blk_it;
271
272		// In case of ties pick up the one in pre (pre stands for
273		// precedence)
274		for (const CHandle& ch : block.first)
275		if (inherit(ch, least_abstract)
276		and
277		(not ch.is_free_variable()
278		or is_unquoted_unscoped_in_tree(pre, ch.handle)))
279		least_abstract = ch;
280
281		return least_abstract;
282		}
283
284		Unify::HandleCHandleMap Unify::substitution_closure(const HandleCHandleMap& var2cval) const
285		{
286		// Strip var2cval from its contexts
287		HandleMap var2val = strip_context(var2cval);
288
289		// Substitute every value that have variables by other values
290		// associated to these variables.
291		HandleCHandleMap result(var2cval);
292		for (auto& el : result) {
293		HandleSet free_vars = el.second.get_free_variables();
294		HandleSeq free_list(free_vars.begin(), free_vars.end());
295		Variables variables(free_list);
296		HandleSeq values = variables.make_sequence(var2val);
297		el.second.handle = variables.substitute_nocheck(el.second.handle, values);
298		}
299
300		// If we have reached a fixed point then return substitution,
301		// otherwise re-iterate
302		return hchm_content_eq(result, var2cval) ?
303		result : substitution_closure(result);
304		}
305
306		Handle Unify::substitution_vardecl(const HandleCHandleMap& var2val) const
307		{
308		// Build the type declaration for this substitution. For now, the
309		// type is merely lhs_vardecl and rhs_vardecl merged together,
310		// then all variables assigned for substitution other than
311		// themselves are removed. To do well it should be taking into
312		// account the possibly more restrictive types found during
313		// unification (i.e. the block types).
314
315		Variables ts_variables = _variables;
316
317		for (const auto& el : var2val)
318		// Make sure it is not a self substitution
319		if (el.first != el.second.handle)
320		ts_variables.erase(el.first);
321
322		return ts_variables.get_vardecl();
323		}
324
325		bool Unify::is_pm_connector(const Handle& h)
326		{
327		return is_pm_connector(h->get_type());
328		}
329
330		bool Unify::is_pm_connector(Type t)
331		{
332		return t == AND_LINK or t == OR_LINK or t == NOT_LINK;
333		}
334
335		HandleMultimap Unify::vargraph(const Partition& partition)
336		{
337		HandleMultimap vg;
338		for (const auto& blk : partition) {
339		HandleMultimap bvg = vargraph(blk.first);
340		for (const auto& vvs : bvg) {
341		vg[vvs.first].insert(vvs.second.begin(), vvs.second.end());
342		}
343		}
344		return vg;
345		}
346
347		HandleMultimap Unify::vargraph(const Block& blk)
348		{
349		// Standalone variables
350		HandleSet stdvars;
351		// Variables buried inside terms
352		HandleSet trmvars;
353
354		// Fill stdvars and trmvars
355		for (const CHandle& ch : blk) {
356		if (ch.is_free_variable()) {
357		stdvars.insert(ch.handle);
358		continue;
359		}
360		HandleSet fvs = ch.get_free_variables();
361		trmvars.insert(fvs.begin(), fvs.end());
362		}
363
364		// For each standaline variable associate all terms variables
365		HandleMultimap vg;
366		for (const Handle& stv : stdvars)
367		vg[stv] = trmvars;
368		return vg;
369		}
370
371		bool Unify::has_cycle(const Partition& partition)
372		{
373		return has_cycle(vargraph(partition));
374		}
375
376		bool Unify::has_cycle(const Block& blk)
377		{
378		return has_cycle(vargraph(blk));
379		}
380
381		bool Unify::has_cycle(const HandleMultimap& vg)
382		{
383		using boost::algorithm::any_of;
384		HandleMultimap cvg = closure(vg);
385		return any_of(cvg, [](const HandleMultimap::value_type& vvs) {
386		return contains(vvs.second, vvs.first); });
387		}
388
389		HandleMultimap Unify::closure(const HandleMultimap& vg)
390		{
391		return fixpoint(&Unify::closure_step, vg);
392		}
393
394		HandleMultimap Unify::closure_step(const HandleMultimap& vg)
395		{
396		HandleMultimap nvg(vg);
397		for (const auto& vvs : vg) {
398		for (const Handle& v : vvs.second) {
399		const HandleSet& third = nvg[v];
400		nvg[vvs.first].insert(third.begin(), third.end());
401		}
402		}
403		return nvg;
404		}
405
406		Handle Unify::substitute(BindLinkPtr bl, const TypedSubstitution& ts,
407		const AtomSpace* queried_as)
408		{
409		// TODO: make sure that ts.second contains the declaration of all
410		// variables
411		return substitute(bl, strip_context(ts.first), ts.second, queried_as);
412		}
413
414		static Handle make_vardecl(const Handle& h)
415		{
416		HandleSet vars = get_free_variables(h);
417		return Handle(createVariableSet(HandleSeq(vars.begin(), vars.end())));
418		}
419
420		Handle Unify::substitute(BindLinkPtr bl, const HandleMap& var2val,
421		Handle vardecl, const AtomSpace* queried_as)
422		{
423		// Perform substitution over the existing variable declaration, if
424		// no new alternative is provided.
425		if (not vardecl) {
426		// If the bind link has no variable declaration either then
427		// infer one
428		Handle old_vardecl = bl->get_vardecl() ? bl->get_vardecl()
429		: make_vardecl(bl->get_body());
430		// Substitute the variables in the old vardecl to obtain the
431		// new one.
432		vardecl = substitute_vardecl(old_vardecl, var2val);
433		}
434
435		const Variables& variables = bl->get_variables();
436
437		// Turn the map into a vector of new variable names/values
438		HandleSeq values = variables.make_sequence(var2val);
439
440		// Substituted BindLink outgoings
441		HandleSeq hs;
442
443		// Perform substitution over the pattern term, then remove
444		// constant clauses
445		Handle clauses = variables.substitute_nocheck(bl->get_body(), values);
446		Variables tmpv(vardecl);
447		bool needless_quotation = true;
448		clauses = RewriteLink::consume_quotations(tmpv, clauses,
449		Quotation(), needless_quotation, true);
450		if (queried_as)
451		clauses = remove_constant_clauses(vardecl, clauses, queried_as);
452		hs.push_back(clauses);
453
454		// Perform substitution over the rewrite terms
455		for (const Handle& himp: bl->get_implicand())
456		{
457		Handle rewrite = variables.substitute_nocheck(himp, values);
458		Variables tmpv(vardecl);
459		bool needless_quotation = true;
460		rewrite = RewriteLink::consume_quotations(tmpv, rewrite,
461		Quotation(), needless_quotation, false);
462		hs.push_back(rewrite);
463		}
464
465		// Filter vardecl
466		vardecl = filter_vardecl(vardecl, hs);
467
468		// Insert vardecl in hs if defined
469		if (vardecl)
470		hs.insert(hs.begin(), vardecl);
471
472		// Create the substituted BindLink
473		return createLink(std::move(hs), bl->get_type());
474		}
475
476		Handle Unify::substitute_vardecl(const Handle& vardecl,
477		const HandleMap& var2val)
478		{
479		if (not vardecl)
480		return Handle::UNDEFINED;
481
482		Type t = vardecl->get_type();
483
484		// Base cases
485
486		if (t == VARIABLE_NODE) {
487		auto it = var2val.find(vardecl);
488		// Only substitute if the variable is substituted by another variable
489		if (it != var2val.end() and it->second->get_type() == VARIABLE_NODE)
490		return it->second;
491		return Handle::UNDEFINED;
492		}
493
494		// Recursive cases
495
496		HandleSeq oset;
497
498		if (t == VARIABLE_LIST or t == VARIABLE_SET) {
499		for (const Handle& h : vardecl->getOutgoingSet()) {
500		Handle nh = substitute_vardecl(h, var2val);
501		if (nh)
502		oset.push_back(nh);
503		}
504		if (oset.empty())
505		return Handle::UNDEFINED;
506		}
507		else if (t == TYPED_VARIABLE_LINK) {
508		Handle new_var = substitute_vardecl(vardecl->getOutgoingAtom(0),
509		var2val);
510		if (new_var) {
511		oset.push_back(new_var);
512		oset.push_back(vardecl->getOutgoingAtom(1));
513		} else return Handle::UNDEFINED;
514		}
515		else {
516		OC_ASSERT(false, "Not implemented");
517		}
518		return createLink(std::move(oset), t);
519		}
520
521		// Return true iff the given handle is not in the given atomspace (if
522		// any).
523		static bool not_in_atomspace(const Handle& handle, const AtomSpace* atomspace)
524		{
525		return nullptr != atomspace
526		and nullptr == atomspace->get_atom(handle);
527		}
528
529		// Return true iff the given clause is constant and is not in the
530		// given atomspace. A set of variables is provided to make the
531		// distinction between variables and variable interpreted as constants
532		// (they are constants is not in vars). Checking the present of the
533		// clause in the atomspace matters because we don't want to trigger a
534		// rule that will produce a term conditioned on the presence of a
535		// clause that was actually not in the atomspace (that would have been
536		// turned into a constant due to partial instantiation of a rule).
537		static bool not_constant(const HandleSet& vars,
538		const Handle& clause,
539		const AtomSpace* as)
540		{
541		return not_in_atomspace(clause, as) or not is_constant(vars, clause);
542		}
543
544		// TODO: for now it is assumed clauses are connected by an AndLink
545		// only. To fix that one needs to generalize
546		// PatternLink::unbundle_clauses to make it usable in that code too.
547		//
548		// TODO: maybe replace Handle vardecl by Variables variables.
549		Handle Unify::remove_constant_clauses(const Handle& vardecl,
550		const Handle& clauses,
551		const AtomSpace* as)
552		{
553		VariableListPtr vl = createVariableList(vardecl);
554		HandleSet vars = vl->get_variables().varset;
555
556		// Remove constant clauses
557		Type t = clauses->get_type();
558		HandleSeq hs;
559		if (t == AND_LINK) {
560		for (const Handle& clause : clauses->getOutgoingSet()) {
561		if (not_constant(vars, clause, as)) {
562		hs.push_back(clause);
563		}
564		}
565		} else if (not_constant(vars, clauses, as)) {
566		return clauses;
567		}
568		return createLink(std::move(hs), AND_LINK);
569		}
570
571		Unify::SolutionSet Unify::operator()()
572		{
573		// If the declaration is ill typed, there is no solution
574		if (not _variables.is_well_typed())
575		return SolutionSet();
576
577		// It is well typed, perform the unification
578		SolutionSet sol = unify(_lhs, _rhs);
579
580		// Remove partitions with cycles
581		sol.remove_cycles();
582
583		return sol;
584		}
585
586		Unify::SolutionSet Unify::unify(const CHandle& lhs, const CHandle& rhs) const
587		{
588		return unify(lhs.handle, rhs.handle, lhs.context, rhs.context);
589		}
590
591		Unify::SolutionSet Unify::unify(const Handle& lh, const Handle& rh,
592		Context lc, Context rc) const
593		{
594		Type lt(lh->get_type());
595		Type rt(rh->get_type());
596
597		///////////////////
598		// Base cases //
599		///////////////////
600
601		// Make sure both handles are defined
602		if (not lh or not rh)
603		return SolutionSet();
604
605		CHandle lch(lh, lc);
606		CHandle rch(rh, rc);
607
608		bool lq = lc.quotation.consumable(lt);
609		bool rq = rc.quotation.consumable(rt);
610
611		// If one is a node
612		if (lh->is_node() or rh->is_node()) {
613		// If one is a free variable that is declared in _variables, and
614		// they are different, then unifies.
615		if (is_free_declared_variable(lch) or is_free_declared_variable(rch)) {
616		if (lch == rch) {
617		// Do not construct a solution like {X}->X to not
618		// overload the solution set.
619		//
620		// Since the context is taken into account they have
621		// the same context, thus if one of them is free, the
622		// other is free as well, therefore they are
623		// satisfiable.
624		return SolutionSet(true);
625		} else {
626		return mkvarsol(lch, rch);
627		}
628		} else if (!lq and !rq)
629		return SolutionSet(is_node_satisfiable(lch, rch));
630		}
631
632		////////////////////////
633		// Recursive cases //
634		////////////////////////
635
636		// Consume quotations
637		if (lq and rq) {
638		lc.quotation.update(lt);
639		rc.quotation.update(rt);
640		return unify(lh->getOutgoingAtom(0), rh->getOutgoingAtom(0), lc, rc);
641		}
642		if (lq) {
643		lc.quotation.update(lt);
644		return unify(lh->getOutgoingAtom(0), rh, lc, rc);
645		}
646		if (rq) {
647		rc.quotation.update(rt);
648		return unify(lh, rh->getOutgoingAtom(0), lc, rc);
649		}
650
651		// Update contexts
652		lc.update(lh);
653		rc.update(rh);
654
655		// At least one of them is a link, check if they have the same
656		// type (e.i. do they match so far)
657		if (lt != rt)
658		return SolutionSet();
659
660		// At this point they are both links of the same type.
661		if (rh->is_unordered_link())
662		return unordered_unify(lh->getOutgoingSet(), rh->getOutgoingSet(), lc, rc);
663		else
664		return ordered_unify(lh->getOutgoingSet(), rh->getOutgoingSet(), lc, rc);
665		}
666
667		Unify::SolutionSet Unify::unordered_unify(const HandleSeq& lhs,
668		const HandleSeq& rhs,
669		Context lc, Context rc) const
670		{
671		SolutionSet sol(false);
672
673		HandleSeq perm(rhs);
674		do {
675		sol.insert(ordered_unify(lhs, perm, lc, rc));
676		} while (std::next_permutation(perm.begin(), perm.end()));
677
678		return sol;
679		}
680
681		Unify::SolutionSet Unify::ordered_unify(const HandleSeq& lhs,
682		const HandleSeq& rhs,
683		Context lc, Context rc) const
684		{
685		SolutionSet sol(false);
686
687		if (lhs.empty() and rhs.empty()) return SolutionSet(true);
688
689		#define is_lh_glob lhs[0]->get_type() == GLOB_NODE and is_declared_variable(lhs[0])
690		#define is_rh_glob rhs[0]->get_type() == GLOB_NODE and is_declared_variable(rhs[0])
691
692		if (!lhs.empty() and !rhs.empty() and !(is_lh_glob) and !(is_rh_glob)){
693		const auto head_sol = unify(lhs[0], rhs[0], lc, rc);
694		const auto tail_sol = ordered_unify(tail(lhs), tail(rhs), lc, rc);
695		return join(head_sol, tail_sol);
696		}
697
698		// If lhs[0] we need to try to unify for every possible number
699		// of arguments the glob can contain.
700		if (!lhs.empty() and is_lh_glob)
701		ordered_unify_glob(lhs, rhs, sol, lc, rc);
702
703		// The flip flag is to prevent redundant partitions.
704		// i:e for globs X and U with the same type restriction
705		// {{{X, U}, U}} and {{{X, U}, X}} are equivalent.
706		if (!rhs.empty() and is_rh_glob)
707		ordered_unify_glob(rhs, lhs, sol, rc, lc, true);
708
709		#undef is_lh_glob
710		#undef is_rh_glob
711
712		return sol;
713		}
714
715		void Unify::ordered_unify_glob(const HandleSeq &lhs,
716		const HandleSeq &rhs,
717		Unify::SolutionSet &sol,
718		Context lc, Context rc, bool flip) const
719		{
720		const auto inter = _variables.get_interval(lhs[0]);
721		for (size_t i = inter.first;
722		(i <= inter.second and i <= rhs.size()); i++) {
723		// The condition is to avoid extra complexity when calculating
724		// type-intersection for glob. Should be fixed from the atomspace
725		// Variables::is_type.
726		Handle r_h;
727		if (i == 1) {
728		Type rtype = (*rhs.begin())->get_type();
729		if (GLOB_NODE == rtype)
730		r_h = *rhs.begin();
731		else if (QUOTE_LINK == rtype or UNQUOTE_LINK == rtype)
732		r_h = createLink((*rhs.begin())->getOutgoingSet(), LIST_LINK);
733		else r_h = createLink(HandleSeq(rhs.begin(), rhs.begin() + i), LIST_LINK);
734		}
735		else r_h = createLink(HandleSeq(rhs.begin(), rhs.begin() + i), LIST_LINK);
736
737		auto head_sol = flip ?
738		unify(r_h, lhs[0], rc, lc) :
739		unify(lhs[0], r_h, lc, rc);
740		auto tail_sol = flip ?
741		ordered_unify(tail(rhs, i), tail(lhs), rc, lc) :
742		ordered_unify(tail(lhs), tail(rhs, i), lc, rc);
743		sol.insert(join(tail_sol, head_sol));
744		}
745		}
746
747		HandleSeq Unify::tail(const HandleSeq &seq) const
748		{
749		return seq.empty() ? seq : HandleSeq(std::next(seq.begin()), seq.end());
750		}
751
752		HandleSeq Unify::tail(const HandleSeq &seq, const size_t offset) const
753		{
754		return seq.size() < offset ? seq : HandleSeq(seq.begin() + offset, seq.end());
755		}
756
757		Unify::SolutionSet Unify::pairwise_unify(const std::set<CHandlePair>& pchs) const
758		{
759		SolutionSet sol(true);
760		for (const CHandlePair& pch : pchs) {
761		auto rs = unify(pch.first, pch.second);
762		sol = join(sol, rs);
763		if (not sol.is_satisfiable()) // Stop if unification has failed
764		return sol;
765		}
766		return sol;
767		}
768
769		Unify::SolutionSet Unify::comb_unify(const std::set<CHandle>& lhs,
770		const std::set<CHandle>& rhs) const
771		{
772		SolutionSet sol(true);
773		for (const CHandle& lch : lhs) {
774		for (const CHandle& rch : rhs) {
775		auto rs = unify(lch, rch);
776		sol = join(sol, rs);
777		if (not sol.is_satisfiable()) // Stop if unification has failed
778		return sol;
779		}
780		}
781		return sol;
782		}
783
784		Unify::SolutionSet Unify::comb_unify(const std::set<CHandle>& chs) const
785		{
786		SolutionSet sol(true);
787		for (auto lit = chs.begin(); lit != chs.end(); ++lit) {
788		for (auto rit = std::next(lit); rit != chs.end(); ++rit) {
789		auto rs = unify(lit, rit);
790		sol = join(sol, rs);
791		if (not sol.is_satisfiable()) // Stop if unification has failed
792		return sol;
793		}
794		}
795		return sol;
796		}
797
798		HandleSeq Unify::cp_erase(const HandleSeq& hs, Arity i) const
799		{
800		HandleSeq hs_cp(hs);
801		hs_cp.erase(hs_cp.begin() + i);
802		return hs_cp;
803		}
804
805		Unify::SolutionSet Unify::mkvarsol(CHandle lch, CHandle rch) const
806		{
807		// Attempt to consume quotation to avoid putting quoted elements
808		// in the block.
809		if (lch.is_free_variable() and rch.is_consumable() and rch.is_quoted())
810		rch.update();
811		if (rch.is_free_variable() and lch.is_consumable() and lch.is_quoted())
812		lch.update();
813
814		CHandle inter = type_intersection(lch, rch);
815		if (not inter)
816		return SolutionSet();
817		else {
818
819		// Special case: if the variable is a glob, and it matched
820		// just one item, then unwrap that item. This seems ...
821		// kind of perverse to me, but the unit tests expect this
822		// behavior. Maybe change things in the future?
823		if (GLOB_NODE == lch.handle->get_type() and
824		LIST_LINK == rch.handle->get_type() and
825		1 == rch.handle->get_arity())
826		{
827		rch.handle = rch.handle->getOutgoingAtom(0);
828		if (rch.handle == lch.handle) return SolutionSet(true);
829		inter.handle = rch.handle;
830		}
831		if (GLOB_NODE == rch.handle->get_type() and
832		LIST_LINK == lch.handle->get_type() and
833		1 == lch.handle->get_arity())
834		{
835		lch.handle = lch.handle->getOutgoingAtom(0);
836		if (rch.handle == lch.handle) return SolutionSet(true);
837		inter.handle = lch.handle;
838		}
839		Block pblock{lch, rch};
840		Partitions par{{{pblock, inter}}};
841		return SolutionSet(par);
842		}
843		}
844
845		Unify::SolutionSet Unify::join(const SolutionSet& lhs,
846		const SolutionSet& rhs) const
847		{
848		// No need to join if one of them is non satisfiable
849		if (not lhs.is_satisfiable() or not rhs.is_satisfiable())
850		return SolutionSet();
851
852		// By now both are satisfiable, thus non empty, join them
853		SolutionSet result;
854		for (const Partition& rp : rhs)
855		result.insert(join(lhs, rp));
856		return result;
857		}
858
859		Unify::SolutionSet Unify::join(const SolutionSet& lhs, const Partition& rhs) const
860		{
861		// Base cases
862		if (rhs.empty())
863		return lhs;
864
865		// Recursive case (a loop actually)
866		SolutionSet result;
867		for (const auto& par : lhs)
868		result.insert(join(par, rhs));
869		return result;
870		}
871
872		Unify::SolutionSet Unify::join(const Partition& lhs, const Partition& rhs) const
873		{
874		// Don't bother joining if lhs is empty (saves a bit of computation)
875		if (lhs.empty())
876		return SolutionSet({rhs});
877
878		// Join
879		SolutionSet result({lhs});
880		for (const TypedBlock& rhs_block : rhs) {
881		// For now we assume result has only 0 or 1 partition
882		result = join(result, rhs_block);
883		if (not result.is_satisfiable())
884		return SolutionSet();
885		}
886
887		return result;
888		}
889
890		Unify::SolutionSet Unify::join(const SolutionSet& sol,
891		const TypedBlock& block) const
892		{
893		SolutionSet result;
894		for (const Partition& partition : sol)
895		result.insert(join(partition, block));
896		return result;
897		}
898
899		Unify::SolutionSet Unify::join(const Partition& partition,
900		const TypedBlock& block) const
901		{
902		// Find all partition blocks that have elements in common with block
903		TypedBlockSeq common_blocks;
904		for (const TypedBlock& p_block : partition)
905		if (not has_empty_intersection(block.first, p_block.first))
906		common_blocks.push_back(p_block);
907
908		Partition jp(partition);
909		if (common_blocks.empty()) {
910		// If none then merely insert the independent block
911		jp.insert(block);
912		return SolutionSet({jp});
913		} else {
914		// Otherwise join block with all common blocks and replace
915		// them by the result (if satisfiable, otherwise return the
916		// empty solution set)
917		TypedBlock j_block = join(common_blocks, block);
918		if (is_satisfiable(j_block)) {
919		for (const TypedBlock& rm : common_blocks)
920		jp.erase(rm.first);
921		jp.insert(j_block);
922
923		// Perform the sub-unification of all common blocks with
924		// block and join the solution set to jp
925		SolutionSet sol = subunify(common_blocks, block);
926		if (sol.is_satisfiable())
927		return join(sol, jp);
928		}
929		return SolutionSet();
930		}
931		}
932
933		Unify::TypedBlock Unify::join(const TypedBlockSeq& common_blocks,
934		const TypedBlock& block) const
935		{
936		std::pair<Block, CHandle> result{block};
937		for (const auto& c_block : common_blocks) {
938		result = join(result, c_block);
939		// Abort if unsatisfiable
940		if (not is_satisfiable(result))
941		return result;
942		}
943		return result;
944		}
945
946		Unify::TypedBlock Unify::join(const TypedBlock& lhs, const TypedBlock& rhs) const
947		{
948		OC_ASSERT(lhs.second and rhs.second, "Can only join 2 satisfiable blocks");
949		return {set_union(lhs.first, rhs.first),
950		type_intersection(lhs.second, rhs.second)};
951		}
952
953		Unify::SolutionSet Unify::subunify(const TypedBlockSeq& common_blocks,
954		const TypedBlock& block) const
955		{
956		// Form a set with all terms
957		std::set<CHandle> all_chs(block.first);
958		for (const TypedBlock& cb : common_blocks)
959		all_chs.insert(cb.first.begin(), cb.first.end());
960
961		// Build a set of all pairs of terms that may have not been
962		// unified so far.
963		std::set<CHandlePair> not_unified;
964		// This function returns true iff both terms are in the given
965		// block. If so it means they have already been unified.
966		auto both_in_block = [](const CHandle& lch, const CHandle& rch,
967		const TypedBlock& block) {
968		return contains(block.first, lch) and contains(block.first, rch);
969		};
970		for (auto lit = all_chs.begin(); lit != all_chs.end(); ++lit) {
971		for (auto rit = std::next(lit); rit != all_chs.end(); ++rit) {
972		// Check if they are in block
973		bool already_unified = both_in_block(lit, rit, block);
974		// If not, then check if they are in one of the common
975		// blocks
976		if (not already_unified) {
977		for (const TypedBlock& cb : common_blocks) {
978		already_unified = both_in_block(lit, rit, cb);
979		if (already_unified)
980		break;
981		}
982		}
983		if (not already_unified)
984		not_unified.insert({lit, rit});
985		}
986		}
987
988		// Unify all not unified yet terms
989		return pairwise_unify(not_unified);
990		}
991
992		Unify::SolutionSet Unify::subunify(const TypedBlock& lhs,
993		const TypedBlock& rhs) const
994		{
995		return comb_unify(set_symmetric_difference(lhs.first, rhs.first));
996		}
997
998		bool Unify::is_satisfiable(const TypedBlock& block) const
999		{
1000		return (bool)block.second;
1001		}
1002
1003		bool unifiable(const Handle& lhs, const Handle& rhs,
1004		const Handle& lhs_vardecl, const Handle& rhs_vardecl)
1005		{
1006		Unify unify(lhs, rhs, lhs_vardecl, rhs_vardecl);
1007		return unify().is_satisfiable();
1008		}
1009
1010		bool hm_content_eq(const HandleMap& lhs, const HandleMap& rhs)
1011		{
1012		if (lhs.size() != rhs.size())
1013		return false;
1014
1015		auto lit = lhs.begin();
1016		auto rit = rhs.begin();
1017		while (lit != lhs.end()) {
1018		if (not content_eq(lit->first, rit->first)
1019		or not content_eq(lit->second, rit->second))
1020		return false;
1021		++lit; ++rit;
1022		}
1023		return true;
1024		}
1025
1026		bool hchm_content_eq(const Unify::HandleCHandleMap& lhs,
1027		const Unify::HandleCHandleMap& rhs)
1028		{
1029		if (lhs.size() != rhs.size())
1030		return false;
1031
1032		auto lit = lhs.begin();
1033		auto rit = rhs.begin();
1034		while (lit != lhs.end()) {
1035		if (not content_eq(lit->first, rit->first)
1036		or lit->second != rit->second)
1037		return false;
1038		++lit; ++rit;
1039		}
1040		return true;
1041		}
1042
1043		bool ts_content_eq(const Unify::TypedSubstitution& lhs,
1044		const Unify::TypedSubstitution& rhs)
1045		{
1046		return lhs.first.size() == rhs.first.size()
1047		and hchm_content_eq(lhs.first, rhs.first)
1048		and content_eq(lhs.second, rhs.second);
1049		}
1050
1051		bool tss_content_eq(const Unify::TypedSubstitutions& lhs,
1052		const Unify::TypedSubstitutions& rhs)
1053		{
1054		if (lhs.size() != rhs.size())
1055		return false;
1056
1057		auto lit = lhs.begin();
1058		auto rit = rhs.begin();
1059		while (lit != lhs.end()) {
1060		if (not ts_content_eq(lit, rit))
1061		return false;
1062		++lit; ++rit;
1063		}
1064		return true;
1065		}
1066
1067		HandleMap strip_context(const Unify::HandleCHandleMap& hchm)
1068		{
1069		HandleMap result;
1070		for (auto& el : hchm) {
1071		const Context& ctx = el.second.context;
1072		Handle val = el.second.handle;
1073
1074		// Insert quotation links if necessary
1075		for (int i = 0; i < ctx.quotation.level(); i++) {
1076		if (i == 0 and ctx.quotation.is_locally_quoted())
1077		val = Handle(createLink(LOCAL_QUOTE_LINK, val));
1078		else
1079		val = Handle(createLink(QUOTE_LINK, val));
1080		}
1081
1082		// Recreate variable to value mapping without context
1083		result.insert({el.first, val});
1084		}
1085		return result;
1086		}
1087
1088		Unify::CHandle Unify::type_intersection(const CHandle& lch, const CHandle& rch) const
1089		{
1090		if (inherit(lch, rch))
1091		return lch;
1092		if (inherit(rch, lch))
1093		return rch;
1094		return Handle::UNDEFINED;
1095		}
1096
1097		TypeSet Unify::simplify_type_union(TypeSet& type) const
1098		{
1099		return {}; // TODO: do we really need that?
1100		}
1101
1102		TypeSet Unify::get_union_type(const Handle& h) const
1103		{
1104		const VariableTypeMap& vtm = _variables._typemap;
1105		auto it = vtm.find(h);
1106		if (it == vtm.end() or it->second->get_simple_typeset().empty())
1107		return {ATOM};
1108		else {
1109		return it->second->get_simple_typeset();
1110		}
1111		}
1112
1113		bool Unify::inherit(const CHandle& lch, const CHandle& rch) const
1114		{
1115		return inherit(lch.handle, rch.handle, lch.context, rch.context);
1116		}
1117
1118		bool Unify::inherit(const Handle& lh, const Handle& rh,
1119		Context lc, Context rc) const
1120		{
1121		Type lt = lh->get_type();
1122		Type rt = rh->get_type();
1123
1124		// Recursive cases
1125
1126		// Consume quotations
1127		if (lc.quotation.consumable(lt)) {
1128		lc.quotation.update(lt);
1129		return inherit(lh->getOutgoingAtom(0), rh, lc, rc);
1130		}
1131		if (rc.quotation.consumable(rt)) {
1132		rc.quotation.update(rt);
1133		return inherit(lh, rh->getOutgoingAtom(0), lc, rc);
1134		}
1135
1136		// If both are links then check that the outgoings of lhs inherit
1137		// the outgoings of rhs.
1138		if (lh->is_link() and rh->is_link() and (lt == rt)) {
1139		if (lh->get_arity() == rh->get_arity()) {
1140		for (size_t i = 0; i < lh->get_arity(); i++) {
1141		if (not inherit(lh->getOutgoingAtom(i),
1142		rh->getOutgoingAtom(i),
1143		lc, rc))
1144		return false;
1145		}
1146		return true;
1147		} else return false;
1148		}
1149
1150		// Base cases
1151
1152		// If they are equal then lh trivial inherits from rh
1153		if (lh == rh)
1154		return true;
1155
1156		// If both are free variables and declared then look at their types
1157		// (only simple types are considered for now).
1158		if (is_free_declared_variable(lc, lh) and is_free_declared_variable(rc, rh))
1159		return inherit(get_union_type(lh), get_union_type(rh)) and
1160		inherit(_variables.get_interval(lh), _variables.get_interval(rh));
1161
1162		// If only rh is a free and declared variable then check whether lh
1163		// type inherits from it (using Variables::is_type).
1164		if (is_free_declared_variable(rc, rh))
1165		return _variables.is_type(rh, lh);
1166
1167		return false;
1168		}
1169
1170		bool Unify::inherit(Type lhs, Type rhs) const
1171		{
1172		return nameserver().isA(lhs, rhs);
1173		}
1174
1175		bool Unify::inherit(Type lhs, const TypeSet& rhs) const
1176		{
1177		for (Type ty : rhs)
1178		if (inherit(lhs, ty))
1179		return true;
1180		return false;
1181		}
1182
1183		bool Unify::inherit(const TypeSet& lhs, const TypeSet& rhs) const
1184		{
1185		for (Type ty : lhs)
1186		if (not inherit(ty, rhs))
1187		return false;
1188		return true;
1189		}
1190
1191		bool Unify::inherit(const std::pair<double, double> &lgm,
1192		const std::pair<double, double> &rgm) const
1193		{
1194		return rgm.first <= lgm.first and rgm.second >= lgm.second;
1195		}
1196
1197		bool Unify::is_declared_variable(const Handle& h) const
1198		{
1199		return _variables.varset_contains(h);
1200		}
1201
1202		bool Unify::is_declared_variable(const CHandle& ch) const
1203		{
1204		return is_declared_variable(ch.handle);
1205		}
1206
1207		bool Unify::is_free_declared_variable(const CHandle& ch) const
1208		{
1209		return ch.is_free_variable() and is_declared_variable(ch);
1210		}
1211
1212		bool Unify::is_free_declared_variable(const Context& c, const Handle& h) const
1213		{
1214		return c.is_free_variable(h) and is_declared_variable(h);
1215		}
1216
1217		bool Unify::is_node_satisfiable(const CHandle& lch, const CHandle& rch) const
1218		{
1219		// First take care of free undeclared variables treated as
1220		// constants
1221		if (lch.is_free_variable() and not is_declared_variable(lch) and
1222		rch.is_free_variable() and not is_declared_variable(rch))
1223		return content_eq(lch.handle, rch.handle);
1224		return lch.is_node_satisfiable(rch);
1225		}
1226
1227		Variables merge_variables(const Variables& lhs, const Variables& rhs)
1228		{
1229		Variables new_vars(lhs);
1230		new_vars.extend_intersect(rhs);
1231		return new_vars;
1232		}
1233
1234		Handle merge_vardecl(const Handle& lhs_vardecl, const Handle& rhs_vardecl)
1235		{
1236		if (not lhs_vardecl)
1237		return rhs_vardecl;
1238		if (not rhs_vardecl)
1239		return lhs_vardecl;
1240
1241		Variables
1242		lhs_vl(lhs_vardecl),
1243		rhs_vl(rhs_vardecl);
1244
1245		Variables new_vars = merge_variables(lhs_vl, rhs_vl);
1246		return new_vars.get_vardecl();
1247		}
1248
1249		std::string oc_to_string(const Unify::CHandle& ch, const std::string& indent)
1250		{
1251		std::stringstream ss;
1252		ss << indent << "context:" << std::endl
1253		<< oc_to_string(ch.context, indent + OC_TO_STRING_INDENT) << std::endl
1254		<< indent << "atom:" << std::endl
1255		<< oc_to_string(ch.handle, indent + OC_TO_STRING_INDENT);
1256		return ss.str();
1257		}
1258
1259		std::string oc_to_string(const Unify::Block& pb, const std::string& indent)
1260		{
1261		std::stringstream ss;
1262		ss << indent << "size = " << pb.size();
1263		int i = 0;
1264		for (const auto& el : pb)
1265		ss << std::endl << indent << "catom[" << i++ << "]:" << std::endl
1266		<< oc_to_string(el, indent + OC_TO_STRING_INDENT);
1267		return ss.str();
1268		}
1269
1270		std::string oc_to_string(const Unify::TypedBlock& tb, const std::string& indent)
1271		{
1272		std::stringstream ss;
1273		ss << indent << "block:" << std::endl
1274		<< oc_to_string(tb.first, indent + OC_TO_STRING_INDENT) << std::endl
1275		<< indent << "type:" << std::endl
1276		<< oc_to_string(tb.second, indent + OC_TO_STRING_INDENT);
1277		return ss.str();
1278		}
1279
1280		std::string oc_to_string(const Unify::TypedBlockSeq& tbs, const std::string& indent)
1281		{
1282		std::stringstream ss;
1283		ss << indent << "size = " << tbs.size();
1284		for (size_t i = 0; i < tbs.size(); i++)
1285		ss << std::endl << indent << "typed block[" << i << "]:" << std::endl
1286		<< oc_to_string(tbs[i], indent + OC_TO_STRING_INDENT);
1287		return ss.str();
1288		}
1289
1290		std::string oc_to_string(const Unify::Partition& up, const std::string& indent)
1291		{
1292		std::stringstream ss;
1293		ss << indent << "size = " << up.size();
1294		int i = 0;
1295		for (const auto& p : up) {
1296		ss << std::endl << indent << "block[" << i << "]:" << std::endl
1297		<< oc_to_string(p.first, indent + OC_TO_STRING_INDENT) << std::endl
1298		<< indent << "type[" << i << "]:" << std::endl
1299		<< oc_to_string(p.second, indent + OC_TO_STRING_INDENT);
1300		i++;
1301		}
1302		return ss.str();
1303		}
1304
1305		std::string oc_to_string(const Unify::Partitions& par, const std::string& indent)
1306		{
1307		std::stringstream ss;
1308		ss << indent << "size = " << par.size();
1309		int i = 0;
1310		for (const auto& el : par) {
1311		ss << std::endl << indent << "typed partition[" << i << "]:"
1312		<< std::endl << oc_to_string(el, indent + OC_TO_STRING_INDENT);
1313		i++;
1314		}
1315		return ss.str();
1316		}
1317
1318		std::string oc_to_string(const Unify::HandleCHandleMap& hchm,
1319		const std::string& indent)
1320		{
1321		std::stringstream ss;
1322		ss << indent << "size = " << hchm.size();
1323		int i = 0;
1324		for (const auto& hch : hchm) {
1325		ss << std::endl << indent << "atom[" << i << "]:" << std::endl
1326		<< oc_to_string(hch.first, indent + OC_TO_STRING_INDENT) << std::endl;
1327		ss << indent << "catom[" << i << "]:" << std::endl
1328		<< oc_to_string(hch.second, indent + OC_TO_STRING_INDENT);
1329		i++;
1330		}
1331		return ss.str();
1332		}
1333
1334		std::string oc_to_string(const Unify::HandleCHandleMap::value_type& hch,
1335		const std::string& indent)
1336		{
1337		std::stringstream ss;
1338		ss << indent << "atom:" << std::endl
1339		<< oc_to_string(hch.first, indent + OC_TO_STRING_INDENT) << std::endl;
1340		ss << indent << "catom:" << std::endl
1341		<< oc_to_string(hch.second, indent + OC_TO_STRING_INDENT);
1342		return ss.str();
1343		}
1344
1345		std::string oc_to_string(const Unify::TypedSubstitution& ts,
1346		const std::string& indent)
1347		{
1348		std::stringstream ss;
1349		ss << indent << "substitution:" << std::endl
1350		<< oc_to_string(ts.first, indent + OC_TO_STRING_INDENT) << std::endl
1351		<< indent << "vardecl:" << std::endl
1352		<< oc_to_string(ts.second, indent + OC_TO_STRING_INDENT);
1353		return ss.str();
1354		}
1355
1356		std::string oc_to_string(const Unify::TypedSubstitutions::value_type& ts,
1357		const std::string& indent)
1358		{
1359		std::stringstream ss;
1360		ss << indent << "substitution:" << std::endl
1361		<< oc_to_string(ts.first, indent + OC_TO_STRING_INDENT) << std::endl
1362		<< indent << "vardecl:" << std::endl
1363		<< oc_to_string(ts.second, indent + OC_TO_STRING_INDENT);
1364		return ss.str();
1365		}
1366
1367		std::string oc_to_string(const Unify::TypedSubstitutions& tss,
1368		const std::string& indent)
1369		{
1370		std::stringstream ss;
1371		ss << indent << "size = " << tss.size();
1372		int i = 0;
1373		for (const auto& ts : tss) {
1374		ss << std::endl << indent << "typed substitution[" << i << "]:"
1375		<< std::endl << oc_to_string(ts, indent + OC_TO_STRING_INDENT);
1376		i++;
1377		}
1378		return ss.str();
1379		}
1380
1381		} // namespace opencog

opencog/unify/Unify.h +0 -908

…	…	@@ -1,908 +0,0 @@
1		/**
2		* Unify.h
3		*
4		* Utilities for unifying atoms.
5		*
6		* Copyright (C) 2016 OpenCog Foundation
7		* All Rights Reserved
8		* Author: Nil Geisweiller
9		*
10		* This program is free software; you can redistribute it and/or modify
11		* it under the terms of the GNU Affero General Public License v3 as
12		* published by the Free Software Foundation and including the exceptions
13		* at http://opencog.org/wiki/Licenses
14		*
15		* This program is distributed in the hope that it will be useful,
16		* but WITHOUT ANY WARRANTY; without even the implied warranty of
17		* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
18		* GNU General Public License for more details.
19		*
20		* You should have received a copy of the GNU Affero General Public License
21		* along with this program; if not, write to:
22		* Free Software Foundation, Inc.,
23		* 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
24		*/
25
26		#ifndef _OPENCOG_UNIFY_UTILS_H
27		#define _OPENCOG_UNIFY_UTILS_H
28
29		#include <boost/operators.hpp>
30
31		#include <opencog/util/empty_string.h>
32		#include <opencog/atoms/atom_types/atom_types.h>
33		#include <opencog/atoms/base/Handle.h>
34		#include <opencog/atoms/core/Context.h>
35		#include <opencog/atoms/core/VariableList.h>
36		#include <opencog/atoms/core/Variables.h>
37		#include <opencog/atoms/pattern/BindLink.h>
38
39		namespace opencog {
40
41		class Unify
42		{
43		friend class UnifyUTest;
44
45		public:
46		// Contextual Handle
47		//
48		// TODO: the notion of equality between 2 CHandles might one where
49		// the Context isn't necessarily equal but where the 2 handles
50		// (besides being equal) have the same quotation and same
51		// (free inter shadow) variables.
52		struct CHandle : public boost::totally_ordered<CHandle>
53		{
54		CHandle(const Handle& handle, const Context& context=Context());
55
56		Handle handle;
57		Context context;
58
59		/**
60		* Return true iff the atom in that context is a variable,
61		* free or not.
62		*/
63		bool is_variable() const;
64
65		/**
66		* Return true iff the atom in that context is a free
67		* variable, that is unquoted and unshadowed.
68		*/
69		bool is_free_variable() const;
70
71		/**
72		* Return the set of free visible variables from that context.
73		*/
74		HandleSet get_free_variables() const;
75
76		/**
77		* Return iterator of the variable declaration containing a given
78		* variable, if so.
79		*/
80		Context::VariablesStack::const_iterator
81		find_variables(const Handle& h) const;
82
83		/**
84		* Return true iff has a consumable quotation
85		*/
86		bool is_consumable() const;
87
88		/**
89		* Return true iff it is quoted.
90		*/
91		bool is_quoted() const;
92
93		/**
94		* Return true iff it is unquoted.
95		*/
96		bool is_unquoted() const;
97
98		/**
99		* Update its context, and if consumable update the Handle as
100		* well, that is replace itself by its child.
101		*/
102		void update();
103
104		/**
105		* Return true if 2 contextual handles are satisfiable in some
106		* restricted sense, it assumes that
107		*
108		* 1. at least one of them is a node
109		* 2. none is a free variable (i.e. unfree or not a variable)
110		*
111		* Given these 2 assumptions fulfilled, it will check whether
112		* the 2 atoms are equal, and if there are not could there be
113		* alpha equivalent (assuming they are variables).
114		*/
115		bool is_node_satisfiable(const CHandle& other) const;
116
117		/**
118		* Comparison.
119		*/
120		bool operator==(const CHandle& other) const;
121		bool operator<(const CHandle& other) const;
122
123		/**
124		* Cast operators
125		*/
126		explicit operator bool() const;
127		};
128
129		// Pair of CHandles
130		typedef std::pair<CHandle, CHandle> CHandlePair;
131
132		// Partition block. A block is a set of CHandles that are
133		// hypothesized as being unifiable, that is there exists a
134		// substitution making them equal.
135		typedef std::set<CHandle> Block;
136
137		// Mapping from partition blocks to type. The type for now is the
138		// most specialized term of the block, till types are better
139		// supported.
140		typedef std::map<Block, CHandle> Partition;
141
142		// Element of a partition, that is a pair of block and its type.
143		typedef Partition::value_type TypedBlock;
144
145		// Useful for representing common block before sub-unification.
146		typedef std::vector<TypedBlock> TypedBlockSeq;
147
148		// Set of partitions, that is a solution set, typically assumed
149		// satisfiable when used in standalone.
150		typedef std::set<Partition> Partitions;
151
152		// Empty partition set
153		static const Partitions empty_partitions;
154
155		// Partition set singleton containing an empty partition. This is
156		// the simplest satisfiable solution set.
157		static const Partitions empty_partition_singleton;
158
159		// TODO: the type of a typed block is currently a handle of the
160		// variable or ground it is exists, instead of an actual type.
161		struct SolutionSet : Partitions
162		{
163		// Default ctor
164		explicit SolutionSet(const Partitions& p);
165		// Helper ctor. Initialize with the empty partition as
166		// singleton, i.e. a satisfiable solution, if s == true, or
167		// the empty partition set if unsatisfiable.
168		explicit SolutionSet(bool s=false);
169
170		// Return true iff the solution set is satisfiable which is
171		// indicated by whether it is empty or not.
172		bool is_satisfiable() const;
173
174		// Insert sol to the existing solution set. Merely perform the
175		// union of solutions, not the join.
176		void insert(const SolutionSet& sol);
177
178		// Remove partitions with cycles from the solution set.
179		void remove_cycles();
180		};
181
182		// Mapping from Handle (typically a variable) to a contextual handle
183		typedef std::map<Handle, CHandle> HandleCHandleMap;
184
185		// Subtitution values and their corresponding variable declaration
186		// after substitution (cause some values may be variables).
187		//
188		// TODO: maybe we could simplify a great deal of code by replacing
189		// Handle by Variables.
190		typedef std::map<HandleCHandleMap, Handle> TypedSubstitutions;
191		typedef std::pair<HandleCHandleMap, Handle> TypedSubstitution;
192
193		/**
194		* Ctor. Initialize for the unification of lhs and rhs, with
195		* respective variable declarations lhs_vardecl and rhs_vardecl.
196		*/
197		Unify(const Handle& lhs, const Handle& rhs,
198		const Handle& lhs_vardecl=Handle::UNDEFINED,
199		const Handle& rhs_vardecl=Handle::UNDEFINED);
200		Unify(const Handle& lhs, const Handle& rhs,
201		const Variables& lhs_vars, const Variables& rhs_vars);
202
203		/**
204		* Generate typed substitution rules, given a satisfiable
205		* SolutionSet and the term from which to select the variables as
206		* values in case multiple choices are possible.
207		*/
208		TypedSubstitutions typed_substitutions(const SolutionSet& sol,
209		const Handle& pre) const;
210
211		/**
212		* Like typed_substitutions but generate a single typed
213		* substitution of a supposedly satisfiable partition.
214		*/
215		TypedSubstitution typed_substitution(const Partition& partition,
216		const Handle& pre) const;
217
218		/**
219		* Calculate the closure of a typed substitution. That is apply
220		* self-substitution to each values till a fixed point is
221		* reached. For instance given the variable to value mapping
222		*
223		* (Variable "$X") -> (Inheritance (Variable "$P") (Variable "$Q"))
224		* (Variable "$P") -> (Concept "A")
225		* (Variable "$Q") -> (Concept "B")
226		*
227		* produces
228		*
229		* (Variable "$X") -> (Inheritance (Concept "A") (Concept "B"))
230		* (Variable "$P") -> (Concept "A")
231		* (Variable "$Q") -> (Concept "B")
232		*/
233		HandleCHandleMap substitution_closure(const HandleCHandleMap& var2val) const;
234
235		/**
236		* Calculate the variable declaration of the underlying new scope
237		* link after substitution would have occured given a substitution
238		* mapping.
239		*/
240		Handle substitution_vardecl(const HandleCHandleMap& var2val) const;
241
242		/**
243		* If the quotations are useless or harmful, which might be the
244		* case if they deprive a ScopeLink from hiding supposedly hidden
245		* variables, consume them. See RewriteLink::consume_quotations
246		* comment for more details.
247		*/
248		static BindLinkPtr consume_quotations(BindLinkPtr bl);
249
250		/**
251		* Return true iff the handle or type correspond to a pattern
252		* matcher connector.
253		*/
254		static bool is_pm_connector(const Handle& h);
255		static bool is_pm_connector(Type t);
256
257		/**
258		* Given a partition, return a mapping between any standalone
259		* variable X and the union of the other variables present in the
260		* blocks where X appears.
261		*
262		* For instance (ignoring types for simplicity):
263		*
264		* partition = { {X, (Inheritance X, Y)}, {Z, X} }
265		*
266		* then vargraph returns
267		*
268		* { { X : {X, Y, Z} },
269		* { Z : {X} } }
270		*
271		* Another example:
272		*
273		* partition = { {X, (Inheritance A, Y)}, {Y, (Inheritance B, X)} }
274		*
275		* then vargraph returns
276		*
277		* { { X : {Y} },
278		* { Y : {X} } }
279		*/
280		static HandleMultimap vargraph(const Partition& partition);
281		static HandleMultimap vargraph(const Block& blk);
282
283		/**
284		* Return true iff partition has one or more cycles. For example if
285		* we are trying to unify
286		*
287		* (List (List X Y))
288		*
289		* with
290		*
291		* (List (List (List Y) (List X)))
292		*
293		* its solution (ignoring types for simplicity) is
294		*
295		* { // Block 1
296		* { X, List Y },
297		* // Block 2
298		* { Y, List X } }
299		*
300		* One can see that such solution contains a cycle would result in
301		* a never-ending substituion
302		*
303		* X -> List Y -> List List X -> List List List Y -> ...
304		*/
305		static bool has_cycle(const Partition& partition);
306		static bool has_cycle(const Block& blk);
307
308		/**
309		* Same above but uses a graph obtained from vargraph.
310		*
311		* Note: argument is passed by copy for implementational convenience.
312		*/
313		static bool has_cycle(const HandleMultimap& vg);
314
315		/**
316		* Return the closure of vg.
317		*/
318		static HandleMultimap closure(const HandleMultimap& vg);
319
320		/**
321		* Return one step of closure of vg.
322		*/
323		static HandleMultimap closure_step(const HandleMultimap& vg);
324
325		/**
326		* Given a typed substitution, perform the substitution over a scope
327		* link (for now only BindLinks are supported).
328		*
329		* If an atomspace is provided then remove constant clauses
330		* present in the atomspace.
331		*/
332		static Handle substitute(BindLinkPtr bl,
333		const TypedSubstitution& ts,
334		const AtomSpace* queried_as=nullptr);
335
336		/**
337		* Given a mapping from variables to values, return a copy of
338		* itself with variables substituted by the values. Values could
339		* be variable as well. The variable declaration is automatically
340		* adjusted so only the new variables remain. Optionally, if the
341		* types have changed, a new variable declaration is provided to
342		* replace the existing one. Constant clauses are automatically
343		* removed from the BindLink. If no clause remains then the
344		* pattern body is left with an empty AndLink.
345		*
346		* If an atomspace is provided then remove constant clauses
347		* present in the atomspace.
348		*
349		* Examples:
350		*
351		* Assume the instance is:
352		*
353		* (BindLink
354		* (VariableList (Variable "$X") (Variable "$Y"))
355		* (Inheritance (Variable "$X") (Variable "$Y"))
356		* (ExecutionOutputLink
357		* (GroundedSchemaNode "gsn")
358		* (Inheritance (Variable "$X") (Variable "$Y"))))
359		*
360		* 1. substitute([(Variable "$W"), (Variable "$Z")]) returns:
361		*
362		* (BindLink
363		* (VariableList (Variable "$W") (Variable "$Z"))
364		* (Inheritance (Variable "$W") (Variable "$Z"))
365		* (ExecutionOutputLink
366		* (GroundedSchemaNode "gsn")
367		* (Inheritance (Variable "$W") (Variable "$Z"))))
368		*
369		* 2. substitute([(Variable "$W"), (Variable "$Z")], variables)
370		* such that variables associates a ConceptNode type to $W and $Z
371		* returns:
372		*
373		* (BindLink
374		* (VariableList
375		* (TypedVariable (Variable "$W") (Type "ConceptNode"))
376		* (TypedVariable (Variable "$Z") (Type "ConceptNode")))
377		* (Inheritance (Variable "$W") (Variable "$Z")))
378		* (ExecutionOutputLink
379		* (GroundedSchemaNode "gsn")
380		* (Inheritance (Variable "$W") (Variable "$Z"))))
381		*
382		* 3. substitute([(Variable "$W"), (Concept "B")]) returns:
383		*
384		* (BindLink
385		* (Variable "$W")
386		* (Inheritance (Variable "$W") (Concept "B"))
387		* (ExecutionOutputLink
388		* (GroundedSchemaNode "gsn")
389		* (Inheritance (Variable "$W") (Concept "B"))))
390		*
391		* 4. substitute([(Concept "A"), (Concept "B")]) returns:
392		*
393		* (BindLink
394		* (AndLink)
395		* (ExecutionOutputLink
396		* (GroundedSchemaNode "gsn")
397		* (Inheritance (Concept "$A") (Concept "B"))))
398		*
399		* TODO: replace by RewriteLink methods!
400		*/
401		static Handle substitute(BindLinkPtr bl, const HandleMap& var2val,
402		Handle vardecl=Handle::UNDEFINED,
403		const AtomSpace* queried_as=nullptr);
404
405		/**
406		* Substitute the variable declaration of a BindLink. Remove
407		* variables that are substituted by values. If all variables are
408		* removed it returns Handle::UNDEFINED.
409		*
410		* TODO: replace by RewriteLink methods!
411		*/
412		static Handle substitute_vardecl(const Handle& vardecl,
413		const HandleMap& var2val);
414
415		/**
416		* Given a pattern term (a conjunction of clauses) and a variable
417		* declaration, remove the constant clauses. If all clauses are
418		* constants then return an empty AndLink.
419		*
420		* If an atomspace is provided then check that the constant is in
421		* the atomspace as well, otherwise do not remove it.
422		*
423		* The variable declaration is assumed defined. That is if there
424		* are no variable, rather than Handle::UNDEFINED the vardecl will
425		* have to be a empty VariableList. That is because an undefined
426		* variable declaration is ambiguous as we don't know what whether
427		* it means empty or containing all free variables.
428		*/
429		static Handle remove_constant_clauses(const Handle& vardecl,
430		const Handle& clauses,
431		const AtomSpace* queried_as=nullptr);
432
433		/**
434		* Perform unification by recursively
435		*
436		* 1. Generate all equality partitions
437		*
438		* 2. Decorate partition blocks with types
439		*
440		* 3. Only retain partitions that are satisfiable
441		*
442		* 4. Only retain partitions that do not have cycles
443		*
444		* For now the types in 2. are represented by the substitutions, for
445		* instance the typed block {{X, A}, A} means that X is A. Later one
446		* we will replace that by deep types as to represents things like
447		* {{X, Y}, ConceptNode} meaning that X and Y must be concept nodes is
448		* order to be satisfiable, of course the deep will still need to
449		* capture grounds such as {{X, A}, A}, it's not clear excatly how,
450		* maybe Linas deep type implementation can already do that.
451		*
452		* To solve 3, for each partition block, it computes the type that
453		* intersects all its elements and repeat till a fixed point is
454		* reached. To do that efficiently we would need to build a dependency
455		* DAG, but at first we can afford to compute type intersections is
456		* random order.
457		*
458		* Also, permutations are supported though very slow.
459		*
460		* Examples:
461		*
462		* 1.
463		*
464		* unify((Variable "$X"), (Concept "A"))
465		* ->
466		* {{<{(Variable "$X"), (Concept "A")}, (Concept "A")>}}
467		*
468		* meaning that the partition block {(Variable "$X"), (Concept "A")}
469		* has type (Concept "A"), and there is only one partition in the
470		* solution set.
471		*
472		* 2.
473		*
474		* unify((Concept "A"), (Concept "$X"))
475		* ->
476		* {{<{(Variable "$X"), (Concept "A")}, (Concept "A")>}}
477		*
478		* 3.
479		*
480		* unify((Inheritance (Concept "A") (Concept "B")), (Variable "$X"))
481		* ->
482		* {{<{(Variable "$X"), (Inheritance (Concept "A") (Concept "B"))},
483		* (Inheritance (Concept "A") (Concept "B"))>}}
484		*
485		* 4.
486		*
487		* unify((Inheritance (Concept "A") (Variable "$Y")),
488		* (Inheritance (Variable "$X") (Concept "B"))
489		* ->
490		* {{<{(Variable "$X"), (Concept "A")}, (Concept "A")>,
491		* <{(Variable "$Y"), (Concept "B")}, (Concept "B")>}}
492		*
493		* 5.
494		*
495		* unify((And (Concept "A") (Concept "B")),
496		* (And (Variable "$X") (Variable "$Y"))
497		* ->
498		* {
499		* {<{(Variable "$X"), (Concept "A")}, (Concept "A")>,
500		* <{(Variable "$Y"), (Concept "B")}, (Concept "B")>},
501		*
502		* {<{(Variable "$X"), (Concept "B")}, (Concept "B")>,
503		* <{(Variable "$Y"), (Concept "A")}, (Concept "A")>}
504		* }
505		*
506		* mean that the solution set has 2 partitions, one where X unifies to
507		* A and Y unifies to B, and another one where X unifies to B and Y
508		* unifies to A.
509		*/
510		SolutionSet operator()();
511
512		private:
513		// Terms to unify
514		Handle _lhs;
515		Handle _rhs;
516
517		// Common variable declaration of the two terms to unify.
518		Variables _variables;
519
520		public: // ???? It's a friend yet
521		/**
522		* Set Unify::_variables given the variable declarations of the
523		* two terms to unify.
524		*/
525		void set_variables(const Handle& lhs, const Handle& rhs,
526		const Handle& lhs_vardecl=Handle::UNDEFINED,
527		const Handle& rhs_vardecl=Handle::UNDEFINED);
528
529		private:
530		/**
531		* Find the least abstract atom in the given block.
532		*/
533		CHandle find_least_abstract(const TypedBlock& block, const Handle& pre) const;
534
535		/**
536		* Unify lhs and rhs. _lhs_vardecl and _rhs_vardecl should be set
537		* prior to run this method.
538		*
539		* Note that unify does not check for cycles, only operator() does,
540		* this is because it is an expensive operation, and cycles are
541		* extremely rare in practice, so it is better to check in the end,
542		* once all solutions have been constructed, and remove partitions
543		* with cycles if necessary.
544		*
545		* TODO: could probably optimize by memoizing unify, due to
546		* subunify being called redundantly.
547		*/
548		SolutionSet unify(const CHandle& lhs, const CHandle& rhs) const;
549		SolutionSet unify(const Handle& lhs, const Handle& rhs,
550		Context lhs_context=Context(),
551		Context rhs_context=Context()) const;
552
553		/**
554		* Unify all elements of lhs with all elements of rhs, considering
555		* all permutations.
556		*/
557		SolutionSet unordered_unify(const HandleSeq& lhs, const HandleSeq& rhs,
558		Context lhs_context=Context(),
559		Context rhs_context=Context()) const;
560
561		/**
562		* Unify all elements of lhs with all elements of rhs, in the
563		* provided order.
564		*/
565		SolutionSet ordered_unify(const HandleSeq& lhs, const HandleSeq& rhs,
566		Context lhs_context=Context(),
567		Context rhs_context=Context()) const;
568
569		/**
570		* Unify all pairs of CHandles.
571		*/
572		SolutionSet pairwise_unify(const std::set<CHandlePair>& pchs) const;
573
574		/**
575		* Unify all elements of lhs with all elements of rhs, considering
576		* all pairwise combinations.
577		*/
578		SolutionSet comb_unify(const std::set<CHandle>& lhs,
579		const std::set<CHandle>& rhs) const;
580
581		/**
582		* Unify all pairs of elements in chs.
583		*/
584		SolutionSet comb_unify(const std::set<CHandle>& chs) const;
585
586		/**
587		* Return a copy of a HandleSeq with the ith element removed.
588		*/
589		HandleSeq cp_erase(const HandleSeq& hs, Arity i) const;
590
591		/**
592		* Build elementary solution set between 2 atoms given that at
593		* least one of them is a variable.
594		*
595		* Passed by copy because this method may use and modify the copy.
596		*/
597		SolutionSet mkvarsol(CHandle lhs, CHandle rhs) const;
598
599		public: // TODO: being friend with UnifyUTest
600		// somehow doesn't work
601		/**
602		* Join 2 solution sets. Generate the product of all consistent
603		* solutions (with partitions so that all blocks are typed with a
604		* defined Handle).
605		*/
606		SolutionSet join(const SolutionSet& lhs, const SolutionSet& rhs) const;
607
608		private:
609		/**
610		* Join a satisfiable partition sets with a satisfiable partition.
611		*/
612		SolutionSet join(const SolutionSet& lhs, const Partition& rhs) const;
613
614		/**
615		* Join 2 partitions. The result can be set of partitions (see
616		* join(const Partition&, const TypedBlock&) for explanation).
617		*/
618		SolutionSet join(const Partition& lhs, const Partition& rhs) const;
619
620		/**
621		* Join a block with a partition set. The partition set is assumed
622		* non empty and satisfiable.
623		*/
624		SolutionSet join(const SolutionSet& sol, const TypedBlock& block) const;
625
626		/**
627		* Join a partition and a block. If the block has no element in
628		* common with any block of the partition, merely insert
629		* it. Otherwise fuse the blocks with common elements into
630		* one. During this fusion new unification problems may arise
631		* (TODO: explain why) thus possibly multiple partitions will be
632		* returned.
633		*/
634		SolutionSet join(const Partition& partition, const TypedBlock &block) const;
635
636		/**
637		* Join a block to a partition to form a single block. It is
638		* assumed that all blocks have elements in common.
639		*/
640		TypedBlock join(const TypedBlockSeq& common_blocks,
641		const TypedBlock& block) const;
642
643		/**
644		* Join 2 blocks (supposedly satisfiable).
645		*
646		* That is compute their type intersection and if defined, then build
647		* the block as the union of the 2 blocks, typed with their type
648		* intersection.
649		*/
650		TypedBlock join(const TypedBlock& lhs, const TypedBlock& rhs) const;
651
652		/**
653		* Unify all terms that are not in the intersection of block and
654		* each block of common_blocks.
655		*/
656		SolutionSet subunify(const TypedBlockSeq& common_blocks,
657		const TypedBlock& block) const;
658
659		/**
660		* Unify all terms that are not in the intersection of blocks lhs
661		* and rhs.
662		*/
663		SolutionSet subunify(const TypedBlock& lhs, const TypedBlock& rhs) const;
664
665		/**
666		* Return true if a unification block is satisfiable. A unification
667		* block is not satisfiable if it's type is undefined (bottom).
668		*/
669		bool is_satisfiable(const TypedBlock& block) const;
670
671		/**
672		* Calculate type intersection.
673		*
674		* What we would like:
675		* ==================
676		*
677		* For example: say you have for a block
678		* with
679		*
680		* X
681		* ListLink(Y)
682		* ListLink(Z)
683		*
684		* meaning that X is equal to ListLink Y which is equal to ListLink Z,
685		* each having the following types at that point (i.e. not having
686		* reached the fixed point yet)
687		*
688		* X:Atom
689		* ListLink(Y):ListLink(Atom)
690		* ListLink(Z):ListLink(Atom)
691		*
692		* then their type intersection will be
693		*
694		* ListLink(Atom)
695		*
696		* which is supposed to represent the set of all potential groundings
697		* that may satisfy that block.
698		*
699		* What we have:
700		* ============
701		*
702		* The type is represented by the term itself. For instance, to
703		* take the example above, the terms and their types are
704		*
705		* X:X
706		* ListLink(Y):ListLink(Y)
707		* ListLink(Z):ListLink(Z)
708		*
709		* and their intersection is the most restricted one, for that one
710		* looks at the type declarations of X, Y and Z. So assuming that
711		* Y has type Node and Z has type ConceptNode, then Z is most
712		* resticted, so the result of their intersection will be
713		*
714		* ListLink(Z)
715		*
716		* In case the intersection is empty, then Handle::UNDEFINED is
717		* returned.
718		*
719		* A contextual handle is returned to keep track of scoped
720		* variable, which are essentially considered as constant.
721		*/
722		public:
723		CHandle type_intersection(const CHandle& lch, const CHandle& rch) const;
724		private:
725
726		/**
727		* Return a simplification of a type union, by eliminating all types
728		* that are redundant. For instance
729		*
730		* {Node, ConceptNode, ListLink}
731		*
732		* would return
733		*
734		* {Node, ListLink}
735		*
736		* As ConceptNode inherits Node.
737		*/
738		TypeSet simplify_type_union(TypeSet& type) const;
739
740		/**
741		* Return the union type of a variable. If the variable
742		* declaration is empty (Handle::UNDEFINED) then the union type is
743		* not empty, instead it contains the singleton {ATOM}. An empty
744		* union type would instead mean the bottom type (that nothing can
745		* inherit).
746		*/
747		TypeSet get_union_type(const Handle& h) const;
748
749		/**
750		* Return true if lhs inherit rhs. If lhs is not a variable then it
751		* relays that to VariableList::is_type, otherwise their type
752		* declarations are compared.
753		*/
754		bool inherit(const CHandle& lhs, const CHandle& rhs) const;
755		bool inherit(const Handle& lhs, const Handle& rhs,
756		Context lc=Context(), Context rc=Context()) const;
757
758		/**
759		* Return true if lhs inherits rhs.
760		*/
761		bool inherit(Type lhs, Type rhs) const;
762
763		/**
764		* Return true if a type inherits a type union.
765		*/
766		bool inherit(Type lhs, const TypeSet& rhs) const;
767
768		/**
769		* Return true if lhs inherits rhs. That is if all elements of lhs
770		* inherits rhs.
771		*/
772		bool inherit(const TypeSet& lhs, const TypeSet& rhs) const;
773
774		/**
775		* Return true if lgm is in rgm.
776		*/
777		bool inherit(const std::pair<double, double> &lgm,
778		const std::pair<double, double> &rgm) const;
779
780		/**
781		* Return true iff h (or ch) is a variable that is declared in
782		* _variables.
783		*/
784		bool is_declared_variable(const Handle& h) const;
785		bool is_declared_variable(const CHandle& ch) const;
786
787		/**
788		* Return true iff the given CHandle is a free variable and is
789		* declared in _variables
790		*/
791		bool is_free_declared_variable(const CHandle& ch) const;
792		bool is_free_declared_variable(const Context& c, const Handle& h) const;
793
794		/**
795		* Return true iff both nodes are satisfiable, which would be the
796		* case if both are equal constants (either actual constants or
797		* undeclared variables), or alpha-equivalent.
798		*/
799		bool is_node_satisfiable(const CHandle& lch, const CHandle& rch) const;
800
801		/**
802		* Return the attractive fixpoint of a unary function and its
803		* argument, if it exists. If no attractive fixpoint exists then it
804		* may never return.
805		*
806		* For the definition of fixpoint see
807		*
808		* https://en.wikipedia.org/wiki/Fixed_point_(mathematics)
809		*/
810		template<typename F, typename A>
811		static A fixpoint(const F& fun, const A& arg)
812		{
813		A res = fun(arg);
814		if (res == arg)
815		return res;
816		return fixpoint(fun, res);
817		}
818
819		HandleSeq tail(const HandleSeq &seq) const;
820
821		HandleSeq tail(const HandleSeq &seq, const size_t offset) const;
822
823		/**
824		* Unify lhs and rhs where at least lhs contains a glob.
825		*
826		* For every possible allowed interval of the glob in lhs
827		* three operations will be undergone:
828		*
829		* 1/ pick that many elements from rhs and unify with glob as head_sol.
830		* Example: lhs = X[2, 3]Y[0, inf], rhs = ABC
831		* 2 is the first allowed interval for X
832		* head_sol = unify(X, AB) = {{X, List(A, B)}, List(A, B)}
833		*
834		* 2/ remove glob from lhs and unified atoms from rhs. Then recurse over
835		* the the remaining as tail_sol.
836		* Example: ordered_unify(Y[0, inf], C)
837		*
838		* 3/ join the head_sol and tail_sol into a complite solution and insert
839		* it tosolutions.
840		*/
841		void ordered_unify_glob(const HandleSeq &lhs, const HandleSeq &rhs,
842		SolutionSet &sol,
843		Context lhs_context=Context(),
844		Context rhs_context=Context(),
845		bool flip=false) const;
846		};
847
848		bool unifiable(const Handle& lhs, const Handle& rhs,
849		const Handle& lhs_vardecl=Handle::UNDEFINED,
850		const Handle& rhs_vardecl=Handle::UNDEFINED);
851
852		/**
853		* Till content equality between atoms become the default.
854		*/
855		bool hm_content_eq(const HandleMap& lhs, const HandleMap& rhs);
856		bool hchm_content_eq(const Unify::HandleCHandleMap& lhs,
857		const Unify::HandleCHandleMap& rhs);
858		bool ts_content_eq(const Unify::TypedSubstitution& lhs,
859		const Unify::TypedSubstitution& rhs);
860		bool tss_content_eq(const Unify::TypedSubstitutions& lhs,
861		const Unify::TypedSubstitutions& rhs);
862
863		/**
864		* Strip the context from hchm. Add quotation links when necessary.
865		*/
866		HandleMap strip_context(const Unify::HandleCHandleMap& hchm);
867
868		/**
869		* Merge two vardecls into one. If a variable is present in both
870		* vardecls then the more restrictive one replaces the less
871		* restrictive one.
872		*
873		* TODO: give example.
874		*/
875		Variables merge_variables(const Variables& lv, const Variables& rv);
876		Handle merge_vardecl(const Handle& l_vardecl, const Handle& r_vardecl);
877
878		// Debugging helpers see
879		// http://wiki.opencog.org/w/Development_standards#Print_OpenCog_Objects
880		// The reason indent is not an optional argument with default is
881		// because gdb doesn't support that, see
882		// http://stackoverflow.com/questions/16734783 for more explanation.
883		std::string oc_to_string(const Unify::CHandle& ch,
884		const std::string& indent=empty_string);
885		std::string oc_to_string(const Unify::Block& pb,
886		const std::string& indent=empty_string);
887		std::string oc_to_string(const Unify::Partition& hshm,
888		const std::string& indent=empty_string);
889		std::string oc_to_string(const Unify::TypedBlock& tb,
890		const std::string& indent=empty_string);
891		std::string oc_to_string(const Unify::TypedBlockSeq& tbs,
892		const std::string& indent=empty_string);
893		std::string oc_to_string(const Unify::Partitions& par,
894		const std::string& indent=empty_string);
895		std::string oc_to_string(const Unify::HandleCHandleMap& hchm,
896		const std::string& indent=empty_string);
897		std::string oc_to_string(const Unify::HandleCHandleMap::value_type& hch,
898		const std::string& indent=empty_string);
899		std::string oc_to_string(const Unify::TypedSubstitution& ts,
900		const std::string& indent=empty_string);
901		std::string oc_to_string(const Unify::TypedSubstitutions::value_type& ts,
902		const std::string& indent=empty_string);
903		std::string oc_to_string(const Unify::TypedSubstitutions& tss,
904		const std::string& indent=empty_string);
905
906		} // namespace opencog
907
908		#endif // _OPENCOG_UNIFY_UTILS_H

tests/CMakeLists.txt +0 -4

…	…	@@ -8,12 +8,8 @@ ADD_DEFINITIONS(-DPROJECT_SOURCE_DIR="${CMAKE_SOURCE_DIR}"
8	8	# file is specific to the test (this variable is used by ADD_CXXTEST)
9	9	SET(GUILE_LOAD_PATH "${PROJECT_BINARY_DIR}/opencog/scm")
10	10
11		# Perform tests in component-dependency order, as much as possible.
12		# For example, since most things depends on the atomspace,
13		# its is tested first.
14	11	IF (CXXTEST_FOUND)
15	12
16		ADD_SUBDIRECTORY (unify)
17	13	ADD_SUBDIRECTORY (ure)
18	14
19	15	IF (HAVE_CYTHON AND HAVE_NOSETESTS)

tests/unify/CMakeLists.txt +0 -11

…	…	@@ -1,11 +0,0 @@
1		LINK_LIBRARIES(
2		unify
3		atomspace
4		clearbox
5		)
6		IF (HAVE_GUILE)
7		LINK_LIBRARIES(smob)
8		ENDIF (HAVE_GUILE)
9
10		ADD_CXXTEST(UnifyUTest)
11		ADD_CXXTEST(UnifyGlobUTest)

tests/unify/UnifyGlobUTest.cxxtest +0 -662

…	…	@@ -1,662 +0,0 @@
1		/**
2		* tests/unify/UnifyGlobUTest.cxxtest
3		*
4		* Copyright (C) 2019 OpenCog Foundation
5		* All Rights Reserved
6		* Author: Kasim Ebrahim
7		*
8		* This program is free software; you can redistribute it and/or modify
9		* it under the terms of the GNU Affero General Public License v3 as
10		* published by the Free Software Foundation and including the exceptions
11		* at http://opencog.org/wiki/Licenses
12		*
13		* This program is distributed in the hope that it will be useful,
14		* but WITHOUT ANY WARRANTY; without even the implied warranty of
15		* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
16		* GNU General Public License for more details.
17		*
18		* You should have received a copy of the GNU Affero General Public License
19		* along with this program; if not, write to:
20		* Free Software Foundation, Inc.,
21		* 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
22		*/
23
24		#include <opencog/util/Logger.h>
25
26		#include <opencog/atoms/core/Context.h>
27		#include <opencog/unify/Unify.h>
28		#include <opencog/atomspace/AtomSpace.h>
29		#include <opencog/guile/SchemeEval.h>
30
31		#include <cxxtest/TestSuite.h>
32
33		using namespace opencog;
34
35		#define al _asp->add_link
36		#define an _asp->add_node
37
38		class UnifyGlobUTest : public CxxTest::TestSuite
39		{
40		private:
41		AtomSpacePtr _asp = createAtomSpace();
42		SchemeEval _eval;
43		// Note: GlobNodes are in uppercase and
44		// variables are in lower case.
45		Handle X, Y, Z, U, x, y, XY, XYZ, A, B, C, AB, ABC, ABx, YBC,
46		P, Q, R, ABCXR, YCPQR, XYA, PQRU;
47		Context::VariablesStack X_varstack;
48
49		public:
50		UnifyGlobUTest() : _eval(_asp)
51		{
52		logger().set_level(Logger::DEBUG);
53		logger().set_print_to_stdout_flag(true);
54		logger().set_timestamp_flag(false);
55
56		X = an(GLOB_NODE, "$X");
57		Y = an(GLOB_NODE, "$Y");
58		Z = an(GLOB_NODE, "$Z");
59		U = an(GLOB_NODE, "$U");
60
61		x = an(VARIABLE_NODE, "$x");
62		y = an(VARIABLE_NODE, "$y");
63
64		XY = al(LIST_LINK, X, Y);
65		XYZ = al(LIST_LINK, X, Y, Z);
66
67		A = an(CONCEPT_NODE, "A");
68		B = an(CONCEPT_NODE, "B");
69		C = an(CONCEPT_NODE, "C");
70
71		P = an(PREDICATE_NODE, "P");
72		Q = an(PREDICATE_NODE, "Q");
73		R = an(PREDICATE_NODE, "R");
74
75		AB = al(LIST_LINK, A, B);
76		ABC = al(LIST_LINK, A, B, C);
77		ABx = al(LIST_LINK, A, B, x);
78		YBC = al(LIST_LINK, Y, B, C);
79
80		ABCXR = al(LIST_LINK, A, B, C, X, R);
81		YCPQR = al(LIST_LINK, Y, C, P, Q, R);
82		XYA = al(LIST_LINK, X, Y, A);
83		PQRU = al(LIST_LINK, P, Q, R, U);
84		}
85
86		void setUp();
87
88		void test_type_intersection_1();
89		void test_type_intersection_2();
90		void test_type_intersection_3();
91		void test_type_intersection_4();
92		void test_type_intersection_5();
93
94		void test_unify_basic_1();
95		void test_unify_basic_2();
96		void test_unify_basic_3();
97		void test_unify_basic_4();
98		void test_unify_basic_5();
99
100		void test_unify_multi_val_1();
101		void test_unify_multi_val_2();
102		void test_unify_multi_val_3();
103		void test_unify_multi_val_4();
104
105		void test_unify_typed_1();
106		void test_unify_typed_2();
107		void test_unify_typed_3();
108		void test_unify_typed_4();
109		void test_unify_typed_5();
110		void test_unify_typed_6();
111		};
112
113		void UnifyGlobUTest::setUp(void)
114		{
115		}
116
117		void UnifyGlobUTest::test_type_intersection_1()
118		{
119		logger().info("BEGIN TEST: %s", __FUNCTION__);
120
121		Handle lhs = X;
122		Handle rhs = x;
123		Unify unify(lhs, rhs);
124		Unify::CHandle result = unify.type_intersection(lhs, rhs),
125		expected = rhs;
126
127		TS_ASSERT_EQUALS(result, expected)
128
129		logger().info("END TEST: %s", __FUNCTION__);
130		}
131
132		void UnifyGlobUTest::test_type_intersection_2()
133		{
134		logger().info("BEGIN TEST: %s", __FUNCTION__);
135
136		Handle lhs = X;
137		Handle rhs = Y;
138
139		Handle l_decl = al(TYPED_VARIABLE_LINK,
140		X,
141		al(TYPE_INTERSECTION_LINK,
142		al(INTERVAL_LINK,
143		an(NUMBER_NODE, "1"),
144		an(NUMBER_NODE, "4")),
145		an(TYPE_NODE, "PredicateNode")));
146
147		Handle r_decl = al(TYPED_VARIABLE_LINK,
148		Y,
149		al(TYPE_INTERSECTION_LINK,
150		al(INTERVAL_LINK,
151		an(NUMBER_NODE, "2"),
152		an(NUMBER_NODE, "3")),
153		an(TYPE_NODE, "PredicateNode")));
154
155		Unify unify(lhs, rhs, l_decl, r_decl);
156		Unify::CHandle result = unify.type_intersection(lhs, rhs),
157		expected = rhs;
158
159		TS_ASSERT_EQUALS(result, expected)
160
161		logger().info("END TEST: %s", __FUNCTION__);
162		}
163
164		void UnifyGlobUTest::test_type_intersection_3()
165		{
166		logger().info("BEGIN TEST: %s", __FUNCTION__);
167
168		Handle lhs = X;
169		Handle rhs = AB;
170
171		Handle l_decl = al(VARIABLE_LIST,
172		al(TYPED_VARIABLE_LINK,
173		X,
174		al(TYPE_INTERSECTION_LINK,
175		al(INTERVAL_LINK,
176		an(NUMBER_NODE, "1"),
177		an(NUMBER_NODE, "2")),
178		an(TYPE_NODE, "ConceptNode"))));
179
180		Unify unify(lhs, rhs, l_decl);
181		Unify::CHandle result = unify.type_intersection(lhs, rhs),
182		expected = rhs;
183
184		TS_ASSERT_EQUALS(result, expected)
185
186		logger().info("END TEST: %s", __FUNCTION__);
187		}
188
189		void UnifyGlobUTest::test_type_intersection_4()
190		{
191		logger().info("BEGIN TEST: %s", __FUNCTION__);
192
193		Handle lhs = X;
194		Handle rhs = AB;
195
196		Handle l_decl = al(VARIABLE_LIST,
197		al(TYPED_VARIABLE_LINK,
198		X,
199		al(TYPE_INTERSECTION_LINK,
200		al(INTERVAL_LINK,
201		an(NUMBER_NODE, "1"),
202		an(NUMBER_NODE, "1")),
203		an(TYPE_NODE, "ConceptNode"))));
204
205		Unify unify(lhs, rhs, l_decl);
206		Unify::CHandle result = unify.type_intersection(lhs, rhs),
207		expected = Unify::CHandle(Handle::UNDEFINED);
208
209		TS_ASSERT_EQUALS(result, expected)
210
211		logger().info("END TEST: %s", __FUNCTION__);
212		}
213
214		void UnifyGlobUTest::test_type_intersection_5()
215		{
216		logger().info("BEGIN TEST: %s", __FUNCTION__);
217
218		Handle lhs = X;
219		Handle rhs = AB;
220
221		Handle l_decl = al(VARIABLE_LIST,
222		al(TYPED_VARIABLE_LINK,
223		X,
224		al(TYPE_INTERSECTION_LINK,
225		al(INTERVAL_LINK,
226		an(NUMBER_NODE, "1"),
227		an(NUMBER_NODE, "2")),
228		an(TYPE_NODE, "ConceptNode"))));
229
230		Unify unify(lhs, rhs, l_decl);
231		Unify::CHandle result = unify.type_intersection(lhs, rhs),
232		expected = rhs;
233
234		TS_ASSERT_EQUALS(result, expected)
235
236		logger().info("END TEST: %s", __FUNCTION__);
237		}
238
239		void UnifyGlobUTest::test_unify_basic_1()
240		{
241		logger().info("BEGIN TEST: %s", __FUNCTION__);
242
243		Unify unify(X, A);
244		Unify::SolutionSet result = unify();
245		Unify::SolutionSet expected =
246		Unify::SolutionSet({{{{X, A}, A}}});
247
248		std::cout << "result = " << oc_to_string(result) << std::endl;
249		std::cout << "expected = " << oc_to_string(expected) << std::endl;
250
251		TS_ASSERT_EQUALS(result, expected)
252
253		logger().info("END TEST: %s", __FUNCTION__);
254		}
255
256		void UnifyGlobUTest::test_unify_basic_2()
257		{
258		logger().info("BEGIN TEST: %s", __FUNCTION__);
259
260		Unify unify(X, Y);
261		Unify::SolutionSet result = unify();
262
263		// Note: The second element in a TypedBlock contains the most
264		// specialized term. Yet at this instance neither[X nor Y] is more
265		// specialized than the other.
266		// The most specialized term is used to designate the type, meaning
267		// for variables 'X' and 'Y' {{X, Y}, Y} and {{X, Y}, X} are considered
268		// the same and wont be considered as two partitions of a solutionset.
269		Unify::SolutionSet expected_1 =
270		Unify::SolutionSet({{{{X, Y}, Y}}});
271		Unify::SolutionSet expected_2 =
272		Unify::SolutionSet({{{{X, Y}, X}}});
273
274		std::cout << "result = " << oc_to_string(result) << std::endl;
275		std::cout << "expected_1 = " << oc_to_string(expected_1) << std::endl;
276		std::cout << "expected_2 = " << oc_to_string(expected_2) << std::endl;
277
278		TS_ASSERT((result==expected_1) or (result==expected_2))
279
280		logger().info("END TEST: %s", __FUNCTION__);
281		}
282
283		void UnifyGlobUTest::test_unify_basic_3()
284		{
285		logger().info("BEGIN TEST: %s", __FUNCTION__);
286
287		Unify unify(X, x);
288		Unify::SolutionSet result = unify();
289
290		// Note: For two type undeclared Glob 'X' and Variable 'x', the
291		// variable x is considered more specialized than the GlobNode.
292		Unify::SolutionSet expected =
293		Unify::SolutionSet({{{{X, x}, x}}});
294
295		std::cout << "result = " << oc_to_string(result) << std::endl;
296		std::cout << "expected = " << oc_to_string(expected) << std::endl;
297
298		TS_ASSERT_EQUALS(result, expected)
299
300		logger().info("END TEST: %s", __FUNCTION__);
301		}
302
303		void UnifyGlobUTest::test_unify_basic_4()
304		{
305		logger().info("BEGIN TEST: %s", __FUNCTION__);
306
307		Unify unify(x, X);
308		Unify::SolutionSet result = unify();
309
310		// Note: For two type undeclared Glob 'X' and Variable 'x', the
311		// variable x is considered more specialized than the GlobNode.
312		Unify::SolutionSet expected =
313		Unify::SolutionSet({{{{X, x}, x}}});
314
315		std::cout << "result = " << oc_to_string(result) << std::endl;
316		std::cout << "expected = " << oc_to_string(expected) << std::endl;
317
318		TS_ASSERT_EQUALS(result, expected)
319
320		logger().info("END TEST: %s", __FUNCTION__);
321		}
322
323		void UnifyGlobUTest::test_unify_basic_5()
324		{
325		logger().info("BEGIN TEST: %s", __FUNCTION__);
326
327		Unify unify(X, AB);
328		Unify::SolutionSet result = unify();
329
330		Unify::SolutionSet expected =
331		Unify::SolutionSet({{{{X, al(LIST_LINK, A, B)}, al(LIST_LINK, A, B)}}});
332
333		std::cout << "result = " << oc_to_string(result) << std::endl;
334		std::cout << "expected = " << oc_to_string(expected) << std::endl;
335
336		TS_ASSERT_EQUALS(result, expected)
337
338		logger().info("END TEST: %s", __FUNCTION__);
339		}
340
341		void UnifyGlobUTest::test_unify_multi_val_1()
342		{
343		logger().info("BEGIN TEST: %s", __FUNCTION__);
344
345		Unify unify(XY, ABC);
346		Unify::SolutionSet result = unify();
347
348		Unify::SolutionSet expected =
349		Unify::SolutionSet(
350		{{{{X, A}, A},
351		{{Y, al(LIST_LINK, HandleSeq{B, C})}, al(LIST_LINK, HandleSeq{B, C})}},
352		{{{X, al(LIST_LINK, HandleSeq{A, B})}, al(LIST_LINK, HandleSeq{A, B})},
353		{{Y, C}, C}}});
354
355		std::cout << "result = " << oc_to_string(result) << std::endl;
356		std::cout << "expected = " << oc_to_string(expected) << std::endl;
357
358		TS_ASSERT_EQUALS(result, expected)
359
360		logger().info("END TEST: %s", __FUNCTION__);
361		}
362
363		void UnifyGlobUTest::test_unify_multi_val_2()
364		{
365		logger().info("BEGIN TEST: %s", __FUNCTION__);
366
367		Unify unify(al(LIST_LINK, U), al(LIST_LINK, U));
368		Unify::SolutionSet result = unify();
369		std::cout << "\n result\n" << oc_to_string(result) << std::endl;
370
371		Unify::SolutionSet expected = Unify::SolutionSet(true);
372		std::cout << "\n expected\n" << oc_to_string(expected) << std::endl;
373
374		TS_ASSERT_EQUALS(result, expected)
375
376		logger().info("END TEST: %s", __FUNCTION__);
377		}
378
379		void UnifyGlobUTest::test_unify_multi_val_3()
380		{
381		logger().info("BEGIN TEST: %s", __FUNCTION__);
382
383		Unify unify(XYZ, al(LIST_LINK, U));
384		Unify::SolutionSet result = unify();
385		std::cout << "\n result\n" << oc_to_string(result) << std::endl;
386
387		Unify::SolutionSet expected =
388		Unify::SolutionSet(
389		{{{{U, al(LIST_LINK, {X, Y, Z})}, al(LIST_LINK, {X, Y, Z})}}});
390		std::cout << "\n expected\n" << oc_to_string(expected) << std::endl;
391
392		TS_ASSERT_EQUALS(result, expected);
393
394		logger().info("END TEST: %s", __FUNCTION__);
395		}
396
397		void UnifyGlobUTest::test_unify_multi_val_4()
398		{
399		logger().info("BEGIN TEST: %s", __FUNCTION__);
400
401		Unify unify(ABx, YBC);
402		Unify::SolutionSet result = unify();
403		std::cout << "\n result\n" << oc_to_string(result) << std::endl;
404
405		Unify::SolutionSet expected =
406		Unify::SolutionSet({{{{Y, A}, A}, {{x, C}, C}}});
407		std::cout << "\n expected\n" << oc_to_string(expected) << std::endl;
408
409		TS_ASSERT_EQUALS(result, expected)
410
411		logger().info("END TEST: %s", __FUNCTION__);
412		}
413
414		void UnifyGlobUTest::test_unify_typed_1()
415		{
416		logger().info("BEGIN TEST: %s", __FUNCTION__);
417
418		Handle l_decl = al(TYPED_VARIABLE_LINK,
419		Y,
420		an(TYPE_NODE, "ConceptNode"));
421
422		Unify unify(X, A, l_decl);
423		Unify::SolutionSet result = unify();
424		std::cout<< "\n result\n" << oc_to_string(result) <<std::endl;
425
426		// If X is not in the var declaration it is
427		// treated as a constant term.
428		Unify::SolutionSet expected(false);
429		std::cout<< "\n expected\n" << oc_to_string(expected) <<std::endl;
430
431		TS_ASSERT_EQUALS(result, expected)
432
433		logger().info("END TEST: %s", __FUNCTION__);
434		}
435
436		void UnifyGlobUTest::test_unify_typed_2()
437		{
438		logger().info("BEGIN TEST: %s", __FUNCTION__);
439
440		Handle l_decl = al(TYPED_VARIABLE_LINK,
441		X,
442		an(TYPE_NODE, "PredicateNode"));
443
444		Handle r_decl = al(TYPED_VARIABLE_LINK,
445		Y,
446		an(TYPE_NODE, "ConceptNode"));
447
448		Unify unify(ABCXR, YCPQR, l_decl, r_decl);
449		Unify::SolutionSet result = unify();
450		std::cout<< "\n result\n" << oc_to_string(result) <<std::endl;
451
452		Unify::SolutionSet expected({{{{Y, al(LIST_LINK, {A, B})}, al(LIST_LINK, {A, B})},
453		{{X, al(LIST_LINK, {P, Q})}, al(LIST_LINK, {P, Q})}}});
454		std::cout<< "\n expected\n" << oc_to_string(expected) <<std::endl;
455
456		TS_ASSERT_EQUALS(result, expected)
457
458		logger().info("END TEST: %s", __FUNCTION__);
459		}
460
461		void UnifyGlobUTest::test_unify_typed_3()
462		{
463		logger().info("BEGIN TEST: %s", __FUNCTION__);
464
465		Handle l_decl = al(TYPED_VARIABLE_LINK,
466		U,
467		al(TYPE_INTERSECTION_LINK,
468		al(INTERVAL_LINK,
469		an(NUMBER_NODE, "0"),
470		an(NUMBER_NODE, "2")),
471		an(TYPE_NODE, "GlobNode")));
472		Handle r_decl = al(VARIABLE_LIST,
473		al(TYPED_VARIABLE_LINK,
474		X,
475		al(TYPE_INTERSECTION_LINK,
476		al(INTERVAL_LINK,
477		an(NUMBER_NODE, "1"),
478		an(NUMBER_NODE, "1")),
479		an(TYPE_NODE, "GlobNode"))),
480		al(TYPED_VARIABLE_LINK,
481		Y,
482		al(TYPE_INTERSECTION_LINK,
483		al(INTERVAL_LINK,
484		an(NUMBER_NODE, "0"),
485		an(NUMBER_NODE, "+inf")),
486		an(TYPE_NODE, "GlobNode"))),
487		al(TYPED_VARIABLE_LINK,
488		Z,
489		al(TYPE_INTERSECTION_LINK,
490		al(INTERVAL_LINK,
491		an(NUMBER_NODE, "0"),
492		an(NUMBER_NODE, "+inf")),
493		an(TYPE_NODE, "GlobNode"))));
494
495		Unify unify(al(LIST_LINK, U), XYZ, l_decl, r_decl);
496		Unify::SolutionSet result = unify();
497		std::cout << "\n result\n" << oc_to_string(result) << std::endl;
498
499		Unify::SolutionSet expected =
500		Unify::SolutionSet(
501		{{{{U, al(LIST_LINK, {X, Y})}, al(LIST_LINK, {X, Y})},
502		{{Z, al(LIST_LINK, HandleSeq{})}, al(LIST_LINK, HandleSeq{})}},
503		{{{U, X}, X},
504		{{Y, Z, al(LIST_LINK, HandleSeq{})}, al(LIST_LINK, HandleSeq{})}}});
505		std::cout << "\n expected\n" << oc_to_string(expected) << std::endl;
506
507		TS_ASSERT_EQUALS(result, expected)
508
509		logger().info("END TEST: %s", __FUNCTION__);
510		}
511
512		void UnifyGlobUTest::test_unify_typed_4()
513		{
514		logger().info("BEGIN TEST: %s", __FUNCTION__);
515
516		Handle l_decl = al(TYPED_VARIABLE_LINK,
517		U,
518		al(TYPE_INTERSECTION_LINK,
519		al(INTERVAL_LINK,
520		an(NUMBER_NODE, "0"),
521		an(NUMBER_NODE, "inf")),
522		an(TYPE_NODE, "GlobNode")));
523		Handle r_decl = al(VARIABLE_LIST,
524		al(TYPED_VARIABLE_LINK,
525		X,
526		al(TYPE_INTERSECTION_LINK,
527		al(INTERVAL_LINK,
528		an(NUMBER_NODE, "0"),
529		an(NUMBER_NODE, "+inf")),
530		an(TYPE_NODE, "GlobNode"))),
531		al(TYPED_VARIABLE_LINK,
532		Y,
533		al(TYPE_INTERSECTION_LINK,
534		al(INTERVAL_LINK,
535		an(NUMBER_NODE, "0"),
536		an(NUMBER_NODE, "+inf")),
537		an(TYPE_NODE, "GlobNode"))),
538		al(TYPED_VARIABLE_LINK,
539		Z,
540		al(TYPE_INTERSECTION_LINK,
541		al(INTERVAL_LINK,
542		an(NUMBER_NODE, "0"),
543		an(NUMBER_NODE, "+inf")),
544		an(TYPE_NODE, "GlobNode"))));
545
546		Unify unify(al(LIST_LINK, U), XYZ, l_decl, r_decl);
547		Unify::SolutionSet result = unify();
548
549		std::cout << "\n result\n" << oc_to_string(result) << std::endl;
550		Unify::SolutionSet expected =
551		Unify::SolutionSet(
552		{{{{U, al(LIST_LINK, {Y, Z})}, al(LIST_LINK, {Y, Z})},
553		{{X, al(LIST_LINK, HandleSeq{})}, al(LIST_LINK, HandleSeq{})}},
554		{{{U, al(LIST_LINK, {X, Y})}, al(LIST_LINK, {X, Y})},
555		{{Z, al(LIST_LINK, HandleSeq{})}, al(LIST_LINK, HandleSeq{})}},
556		{{{U, X}, U},
557		{{Y, Z, al(LIST_LINK, HandleSeq{})}, al(LIST_LINK, HandleSeq{})}},
558		{{{U, Z}, U},
559		{{Y, X, al(LIST_LINK, HandleSeq{})}, al(LIST_LINK, HandleSeq{})}},
560		{{{U, Y}, U},
561		{{Z, X, al(LIST_LINK, HandleSeq{})}, al(LIST_LINK, HandleSeq{})}},
562		{{{U, al(LIST_LINK, {X, Y, Z})}, al(LIST_LINK, {X, Y, Z})}},
563		{{{U, X, Y, Z, al(LIST_LINK, HandleSeq{})}, al(LIST_LINK, HandleSeq{})}}});
564		std::cout << "\n expected\n" << oc_to_string(expected) << std::endl;
565
566		TS_ASSERT_EQUALS(result, expected)
567
568		logger().info("END TEST: %s", __FUNCTION__);
569		}
570
571		void UnifyGlobUTest::test_unify_typed_5()
572		{
573		logger().info("BEGIN TEST: %s", __FUNCTION__);
574
575		Handle l_decl = al(TYPED_VARIABLE_LINK,
576		U,
577		al(TYPE_INTERSECTION_LINK,
578		al(INTERVAL_LINK,
579		an(NUMBER_NODE, "2"),
580		an(NUMBER_NODE, "inf")),
581		an(TYPE_NODE, "GlobNode")));
582		Handle r_decl = al(VARIABLE_LIST,
583		al(TYPED_VARIABLE_LINK,
584		X,
585		al(TYPE_INTERSECTION_LINK,
586		al(INTERVAL_LINK,
587		an(NUMBER_NODE, "0"),
588		an(NUMBER_NODE, "+inf")),
589		an(TYPE_NODE, "GlobNode"))),
590		al(TYPED_VARIABLE_LINK,
591		Y,
592		al(TYPE_INTERSECTION_LINK,
593		al(INTERVAL_LINK,
594		an(NUMBER_NODE, "2"),
595		an(NUMBER_NODE, "+inf")),
596		an(TYPE_NODE, "GlobNode"))),
597		al(TYPED_VARIABLE_LINK,
598		Z,
599		al(TYPE_INTERSECTION_LINK,
600		al(INTERVAL_LINK,
601		an(NUMBER_NODE, "2"),
602		an(NUMBER_NODE, "+inf")),
603		an(TYPE_NODE, "GlobNode"))));
604
605		Unify unify(al(LIST_LINK, U), XYZ, l_decl, r_decl);
606		Unify::SolutionSet result = unify();
607
608		std::cout << "\n result\n" << oc_to_string(result) << std::endl;
609		Unify::SolutionSet expected =
610		Unify::SolutionSet(
611		{{{{U, al(LIST_LINK, {Y, Z})}, al(LIST_LINK, {Y, Z})},
612		{{X, al(LIST_LINK, HandleSeq{})}, al(LIST_LINK, HandleSeq{})}},
613		{{{U, al(LIST_LINK, {X, Y, Z})}, al(LIST_LINK, {X, Y, Z})}}});
614		std::cout << "\n expected\n" << oc_to_string(expected) << std::endl;
615
616		TS_ASSERT_EQUALS(result, expected)
617
618		logger().info("END TEST: %s", __FUNCTION__);
619		}
620
621		void UnifyGlobUTest::test_unify_typed_6()
622		{
623		logger().info("BEGIN TEST: %s", __FUNCTION__);
624
625		Handle l_decl = al(VARIABLE_LIST,
626		al(TYPED_VARIABLE_LINK,
627		X,
628		al(INTERVAL_LINK,
629		an(NUMBER_NODE, "2"),
630		an(NUMBER_NODE, "3"))),
631		al(TYPED_VARIABLE_LINK,
632		Y,
633		al(INTERVAL_LINK,
634		an(NUMBER_NODE, "0"),
635		an(NUMBER_NODE, "1"))));
636		Handle r_decl = al(TYPED_VARIABLE_LINK,
637		U,
638		al(INTERVAL_LINK,
639		an(NUMBER_NODE, "1"),
640		an(NUMBER_NODE, "1")));
641
642		Unify unify(XYA, PQRU, l_decl, r_decl);
643		Unify::SolutionSet result = unify();
644
645		std::cout << "\n result\n" << oc_to_string(result) << std::endl;
646		Unify::SolutionSet expected =
647		Unify::SolutionSet(
648		{{{{X, al(LIST_LINK, {P, Q})}, al(LIST_LINK, {P, Q})},
649		{{Y, R}, R},
650		{{U, A}, A}},
651		{{{X, al(LIST_LINK, {P, Q, R})}, al(LIST_LINK, {P, Q, R})},
652		{{Y, al(LIST_LINK, HandleSeq{})}, al(LIST_LINK, HandleSeq{})},
653		{{U, A}, A}}});
654		std::cout << "\n expected\n" << oc_to_string(expected) << std::endl;
655
656		TS_ASSERT_EQUALS(result, expected)
657
658		logger().info("END TEST: %s", __FUNCTION__);
659		}
660
661		#undef al
662		#undef an

tests/unify/UnifyUTest.cxxtest +0 -2794

…	…	@@ -1,2794 +0,0 @@
1		/**
2		* tests/unify/UnifyUTest.cxxtest
3		*
4		* Copyright (C) 2016 OpenCog Foundation
5		* All Rights Reserved
6		* Author: Nil Geisweiller
7		*
8		* This program is free software; you can redistribute it and/or modify
9		* it under the terms of the GNU Affero General Public License v3 as
10		* published by the Free Software Foundation and including the exceptions
11		* at http://opencog.org/wiki/Licenses
12		*
13		* This program is distributed in the hope that it will be useful,
14		* but WITHOUT ANY WARRANTY; without even the implied warranty of
15		* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
16		* GNU General Public License for more details.
17		*
18		* You should have received a copy of the GNU Affero General Public License
19		* along with this program; if not, write to:
20		* Free Software Foundation, Inc.,
21		* 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
22		*/
23
24		#include <opencog/util/Logger.h>
25
26		#include <opencog/atoms/core/Context.h>
27		#include <opencog/unify/Unify.h>
28		#include <opencog/atomspace/AtomSpace.h>
29		#include <opencog/guile/SchemeEval.h>
30
31		#include <cxxtest/TestSuite.h>
32
33		using namespace opencog;
34
35		#define al _as->add_link
36		#define an _as->add_node
37
38		class UnifyUTest : public CxxTest::TestSuite
39		{
40		private:
41		AtomSpacePtr _as;
42		SchemeEval _eval;
43		Handle X, Y, Z, W, V, A, B,
44		InhAB, InhXB, InhAY, InhXY, InhAZ, InhAW, InhAV,
45		AndAA, AndAB, AndAY, AndXB, AndXY,
46		AndAABB, AndXYAB, AndAAABBB, AndXXYYAB, AndAAAABBBB, AndXXXYYYAB,
47		AndAAAAABBBBB, AndXXXXYYYYAB,
48		CT, PT, IT, CPT,
49		X_vardecl, X_cyclic_vardecl, Y_vardecl, Z_vardecl, W_vardecl, V_vardecl,
50		XY_vardecl;
51		Context::VariablesStack X_varstack;
52
53		public:
54		UnifyUTest() : _as(createAtomSpace()), _eval(_as)
55		{
56		logger().set_level(Logger::INFO);
57		logger().set_print_to_stdout_flag(true);
58		logger().set_timestamp_flag(false);
59
60		X = an(VARIABLE_NODE, "$X");
61		Y = an(VARIABLE_NODE, "$Y");
62		Z = an(VARIABLE_NODE, "$Z");
63		W = an(VARIABLE_NODE, "$W");
64		V = an(VARIABLE_NODE, "$V");
65		A = an(CONCEPT_NODE, "A");
66		B = an(CONCEPT_NODE, "B");
67		InhAB = al(INHERITANCE_LINK, A, B);
68		InhXB = al(INHERITANCE_LINK, X, B);
69		InhAY = al(INHERITANCE_LINK, A, Y);
70		InhXY = al(INHERITANCE_LINK, X, Y);
71		InhAZ = al(INHERITANCE_LINK, A, Z);
72		InhAW = al(INHERITANCE_LINK, A, W);
73		InhAV = al(INHERITANCE_LINK, A, V);
74		AndAA = al(AND_LINK, A, A);
75		AndAB = al(AND_LINK, A, B);
76		AndAY = al(AND_LINK, A, Y);
77		AndXB = al(AND_LINK, X, B);
78		AndXY = al(AND_LINK, X, Y);
79		AndAABB = al(AND_LINK, {A, A, B, B});
80		AndXYAB = al(AND_LINK, {X, Y, A, B});
81		AndAAABBB = al(AND_LINK, {A, A, A, B, B, B});
82		AndXXYYAB = al(AND_LINK, {X, X, Y, Y, A, B});
83		AndAAAABBBB = al(AND_LINK, {A, A, A, A, B, B, B, B});
84		AndXXXYYYAB = al(AND_LINK, {X, X, X, Y, Y, Y, A, B});
85		AndAAAAABBBBB = al(AND_LINK, {A, A, A, A, A, B, B, B, B, B});
86		AndXXXXYYYYAB = al(AND_LINK, {X, X, X, X, Y, Y, Y, Y, A, B});
87		CT = an(TYPE_NODE, "ConceptNode");
88		PT = an(TYPE_NODE, "PredicateNode");
89		IT = an(TYPE_NODE, "InheritanceLink");
90		CPT = al(TYPE_CHOICE, CT, PT);
91		X_vardecl = al(TYPED_VARIABLE_LINK, X, CT);
92		X_cyclic_vardecl = al(TYPED_VARIABLE_LINK, X, IT);
93		Y_vardecl = al(TYPED_VARIABLE_LINK, Y, CT);
94		Z_vardecl = al(TYPED_VARIABLE_LINK, Z, CT);
95		W_vardecl = al(TYPED_VARIABLE_LINK, W, PT);
96		V_vardecl = al(TYPED_VARIABLE_LINK, V, CPT);
97		XY_vardecl = al(VARIABLE_LIST,
98		al(TYPED_VARIABLE_LINK, X, CT),
99		al(TYPED_VARIABLE_LINK, Y, CT));
100
101		Handle X_varlist = al(VARIABLE_LIST, X_vardecl);
102		Variables X_CT_variables(X_vardecl);
103		X_varstack.push_back(X_CT_variables);
104		}
105
106		void setUp();
107
108		// TODO: move elsewhere once the unification type routines are
109		// moved elsewhere
110		void test_type_intersection();
111
112		void test_join_1();
113		void test_join_2();
114		void test_join_3();
115
116		void test_unify_without_var_1();
117		void test_unify_without_var_2();
118
119		void test_unify_basic_1();
120		void test_unify_basic_2();
121		void test_unify_basic_3();
122		void test_unify_basic_4();
123		void test_unify_basic_5();
124		void test_unify_basic_6();
125		void test_unify_basic_7();
126		void test_unify_basic_8();
127
128		// Variable declaration
129		void test_unify_undeclared_var_1();
130		void test_unify_undeclared_var_2();
131		void test_unify_undeclared_var_3();
132		void test_unify_vardecl_1();
133		void test_unify_vardecl_2();
134		void test_unify_vardecl_3();
135		void test_unify_vardecl_4();
136		void test_unify_vardecl_5();
137
138		// Cyclic dependence
139		void test_unify_cyclic_dependence_1();
140		void test_unify_cyclic_dependence_2();
141		void test_unify_cyclic_dependence_3();
142		void test_unify_cyclic_dependence_4();
143
144		// Type union
145		// TODO: for that we need to support more powerful type
146		void xtest_unify_type_union_1();
147
148		// Unordered link
149		void test_unify_unordered_1();
150		void test_unify_unordered_2();
151		void test_unify_unordered_3();
152		void test_unify_unordered_4();
153		void test_unify_unordered_5();
154		void test_unify_unordered_6();
155		void test_unify_unordered_7();
156		void test_unify_unordered_8();
157
158		void test_unify_alpha_equivalence();
159
160		void test_substitute();
161
162		// Various complex unify queries
163		void test_unify_complex_1();
164		void test_unify_complex_2();
165		void test_unify_complex_3();
166		void test_unify_complex_4();
167		void test_unify_complex_5();
168		void test_unify_complex_6();
169		void test_unify_complex_7();
170		void test_unify_complex_8();
171		void test_unify_complex_9();
172		void test_unify_complex_10();
173		void test_unify_complex_11();
174		void test_unify_complex_12();
175		};
176
177		void UnifyUTest::setUp(void)
178		{
179		}
180
181		void UnifyUTest::test_type_intersection()
182		{
183		logger().info("BEGIN TEST: %s", __FUNCTION__);
184
185		Handle lhs =
186		_eval.eval_h("(QuoteLink"
187		" (LambdaLink"
188		" (UnquoteLink"
189		" (VariableNode \"$TyVs\"))"
190		" (UnquoteLink"
191		" (VariableNode \"$A1\"))))");
192		Handle rhs =
193		_eval.eval_h("(LambdaLink"
194		" (TypedVariableLink"
195		" (VariableNode \"$X\")"
196		" (TypeNode \"ConceptNode\"))"
197		" (EvaluationLink"
198		" (PredicateNode \"take\")"
199		" (ListLink"
200		" (VariableNode \"$X\")"
201		" (ConceptNode \"treatment-1\"))))");
202
203		Unify unify(lhs, rhs);
204		Unify::CHandle result = unify.type_intersection(lhs, rhs),
205		expected = rhs;
206
207		logger().debug() << "result = " << oc_to_string(result);
208		logger().debug() << "expected = " << oc_to_string(expected);
209
210		TS_ASSERT_EQUALS(result, expected);
211
212		logger().info("END TEST: %s", __FUNCTION__);
213		}
214
215		void UnifyUTest::test_join_1()
216		{
217		logger().info("BEGIN TEST: %s", __FUNCTION__);
218
219		Unify unify(A, B); // dummy unify construction to test join
220		Unify::Block pb1{X, A};
221		Unify::SolutionSet s1 = Unify::SolutionSet({{{pb1, A}}});
222		Unify::Block pb2{X, B};
223		Unify::SolutionSet s2 = Unify::SolutionSet({{{pb2, B}}}),
224		result = unify.join(s1, s2),
225		expected = Unify::SolutionSet(false);
226
227		logger().debug() << "result = " << oc_to_string(result);
228		logger().debug() << "expected = " << oc_to_string(expected);
229
230		TS_ASSERT_EQUALS(result, expected);
231
232		logger().info("END TEST: %s", __FUNCTION__);
233		}
234
235		void UnifyUTest::test_join_2()
236		{
237		logger().info("BEGIN TEST: %s", __FUNCTION__);
238
239		Handle P = _eval.eval_h("(VariableNode \"$P\")");
240		Handle TyVs = _eval.eval_h("(VariableNode \"$TyVs\")");
241		Handle A1 = _eval.eval_h("(VariableNode \"$A1\")");
242
243		Handle implicant =
244		_eval.eval_h("(LambdaLink"
245		" (TypedVariableLink"
246		" (VariableNode \"$X\")"
247		" (TypeNode \"ConceptNode\"))"
248		" (EvaluationLink"
249		" (PredicateNode \"take\")"
250		" (ListLink"
251		" (VariableNode \"$X\")"
252		" (ConceptNode \"treatment-1\"))))");
253
254		Handle quoted_implicant =
255		_eval.eval_h("(QuoteLink"
256		" (LambdaLink"
257		" (UnquoteLink"
258		" (VariableNode \"$TyVs\"))"
259		" (UnquoteLink"
260		" (VariableNode \"$A1\"))))");
261
262		Handle implicant_vardecl =
263		_eval.eval_h("(TypedVariableLink"
264		" (VariableNode \"$X\")"
265		" (TypeNode \"ConceptNode\"))");
266
267		Handle implicant_body =
268		_eval.eval_h("(EvaluationLink"
269		" (PredicateNode \"take\")"
270		" (ListLink"
271		" (VariableNode \"$X\")"
272		" (ConceptNode \"treatment-1\")))");
273
274		Context C(Quotation(), {X}, true, X_varstack);
275		logger().debug() << "C = " << oc_to_string(C);
276		Unify::CHandle Cimplicant_vardecl(implicant_vardecl, C),
277		Cimplicant_body(implicant_body, C);
278
279		Unify unify(P, quoted_implicant); // dummy unify construction to test join
280		Unify::Block pb1{P, implicant};
281		Unify::SolutionSet s1 = Unify::SolutionSet({{{pb1, implicant}}});
282		Unify::Block pb2{P, quoted_implicant};
283		Unify::SolutionSet s2 = Unify::SolutionSet({{{pb2, quoted_implicant}}});
284		Unify::SolutionSet result = unify.join(s1, s2);
285		Unify::Block pb1_expected{P, implicant, quoted_implicant};
286		Unify::Block pb2_expected{TyVs, Cimplicant_vardecl};
287		Unify::Block pb3_expected{A1, Cimplicant_body};
288		Unify::SolutionSet expected =
289		Unify::SolutionSet({{{pb1_expected, implicant},
290		{pb2_expected, Cimplicant_vardecl},
291		{pb3_expected, Cimplicant_body}}});
292
293		logger().debug() << "result = " << oc_to_string(result);
294		logger().debug() << "expected = " << oc_to_string(expected);
295
296		TS_ASSERT_EQUALS(result, expected);
297
298		logger().info("END TEST: %s", __FUNCTION__);
299		}
300
301		// Same as test_join_2 but using A2 as well. See test_complex_1
302		void UnifyUTest::test_join_3()
303		{
304		logger().info("BEGIN TEST: %s", __FUNCTION__);
305
306		Handle P = _eval.eval_h("(VariableNode \"$P\")");
307		Handle Q = _eval.eval_h("(VariableNode \"$Q\")");
308		Handle TyVs = _eval.eval_h("(VariableNode \"$TyVs\")");
309		Handle A1 = _eval.eval_h("(VariableNode \"$A1\")");
310		Handle A2 = _eval.eval_h("(VariableNode \"$A2\")");
311
312		Handle implicant =
313		_eval.eval_h("(LambdaLink"
314		" (TypedVariableLink"
315		" (VariableNode \"$X\")"
316		" (TypeNode \"ConceptNode\"))"
317		" (EvaluationLink"
318		" (PredicateNode \"take\")"
319		" (ListLink"
320		" (VariableNode \"$X\")"
321		" (ConceptNode \"treatment-1\"))))");
322
323		Handle quoted_LA1 =
324		_eval.eval_h("(QuoteLink"
325		" (LambdaLink"
326		" (UnquoteLink"
327		" (VariableNode \"$TyVs\"))"
328		" (UnquoteLink"
329		" (VariableNode \"$A1\"))))");
330
331		Handle quoted_LA2 =
332		_eval.eval_h("(QuoteLink"
333		" (LambdaLink"
334		" (UnquoteLink"
335		" (VariableNode \"$TyVs\"))"
336		" (UnquoteLink"
337		" (VariableNode \"$A2\"))))");
338
339		Handle implicant_vardecl =
340		_eval.eval_h("(TypedVariableLink"
341		" (VariableNode \"$X\")"
342		" (TypeNode \"ConceptNode\"))");
343
344		Handle implicant_body =
345		_eval.eval_h("(EvaluationLink"
346		" (PredicateNode \"take\")"
347		" (ListLink"
348		" (VariableNode \"$X\")"
349		" (ConceptNode \"treatment-1\")))");
350
351		Context C(Quotation(), {X}, true, X_varstack);
352		Unify::CHandle Cimplicant_vardecl(implicant_vardecl, C),
353		Cimplicant_body(implicant_body, C);
354
355		// dummy unify construction to test join
356		Unify unify(al(AND_LINK, P, Q), al(AND_LINK, quoted_LA1, quoted_LA2));
357
358		Unify::SolutionSet
359		s1 = Unify::SolutionSet({{{{P, implicant}, implicant}}}),
360		s2 = Unify::SolutionSet(
361		{{{{P, quoted_LA1}, quoted_LA1},
362		{{Q, quoted_LA2}, quoted_LA2}},
363		{{{Q, quoted_LA1}, quoted_LA1},
364		{{P, quoted_LA2}, quoted_LA2}}}),
365		result = unify.join(s1, s2),
366		expected = Unify::SolutionSet({{{{P, implicant, quoted_LA2},
367		implicant},
368		{{TyVs, Cimplicant_vardecl},
369		Cimplicant_vardecl},
370		{{A2, Cimplicant_body},
371		Cimplicant_body},
372		{{Q, quoted_LA1},
373		quoted_LA1}},
374		{{{P, implicant, quoted_LA1},
375		implicant},
376		{{TyVs, Cimplicant_vardecl},
377		Cimplicant_vardecl},
378		{{A1, Cimplicant_body},
379		Cimplicant_body},
380		{{Q, quoted_LA2},
381		quoted_LA2}}});
382
383		logger().debug() << "result = " << oc_to_string(result);
384		logger().debug() << "expected = " << oc_to_string(expected);
385
386		TS_ASSERT_EQUALS(result, expected);
387
388		logger().info("END TEST: %s", __FUNCTION__);
389		}
390
391		void UnifyUTest::test_unify_without_var_1()
392		{
393		logger().info("BEGIN TEST: %s", __FUNCTION__);
394
395		Unify unify(InhAB, A);
396		Unify::SolutionSet result = unify(),
397		expected(false);
398
399		logger().debug() << "result = " << oc_to_string(result);
400		logger().debug() << "expected = " << oc_to_string(expected);
401
402		TS_ASSERT_EQUALS(result, expected);
403
404		// On top of that make sure that the solution is empty as it is
405		// how failing is represented
406		TS_ASSERT(result.empty());
407
408		logger().info("END TEST: %s", __FUNCTION__);
409		}
410
411		void UnifyUTest::test_unify_without_var_2()
412		{
413		logger().info("BEGIN TEST: %s", __FUNCTION__);
414
415		Unify unify(InhAB, InhAB);
416		Unify::SolutionSet result = unify(),
417		expected(true);
418
419		logger().debug() << "result = " << oc_to_string(result);
420		logger().debug() << "expected = " << oc_to_string(expected);
421
422		TS_ASSERT_EQUALS(result, expected);
423
424		// On top of that make sure that the solution is not empty as it
425		// is how success is represented
426		TS_ASSERT(not result.empty());
427
428		logger().info("END TEST: %s", __FUNCTION__);
429		}
430
431		void UnifyUTest::test_unify_basic_1()
432		{
433		logger().info("BEGIN TEST: %s", __FUNCTION__);
434
435		Unify unify(X, A);
436		Unify::SolutionSet result = unify(),
437		expected = Unify::SolutionSet({{{{X, A}, A}}});
438
439		logger().debug() << "result = " << oc_to_string(result);
440		logger().debug() << "expected = " << oc_to_string(expected);
441
442		TS_ASSERT_EQUALS(result, expected);
443
444		logger().info("END TEST: %s", __FUNCTION__);
445		}
446
447		void UnifyUTest::test_unify_basic_2()
448		{
449		logger().info("BEGIN TEST: %s", __FUNCTION__);
450
451		Unify unify(A, X);
452		Unify::SolutionSet result = unify(),
453		expected = Unify::SolutionSet({{{{X, A}, A}}});
454
455		logger().debug() << "result = " << oc_to_string(result);
456		logger().debug() << "expected = " << oc_to_string(expected);
457
458		TS_ASSERT_EQUALS(result, expected);
459
460		logger().info("END TEST: %s", __FUNCTION__);
461		}
462
463		void UnifyUTest::test_unify_basic_3()
464		{
465		logger().info("BEGIN TEST: %s", __FUNCTION__);
466
467		Unify unify(X, InhAB);
468		Unify::SolutionSet result = unify(),
469		expected = Unify::SolutionSet({{{{X, InhAB}, InhAB}}});
470
471		logger().debug() << "result = " << oc_to_string(result);
472		logger().debug() << "expected = " << oc_to_string(expected);
473
474		TS_ASSERT_EQUALS(result, expected);
475
476		logger().info("END TEST: %s", __FUNCTION__);
477		}
478
479		void UnifyUTest::test_unify_basic_4()
480		{
481		logger().info("BEGIN TEST: %s", __FUNCTION__);
482
483		Unify unify(InhXB, InhAY);
484		Unify::SolutionSet result = unify(),
485		expected = Unify::SolutionSet({{{{X, A}, A}, {{Y, B}, B}}});
486
487		logger().debug() << "result = " << oc_to_string(result);
488		logger().debug() << "expected = " << oc_to_string(expected);
489
490		TS_ASSERT_EQUALS(result, expected);
491
492		logger().info("END TEST: %s", __FUNCTION__);
493		}
494
495		void UnifyUTest::test_unify_basic_5()
496		{
497		logger().info("BEGIN TEST: %s", __FUNCTION__);
498
499		Unify unify(InhXY, InhAY);
500		Unify::SolutionSet result = unify(),
501		expected = Unify::SolutionSet({{{{X, A}, A}}});
502
503		logger().debug() << "result = " << oc_to_string(result);
504		logger().debug() << "expected = " << oc_to_string(expected);
505
506		TS_ASSERT_EQUALS(result, expected);
507
508		logger().info("END TEST: %s", __FUNCTION__);
509		}
510
511		void UnifyUTest::test_unify_basic_6()
512		{
513		logger().info("BEGIN TEST: %s", __FUNCTION__);
514
515		// This one is supposed to fail
516		Unify unify(A, B);
517		Unify::SolutionSet result = unify();
518
519		logger().debug() << "result = " << oc_to_string(result);
520
521		TS_ASSERT(not result.is_satisfiable());
522
523		logger().info("END TEST: %s", __FUNCTION__);
524		}
525
526		void UnifyUTest::test_unify_basic_7()
527		{
528		logger().info("BEGIN TEST: %s", __FUNCTION__);
529
530		// This one is supposed to fail
531		Unify unify(InhXB, B);
532		Unify::SolutionSet result = unify();
533
534		TS_ASSERT(not result.is_satisfiable());
535
536		logger().info("END TEST: %s", __FUNCTION__);
537		}
538
539		void UnifyUTest::test_unify_basic_8()
540		{
541		logger().info("BEGIN TEST: %s", __FUNCTION__);
542
543		Unify unify(InhXY, InhAZ);
544		Unify::SolutionSet result = unify(),
545		expected = Unify::SolutionSet({{{{X, A}, A}, {{Y, Z}, Y}}});
546
547		logger().debug() << "result = " << oc_to_string(result);
548		logger().debug() << "expected = " << oc_to_string(expected);
549
550		TS_ASSERT_EQUALS(result, expected);
551
552		logger().info("END TEST: %s", __FUNCTION__);
553		}
554
555		void UnifyUTest::test_unify_undeclared_var_1()
556		{
557		logger().info("BEGIN TEST: %s", __FUNCTION__);
558
559		// The variable declaration provided, Y, is not present in the left
560		// term, X, thus unification is not possible, since X viewed as
561		// constant is different than A.
562		Unify unify(X, A, Y);
563		Unify::SolutionSet result = unify(),
564		expected(false);
565
566		logger().debug() << "result = " << oc_to_string(result);
567		logger().debug() << "expected = " << oc_to_string(expected);
568
569		TS_ASSERT_EQUALS(result, expected);
570
571		// On top of that make sure that the solution is empty as it is
572		// how failing is represented
573		TS_ASSERT(result.empty());
574
575		logger().info("END TEST: %s", __FUNCTION__);
576		}
577
578		void UnifyUTest::test_unify_undeclared_var_2()
579		{
580		logger().info("BEGIN TEST: %s", __FUNCTION__);
581
582		// The variable declaration provided, Y, is not present in the left
583		// term, X, however unification is possible by unifying Z and X
584		// viewed as constant.
585		Unify unify(X, Z, Y);
586		Unify::SolutionSet result = unify(),
587		expected = Unify::SolutionSet({{{{Z, X}, X}}});
588
589		logger().debug() << "result = " << oc_to_string(result);
590		logger().debug() << "expected = " << oc_to_string(expected);
591
592		TS_ASSERT_EQUALS(result, expected);
593
594		logger().info("END TEST: %s", __FUNCTION__);
595		}
596
597		void UnifyUTest::test_unify_undeclared_var_3()
598		{
599		logger().info("BEGIN TEST: %s", __FUNCTION__);
600
601		// Both X and Y as treated as constants
602		Handle empty_vardecl = al(VARIABLE_LIST);
603		Unify unify(X, Y, empty_vardecl, empty_vardecl);
604		Unify::SolutionSet result = unify(),
605		expected = Unify::SolutionSet(false);
606
607		logger().debug() << "result = " << oc_to_string(result);
608		logger().debug() << "expected = " << oc_to_string(expected);
609
610		TS_ASSERT_EQUALS(result, expected);
611
612		logger().info("END TEST: %s", __FUNCTION__);
613		}
614
615		void UnifyUTest::test_unify_vardecl_1()
616		{
617		logger().info("BEGIN TEST: %s", __FUNCTION__);
618
619		Unify unify(InhXY, InhAY, XY_vardecl, Y_vardecl);
620		Unify::SolutionSet result = unify(),
621		expected = Unify::SolutionSet({{{{X, A}, A}}});
622
623		logger().debug() << "result = " << oc_to_string(result);
624		logger().debug() << "expected = " << oc_to_string(expected);
625
626		TS_ASSERT_EQUALS(result, expected);
627
628		logger().info("END TEST: %s", __FUNCTION__);
629		}
630
631		void UnifyUTest::test_unify_vardecl_2()
632		{
633		logger().info("BEGIN TEST: %s", __FUNCTION__);
634
635		Unify unify(InhXY, InhAY, XY_vardecl, Y_vardecl);
636		Unify::SolutionSet result = unify(),
637		expected = Unify::SolutionSet({{{{X, A}, A}}});
638
639		logger().debug() << "result = " << oc_to_string(result);
640		logger().debug() << "expected = " << oc_to_string(expected);
641
642		TS_ASSERT_EQUALS(result, expected);
643
644		logger().info("END TEST: %s", __FUNCTION__);
645		}
646
647		void UnifyUTest::test_unify_vardecl_3()
648		{
649		logger().info("BEGIN TEST: %s", __FUNCTION__);
650
651		Unify unify(InhXB, InhAY, X_vardecl, Y_vardecl);
652		Unify::SolutionSet result = unify(),
653		expected = Unify::SolutionSet({{{{X, A}, A}, {{Y, B}, B}}});
654
655		TS_ASSERT_EQUALS(result, expected);
656
657		logger().info("END TEST: %s", __FUNCTION__);
658		}
659
660		void UnifyUTest::test_unify_vardecl_4()
661		{
662		logger().info("BEGIN TEST: %s", __FUNCTION__);
663
664		Unify unify(InhXY, InhAZ, XY_vardecl, Z_vardecl);
665		Unify::SolutionSet result = unify(),
666		expected = Unify::SolutionSet({{{{X, A}, A}, {{Y, Z}, Y}}});
667
668		logger().debug() << "result = " << oc_to_string(result);
669		logger().debug() << "expected = " << oc_to_string(expected);
670
671		TS_ASSERT_EQUALS(result, expected);
672
673		logger().info("END TEST: %s", __FUNCTION__);
674		}
675
676		void UnifyUTest::test_unify_vardecl_5()
677		{
678		logger().info("BEGIN TEST: %s", __FUNCTION__);
679
680		// This one is supposed to fail as the types of Y and W have empty
681		// intersection.
682		Unify unify(InhXY, InhAW, XY_vardecl, W_vardecl);
683		Unify::SolutionSet result = unify();
684
685		logger().debug() << "result = " << oc_to_string(result);
686
687		TS_ASSERT(not result.is_satisfiable());
688
689		logger().info("END TEST: %s", __FUNCTION__);
690		}
691
692		void UnifyUTest::test_unify_cyclic_dependence_1()
693		{
694		logger().info("BEGIN TEST: %s", __FUNCTION__);
695
696		// Fails because X cannot be finitely equal to (Inheritance X Y)
697		Unify::SolutionSet result = Unify(InhXY, X)();
698
699		logger().debug() << "result = " << oc_to_string(result);
700
701		TS_ASSERT(not result.is_satisfiable());
702
703		logger().info("END TEST: %s", __FUNCTION__);
704		}
705
706		void UnifyUTest::test_unify_cyclic_dependence_2()
707		{
708		logger().info("BEGIN TEST: %s", __FUNCTION__);
709
710		// Fails because X cannot be an InheritanceLink and a ConceptNode
711		// at once, according to the type declarations.
712		Unify::SolutionSet result = Unify(InhXY, X, XY_vardecl, X_cyclic_vardecl)();
713
714		logger().debug() << "result = " << oc_to_string(result);
715
716		TS_ASSERT(not result.is_satisfiable());
717
718		logger().info("END TEST: %s", __FUNCTION__);
719		}
720
721		void UnifyUTest::test_unify_cyclic_dependence_3()
722		{
723		logger().info("BEGIN TEST: %s", __FUNCTION__);
724
725		// Fails because X and Y are in a cycle.
726		Handle lh = al(LIST_LINK, X, Y);
727		Handle rh = al(LIST_LINK, al(LIST_LINK, Y), al(LIST_LINK, X));
728		Unify::SolutionSet result = Unify(lh, rh)();
729
730		logger().debug() << "result = " << oc_to_string(result);
731
732		TS_ASSERT(not result.is_satisfiable());
733
734		logger().info("END TEST: %s", __FUNCTION__);
735		}
736
737		void UnifyUTest::test_unify_cyclic_dependence_4()
738		{
739		logger().info("BEGIN TEST: %s", __FUNCTION__);
740
741		// This is an example of cycle occuring in spite of the fact that
742		// the left and right terms have no variable in common. X is in a
743		// cycle via unification with Y.
744		Handle lh = al(LIST_LINK, X, al(LIST_LINK, X));
745		Handle rh = al(LIST_LINK, Y, Y);
746		Unify::SolutionSet result = Unify(lh, rh)();
747
748		logger().debug() << "result = " << oc_to_string(result);
749
750		TS_ASSERT(not result.is_satisfiable());
751
752		logger().info("END TEST: %s", __FUNCTION__);
753		}
754
755		void UnifyUTest::xtest_unify_type_union_1()
756		{
757		Unify::SolutionSet result = Unify(InhXY, InhAV, XY_vardecl, V_vardecl)(),
758		expected = Unify::SolutionSet({{{{X, A}, A}, {{Y, V}, Y}}});
759
760		logger().debug() << "result = " << oc_to_string(result);
761		logger().debug() << "expected = " << oc_to_string(expected);
762
763		TS_ASSERT_EQUALS(result, expected);
764
765		logger().info("END TEST: %s", __FUNCTION__);
766		}
767
768		void UnifyUTest::test_unify_unordered_1()
769		{
770		logger().info("BEGIN TEST: %s", __FUNCTION__);
771
772		Unify unify(AndAA, AndAB);
773		Unify::SolutionSet result = unify();
774
775		logger().debug() << "result = " << oc_to_string(result);
776
777		TS_ASSERT(not result.is_satisfiable());
778
779		logger().info("END TEST: %s", __FUNCTION__);
780		}
781
782		void UnifyUTest::test_unify_unordered_2()
783		{
784		logger().info("BEGIN TEST: %s", __FUNCTION__);
785
786		Unify unify(AndAB, AndAY, Handle::UNDEFINED, Y_vardecl);
787		Unify::SolutionSet result = unify(),
788		expected = Unify::SolutionSet({{{{Y, B}, B}}});
789
790		logger().debug() << "result = " << oc_to_string(result);
791		logger().debug() << "expected = " << oc_to_string(expected);
792
793		TS_ASSERT_EQUALS(result, expected);
794
795		logger().info("END TEST: %s", __FUNCTION__);
796		}
797
798		void UnifyUTest::test_unify_unordered_3()
799		{
800		logger().info("BEGIN TEST: %s", __FUNCTION__);
801
802		Unify unify(AndAY, AndXB);
803		Unify::SolutionSet result = unify(),
804		expected = Unify::SolutionSet({{{{X, A}, A}, {{Y, B}, B}}});
805
806		logger().debug() << "result = " << oc_to_string(result);
807		logger().debug() << "expected = " << oc_to_string(expected);
808
809		TS_ASSERT_EQUALS(result, expected);
810
811		logger().info("END TEST: %s", __FUNCTION__);
812		}
813
814		void UnifyUTest::test_unify_unordered_4()
815		{
816		logger().info("BEGIN TEST: %s", __FUNCTION__);
817
818		Unify unify(AndAB, AndXY, Handle::UNDEFINED, XY_vardecl);
819		Unify::SolutionSet result = unify(),
820		expected = Unify::SolutionSet({{{{X, A}, A}, {{Y, B}, B}},
821		{{{Y, A}, A}, {{X, B}, B}}});
822
823		logger().debug() << "result = " << oc_to_string(result);
824		logger().debug() << "expected = " << oc_to_string(expected);
825
826		logger().info("END TEST: %s", __FUNCTION__);
827		}
828
829		void UnifyUTest::test_unify_unordered_5()
830		{
831		logger().info("BEGIN TEST: %s", __FUNCTION__);
832
833		Unify unify(AndAABB, AndXYAB);
834		Unify::SolutionSet result = unify(),
835		expected = Unify::SolutionSet({{{{X, A}, A}, {{Y, B}, B}},
836		{{{Y, A}, A}, {{X, B}, B}}});
837
838		logger().debug() << "result = " << oc_to_string(result);
839		logger().debug() << "expected = " << oc_to_string(expected);
840
841		TS_ASSERT_EQUALS(result, expected);
842
843		logger().info("END TEST: %s", __FUNCTION__);
844		}
845
846		void UnifyUTest::test_unify_unordered_6()
847		{
848		logger().info("BEGIN TEST: %s", __FUNCTION__);
849
850		Unify unify(AndAAABBB, AndXXYYAB);
851		Unify::SolutionSet result = unify(),
852		expected = Unify::SolutionSet({{{{X, A}, A}, {{Y, B}, B}},
853		{{{Y, A}, A}, {{X, B}, B}}});
854
855		logger().debug() << "result = " << oc_to_string(result);
856		logger().debug() << "expected = " << oc_to_string(expected);
857
858		TS_ASSERT_EQUALS(result, expected);
859
860		logger().info("END TEST: %s", __FUNCTION__);
861		}
862
863		void UnifyUTest::test_unify_unordered_7()
864		{
865		logger().info("BEGIN TEST: %s", __FUNCTION__);
866
867		Unify unify(AndAAAABBBB, AndXXXYYYAB);
868		Unify::SolutionSet result = unify(),
869		expected = Unify::SolutionSet({{{{X, A}, A}, {{Y, B}, B}},
870		{{{Y, A}, A}, {{X, B}, B}}});
871
872		logger().debug() << "result = " << oc_to_string(result);
873		logger().debug() << "expected = " << oc_to_string(expected);
874
875		TS_ASSERT_EQUALS(result, expected);
876
877		logger().info("END TEST: %s", __FUNCTION__);
878		}
879
880		void UnifyUTest::test_unify_unordered_8()
881		{
882		logger().info("BEGIN TEST: %s", __FUNCTION__);
883
884		Unify unify(AndAAAAABBBBB, AndXXXXYYYYAB);
885		Unify::SolutionSet result = unify(),
886		expected = Unify::SolutionSet({{{{X, A}, A}, {{Y, B}, B}},
887		{{{Y, A}, A}, {{X, B}, B}}});
888
889		logger().debug() << "result = " << oc_to_string(result);
890		logger().debug() << "expected = " << oc_to_string(expected);
891
892		TS_ASSERT_EQUALS(result, expected);
893
894		logger().info("END TEST: %s", __FUNCTION__);
895		}
896
897		void UnifyUTest::test_unify_alpha_equivalence()
898		{
899		logger().info("BEGIN TEST: %s", __FUNCTION__);
900
901		Handle lhs =
902		_eval.eval_h("(ExistsLink"
903		" (TypedVariableLink"
904		" (VariableNode \"?MEMBER\")"
905		" (TypeChoice"
906		" (TypeNode \"ConceptNode\")"
907		" (TypeNode \"SchemaNode\")"
908		" (TypeNode \"PredicateNode\")"
909		" )"
910		" )"
911		" (MemberLink"
912		" (VariableNode \"?MEMBER\")"
913		" (ConceptNode \"Org1-1\")"
914		" )"
915		")");
916
917		Handle rhs =
918		_eval.eval_h("(ExistsLink"
919		" (TypedVariableLink"
920		" (VariableNode \"?OBJ\")"
921		" (TypeChoice"
922		" (TypeNode \"ConceptNode\")"
923		" (TypeNode \"SchemaNode\")"
924		" (TypeNode \"PredicateNode\")"
925		" )"
926		" )"
927		" (MemberLink"
928		" (VariableNode \"?OBJ\")"
929		" (VariableNode \"?COLL-6c74a409\")"
930		" )"
931		")");
932
933		Handle lhs_vardecl;
934
935		Handle rhs_vardecl =
936		_eval.eval_h("(TypedVariableLink"
937		" (VariableNode \"?COLL-6c74a409\")"
938		" (TypeChoice"
939		" (TypeNode \"ConceptNode\")"
940		" (TypeNode \"SchemaNode\")"
941		" (TypeNode \"PredicateNode\")"
942		" )"
943		")");
944
945		Handle MEMBER = an(VARIABLE_NODE, "?MEMBER");
946		Handle OBJ = an(VARIABLE_NODE, "?OBJ");
947		Handle COLL = an(VARIABLE_NODE, "?COLL-6c74a409");
948		Handle Org1 = an(CONCEPT_NODE, "Org1-1");
949		Context C1(Quotation(), {MEMBER}, false);
950		Context C2(Quotation(), {OBJ}, false);
951		Unify::CHandle C1Org1(Org1, C1), C2COLL(COLL, C2);
952
953		Unify unify(lhs, rhs, lhs_vardecl, rhs_vardecl);
954		Unify::SolutionSet result = unify(),
955		expected = Unify::SolutionSet({{{{C1Org1, C2COLL}, C1Org1}}});
956
957		logger().debug() << "result = " << oc_to_string(result);
958		logger().debug() << "expected = " << oc_to_string(expected);
959
960		TS_ASSERT_EQUALS(result, expected);
961
962		logger().info("END TEST: %s", __FUNCTION__);
963		}
964
965		void UnifyUTest::test_substitute()
966		{
967		logger().info("BEGIN TEST: %s", __FUNCTION__);
968
969		// Test simple BindLink
970		Handle X = an(VARIABLE_NODE, "$X"),
971		Y = an(VARIABLE_NODE, "$Y"),
972		CT = an(TYPE_NODE, "ConceptNode"),
973		Y_vardecl = al(TYPED_VARIABLE_LINK, Y, CT),
974		hbl = al(BIND_LINK, al(AND_LINK, X), al(OR_LINK, X)),
975		expected = al(BIND_LINK, Y_vardecl,
976		al(AND_LINK, Y), al(OR_LINK, Y));
977
978		BindLinkPtr bl(BindLinkCast(hbl));
979
980		Handle result = _as->add_atom(Unify::substitute(bl, {{X, Y}}, Y_vardecl));
981
982		logger().debug() << "result = " << oc_to_string(result);
983		logger().debug() << "expected = " << oc_to_string(expected);
984
985		TS_ASSERT_EQUALS(result, expected);
986
987		logger().info("END TEST: %s", __FUNCTION__);
988		}
989
990		void UnifyUTest::test_unify_complex_1()
991		{
992		logger().info("BEGIN TEST: %s", __FUNCTION__);
993
994		Handle lhs =
995		_eval.eval_h("(ImplicationLink"
996		" (LambdaLink"
997		" (TypedVariableLink"
998		" (VariableNode \"$X\")"
999		" (TypeNode \"ConceptNode\"))"
1000		" (EvaluationLink"
1001		" (PredicateNode \"take\")"
1002		" (ListLink"
1003		" (VariableNode \"$X\")"
1004		" (ConceptNode \"treatment-1\"))))"
1005		" (AndLink"
1006		" (QuoteLink"
1007		" (LambdaLink"
1008		" (UnquoteLink"
1009		" (VariableNode \"$TyVs\"))"
1010		" (UnquoteLink"
1011		" (VariableNode \"$A1\"))))"
1012		" (QuoteLink"
1013		" (LambdaLink"
1014		" (UnquoteLink"
1015		" (VariableNode \"$TyVs\"))"
1016		" (UnquoteLink"
1017		" (VariableNode \"$A2\"))))))");
1018		Handle rhs =
1019		_eval.eval_h("(ImplicationLink"
1020		" (VariableNode \"$P\")"
1021		" (And"
1022		" (VariableNode \"$P\")"
1023		" (VariableNode \"$Q\")))");
1024		Handle lhs_vardecl =
1025		_eval.eval_h("(VariableList"
1026		" (TypedVariableLink"
1027		" (VariableNode \"$TyVs\")"
1028		" (TypeChoice"
1029		" (TypeNode \"TypedVariableLink\")"
1030		" (TypeNode \"VariableNode\")"
1031		" (TypeNode \"VariableList\")))"
1032		" (TypedVariableLink"
1033		" (VariableNode \"$A1\")"
1034		" (TypeNode \"EvaluationLink\"))"
1035		" (TypedVariableLink"
1036		" (VariableNode \"$A2\")"
1037		" (TypeNode \"EvaluationLink\")))");
1038		Handle rhs_vardecl =
1039		_eval.eval_h("(VariableList"
1040		" (TypedVariableLink"
1041		" (VariableNode \"$P\")"
1042		" (TypeChoice"
1043		" (TypeNode \"PredicateNode\")"
1044		" (TypeNode \"LambdaLink\")))"
1045		" (TypedVariableLink"
1046		" (VariableNode \"$Q\")"
1047		" (TypeChoice"
1048		" (TypeNode \"PredicateNode\")"
1049		" (TypeNode \"LambdaLink\")))))");
1050
1051		Handle P = _eval.eval_h("(VariableNode \"$P\")");
1052		Handle Q = _eval.eval_h("(VariableNode \"$Q\")");
1053		Handle TyVs = _eval.eval_h("(VariableNode \"$TyVs\")");
1054		Handle A1 = _eval.eval_h("(VariableNode \"$A1\")");
1055		Handle A2 = _eval.eval_h("(VariableNode \"$A2\")");
1056
1057		Handle implicant =
1058		_eval.eval_h("(LambdaLink"
1059		" (TypedVariableLink"
1060		" (VariableNode \"$X\")"
1061		" (TypeNode \"ConceptNode\"))"
1062		" (EvaluationLink"
1063		" (PredicateNode \"take\")"
1064		" (ListLink"
1065		" (VariableNode \"$X\")"
1066		" (ConceptNode \"treatment-1\"))))");
1067
1068		Handle quoted_LA1 =
1069		_eval.eval_h("(QuoteLink"
1070		" (LambdaLink"
1071		" (UnquoteLink"
1072		" (VariableNode \"$TyVs\"))"
1073		" (UnquoteLink"
1074		" (VariableNode \"$A1\"))))");
1075
1076		Handle quoted_LA2 =
1077		_eval.eval_h("(QuoteLink"
1078		" (LambdaLink"
1079		" (UnquoteLink"
1080		" (VariableNode \"$TyVs\"))"
1081		" (UnquoteLink"
1082		" (VariableNode \"$A2\"))))");
1083
1084		Handle implicant_vardecl =
1085		_eval.eval_h("(TypedVariableLink"
1086		" (VariableNode \"$X\")"
1087		" (TypeNode \"ConceptNode\"))");
1088
1089		Handle implicant_body =
1090		_eval.eval_h("(EvaluationLink"
1091		" (PredicateNode \"take\")"
1092		" (ListLink"
1093		" (VariableNode \"$X\")"
1094		" (ConceptNode \"treatment-1\")))");
1095
1096		Variables X_vars = ScopeLinkCast(implicant)->get_variables();
1097		Context::VariablesStack varstack({X_vars});
1098		Context C(Quotation(), {X}, true, varstack);
1099		Unify::CHandle Cimplicant_vardecl(implicant_vardecl, C),
1100		Cimplicant_body(implicant_body, C);
1101
1102		Unify unify(lhs, rhs, lhs_vardecl, rhs_vardecl);
1103		Unify::SolutionSet result = unify(),
1104		expected = Unify::SolutionSet({{{{P, implicant, quoted_LA2},
1105		implicant},
1106		{{TyVs, Cimplicant_vardecl},
1107		Cimplicant_vardecl},
1108		{{A2, Cimplicant_body},
1109		Cimplicant_body},
1110		{{Q, quoted_LA1},
1111		quoted_LA1}},
1112		{{{P, implicant, quoted_LA1},
1113		implicant},
1114		{{TyVs, Cimplicant_vardecl},
1115		Cimplicant_vardecl},
1116		{{A1, Cimplicant_body},
1117		Cimplicant_body},
1118		{{Q, quoted_LA2},
1119		quoted_LA2}}});
1120
1121		logger().debug() << "result = " << oc_to_string(result);
1122		logger().debug() << "expected = " << oc_to_string(expected);
1123
1124		TS_ASSERT_EQUALS(result, expected);
1125
1126		Handle A1_vardecl = _eval.eval_h("(TypedVariableLink"
1127		" (VariableNode \"$A1\")"
1128		" (TypeNode \"EvaluationLink\"))");
1129
1130		Handle A2_vardecl = _eval.eval_h("(TypedVariableLink"
1131		" (VariableNode \"$A2\")"
1132		" (TypeNode \"EvaluationLink\"))");
1133
1134		Handle consumed_LA1 =
1135		_eval.eval_h("(LambdaLink"
1136		" (TypedVariableLink"
1137		" (VariableNode \"$X\")"
1138		" (TypeNode \"ConceptNode\"))"
1139		" (VariableNode \"$A1\"))");
1140
1141		Handle consumed_LA2 =
1142		_eval.eval_h("(LambdaLink"
1143		" (TypedVariableLink"
1144		" (VariableNode \"$X\")"
1145		" (TypeNode \"ConceptNode\"))"
1146		" (VariableNode \"$A2\"))");
1147
1148		Unify::TypedSubstitutions ts_result =
1149		unify.typed_substitutions(result, lhs);
1150		Unify::TypedSubstitutions ts_expected =
1151		Unify::TypedSubstitutions{{{{P, implicant},
1152		{TyVs, Cimplicant_vardecl},
1153		{A2, Cimplicant_body},
1154		{Q, consumed_LA1}},
1155		A1_vardecl},
1156		{{{P, implicant},
1157		{TyVs, Cimplicant_vardecl},
1158		{A1, Cimplicant_body},
1159		{Q, consumed_LA2}},
1160		A2_vardecl}};
1161
1162		logger().debug() << "ts_result = " << oc_to_string(ts_result);
1163		logger().debug() << "ts_expected = " << oc_to_string(ts_expected);
1164
1165		TS_ASSERT(tss_content_eq(ts_result, ts_expected));
1166
1167		logger().info("END TEST: %s", __FUNCTION__);
1168		}
1169
1170		void UnifyUTest::test_unify_complex_2()
1171		{
1172		logger().info("BEGIN TEST: %s", __FUNCTION__);
1173
1174		Handle lhs =
1175		_eval.eval_h("(ImplicationScopeLink"
1176		" (TypedVariableLink"
1177		" (VariableNode \"$X\")"
1178		" (TypeNode \"ConceptNode\"))"
1179		" (VariableNode \"$P-55ebe96e\")"
1180		" (EvaluationLink"
1181		" (PredicateNode \"take\")"
1182		" (ListLink"
1183		" (VariableNode \"$X\")"
1184		" (ConceptNode \"compound-A\"))))");
1185
1186		Handle rhs =
1187		_eval.eval_h("(ImplicationScopeLink"
1188		" (TypedVariableLink"
1189		" (VariableNode \"$X\")"
1190		" (TypeNode \"ConceptNode\"))"
1191		" (AndLink"
1192		" (EvaluationLink"
1193		" (PredicateNode \"contain\")"
1194		" (ListLink"
1195		" (VariableNode \"$Y-6f50cc6a\")"
1196		" (ConceptNode \"compound-A\")))"
1197		" (EvaluationLink"
1198		" (PredicateNode \"take\")"
1199		" (ListLink"
1200		" (VariableNode \"$X\")"
1201		" (VariableNode \"$Y-6f50cc6a\"))))"
1202		" (EvaluationLink"
1203		" (PredicateNode \"take\")"
1204		" (ListLink"
1205		" (VariableNode \"$X\")"
1206		" (ConceptNode \"compound-A\"))))");
1207
1208		Handle lhs_vardecl =
1209		_eval.eval_h("(VariableNode \"$P-55ebe96e\")");
1210
1211		Handle rhs_vardecl =
1212		_eval.eval_h("(TypedVariableLink"
1213		" (VariableNode \"$Y-6f50cc6a\")"
1214		" (TypeNode \"ConceptNode\"))");
1215
1216		Handle P = _eval.eval_h("(VariableNode \"$P-55ebe96e\")");
1217
1218		Handle conjunction =
1219		_eval.eval_h("(AndLink"
1220		" (EvaluationLink"
1221		" (PredicateNode \"contain\")"
1222		" (ListLink"
1223		" (VariableNode \"$Y-6f50cc6a\")"
1224		" (ConceptNode \"compound-A\")))"
1225		" (EvaluationLink"
1226		" (PredicateNode \"take\")"
1227		" (ListLink"
1228		" (VariableNode \"$X\")"
1229		" (VariableNode \"$Y-6f50cc6a\"))))");
1230
1231		Context C(Quotation(), {X}, true, X_varstack);
1232		Unify::CHandle CP(P, C);
1233		Unify::CHandle Cconjunction(conjunction, C);
1234
1235		Unify unify(lhs, rhs, lhs_vardecl, rhs_vardecl);
1236		Unify::SolutionSet result = unify();
1237		Unify::Block pb_expected{CP, Cconjunction};
1238		Unify::Partition partition_expected{{pb_expected, Cconjunction}};
1239		Unify::SolutionSet expected = Unify::SolutionSet({partition_expected});
1240
1241		logger().debug() << "result = " << oc_to_string(result);
1242		logger().debug() << "expected = " << oc_to_string(expected);
1243
1244		TS_ASSERT_EQUALS(result, expected);
1245
1246		Handle ts_vardecl = _eval.eval_h("(TypedVariableLink"
1247		" (VariableNode \"$Y-6f50cc6a\")"
1248		" (TypeNode \"ConceptNode\"))");
1249
1250		Unify::TypedSubstitutions tss_result =
1251		unify.typed_substitutions(result, lhs);
1252		Unify::HandleCHandleMap hchm_expected =
1253		Unify::HandleCHandleMap{{P, Cconjunction}};
1254		Unify::TypedSubstitution ts_expected =
1255		Unify::TypedSubstitution{hchm_expected, ts_vardecl};
1256		Unify::TypedSubstitutions tss_expected =
1257		Unify::TypedSubstitutions{ts_expected};
1258
1259		logger().debug() << "tss_result = " << oc_to_string(tss_result);
1260		logger().debug() << "tss_expected = " << oc_to_string(tss_expected);
1261
1262		TS_ASSERT(tss_content_eq(tss_result, tss_expected));
1263
1264		logger().info("END TEST: %s", __FUNCTION__);
1265		}
1266
1267		void UnifyUTest::test_unify_complex_3()
1268		{
1269		logger().info("BEGIN TEST: %s", __FUNCTION__);
1270
1271		Handle lhs =
1272		_eval.eval_h("(ImplicationLink"
1273		" (QuoteLink"
1274		" (LambdaLink"
1275		" (UnquoteLink"
1276		" (VariableNode \"$TyVs-3753c5dc\"))"
1277		" (UnquoteLink"
1278		" (VariableNode \"$Q-79152fc8\"))))"
1279		" (LambdaLink"
1280		" (TypedVariableLink"
1281		" (VariableNode \"$X\")"
1282		" (TypeNode \"ConceptNode\"))"
1283		" (EvaluationLink"
1284		" (PredicateNode \"take\")"
1285		" (ListLink"
1286		" (VariableNode \"$X\")"
1287		" (ConceptNode \"compound-A\")))))");
1288
1289		Handle rhs =
1290		_eval.eval_h("(ImplicationLink"
1291		" (QuoteLink"
1292		" (LambdaLink"
1293		" (UnquoteLink"
1294		" (VariableNode \"$TyVs-7b18f3dc\"))"
1295		" (UnquoteLink"
1296		" (VariableNode \"$P-60bdbde3\"))))"
1297		" (QuoteLink"
1298		" (LambdaLink"
1299		" (UnquoteLink"
1300		" (VariableNode \"$TyVs-7b18f3dc\"))"
1301		" (UnquoteLink"
1302		" (VariableNode \"$Q-344be2a0\")))))");
1303
1304		Handle lhs_vardecl =
1305		_eval.eval_h("(VariableList"
1306		" (TypedVariableLink"
1307		" (VariableNode \"$TyVs-3753c5dc\")"
1308		" (TypeChoice"
1309		" (TypeNode \"TypedVariableLink\")"
1310		" (TypeNode \"VariableList\")))"
1311		" (VariableNode \"$Q-79152fc8\"))");
1312
1313		Handle rhs_vardecl =
1314		_eval.eval_h("(VariableList"
1315		" (TypedVariableLink"
1316		" (VariableNode \"$TyVs-7b18f3dc\")"
1317		" (TypeChoice"
1318		" (TypeNode \"TypedVariableLink\")"
1319		" (TypeNode \"VariableList\")))"
1320		" (VariableNode \"$P-60bdbde3\")"
1321		" (VariableNode \"$Q-344be2a0\"))");
1322
1323		Handle TyVs1 = _eval.eval_h("(VariableNode \"$TyVs-3753c5dc\")");
1324		Handle TyVs2 = _eval.eval_h("(VariableNode \"$TyVs-7b18f3dc\")");
1325		Handle Q1 = _eval.eval_h("(VariableNode \"$Q-79152fc8\")");
1326		Handle Q2 = _eval.eval_h("(VariableNode \"$Q-344be2a0\")");
1327		Handle P =_eval.eval_h("(VariableNode \"$P-60bdbde3\")");
1328
1329		Handle vardecl =
1330		_eval.eval_h("(TypedVariableLink"
1331		" (VariableNode \"$X\")"
1332		" (TypeNode \"ConceptNode\"))");
1333
1334		Handle implicant_body =
1335		_eval.eval_h("(EvaluationLink"
1336		" (PredicateNode \"take\")"
1337		" (ListLink"
1338		" (VariableNode \"$X\")"
1339		" (ConceptNode \"compound-A\")))");
1340
1341		Context C(Quotation(), {X}, true, X_varstack);
1342		Unify::CHandle Cvardecl(vardecl, C), Cimplicant_body(implicant_body, C);
1343
1344		Unify unify(lhs, rhs, lhs_vardecl, rhs_vardecl);
1345		Unify::SolutionSet result = unify(),
1346		expected = Unify::SolutionSet({{{{TyVs1, TyVs2, Cvardecl}, Cvardecl},
1347		{{Q1, P}, Q1},
1348		{{Q2, Cimplicant_body}, Cimplicant_body}}});
1349
1350		logger().debug() << "result = " << oc_to_string(result);
1351		logger().debug() << "expected = " << oc_to_string(expected);
1352
1353		TS_ASSERT_EQUALS(result, expected);
1354
1355		logger().info("END TEST: %s", __FUNCTION__);
1356		}
1357
1358		void UnifyUTest::test_unify_complex_4()
1359		{
1360		logger().info("BEGIN TEST: %s", __FUNCTION__);
1361
1362		// Very similar to test_unify_complex_1() but for some reason doesn't work.
1363		Handle target = _eval.eval_h(
1364		"(ImplicationLink"
1365		" (LambdaLink"
1366		" (TypedVariableLink"
1367		" (VariableNode \"$X\")"
1368		" (TypeNode \"ConceptNode\")"
1369		" )"
1370		" (EvaluationLink"
1371		" (PredicateNode \"take\")"
1372		" (ListLink"
1373		" (VariableNode \"$X\")"
1374		" (ConceptNode \"treatment-1\")"
1375		" )"
1376		" )"
1377		" )"
1378		" (AndLink"
1379		" (QuoteLink"
1380		" (LambdaLink"
1381		" (UnquoteLink"
1382		" (VariableNode \"$TyVs-5476a9b9\")"
1383		" )"
1384		" (UnquoteLink"
1385		" (VariableNode \"$A1-7235efc6\")"
1386		" )"
1387		" )"
1388		" )"
1389		" (QuoteLink"
1390		" (LambdaLink"
1391		" (UnquoteLink"
1392		" (VariableNode \"$TyVs-5476a9b9\")"
1393		" )"
1394		" (UnquoteLink"
1395		" (VariableNode \"$A2-1ac8e4a2\")"
1396		" )"
1397		" )"
1398		" )"
1399		" )"
1400		")"
1401		);
1402		Handle alpha_pat = _eval.eval_h(
1403		"(ImplicationLink"
1404		" (VariableNode \"$P-10ea3e30\")"
1405		" (AndLink"
1406		" (VariableNode \"$P-10ea3e30\")"
1407		" (VariableNode \"$Q-78f01c2d\")"
1408		" )"
1409		")"
1410		);
1411		Handle vardecl = _eval.eval_h(
1412		"(VariableList"
1413		" (TypedVariableLink"
1414		" (VariableNode \"$TyVs-5476a9b9\")"
1415		" (TypeChoice"
1416		" (TypeNode \"TypedVariableLink\")"
1417		" (TypeNode \"VariableNode\")"
1418		" (TypeNode \"VariableList\")"
1419		" )"
1420		" )"
1421		" (TypedVariableLink"
1422		" (VariableNode \"$A1-7235efc6\")"
1423		" (TypeNode \"EvaluationLink\")"
1424		" )"
1425		" (TypedVariableLink"
1426		" (VariableNode \"$A2-1ac8e4a2\")"
1427		" (TypeNode \"EvaluationLink\")"
1428		" )"
1429		")"
1430		);
1431		Handle alpha_vardecl = _eval.eval_h(
1432		"(VariableList"
1433		" (TypedVariableLink"
1434		" (VariableNode \"$P-10ea3e30\")"
1435		" (TypeChoice"
1436		" (TypeNode \"LambdaLink\")"
1437		" (TypeNode \"PredicateNode\")"
1438		" )"
1439		" )"
1440		" (TypedVariableLink"
1441		" (VariableNode \"$Q-78f01c2d\")"
1442		" (TypeChoice"
1443		" (TypeNode \"LambdaLink\")"
1444		" (TypeNode \"PredicateNode\")"
1445		" )"
1446		" )"
1447		")"
1448		);
1449
1450		Handle P = _eval.eval_h("(VariableNode \"$P-10ea3e30\")");
1451		Handle Q = _eval.eval_h("(VariableNode \"$Q-78f01c2d\")");
1452		Handle TyVs = _eval.eval_h("(VariableNode \"$TyVs-5476a9b9\")");
1453		Handle A1 = _eval.eval_h("(VariableNode \"$A1-7235efc6\")");
1454		Handle A2 = _eval.eval_h("(VariableNode \"$A2-1ac8e4a2\")");
1455
1456		Handle implicant =
1457		_eval.eval_h("(LambdaLink"
1458		" (TypedVariableLink"
1459		" (VariableNode \"$X\")"
1460		" (TypeNode \"ConceptNode\"))"
1461		" (EvaluationLink"
1462		" (PredicateNode \"take\")"
1463		" (ListLink"
1464		" (VariableNode \"$X\")"
1465		" (ConceptNode \"treatment-1\"))))");
1466
1467		Handle quoted_LA1 =
1468		_eval.eval_h("(QuoteLink"
1469		" (LambdaLink"
1470		" (UnquoteLink"
1471		" (VariableNode \"$TyVs-5476a9b9\"))"
1472		" (UnquoteLink"
1473		" (VariableNode \"$A1-7235efc6\"))))");
1474
1475		Handle quoted_LA2 =
1476		_eval.eval_h("(QuoteLink"
1477		" (LambdaLink"
1478		" (UnquoteLink"
1479		" (VariableNode \"$TyVs-5476a9b9\"))"
1480		" (UnquoteLink"
1481		" (VariableNode \"$A2-1ac8e4a2\"))))");
1482
1483		Handle implicant_vardecl =
1484		_eval.eval_h("(TypedVariableLink"
1485		" (VariableNode \"$X\")"
1486		" (TypeNode \"ConceptNode\"))");
1487
1488		Handle implicant_body =
1489		_eval.eval_h("(EvaluationLink"
1490		" (PredicateNode \"take\")"
1491		" (ListLink"
1492		" (VariableNode \"$X\")"
1493		" (ConceptNode \"treatment-1\")))");
1494
1495		Context C(Quotation(), {X}, true, X_varstack);
1496		Unify::CHandle Cimplicant_vardecl(implicant_vardecl, C),
1497		Cimplicant_body(implicant_body, C);
1498
1499		Unify unify(target, alpha_pat, vardecl, alpha_vardecl);
1500		Unify::SolutionSet result = unify(),
1501		expected = Unify::SolutionSet({{{{P, implicant, quoted_LA2},
1502		implicant},
1503		{{TyVs, Cimplicant_vardecl},
1504		Cimplicant_vardecl},
1505		{{A2, Cimplicant_body},
1506		Cimplicant_body},
1507		{{Q, quoted_LA1},
1508		quoted_LA1}},
1509		{{{P, implicant, quoted_LA1},
1510		implicant},
1511		{{TyVs, Cimplicant_vardecl},
1512		Cimplicant_vardecl},
1513		{{A1, Cimplicant_body},
1514		Cimplicant_body},
1515		{{Q, quoted_LA2},
1516		quoted_LA2}}});
1517
1518		logger().debug() << "result = " << oc_to_string(result);
1519		logger().debug() << "expected = " << oc_to_string(expected);
1520
1521		TS_ASSERT_EQUALS(result, expected);
1522
1523		logger().info("END TEST: %s", __FUNCTION__);
1524		}
1525
1526		void UnifyUTest::test_unify_complex_5()
1527		{
1528		logger().info("BEGIN TEST: %s", __FUNCTION__);
1529
1530		Handle target =
1531		_eval.eval_h("(LambdaLink"
1532		" (TypedVariableLink"
1533		" (VariableNode \"$X\")"
1534		" (TypeNode \"ConceptNode\")"
1535		" )"
1536		" (VariableNode \"$Q-496643b4\")"
1537		")");
1538
1539		Handle alpha_pat =
1540		_eval.eval_h("(QuoteLink"
1541		" (LambdaLink"
1542		" (UnquoteLink"
1543		" (VariableNode \"$TyVs-3e93b595\")"
1544		" )"
1545		" (UnquoteLink"
1546		" (VariableNode \"$A2-76df4103\")"
1547		" )"
1548		" )"
1549		")");
1550
1551		Handle vardecl =
1552		_eval.eval_h("(VariableNode \"$Q-496643b4\")");
1553
1554		Handle alpha_vardecl =
1555		_eval.eval_h("(VariableList"
1556		" (TypedVariableLink"
1557		" (VariableNode \"$TyVs-3e93b595\")"
1558		" (TypeChoice"
1559		" (TypeNode \"TypedVariableLink\")"
1560		" (TypeNode \"VariableNode\")"
1561		" (TypeNode \"VariableList\")"
1562		" )"
1563		" )"
1564		" (TypedVariableLink"
1565		" (VariableNode \"$A2-76df4103\")"
1566		" (TypeNode \"EvaluationLink\")"
1567		" )"
1568		")");
1569
1570		Handle Q = _eval.eval_h("(VariableNode \"$Q-496643b4\")");
1571		Handle TyVs = _eval.eval_h("(VariableNode \"$TyVs-3e93b595\")");
1572		Handle A2 = _eval.eval_h("(VariableNode \"$A2-76df4103\")");
1573
1574		Handle lambda_vardecl =
1575		_eval.eval_h("(TypedVariableLink"
1576		" (VariableNode \"$X\")"
1577		" (TypeNode \"ConceptNode\"))");
1578
1579		Handle take_treatment_1 =
1580		_eval.eval_h("(EvaluationLink"
1581		" (PredicateNode \"take\")"
1582		" (ListLink"
1583		" (VariableNode \"$X\")"
1584		" (ConceptNode \"treatment-1\")))");
1585
1586		Context C(Quotation(), {X}, true, X_varstack);
1587		Unify::CHandle CQ(Q, C),
1588		Clambda_vardecl(lambda_vardecl, C),
1589		Ctake_treatment_1(take_treatment_1, C);
1590
1591		Unify unify(target, alpha_pat, vardecl, alpha_vardecl);
1592		Unify::SolutionSet result = unify(),
1593		expected = Unify::SolutionSet({{{{CQ, A2}, A2},
1594		{{TyVs, Clambda_vardecl},
1595		Clambda_vardecl}}});
1596
1597		logger().debug() << "result = " << oc_to_string(result);
1598		logger().debug() << "expected = " << oc_to_string(expected);
1599
1600		TS_ASSERT_EQUALS(result, expected);
1601
1602		logger().info("END TEST: %s", __FUNCTION__);
1603		}
1604
1605		void UnifyUTest::test_unify_complex_6()
1606		{
1607		logger().info("BEGIN TEST: %s", __FUNCTION__);
1608
1609		Handle target =
1610		_eval.eval_h("(ImplicationLink"
1611		" (AndLink"
1612		" (LambdaLink"
1613		" (TypedVariableLink"
1614		" (VariableNode \"$X\")"
1615		" (TypeNode \"ConceptNode\")"
1616		" )"
1617		" (EvaluationLink"
1618		" (PredicateNode \"take\")"
1619		" (ListLink"
1620		" (VariableNode \"$X\")"
1621		" (ConceptNode \"treatment-1\")"
1622		" )"
1623		" )"
1624		" )"
1625		" (LambdaLink"
1626		" (TypedVariableLink"
1627		" (VariableNode \"$X\")"
1628		" (TypeNode \"ConceptNode\")"
1629		" )"
1630		" (VariableNode \"$Q-496643b4\")"
1631		" )"
1632		" )"
1633		" (LambdaLink"
1634		" (TypedVariableLink"
1635		" (VariableNode \"$X\")"
1636		" (TypeNode \"ConceptNode\")"
1637		" )"
1638		" (AndLink"
1639		" (VariableNode \"$Q-496643b4\")"
1640		" (EvaluationLink"
1641		" (PredicateNode \"take\")"
1642		" (ListLink"
1643		" (VariableNode \"$X\")"
1644		" (ConceptNode \"treatment-1\")"
1645		" )"
1646		" )"
1647		" )"
1648		" )"
1649		")");
1650
1651		Handle alpha_pat =
1652		_eval.eval_h("(ImplicationLink"
1653		" (AndLink"
1654		" (QuoteLink"
1655		" (LambdaLink"
1656		" (UnquoteLink"
1657		" (VariableNode \"$TyVs-3e93b595\")"
1658		" )"
1659		" (UnquoteLink"
1660		" (VariableNode \"$A1-4fd556f2\")"
1661		" )"
1662		" )"
1663		" )"
1664		" (QuoteLink"
1665		" (LambdaLink"
1666		" (UnquoteLink"
1667		" (VariableNode \"$TyVs-3e93b595\")"
1668		" )"
1669		" (UnquoteLink"
1670		" (VariableNode \"$A2-76df4103\")"
1671		" )"
1672		" )"
1673		" )"
1674		" )"
1675		" (QuoteLink"
1676		" (LambdaLink"
1677		" (UnquoteLink"
1678		" (VariableNode \"$TyVs-3e93b595\")"
1679		" )"
1680		" (UnquoteLink"
1681		" (AndLink"
1682		" (VariableNode \"$A1-4fd556f2\")"
1683		" (VariableNode \"$A2-76df4103\")"
1684		" )"
1685		" )"
1686		" )"
1687		" )"
1688		")");
1689
1690		Handle vardecl =
1691		_eval.eval_h("(VariableNode \"$Q-496643b4\")");
1692
1693		Handle alpha_vardecl =
1694		_eval.eval_h("(VariableList"
1695		" (TypedVariableLink"
1696		" (VariableNode \"$TyVs-3e93b595\")"
1697		" (TypeChoice"
1698		" (TypeNode \"TypedVariableLink\")"
1699		" (TypeNode \"VariableNode\")"
1700		" (TypeNode \"VariableList\")"
1701		" )"
1702		" )"
1703		" (TypedVariableLink"
1704		" (VariableNode \"$A1-4fd556f2\")"
1705		" (TypeNode \"EvaluationLink\")"
1706		" )"
1707		" (TypedVariableLink"
1708		" (VariableNode \"$A2-76df4103\")"
1709		" (TypeNode \"EvaluationLink\")"
1710		" )"
1711		")");
1712
1713		Handle Q = _eval.eval_h("(VariableNode \"$Q-496643b4\")");
1714		Handle TyVs = _eval.eval_h("(VariableNode \"$TyVs-3e93b595\")");
1715		Handle A1 = _eval.eval_h("(VariableNode \"$A1-4fd556f2\")");
1716		Handle A2 = _eval.eval_h("(VariableNode \"$A2-76df4103\")");
1717
1718		Handle lambda_vardecl =
1719		_eval.eval_h("(TypedVariableLink"
1720		" (VariableNode \"$X\")"
1721		" (TypeNode \"ConceptNode\"))");
1722
1723		Handle take_treatment_1 =
1724		_eval.eval_h("(EvaluationLink"
1725		" (PredicateNode \"take\")"
1726		" (ListLink"
1727		" (VariableNode \"$X\")"
1728		" (ConceptNode \"treatment-1\")))");
1729
1730		Context C(Quotation(), {X}, true, X_varstack);
1731		Unify::CHandle CQ(Q, C),
1732		Clambda_vardecl(lambda_vardecl, C),
1733		Ctake_treatment_1(take_treatment_1, C);
1734
1735		Unify unify(target, alpha_pat, vardecl, alpha_vardecl);
1736		Unify::SolutionSet result = unify(),
1737		expected = Unify::SolutionSet({{{{CQ, A1}, A1},
1738		{{TyVs, Clambda_vardecl},
1739		Clambda_vardecl},
1740		{{A2, Ctake_treatment_1},
1741		Ctake_treatment_1}},
1742		{{{CQ, A1, A2, Ctake_treatment_1},
1743		Ctake_treatment_1},
1744		{{TyVs, Clambda_vardecl},
1745		Clambda_vardecl}},
1746		{{{CQ, A2}, A2},
1747		{{TyVs, Clambda_vardecl},
1748		Clambda_vardecl},
1749		{{A1, Ctake_treatment_1},
1750		Ctake_treatment_1}}});
1751
1752		logger().debug() << "result = " << oc_to_string(result);
1753		logger().debug() << "expected = " << oc_to_string(expected);
1754
1755		TS_ASSERT_EQUALS(result, expected);
1756
1757		logger().info("END TEST: %s", __FUNCTION__);
1758		}
1759
1760		void UnifyUTest::test_unify_complex_7()
1761		{
1762		logger().info("BEGIN TEST: %s", __FUNCTION__);
1763
1764		Handle target =
1765		_eval.eval_h("(LambdaLink"
1766		" (TypedVariableLink"
1767		" (VariableNode \"$X\")"
1768		" (TypeNode \"ConceptNode\")"
1769		" )"
1770		" (EvaluationLink"
1771		" (PredicateNode \"contain\")"
1772		" (ListLink"
1773		" (ConceptNode \"treatment-1\")"
1774		" (ConceptNode \"compound-A\")"
1775		" )"
1776		" )"
1777		")");
1778
1779		Handle alpha_pat =
1780		_eval.eval_h("(QuoteLink"
1781		" (LambdaLink"
1782		" (UnquoteLink"
1783		" (VariableNode \"$V-6c74a409\")"
1784		" )"
1785		" (UnquoteLink"
1786		" (VariableNode \"$B-6266d6f2\")"
1787		" )"
1788		" )"
1789		")");
1790
1791		Handle vardecl;
1792
1793		Handle alpha_vardecl =
1794		_eval.eval_h("(VariableList"
1795		" (TypedVariableLink"
1796		" (VariableNode \"$V-6c74a409\")"
1797		" (TypeChoice"
1798		" (TypeNode \"TypedVariableLink\")"
1799		" (TypeNode \"VariableNode\")"
1800		" (TypeNode \"VariableList\")"
1801		" )"
1802		" )"
1803		" (VariableNode \"$B-6266d6f2\")"
1804		")");
1805
1806		Handle V = _eval.eval_h("(VariableNode \"$V-6c74a409\")");
1807		Handle B = _eval.eval_h("(VariableNode \"$B-6266d6f2\")");
1808		Handle X_vardecl =
1809		_eval.eval_h("(TypedVariableLink"
1810		" (VariableNode \"$X\")"
1811		" (TypeNode \"ConceptNode\")"
1812		")");
1813		Handle body =
1814		_eval.eval_h("(EvaluationLink"
1815		" (PredicateNode \"contain\")"
1816		" (ListLink"
1817		" (ConceptNode \"treatment-1\")"
1818		" (ConceptNode \"compound-A\")"
1819		" )"
1820		")");
1821
1822		Context C(Quotation(), {X}, true, X_varstack);
1823		Unify::CHandle CX_vardecl(X_vardecl, C), Cbody(body, C);
1824
1825		Unify unify(target, alpha_pat, vardecl, alpha_vardecl);
1826		Unify::SolutionSet result = unify(),
1827		expected = Unify::SolutionSet({{{{V, CX_vardecl}, CX_vardecl},
1828		{{B, Cbody}, Cbody}}});
1829
1830		logger().debug() << "result = " << oc_to_string(result);
1831		logger().debug() << "expected = " << oc_to_string(expected);
1832
1833		TS_ASSERT_EQUALS(result, expected);
1834
1835		Handle ts_vardecl = al(VARIABLE_LIST);
1836
1837		Unify::TypedSubstitutions ts_result =
1838		unify.typed_substitutions(result, target);
1839		Unify::TypedSubstitutions ts_expected =
1840		Unify::TypedSubstitutions{{{{V, CX_vardecl},
1841		{B, Cbody}},
1842		ts_vardecl}};
1843
1844		logger().debug() << "ts_result = " << oc_to_string(ts_result);
1845		logger().debug() << "ts_expected = " << oc_to_string(ts_expected);
1846
1847		TS_ASSERT(tss_content_eq(ts_result, ts_expected));
1848
1849		logger().info("END TEST: %s", __FUNCTION__);
1850		}
1851
1852		void UnifyUTest::test_unify_complex_8()
1853		{
1854		logger().info("BEGIN TEST: %s", __FUNCTION__);
1855
1856		Handle target =
1857		_eval.eval_h("(QuoteLink"
1858		" (LambdaLink"
1859		" (UnquoteLink"
1860		" (VariableNode \"$x\")"
1861		" )"
1862		" (UnquoteLink"
1863		" (VariableNode \"$g\")"
1864		" )"
1865		" )"
1866		")");
1867
1868		Handle alpha_pat =
1869		_eval.eval_h("(LambdaLink"
1870		" (VariableNode \"$X\")"
1871		" (VariableNode \"$X\")"
1872		")");
1873
1874		Handle vardecl =
1875		_eval.eval_h("(VariableList"
1876		" (TypedVariableLink"
1877		" (VariableNode \"$x\")"
1878		" (TypeNode \"VariableNode\")"
1879		" )"
1880		" (VariableNode \"$g\")"
1881		")");
1882
1883		Handle alpha_vardecl;
1884
1885		Handle x_var = _eval.eval_h("(VariableNode \"$x\")");
1886		Handle g_var = _eval.eval_h("(VariableNode \"$g\")");
1887		Handle X = _eval.eval_h("(VariableNode \"$X\")");
1888
1889		Context C(Quotation(), {X}, true, {Variables{X}});
1890		Unify::CHandle CX(X, C);
1891
1892		Unify unify(target, alpha_pat, vardecl, alpha_vardecl);
1893		Unify::SolutionSet result = unify(),
1894		expected = Unify::SolutionSet({{{{x_var, g_var, CX}, CX}}});
1895
1896		logger().debug() << "result = " << oc_to_string(result);
1897		logger().debug() << "expected = " << oc_to_string(expected);
1898
1899		TS_ASSERT_EQUALS(result, expected);
1900
1901		logger().info("END TEST: %s", __FUNCTION__);
1902		}
1903
1904		void UnifyUTest::test_unify_complex_9()
1905		{
1906		logger().info("BEGIN TEST: %s", __FUNCTION__);
1907
1908		Handle target =
1909		_eval.eval_h("(EvaluationLink"
1910		" (PredicateNode \"minsup\")"
1911		" (ListLink"
1912		" (QuoteLink"
1913		" (LambdaLink"
1914		" (UnquoteLink"
1915		" (VariableNode \"$x\")"
1916		" )"
1917		" (UnquoteLink"
1918		" (VariableNode \"$g\")"
1919		" )"
1920		" )"
1921		" )"
1922		" (ConceptNode \"texts\")"
1923		" (NumberNode \"2.000000\")"
1924		" )"
1925		")");
1926
1927		Handle alpha_pat =
1928		_eval.eval_h("(EvaluationLink"
1929		" (PredicateNode \"minsup\")"
1930		" (ListLink"
1931		" (LambdaLink"
1932		" (VariableNode \"$X\")"
1933		" (VariableNode \"$X\")"
1934		" )"
1935		" (VariableNode \"$texts\")"
1936		" (VariableNode \"$ms\")"
1937		" )"
1938		")");
1939
1940		Handle vardecl =
1941		_eval.eval_h("(VariableList"
1942		" (TypedVariableLink"
1943		" (VariableNode \"$x\")"
1944		" (TypeNode \"VariableNode\")"
1945		" )"
1946		" (VariableNode \"$g\")"
1947		" (TypedVariableLink"
1948		" (VariableNode \"$f\")"
1949		" (TypeNode \"LambdaLink\")"
1950		" )"
1951		")");
1952
1953		Handle alpha_vardecl =
1954		_eval.eval_h("(VariableList"
1955		" (TypedVariableLink"
1956		" (VariableNode \"$texts\")"
1957		" (TypeNode \"ConceptNode\")"
1958		" )"
1959		" (TypedVariableLink"
1960		" (VariableNode \"$ms\")"
1961		" (TypeNode \"NumberNode\")"
1962		" )"
1963		")");
1964
1965		Handle x_var = _eval.eval_h("(VariableNode \"$x\")");
1966		Handle f_var = _eval.eval_h("(VariableNode \"$f\")");
1967		Handle g_var = _eval.eval_h("(VariableNode \"$g\")");
1968		Handle texts_var = _eval.eval_h("(VariableNode \"$texts\")");
1969		Handle ms_var = _eval.eval_h("(VariableNode \"$ms\")");
1970		Handle X = _eval.eval_h("(VariableNode \"$X\")");
1971		Handle texts = _eval.eval_h("(ConceptNode \"texts\")");
1972		Handle ms = _eval.eval_h("(NumberNode \"2.0\")");
1973
1974		Context C(Quotation(), {X}, true, {Variables{X}});
1975		Unify::CHandle CX(X, C);
1976
1977		Unify unify(target, alpha_pat, vardecl, alpha_vardecl);
1978		Unify::SolutionSet result = unify(),
1979		expected = Unify::SolutionSet({{{{x_var, g_var, CX}, CX},
1980		{{texts_var, texts}, texts},
1981		{{ms_var, ms}, ms}}});
1982
1983		logger().debug() << "result = " << oc_to_string(result);
1984		logger().debug() << "expected = " << oc_to_string(expected);
1985
1986		TS_ASSERT_EQUALS(result, expected);
1987
1988		logger().info("END TEST: %s", __FUNCTION__);
1989		}
1990
1991		void UnifyUTest::test_unify_complex_10()
1992		{
1993		logger().info("BEGIN TEST: %s", __FUNCTION__);
1994
1995		Handle target =
1996		_eval.eval_h("(EvaluationLink"
1997		" (PredicateNode \"minsup\")"
1998		" (ListLink"
1999		" (QuoteLink"
2000		" (PutLink"
2001		" (LambdaLink"
2002		" (VariableNode \"$top-arg\")"
2003		" (VariableNode \"$top-arg\")"
2004		" )"
2005		" (UnquoteLink"
2006		" (VariableNode \"$patvar\")"
2007		" )"
2008		" )"
2009		" )"
2010		" (ConceptNode \"texts\")"
2011		" (NumberNode \"2\")"
2012		" )"
2013		")");
2014
2015		Handle alpha_pat =
2016		_eval.eval_h("(EvaluationLink"
2017		" (PredicateNode \"minsup\")"
2018		" (ListLink"
2019		" (QuoteLink"
2020		" (PutLink"
2021		" (UnquoteLink"
2022		" (VariableNode \"$g\")"
2023		" )"
2024		" (UnquoteLink"
2025		" (VariableNode \"$f\")"
2026		" )"
2027		" )"
2028		" )"
2029		" (VariableNode \"$texts\")"
2030		" (VariableNode \"$ms\")"
2031		" )"
2032		")");
2033
2034		Handle vardecl =
2035		_eval.eval_h("(VariableNode \"$patvar\")");
2036
2037		Handle alpha_vardecl =
2038		_eval.eval_h("(VariableList"
2039		" (TypedVariableLink"
2040		" (VariableNode \"$g\")"
2041		" (TypeChoice"
2042		" (TypeNode \"LambdaLink\")"
2043		" (TypeNode \"PutLink\")"
2044		" )"
2045		" )"
2046		" (TypedVariableLink"
2047		" (VariableNode \"$texts\")"
2048		" (TypeNode \"ConceptNode\")"
2049		" )"
2050		" (TypedVariableLink"
2051		" (VariableNode \"$ms\")"
2052		" (TypeNode \"NumberNode\")"
2053		" )"
2054		" (TypedVariableLink"
2055		" (VariableNode \"$f\")"
2056		" (TypeChoice"
2057		" (TypeNode \"LambdaLink\")"
2058		" (TypeNode \"ConceptNode\")"
2059		" )"
2060		" )"
2061		")");
2062
2063		Handle g_var = _eval.eval_h("(VariableNode \"$g\")");
2064		Handle top = _eval.eval_h("(LambdaLink"
2065		" (VariableNode \"$top-arg\")"
2066		" (VariableNode \"$top-arg\"))");
2067		Unify::CHandle Ctop(top, Quotation(1));
2068		Handle pat_var = _eval.eval_h("(VariableNode \"$patvar\")");
2069		Handle f_var = _eval.eval_h("(VariableNode \"$f\")");
2070		Handle texts_var = _eval.eval_h("(VariableNode \"$texts\")");
2071		Handle texts = _eval.eval_h("(ConceptNode \"texts\")");
2072		Handle ms_var = _eval.eval_h("(VariableNode \"$ms\")");
2073		Handle ms = _eval.eval_h("(NumberNode \"2\")");
2074
2075		Unify unify(target, alpha_pat, vardecl, alpha_vardecl);
2076		Unify::SolutionSet result = unify(),
2077		expected = Unify::SolutionSet({{{{g_var, Ctop}, Ctop},
2078		{{pat_var, f_var}, f_var},
2079		{{texts_var, texts}, texts},
2080		{{ms_var, ms}, ms}}});
2081
2082		logger().debug() << "result = " << oc_to_string(result);
2083		logger().debug() << "expected = " << oc_to_string(expected);
2084
2085		TS_ASSERT_EQUALS(result, expected);
2086
2087		Handle ts_vardecl = _eval.eval_h("(TypedVariableLink"
2088		" (VariableNode \"$f\")"
2089		" (TypeChoice"
2090		" (TypeNode \"ConceptNode\")"
2091		" (TypeNode \"LambdaLink\")"
2092		" )"
2093		")");
2094
2095		Unify::TypedSubstitutions ts_result =
2096		unify.typed_substitutions(result, target);
2097		Unify::TypedSubstitutions ts_expected =
2098		Unify::TypedSubstitutions{{{{texts_var, texts},
2099		{g_var, Ctop},
2100		{f_var, f_var},
2101		{ms_var, ms},
2102		{pat_var, f_var}},
2103		ts_vardecl}};
2104
2105		logger().debug() << "ts_result = " << oc_to_string(ts_result);
2106		logger().debug() << "ts_expected = " << oc_to_string(ts_expected);
2107
2108		TS_ASSERT(tss_content_eq(ts_result, ts_expected));
2109
2110		logger().info("END TEST: %s", __FUNCTION__);
2111		}
2112
2113		/**
2114		* Test unification and substitution on a complex hypergraph
2115		*/
2116		void UnifyUTest::test_unify_complex_11()
2117		{
2118		logger().info("BEGIN TEST: %s", __FUNCTION__);
2119
2120		// Hypergraph to substitute after unification
2121		Handle bl =
2122		_eval.eval_h("(BindLink"
2123		" (VariableList"
2124		" (TypedVariableLink"
2125		" (VariableNode \"$g\")"
2126		" (TypeChoice"
2127		" (TypeNode \"LambdaLink\")"
2128		" (TypeNode \"PutLink\")"
2129		" )"
2130		" )"
2131		" (TypedVariableLink"
2132		" (VariableNode \"$texts\")"
2133		" (TypeNode \"ConceptNode\")"
2134		" )"
2135		" (TypedVariableLink"
2136		" (VariableNode \"$ms\")"
2137		" (TypeNode \"NumberNode\")"
2138		" )"
2139		" (TypedVariableLink"
2140		" (VariableNode \"$f\")"
2141		" (TypeChoice"
2142		" (TypeNode \"LambdaLink\")"
2143		" (TypeNode \"PutLink\")"
2144		" (TypeNode \"ConceptNode\")"
2145		" )"
2146		" )"
2147		" )"
2148		" (AndLink"
2149		" (VariableNode \"$f\")"
2150		" (EvaluationLink"
2151		" (PredicateNode \"minsup\")"
2152		" (ListLink"
2153		" (VariableNode \"$g\")"
2154		" (VariableNode \"$texts\")"
2155		" (VariableNode \"$ms\")"
2156		" )"
2157		" )"
2158		" (EvaluationLink"
2159		" (GroundedPredicateNode \"scm: absolutely-true\")"
2160		" (EvaluationLink"
2161		" (PredicateNode \"minsup\")"
2162		" (ListLink"
2163		" (VariableNode \"$g\")"
2164		" (VariableNode \"$texts\")"
2165		" (VariableNode \"$ms\")"
2166		" )"
2167		" )"
2168		" )"
2169		" (EvaluationLink"
2170		" (GroundedPredicateNode \"scm: has-arity\")"
2171		" (ListLink"
2172		" (VariableNode \"$g\")"
2173		" (NumberNode \"2\")"
2174		" )"
2175		" )"
2176		" )"
2177		" (ExecutionOutputLink"
2178		" (GroundedSchemaNode \"scm: specialization-formula\")"
2179		" (ListLink"
2180		" (EvaluationLink"
2181		" (PredicateNode \"minsup\")"
2182		" (ListLink"
2183		" (QuoteLink"
2184		" (PutLink"
2185		" (UnquoteLink"
2186		" (VariableNode \"$g\")"
2187		" )"
2188		" (UnquoteLink"
2189		" (ListLink"
2190		" (VariableNode \"$spe-arg-0\")"
2191		" (VariableNode \"$f\")"
2192		" )"
2193		" )"
2194		" )"
2195		" )"
2196		" (VariableNode \"$texts\")"
2197		" (VariableNode \"$ms\")"
2198		" )"
2199		" )"
2200		" (EvaluationLink"
2201		" (PredicateNode \"minsup\")"
2202		" (ListLink"
2203		" (VariableNode \"$g\")"
2204		" (VariableNode \"$texts\")"
2205		" (VariableNode \"$ms\")"
2206		" )"
2207		" )"
2208		" (VariableNode \"$f\")"
2209		" )"
2210		" )"
2211		")");
2212
2213		// Sub-element of bl to unify with
2214		Handle target =
2215		_eval.eval_h("(EvaluationLink"
2216		" (PredicateNode \"minsup\")"
2217		" (ListLink"
2218		" (QuoteLink"
2219		" (PutLink"
2220		" (PutLink"
2221		" (LambdaLink"
2222		" (VariableNode \"$top-arg\")"
2223		" (VariableNode \"$top-arg\")"
2224		" )"
2225		" (UnquoteLink"
2226		" (VariableNode \"$shapat-0\")"
2227		" )"
2228		" )"
2229		" (UnquoteLink"
2230		" (VariableNode \"$shapat-1\")"
2231		" )"
2232		" )"
2233		" )"
2234		" (ConceptNode \"texts\")"
2235		" (NumberNode \"2\")"
2236		" )"
2237		")");
2238
2239		Handle alpha_pat =
2240		_eval.eval_h("(EvaluationLink"
2241		" (PredicateNode \"minsup\")"
2242		" (ListLink"
2243		" (QuoteLink"
2244		" (PutLink"
2245		" (UnquoteLink"
2246		" (VariableNode \"$g\")"
2247		" )"
2248		" (UnquoteLink"
2249		" (ListLink"
2250		" (VariableNode \"$spe-arg-0\")"
2251		" (VariableNode \"$f\")"
2252		" )"
2253		" )"
2254		" )"
2255		" )"
2256		" (VariableNode \"$texts\")"
2257		" (VariableNode \"$ms\")"
2258		" )"
2259		")");
2260
2261		Handle vardecl =
2262		_eval.eval_h("(VariableList"
2263		" (VariableNode \"$shapat-1\")"
2264		" (VariableNode \"$shapat-0\")"
2265		")");
2266
2267		Handle alpha_vardecl =
2268		_eval.eval_h("(VariableList"
2269		" (TypedVariableLink"
2270		" (VariableNode \"$g\")"
2271		" (TypeChoice"
2272		" (TypeNode \"LambdaLink\")"
2273		" (TypeNode \"PutLink\")"
2274		" )"
2275		" )"
2276		" (TypedVariableLink"
2277		" (VariableNode \"$texts\")"
2278		" (TypeNode \"ConceptNode\")"
2279		" )"
2280		" (TypedVariableLink"
2281		" (VariableNode \"$ms\")"
2282		" (TypeNode \"NumberNode\")"
2283		" )"
2284		" (TypedVariableLink"
2285		" (VariableNode \"$f\")"
2286		" (TypeChoice"
2287		" (TypeNode \"LambdaLink\")"
2288		" (TypeNode \"PutLink\")"
2289		" (TypeNode \"ConceptNode\")"
2290		" )"
2291		" )"
2292		")");
2293
2294		Handle shapat1_var = _eval.eval_h("(VariableNode \"$shapat-1\")");
2295		Handle spef_list = _eval.eval_h("(ListLink"
2296		" (VariableNode \"$spe-arg-0\")"
2297		" (VariableNode \"$f\"))");
2298		Handle ms_var = _eval.eval_h("(VariableNode \"$ms\")");
2299		Handle ms = _eval.eval_h("(NumberNode \"2\")");
2300		Handle texts_var = _eval.eval_h("(VariableNode \"$texts\")");
2301		Handle texts = _eval.eval_h("(ConceptNode \"texts\")");
2302		Handle g_var = _eval.eval_h("(VariableNode \"$g\")");
2303		Handle put_top = _eval.eval_h("(PutLink"
2304		" (LambdaLink"
2305		" (VariableNode \"$top-arg\")"
2306		" (VariableNode \"$top-arg\"))"
2307		" (UnquoteLink"
2308		" (VariableNode \"$shapat-0\")))");
2309		Unify::CHandle Cput_top(put_top, Quotation(1));
2310
2311		// Test unification
2312		Unify unify(target, alpha_pat, vardecl, alpha_vardecl);
2313		Unify::SolutionSet result = unify(),
2314		expected = Unify::SolutionSet({{{{shapat1_var, spef_list}, spef_list},
2315		{{ms_var, ms}, ms},
2316		{{texts_var, texts}, texts},
2317		{{g_var, Cput_top}, Cput_top}}});
2318
2319		logger().debug() << "result = " << oc_to_string(result);
2320		logger().debug() << "expected = " << oc_to_string(expected);
2321
2322		TS_ASSERT_EQUALS(result, expected);
2323
2324		// Test substitution structure construction
2325		Handle ts_vardecl = _eval.eval_h("(VariableList"
2326		" (VariableNode \"$shapat-0\")"
2327		" (TypedVariableLink"
2328		" (VariableNode \"$f\")"
2329		" (TypeChoice"
2330		" (TypeNode \"ConceptNode\")"
2331		" (TypeNode \"LambdaLink\")"
2332		" (TypeNode \"PutLink\"))))");
2333
2334		Unify::TypedSubstitutions ts_result =
2335		unify.typed_substitutions(result, target);
2336		Unify::TypedSubstitutions ts_expected =
2337		Unify::TypedSubstitutions{{{{shapat1_var, spef_list},
2338		{ms_var, ms},
2339		{g_var, Cput_top},
2340		{texts_var, texts}},
2341		ts_vardecl}};
2342
2343		logger().debug() << "ts_result = " << oc_to_string(ts_result);
2344		logger().debug() << "ts_expected = " << oc_to_string(ts_expected);
2345
2346		TS_ASSERT(tss_content_eq(ts_result, ts_expected));
2347
2348		// Test substitution itself
2349		BindLinkPtr blptr = BindLinkCast(bl);
2350		Handle sub_result = Unify::substitute(blptr, *ts_result.begin());
2351		Handle sub_expected =
2352		_eval.eval_h("(BindLink"
2353		" (VariableList"
2354		" (VariableNode \"$shapat-0\")"
2355		" (TypedVariableLink"
2356		" (VariableNode \"$f\")"
2357		" (TypeChoice"
2358		" (TypeNode \"LambdaLink\")"
2359		" (TypeNode \"PutLink\")"
2360		" (TypeNode \"ConceptNode\")"
2361		" )"
2362		" )"
2363		" )"
2364		" (AndLink"
2365		" (VariableNode \"$f\")"
2366		" (EvaluationLink"
2367		" (PredicateNode \"minsup\")"
2368		" (ListLink"
2369		" (QuoteLink"
2370		" (PutLink"
2371		" (LambdaLink"
2372		" (VariableNode \"$top-arg\")"
2373		" (VariableNode \"$top-arg\")"
2374		" )"
2375		" (UnquoteLink"
2376		" (VariableNode \"$shapat-0\")"
2377		" )"
2378		" )"
2379		" )"
2380		" (ConceptNode \"texts\")"
2381		" (NumberNode \"2\")"
2382		" )"
2383		" )"
2384		" (EvaluationLink"
2385		" (GroundedPredicateNode \"scm: absolutely-true\")"
2386		" (EvaluationLink"
2387		" (PredicateNode \"minsup\")"
2388		" (ListLink"
2389		" (QuoteLink"
2390		" (PutLink"
2391		" (LambdaLink"
2392		" (VariableNode \"$top-arg\")"
2393		" (VariableNode \"$top-arg\")"
2394		" )"
2395		" (UnquoteLink"
2396		" (VariableNode \"$shapat-0\")"
2397		" )"
2398		" )"
2399		" )"
2400		" (ConceptNode \"texts\")"
2401		" (NumberNode \"2\")"
2402		" )"
2403		" )"
2404		" )"
2405		" (EvaluationLink"
2406		" (GroundedPredicateNode \"scm: has-arity\")"
2407		" (ListLink"
2408		" (QuoteLink"
2409		" (PutLink"
2410		" (LambdaLink"
2411		" (VariableNode \"$top-arg\")"
2412		" (VariableNode \"$top-arg\")"
2413		" )"
2414		" (UnquoteLink"
2415		" (VariableNode \"$shapat-0\")"
2416		" )"
2417		" )"
2418		" )"
2419		" (NumberNode \"2\")"
2420		" )"
2421		" )"
2422		" )"
2423		" (ExecutionOutputLink"
2424		" (GroundedSchemaNode \"scm: specialization-formula\")"
2425		" (ListLink"
2426		" (EvaluationLink"
2427		" (PredicateNode \"minsup\")"
2428		" (ListLink"
2429		" (QuoteLink"
2430		" (PutLink"
2431		" (PutLink"
2432		" (LambdaLink"
2433		" (VariableNode \"$top-arg\")"
2434		" (VariableNode \"$top-arg\")"
2435		" )"
2436		" (UnquoteLink"
2437		" (VariableNode \"$shapat-0\")"
2438		" )"
2439		" )"
2440		" (UnquoteLink"
2441		" (ListLink"
2442		" (VariableNode \"$spe-arg-0\")"
2443		" (VariableNode \"$f\")"
2444		" )"
2445		" )"
2446		" )"
2447		" )"
2448		" (ConceptNode \"texts\")"
2449		" (NumberNode \"2\")"
2450		" )"
2451		" )"
2452		" (EvaluationLink"
2453		" (PredicateNode \"minsup\")"
2454		" (ListLink"
2455		" (QuoteLink"
2456		" (PutLink"
2457		" (LambdaLink"
2458		" (VariableNode \"$top-arg\")"
2459		" (VariableNode \"$top-arg\")"
2460		" )"
2461		" (UnquoteLink"
2462		" (VariableNode \"$shapat-0\")"
2463		" )"
2464		" )"
2465		" )"
2466		" (ConceptNode \"texts\")"
2467		" (NumberNode \"2\")"
2468		" )"
2469		" )"
2470		" (VariableNode \"$f\")"
2471		" )"
2472		" )"
2473		")");
2474
2475		logger().debug() << "sub_result = " << oc_to_string(sub_result);
2476		logger().debug() << "sub_expected = " << oc_to_string(sub_expected);
2477
2478		TS_ASSERT(content_eq(sub_result, sub_expected));
2479
2480		logger().info("END TEST: %s", __FUNCTION__);
2481		}
2482
2483		/**
2484		* Test unification and substitution on a complex hypergraph
2485		*/
2486		void UnifyUTest::test_unify_complex_12()
2487		{
2488		logger().info("BEGIN TEST: %s", __FUNCTION__);
2489
2490		// Hypergraph to substitute after unification
2491		Handle bl =
2492		_eval.eval_h("(BindLink"
2493		" (VariableList"
2494		" (TypedVariableLink"
2495		" (VariableNode \"$g\")"
2496		" (TypeChoice"
2497		" (TypeNode \"LambdaLink\")"
2498		" (TypeNode \"PutLink\")"
2499		" )"
2500		" )"
2501		" (TypedVariableLink"
2502		" (VariableNode \"$texts\")"
2503		" (TypeNode \"ConceptNode\")"
2504		" )"
2505		" (TypedVariableLink"
2506		" (VariableNode \"$ms\")"
2507		" (TypeNode \"NumberNode\")"
2508		" )"
2509		" (TypedVariableLink"
2510		" (VariableNode \"$f\")"
2511		" (TypeNode \"LambdaLink\")"
2512		" )"
2513		" )"
2514		" (AndLink"
2515		" (VariableNode \"$f\")"
2516		" (EvaluationLink"
2517		" (PredicateNode \"minsup\")"
2518		" (ListLink"
2519		" (VariableNode \"$g\")"
2520		" (VariableNode \"$texts\")"
2521		" (VariableNode \"$ms\")"
2522		" )"
2523		" )"
2524		" (EvaluationLink"
2525		" (GroundedPredicateNode \"scm: absolutely-true\")"
2526		" (EvaluationLink"
2527		" (PredicateNode \"minsup\")"
2528		" (ListLink"
2529		" (VariableNode \"$g\")"
2530		" (VariableNode \"$texts\")"
2531		" (VariableNode \"$ms\")"
2532		" )"
2533		" )"
2534		" )"
2535		" (EvaluationLink"
2536		" (GroundedPredicateNode \"scm: has-arity\")"
2537		" (ListLink"
2538		" (VariableNode \"$g\")"
2539		" (NumberNode \"3\")"
2540		" )"
2541		" )"
2542		" )"
2543		" (ExecutionOutputLink"
2544		" (GroundedSchemaNode \"scm: composition-formula\")"
2545		" (ListLink"
2546		" (EvaluationLink"
2547		" (PredicateNode \"minsup\")"
2548		" (ListLink"
2549		" (QuoteLink"
2550		" (PutLink"
2551		" (UnquoteLink"
2552		" (VariableNode \"$g\")"
2553		" )"
2554		" (UnquoteLink"
2555		" (ListLink"
2556		" (VariableNode \"$spe-arg-0\")"
2557		" (VariableNode \"$spe-arg-1\")"
2558		" (VariableNode \"$f\")"
2559		" )"
2560		" )"
2561		" )"
2562		" )"
2563		" (VariableNode \"$texts\")"
2564		" (VariableNode \"$ms\")"
2565		" )"
2566		" )"
2567		" (EvaluationLink"
2568		" (PredicateNode \"minsup\")"
2569		" (ListLink"
2570		" (VariableNode \"$g\")"
2571		" (VariableNode \"$texts\")"
2572		" (VariableNode \"$ms\")"
2573		" )"
2574		" )"
2575		" (VariableNode \"$f\")"
2576		" )"
2577		" )"
2578		")");
2579
2580		// Sub-element of bl to unify with
2581		Handle target =
2582		_eval.eval_h("(EvaluationLink"
2583		" (PredicateNode \"minsup\")"
2584		" (ListLink"
2585		" (QuoteLink"
2586		" (PutLink"
2587		" (LambdaLink"
2588		" (VariableNode \"$top-arg\")"
2589		" (VariableNode \"$top-arg\")"
2590		" )"
2591		" (UnquoteLink"
2592		" (VariableNode \"$shapat-0\")"
2593		" )"
2594		" )"
2595		" )"
2596		" (ConceptNode \"texts\")"
2597		" (NumberNode \"2\")"
2598		" )"
2599		")");
2600
2601		Handle alpha_pat =
2602		_eval.eval_h("(EvaluationLink"
2603		" (PredicateNode \"minsup\")"
2604		" (ListLink"
2605		" (QuoteLink"
2606		" (PutLink"
2607		" (UnquoteLink"
2608		" (VariableNode \"$g\")"
2609		" )"
2610		" (UnquoteLink"
2611		" (ListLink"
2612		" (VariableNode \"$spe-arg-0\")"
2613		" (VariableNode \"$spe-arg-1\")"
2614		" (VariableNode \"$f\")"
2615		" )"
2616		" )"
2617		" )"
2618		" )"
2619		" (VariableNode \"$texts\")"
2620		" (VariableNode \"$ms\")"
2621		" )"
2622		")");
2623
2624		Handle vardecl =
2625		_eval.eval_h("(VariableNode \"$shapat-0\")");
2626
2627		Handle alpha_vardecl =
2628		_eval.eval_h("(VariableList"
2629		" (TypedVariableLink"
2630		" (VariableNode \"$g\")"
2631		" (TypeChoice"
2632		" (TypeNode \"LambdaLink\")"
2633		" (TypeNode \"PutLink\")"
2634		" )"
2635		" )"
2636		" (TypedVariableLink"
2637		" (VariableNode \"$texts\")"
2638		" (TypeNode \"ConceptNode\")"
2639		" )"
2640		" (TypedVariableLink"
2641		" (VariableNode \"$ms\")"
2642		" (TypeNode \"NumberNode\")"
2643		" )"
2644		" (TypedVariableLink"
2645		" (VariableNode \"$f\")"
2646		" (TypeNode \"LambdaLink\")"
2647		" )"
2648		")");
2649
2650		Handle shapat0_var = _eval.eval_h("(VariableNode \"$shapat-0\")");
2651		Handle spef_list = _eval.eval_h("(ListLink"
2652		" (VariableNode \"$spe-arg-0\")"
2653		" (VariableNode \"$spe-arg-1\")"
2654		" (VariableNode \"$f\"))");
2655		Handle ms_var = _eval.eval_h("(VariableNode \"$ms\")");
2656		Handle ms = _eval.eval_h("(NumberNode \"2\")");
2657		Handle texts_var = _eval.eval_h("(VariableNode \"$texts\")");
2658		Handle texts = _eval.eval_h("(ConceptNode \"texts\")");
2659		Handle g_var = _eval.eval_h("(VariableNode \"$g\")");
2660		Handle top = _eval.eval_h("(LambdaLink"
2661		" (VariableNode \"$top-arg\")"
2662		" (VariableNode \"$top-arg\"))");
2663		Unify::CHandle Ctop(top, Quotation(1));
2664
2665		// Test unification
2666		Unify unify(target, alpha_pat, vardecl, alpha_vardecl);
2667		Unify::SolutionSet result = unify(),
2668		expected = Unify::SolutionSet({{{{ms_var, ms}, ms},
2669		{{texts_var, texts}, texts},
2670		{{g_var, Ctop}, Ctop},
2671		{{shapat0_var, spef_list}, spef_list}}});
2672
2673		logger().debug() << "result = " << oc_to_string(result);
2674		logger().debug() << "expected = " << oc_to_string(expected);
2675
2676		TS_ASSERT_EQUALS(result, expected);
2677
2678		// Test substitution structure construction
2679		Handle ts_vardecl = _eval.eval_h("(TypedVariableLink"
2680		" (VariableNode \"$f\")"
2681		" (TypeNode \"LambdaLink\"))");
2682
2683		Unify::TypedSubstitutions ts_result =
2684		unify.typed_substitutions(result, target);
2685		Unify::TypedSubstitutions ts_expected =
2686		Unify::TypedSubstitutions{{{{ms_var, ms},
2687		{g_var, Ctop},
2688		{texts_var, texts},
2689		{shapat0_var, spef_list}},
2690		ts_vardecl}};
2691
2692		logger().debug() << "ts_result = " << oc_to_string(ts_result);
2693		logger().debug() << "ts_expected = " << oc_to_string(ts_expected);
2694
2695		TS_ASSERT(tss_content_eq(ts_result, ts_expected));
2696
2697		// Test substitution itself
2698		BindLinkPtr blptr = BindLinkCast(bl);
2699		Handle sub_result = Unify::substitute(blptr, *ts_result.begin());
2700		Handle sub_expected =
2701		_eval.eval_h("(BindLink"
2702		" (TypedVariableLink"
2703		" (VariableNode \"$f\")"
2704		" (TypeNode \"LambdaLink\")"
2705		" )"
2706		" (AndLink"
2707		" (VariableNode \"$f\")"
2708		" (EvaluationLink"
2709		" (GroundedPredicateNode \"scm: has-arity\")"
2710		" (ListLink"
2711		" (LambdaLink"
2712		" (VariableNode \"$top-arg\")"
2713		" (VariableNode \"$top-arg\")"
2714		" )"
2715		" (NumberNode \"3\")"
2716		" )"
2717		" )"
2718		" (EvaluationLink"
2719		" (PredicateNode \"minsup\")"
2720		" (ListLink"
2721		" (LambdaLink"
2722		" (VariableNode \"$top-arg\")"
2723		" (VariableNode \"$top-arg\")"
2724		" )"
2725		" (ConceptNode \"texts\")"
2726		" (NumberNode \"2\")"
2727		" )"
2728		" )"
2729		" (EvaluationLink"
2730		" (GroundedPredicateNode \"scm: absolutely-true\")"
2731		" (EvaluationLink"
2732		" (PredicateNode \"minsup\")"
2733		" (ListLink"
2734		" (LambdaLink"
2735		" (VariableNode \"$top-arg\")"
2736		" (VariableNode \"$top-arg\")"
2737		" )"
2738		" (ConceptNode \"texts\")"
2739		" (NumberNode \"2\")"
2740		" )"
2741		" )"
2742		" )"
2743		" )"
2744		" (ExecutionOutputLink"
2745		" (GroundedSchemaNode \"scm: composition-formula\")"
2746		" (ListLink"
2747		" (EvaluationLink"
2748		" (PredicateNode \"minsup\")"
2749		" (ListLink"
2750		" (QuoteLink"
2751		" (PutLink"
2752		" (LambdaLink"
2753		" (VariableNode \"$top-arg\")"
2754		" (VariableNode \"$top-arg\")"
2755		" )"
2756		" (UnquoteLink"
2757		" (ListLink"
2758		" (VariableNode \"$spe-arg-0\")"
2759		" (VariableNode \"$spe-arg-1\")"
2760		" (VariableNode \"$f\")"
2761		" )"
2762		" )"
2763		" )"
2764		" )"
2765		" (ConceptNode \"texts\")"
2766		" (NumberNode \"2\")"
2767		" )"
2768		" )"
2769		" (EvaluationLink"
2770		" (PredicateNode \"minsup\")"
2771		" (ListLink"
2772		" (LambdaLink"
2773		" (VariableNode \"$top-arg\")"
2774		" (VariableNode \"$top-arg\")"
2775		" )"
2776		" (ConceptNode \"texts\")"
2777		" (NumberNode \"2\")"
2778		" )"
2779		" )"
2780		" (VariableNode \"$f\")"
2781		" )"
2782		" )"
2783		")");
2784
2785		logger().debug() << "sub_result = " << oc_to_string(sub_result);
2786		logger().debug() << "sub_expected = " << oc_to_string(sub_expected);
2787
2788		TS_ASSERT(content_eq(sub_result, sub_expected));
2789
2790		logger().info("END TEST: %s", __FUNCTION__);
2791		}
2792
2793		#undef al
2794		#undef an

opencog-ure commits / 784d7c3

Changed files (11) +15 -5904