diff --git a/README.md b/README.md
index 74637df1f0c08bbf648611913e8bc0d0b7d2f404..b24b7212bf9ca06365a354d097da05222a31a635 100644
--- a/README.md
+++ b/README.md
@@ -2,9 +2,18 @@
Limbo is a *reasoning system for a first-order logic of **lim**ited
**b**elief*. Limited belief allows for decidable reasoning in first-order
-knowledge bases, and in the propositional case it is even tractable. See
-[\[1,2,3,4,5\]](#references) for details on the theory, or click
-[here](http://www.cse.unsw.edu.au/~cschwering/limbo/) to see some web demos.
+knowledge bases, and in the propositional case it is even tractable.
+
+Where to go from here?
+
+* You could check out the [web
+ demos](http://www.cse.unsw.edu.au/~cschwering/limbo/) to see limited
+ belief in action.
+* You could check out the code and [compile](#installation) it and run
+ Limbo on your computer.
+* You could have a look at one of the [papers](#references) on the
+ theory behind Limbo.
+* You could also send [me](http://www.cse.unsw.edu.au/~cschwering/) an email.
## Features
@@ -78,6 +87,8 @@ have `src/limbo` in the include path.
To compile and run the tests and demos, execute the following:
```shell
+$ git clone https://github.com/schwering/limbo.git
+$ cd limbo
$ git submodule init
$ git submodule update
$ cmake .
@@ -87,26 +98,30 @@ $ make test
## References
-1. C. Schwering.
- A Reasoning System for a First-Order Logic of Limited Belief.
- In *Proc. IJCAI*, 2017 (to appear).
- [PDF](http://www.cse.unsw.edu.au/~cschwering/ijcai-2017.pdf),
+The first paper is the most recent one and describes the theory behind Limbo.
+Many of the ideas were introduced in the earlier papers linked below.
+
+1. A Reasoning System for a First-Order Logic of Limited Belief.
+ C. Schwering.
+ In *Proc. IJCAI*, 2017 (to appear).
+ [pdf](http://www.cse.unsw.edu.au/~cschwering/ijcai-2017.pdf),
+ [proofs](https://arxiv.org/abs/1705.01817),
[slides](http://www.cse.unsw.edu.au/~cschwering/ijcai-2017-slides.pdf)
-2. G. Lakemeyer and H. Levesque.
- Decidable Reasoning in a Logic of Limited Belief with Function Symbols.
- In *Proc. KR*, 2016.
- [PDF](https://kbsg.rwth-aachen.de/sites/kbsg/files/LakemeyerLevesque2016.pdf)
-3. C. Schwering and G. Lakemeyer.
- Decidable Reasoning in a First-Order Logic of Limited Conditional Belief.
- In *Proc. ECAI*, 2016.
- [PDF](http://www.cse.unsw.edu.au/~cschwering/ecai-2016.pdf),
+2. Decidable Reasoning in a Logic of Limited Belief with Function Symbols.
+ G. Lakemeyer and H. Levesque.
+ In *Proc. KR*, 2016.
+ [pdf](https://kbsg.rwth-aachen.de/sites/kbsg/files/LakemeyerLevesque2016.pdf)
+3. Decidable Reasoning in a First-Order Logic of Limited Conditional Belief.
+ C. Schwering and G. Lakemeyer.
+ In *Proc. ECAI*, 2016.
+ [pdf](http://www.cse.unsw.edu.au/~cschwering/ecai-2016.pdf),
[slides](http://www.cse.unsw.edu.au/~cschwering/ecai-2016-slides.pdf)
-4. G. Lakemeyer and H. Levesque.
- Decidable Reasoning in a Fragment of the Epistemic Situation Calculus.
- In *Proc. KR*, 2014.
- [PDF](https://pdfs.semanticscholar.org/8ac9/a2955895cd391ec2b62d8210ee8206979f4a.pdf)
-5. G. Lakemeyer and H. Levesque.
- Decidable Reasoning in a Logic of Limited Belief with Introspection and Unknown Individuals.
- In *Proc. IJCAI*, 2013.
- [PDF](https://pdfs.semanticscholar.org/387c/951016c68aaf8ce36bb87e5ea4d1ef42405d.pdf)
+4. Decidable Reasoning in a Fragment of the Epistemic Situation Calculus.
+ G. Lakemeyer and H. Levesque.
+ In *Proc. KR*, 2014.
+ [pdf](https://pdfs.semanticscholar.org/8ac9/a2955895cd391ec2b62d8210ee8206979f4a.pdf)
+5. Decidable Reasoning in a Logic of Limited Belief with Introspection and Unknown Individuals.
+ G. Lakemeyer and H. Levesque.
+ In *Proc. IJCAI*, 2013.
+ [pdf](https://pdfs.semanticscholar.org/387c/951016c68aaf8ce36bb87e5ea4d1ef42405d.pdf)
diff --git a/src/limbo/formula.h b/src/limbo/formula.h
index 2c38a4d6fa2fd9d0eb275bf5b6d543c3ad474ad6..5c423ee8c37c7445e82b9953b62e6c7a1688d11c 100644
--- a/src/limbo/formula.h
+++ b/src/limbo/formula.h
@@ -14,6 +14,7 @@
#include
+#include
#include
#include
#include
@@ -24,6 +25,7 @@
#include
#include
+#include
#include
#include
@@ -34,6 +36,7 @@ class Formula {
typedef internal::size_t size_t;
typedef std::unique_ptr Ref;
typedef std::unordered_set TermSet;
+ typedef internal::IntMap SortMap;
typedef unsigned int split_level;
enum Type { kAtomic, kNot, kOr, kExists, kKnow, kCons, kBel, kGuarantee };
@@ -95,6 +98,8 @@ class Formula {
return free_vars_.val;
}
+ virtual SortMap n_vars() const = 0;
+
template
void SubstituteFree(UnaryFunction theta, Term::Factory* tf) {
class FreeSubstitution : public ISubstitution {
@@ -235,6 +240,14 @@ class Formula::Atomic : public Formula {
const Clause& arg() const { return c_; }
+ SortMap n_vars() const override {
+ SortMap m;
+ for (Term x : free_vars()) {
+ ++m[x.sort()];
+ }
+ return m;
+ }
+
bool objective() const override { return true; }
bool subjective() const override {
return std::all_of(c_.begin(), c_.end(), [](Literal a) { return !a.lhs().function() && !a.rhs().function(); });
@@ -383,6 +396,16 @@ class Formula::Or : public Formula {
const Formula& lhs() const { return *alpha_; }
const Formula& rhs() const { return *beta_; }
+ SortMap n_vars() const override {
+ SortMap m;
+ for (Term x : free_vars()) {
+ ++m[x.sort()];
+ }
+ m.Zip(alpha_->n_vars(), [](size_t a, size_t b) { return std::max(a, b); });
+ m.Zip(beta_->n_vars(), [](size_t a, size_t b) { return std::max(a, b); });
+ return m;
+ }
+
bool objective() const override { return alpha_->objective() && beta_->objective(); }
bool subjective() const override { return alpha_->subjective() && beta_->subjective(); }
bool quantified_in() const override { return alpha_->quantified_in() || beta_->quantified_in(); }
@@ -395,8 +418,8 @@ class Formula::Or : public Formula {
Or(Ref lhs, Ref rhs) : Formula(kOr), alpha_(std::move(lhs)), beta_(std::move(rhs)) {}
TermSet FreeVars() const override {
- TermSet ts1 = alpha_->FreeVars();
- const TermSet ts2 = beta_->FreeVars();
+ TermSet ts1 = alpha_->free_vars();
+ const TermSet& ts2 = beta_->free_vars();
ts1.insert(ts2.begin(), ts2.end());
return ts1;
}
@@ -478,6 +501,8 @@ class Formula::Exists : public Formula {
Term x() const { return x_; }
const Formula& arg() const { return *alpha_; }
+ SortMap n_vars() const override { return alpha_->n_vars(); }
+
bool objective() const override { return alpha_->objective(); }
bool subjective() const override { return alpha_->subjective(); }
bool quantified_in() const override { return alpha_->quantified_in(); }
@@ -489,7 +514,7 @@ class Formula::Exists : public Formula {
Exists(Term x, Ref alpha) : Formula(kExists), x_(x), alpha_(std::move(alpha)) {}
- TermSet FreeVars() const override { TermSet ts = alpha_->FreeVars(); ts.erase(x_); return ts; }
+ TermSet FreeVars() const override { TermSet ts = alpha_->free_vars(); ts.erase(x_); return ts; }
void ISubstitute(const ISubstitution& theta, Term::Factory* tf) override {
theta.Bind(x_);
@@ -554,6 +579,8 @@ class Formula::Not : public Formula {
const Formula& arg() const { return *alpha_; }
+ SortMap n_vars() const override { return alpha_->n_vars(); }
+
bool objective() const override { return alpha_->objective(); }
bool subjective() const override { return alpha_->subjective(); }
bool quantified_in() const override { return false; }
@@ -565,7 +592,7 @@ class Formula::Not : public Formula {
explicit Not(Ref alpha) : Formula(kNot), alpha_(std::move(alpha)) {}
- TermSet FreeVars() const override { return alpha_->FreeVars(); }
+ TermSet FreeVars() const override { return alpha_->free_vars(); }
void ISubstitute(const ISubstitution& theta, Term::Factory* tf) override { alpha_->ISubstitute(theta, tf); }
void ITraverse(const ITraversal& f) const override { alpha_->ITraverse(f); }
@@ -631,6 +658,8 @@ class Formula::Know : public Formula {
split_level k() const { return k_; }
const Formula& arg() const { return *alpha_; }
+ SortMap n_vars() const override { return alpha_->n_vars(); }
+
bool objective() const override { return false; }
bool subjective() const override { return true; }
bool quantified_in() const override { return !free_vars().empty(); }
@@ -642,7 +671,7 @@ class Formula::Know : public Formula {
Know(split_level k, Ref alpha) : Formula(kKnow), k_(k), alpha_(std::move(alpha)) {}
- TermSet FreeVars() const override { return alpha_->FreeVars(); }
+ TermSet FreeVars() const override { return alpha_->free_vars(); }
void ISubstitute(const ISubstitution& theta, Term::Factory* tf) override { alpha_->ISubstitute(theta, tf); }
void ITraverse(const ITraversal& f) const override { alpha_->ITraverse(f); }
@@ -727,6 +756,8 @@ class Formula::Cons : public Formula {
split_level k() const { return k_; }
const Formula& arg() const { return *alpha_; }
+ SortMap n_vars() const override { return alpha_->n_vars(); }
+
bool objective() const override { return false; }
bool subjective() const override { return true; }
bool quantified_in() const override { return !free_vars().empty(); }
@@ -738,7 +769,7 @@ class Formula::Cons : public Formula {
Cons(split_level k, Ref alpha) : Formula(kCons), k_(k), alpha_(std::move(alpha)) {}
- TermSet FreeVars() const override { return alpha_->FreeVars(); }
+ TermSet FreeVars() const override { return alpha_->free_vars(); }
void ISubstitute(const ISubstitution& theta, Term::Factory* tf) override { alpha_->ISubstitute(theta, tf); }
void ITraverse(const ITraversal& f) const override { alpha_->ITraverse(f); }
@@ -823,6 +854,8 @@ class Formula::Bel : public Formula {
const Formula& consequent() const { return *consequent_; }
const Formula& not_antecedent_or_consequent() const { return *not_antecedent_or_consequent_; }
+ SortMap n_vars() const override { return not_antecedent_or_consequent_->n_vars(); }
+
bool objective() const override { return false; }
bool subjective() const override { return true; }
bool quantified_in() const override { return !free_vars().empty(); }
@@ -840,7 +873,7 @@ class Formula::Bel : public Formula {
consequent_(consequent->Clone()),
not_antecedent_or_consequent_(Factory::Or(Factory::Not(std::move(antecedent)), std::move(consequent))) {}
- TermSet FreeVars() const override { return not_antecedent_or_consequent_->FreeVars(); }
+ TermSet FreeVars() const override { return not_antecedent_or_consequent_->free_vars(); }
void ISubstitute(const ISubstitution& theta, Term::Factory* tf) override {
antecedent_->ISubstitute(theta, tf);
@@ -900,6 +933,8 @@ class Formula::Guarantee : public Formula {
const Formula& arg() const { return *alpha_; }
+ SortMap n_vars() const override { return alpha_->n_vars(); }
+
bool objective() const override { return alpha_->objective(); }
bool subjective() const override { return alpha_->subjective(); }
bool quantified_in() const override { return alpha_->quantified_in(); }
@@ -913,7 +948,7 @@ class Formula::Guarantee : public Formula {
Formula(kGuarantee),
alpha_(std::move(alpha)) {}
- TermSet FreeVars() const override { return alpha_->FreeVars(); }
+ TermSet FreeVars() const override { return alpha_->free_vars(); }
void ISubstitute(const ISubstitution& theta, Term::Factory* tf) override { alpha_->ISubstitute(theta, tf); }
void ITraverse(const ITraversal& f) const override { alpha_->ITraverse(f); }
diff --git a/src/limbo/grounder.h b/src/limbo/grounder.h
index 94582de8044619328ee55b87de50c4becc2c1628..b331bd8aa6416d121153cd53bf6296fbe2eb947c 100644
--- a/src/limbo/grounder.h
+++ b/src/limbo/grounder.h
@@ -40,6 +40,7 @@
#include
#include
+#include
#include
#include
#include
@@ -180,7 +181,7 @@ class Grounder {
}
} else {
const TermSet vars = Mentioned([](Term t) { return t.variable(); }, c);
- for (const Assignments::Assignment& mapping : Assignments(vars, &names_)) {
+ for (const auto& mapping : Assignments(vars, &names_)) {
const Clause ci = c.Substitute(mapping, tf_);
if (!ci.valid()) {
assert(ci.primitive());
@@ -301,116 +302,24 @@ class Grounder {
class Assignments {
public:
- class TermRange {
- public:
- TermRange() = default;
- explicit TermRange(const TermSet* terms) : terms_(terms) { Reset(); }
-
- bool operator==(const TermRange r) const { return terms_ == r.terms_ && begin_ == r.begin_; }
- bool operator!=(const TermRange r) const { return !(*this == r); }
-
- TermSet::const_iterator begin() const { return begin_; }
- TermSet::const_iterator end() const { return terms_->end(); }
-
- bool empty() const { return begin_ == terms_->end(); }
-
- void Reset() { begin_ = terms_->begin(); }
- void Next() { ++begin_; }
-
- private:
- const TermSet* terms_;
- TermSet::const_iterator begin_;
- };
-
- class Assignment {
- public:
- internal::Maybe operator()(Term x) const {
- auto it = map_.find(x);
- if (it != map_.end()) {
- auto r = it->second;
- assert(!r.empty());
- const Term t = *r.begin();
- return internal::Just(t);
- } else {
- return internal::Nothing;
- }
- }
-
- bool operator==(const Assignment& a) const { return map_ == a.map_; }
- bool operator!=(const Assignment& a) const { return !(*this == a); }
-
- TermRange& operator[](Term t) { return map_[t]; }
-
- std::unordered_map::iterator begin() { return map_.begin(); }
- std::unordered_map::iterator end() { return map_.end(); }
-
- private:
- std::unordered_map map_;
- };
-
- struct assignment_iterator {
- typedef std::ptrdiff_t difference_type;
- typedef const Assignment value_type;
- typedef value_type* pointer;
- typedef value_type& reference;
- typedef std::input_iterator_tag iterator_category;
-
- // These iterators are really heavy-weight, especially comparison is
- // unusually expensive. To boost the usual comparison with end(), we
- // hence reset the substitutes_ pointer to nullptr once the end is
- // reached.
- assignment_iterator() {}
- assignment_iterator(const TermSet& vars, const SortedTermSet* substitutes) : substitutes_(substitutes) {
- for (const Term var : vars) {
- assert(var.symbol().variable());
- TermRange r(&((*substitutes_)[var.sort()]));
- assignment_[var] = r;
- assert(!r.empty());
- assert(var.sort() == r.begin()->sort());
- }
- meta_iter_ = assignment_.end();
- }
-
- bool operator==(const assignment_iterator& it) const {
- return substitutes_ == it.substitutes_ &&
- (substitutes_ == nullptr || (assignment_ == it.assignment_ &&
- *meta_iter_ == *it.meta_iter_));
+ struct GetRange {
+ GetRange(const SortedTermSet& substitutes) : substitutes_(substitutes) {}
+ std::pair> operator()(const Term x) const {
+ return std::make_pair(x, std::make_pair(substitutes_[x.sort()].begin(), substitutes_[x.sort()].end()));
}
- bool operator!=(const assignment_iterator& it) const { return !(*this == it); }
-
- reference operator*() const { return assignment_; }
-
- assignment_iterator& operator++() {
- for (meta_iter_ = assignment_.begin(); meta_iter_ != assignment_.end(); ++meta_iter_) {
- TermRange& r = meta_iter_->second;
- assert(meta_iter_->first.symbol().variable());
- assert(!r.empty());
- r.Next();
- if (!r.empty()) {
- break;
- } else {
- r.Reset();
- assert(!r.empty());
- assert(meta_iter_->first.sort() == r.begin()->sort());
- }
- }
- if (meta_iter_ == assignment_.end()) {
- substitutes_ = nullptr;
- assert(*this == assignment_iterator());
- }
- return *this;
- }
-
private:
- const SortedTermSet* substitutes_ = nullptr;
- Assignment assignment_;
- std::unordered_map::iterator meta_iter_;
+ const SortedTermSet& substitutes_;
};
+ typedef internal::transform_iterator domain_codomain_iterator;
+ typedef internal::mapping_iterator mapping_iterator;
Assignments(const TermSet& vars, const SortedTermSet* substitutes) : vars_(vars), substitutes_(substitutes) {}
- assignment_iterator begin() const { return assignment_iterator(vars_, substitutes_); }
- assignment_iterator end() const { return assignment_iterator(); }
+ mapping_iterator begin() const {
+ return mapping_iterator(domain_codomain_iterator(vars_.begin(), GetRange(*substitutes_)),
+ domain_codomain_iterator(vars_.end(), GetRange(*substitutes_)));
+ }
+ mapping_iterator end() const { return mapping_iterator(); }
private:
const TermSet vars_;
@@ -432,7 +341,7 @@ class Grounder {
void Ground(const T ungrounded, U* grounded_set) const {
assert(ungrounded.quasiprimitive());
const TermSet vars = Mentioned([](Term t) { return t.variable(); }, ungrounded);
- for (const Assignments::Assignment& mapping : Assignments(vars, &names_)) {
+ for (const auto& mapping : Assignments(vars, &names_)) {
auto grounded = ungrounded.Substitute(mapping, tf_);
assert(grounded.primitive());
grounded_set->insert(grounded);
diff --git a/src/limbo/internal/iter.h b/src/limbo/internal/iter.h
index 277071414faaa08cf50559da0e5d9581790f3409..7f154b35b4d076b0e4c05986edcf12f044682394 100644
--- a/src/limbo/internal/iter.h
+++ b/src/limbo/internal/iter.h
@@ -12,9 +12,11 @@
#include
#include
+#include
#include
#include
+#include
#include
namespace limbo {
@@ -36,12 +38,9 @@ class iterator_proxy {
mutable typename std::remove_const::type v_;
};
-class Identity {
- public:
+struct Identity {
template
- constexpr auto operator()(T&& x) const noexcept -> decltype(std::forward(x)) {
- return std::forward(x);
- }
+ constexpr auto operator()(T&& x) const noexcept -> decltype(std::forward(x)) { return std::forward(x); }
};
// Encapsulates an integer type.
@@ -365,6 +364,106 @@ filter_range(Range r, UnaryPredicate pred) {
return filter_range(r.begin(), r.end(), pred);
}
+template
+struct mapping_iterator {
+ public:
+ typedef DomainType domain_type;
+ typedef CodomainInputIt codomain_iterator;
+ typedef typename CodomainInputIt::value_type codomain_type;
+
+ struct value_type {
+ value_type(const mapping_iterator& owner) : owner_(owner) {}
+
+ internal::Maybe operator()(domain_type x) const {
+ auto it = owner_.dcd_.find(x);
+ if (it != owner_.dcd_.end()) {
+ auto& cd = it->second;
+ assert(cd.current != cd.end);
+ const codomain_type y = *cd.current;
+ return internal::Just(y);
+ } else {
+ return internal::Nothing;
+ }
+ }
+
+ bool operator==(const value_type& a) const { return owner_ == a.owner_; }
+ bool operator!=(const value_type& a) const { return !(*this == a); }
+
+ private:
+ const mapping_iterator& owner_;
+ };
+
+ typedef std::ptrdiff_t difference_type;
+ typedef value_type* pointer;
+ typedef value_type& reference;
+ typedef typename std::conditional<
+ std::is_convertible::value,
+ std::forward_iterator_tag, std::input_iterator_tag>::type iterator_category;
+ typedef iterator_proxy proxy;
+
+ mapping_iterator() {}
+
+ template
+ explicit mapping_iterator(InputIt begin, InputIt end) {
+ for (; begin != end; ++begin) {
+ domain_type x = begin->first;
+ codomain_iterator y1 = begin->second.first;
+ codomain_iterator y2 = begin->second.second;
+ dcd_.insert(std::make_pair(x, CodomainState(y1, y2)));
+ }
+ iter_ = Just(dcd_.end());
+ }
+
+ // These iterators are really heavy-weight, especially comparison is
+ // unusually expensive. To boost the usual comparison with end(), we
+ // hence reset the iter_ Maybe to Nothing once the end is reached.
+ bool operator==(const mapping_iterator& it) const { return iter_ == it.iter_ && (!iter_ || dcd_ == it.dcd_); }
+ bool operator!=(const mapping_iterator& it) const { return !(*this == it); }
+
+ value_type operator*() const { return value_type(*this); }
+
+ mapping_iterator& operator++() {
+ for (iter_ = Just(dcd_.begin()); iter_.val != dcd_.end(); ++iter_.val) {
+ CodomainState& cd = iter_.val->second;
+ assert(cd.current != cd.end);
+ ++cd.current;
+ if (cd.current != cd.end) {
+ break;
+ } else {
+ cd.current = cd.begin;
+ assert(cd.current != cd.end);
+ }
+ }
+ assert(iter_);
+ if (iter_.val == dcd_.end()) {
+ iter_ = Nothing;
+ assert(*this == mapping_iterator());
+ }
+ return *this;
+ }
+
+ pointer operator->() const { return iter_.operator->(); }
+ proxy operator++(int) { proxy p(operator*()); operator++(); return p; }
+
+ private:
+ friend struct value_type;
+
+ struct CodomainState {
+ CodomainState(codomain_iterator begin, codomain_iterator end) : begin(begin), current(begin), end(end) {}
+
+ bool operator==(const CodomainState& a) const { return begin == a.begin && current == a.current && end == a.end; }
+ bool operator!=(const CodomainState& a) const { return !(*this == a); }
+
+ codomain_iterator begin;
+ codomain_iterator current;
+ codomain_iterator end;
+ };
+ typedef std::unordered_map DomainCodomainState;
+
+ DomainCodomainState dcd_;
+ Maybe iter_;
+};
+
template
class joined_iterator {
public:
diff --git a/tests/grounder.cc b/tests/grounder.cc
index 9c445b9e5251161483b9788aaeed22b7f235eee5..0f572b92e3fb460cf48c2a2216ab332987fef094 100644
--- a/tests/grounder.cc
+++ b/tests/grounder.cc
@@ -366,7 +366,8 @@ TEST(GrounderTest, Assignments) {
EXPECT_EQ(length(as), 1);
Term fx1 = tf.CreateTerm(f, {x1});
Term fn1 = tf.CreateTerm(f, {n1});
- Grounder::Assignments::Assignment a = *as.begin();
+ auto it = as.begin();
+ auto a = *it;
EXPECT_EQ(fx1.Substitute(a, &tf), fx1);
EXPECT_NE(fx1.Substitute(a, &tf), fn1);
}
@@ -377,7 +378,8 @@ TEST(GrounderTest, Assignments) {
EXPECT_EQ(length(as), 1);
Term fx1 = tf.CreateTerm(f, {x1});
Term fn1 = tf.CreateTerm(f, {n1});
- Grounder::Assignments::Assignment a = *as.begin();
+ auto it = as.begin();
+ auto a = *it;
EXPECT_NE(fx1.Substitute(a, &tf), fx1);
EXPECT_EQ(fx1.Substitute(a, &tf), fn1);
}
@@ -392,9 +394,10 @@ TEST(GrounderTest, Assignments) {
Term fn2 = tf.CreateTerm(f, {n2});
Grounder::TermSet substitutes;
auto it = as.begin();
- Grounder::Assignments::Assignment a = *it;
+ auto a = *it;
substitutes.insert(fx1.Substitute(a, &tf));
- Grounder::Assignments::Assignment b = *++it;
+ auto jt = ++it;
+ auto b = *jt;
substitutes.insert(fx1.Substitute(b, &tf));
EXPECT_EQ(substitutes.size(), 2);
EXPECT_EQ(substitutes, Grounder::TermSet({fn1, fn2}));
diff --git a/tests/iter.cc b/tests/iter.cc
index 81263bff5e5877624b143241acb4bcca42717238..f02a24190ff39e36d53a01c0a9ebbed3eee0eb03 100644
--- a/tests/iter.cc
+++ b/tests/iter.cc
@@ -150,6 +150,166 @@ TEST(IterTest, filter_range) {
}
}
+TEST(IterTest, maping_iterator) {
+ {
+ typedef std::vector vec;
+ typedef std::map> map;
+ typedef mapping_iterator iterator;
+ map domain_codomain{};
+ auto begin = iterator(domain_codomain.cbegin(), domain_codomain.cend());
+ auto end = iterator();
+ EXPECT_NE(begin, end);
+ EXPECT_EQ(std::distance(begin, end), 1);
+ EXPECT_NE(begin, end);
+ }
+ {
+ typedef std::vector vec;
+ typedef std::map> map;
+ typedef mapping_iterator iterator;
+ vec one{11};
+ map domain_codomain{
+ {1, {one.begin(), one.end()}}
+ };
+ auto begin = iterator(domain_codomain.cbegin(), domain_codomain.cend());
+ auto end = iterator();
+ EXPECT_NE(begin, end);
+ EXPECT_EQ(std::distance(begin, end), 1);
+ EXPECT_NE(begin, end);
+ EXPECT_EQ((*begin)(1), Just(11));
+ EXPECT_EQ((*begin)(2), Nothing);
+ ++begin;
+ EXPECT_EQ(begin, end);
+ }
+ { typedef std::vector vec;
+ typedef std::map> map;
+ typedef mapping_iterator iterator;
+ vec one{11};
+ vec two{22};
+ map domain_codomain{
+ {1, {one.begin(), one.end()}},
+ {2, {two.begin(), two.end()}}
+ };
+ auto begin = iterator(domain_codomain.cbegin(), domain_codomain.cend());
+ auto end = iterator();
+ EXPECT_NE(begin, end);
+ EXPECT_EQ(std::distance(begin, end), 1);
+ EXPECT_NE(begin, end);
+ EXPECT_EQ((*begin)(1), Just(11));
+ EXPECT_EQ((*begin)(2), Just(22));
+ ++begin;
+ EXPECT_EQ(begin, end);
+ }
+ {
+ typedef std::vector vec;
+ typedef std::map> map;
+ typedef mapping_iterator iterator;
+ vec one{11};
+ vec two{22, 23};
+ map domain_codomain{
+ {1, {one.begin(), one.end()}},
+ {2, {two.begin(), two.end()}}
+ };
+ auto begin = iterator(domain_codomain.cbegin(), domain_codomain.cend());
+ auto end = iterator();
+ EXPECT_NE(begin, end);
+ EXPECT_EQ(std::distance(begin, end), 2);
+ EXPECT_NE(begin, end);
+ EXPECT_EQ((*begin)(1), Just(11));
+ EXPECT_EQ((*begin)(2), Just(22));
+ ++begin;
+ EXPECT_NE(begin, end);
+ EXPECT_EQ((*begin)(1), Just(11));
+ EXPECT_EQ((*begin)(2), Just(23));
+ ++begin;
+ EXPECT_EQ(begin, end);
+ }
+ {
+ typedef std::vector vec;
+ typedef std::map> map;
+ typedef mapping_iterator iterator;
+ vec one{11, 12};
+ vec two{22};
+ map domain_codomain{
+ {1, {one.begin(), one.end()}},
+ {2, {two.begin(), two.end()}}
+ };
+ auto begin = iterator(domain_codomain.cbegin(), domain_codomain.cend());
+ auto end = iterator();
+ EXPECT_NE(begin, end);
+ EXPECT_EQ(std::distance(begin, end), 2);
+ EXPECT_NE(begin, end);
+ EXPECT_EQ((*begin)(1), Just(11));
+ EXPECT_EQ((*begin)(2), Just(22));
+ ++begin;
+ EXPECT_NE(begin, end);
+ EXPECT_EQ((*begin)(1), Just(12));
+ EXPECT_EQ((*begin)(2), Just(22));
+ ++begin;
+ EXPECT_EQ(begin, end);
+ }
+ {
+ typedef std::vector vec;
+ typedef std::map> map;
+ typedef mapping_iterator iterator;
+ vec one{11, 12};
+ vec two{22, 23};
+ map domain_codomain{
+ {1, {one.begin(), one.end()}},
+ {2, {two.begin(), two.end()}}
+ };
+ auto begin = iterator(domain_codomain.cbegin(), domain_codomain.cend());
+ auto end = iterator();
+ EXPECT_NE(begin, end);
+ EXPECT_EQ(std::distance(begin, end), 4);
+ EXPECT_NE(begin, end);
+ EXPECT_EQ((*begin)(1), Just(11));
+ EXPECT_EQ((*begin)(2), Just(22));
+ ++begin;
+ EXPECT_NE(begin, end);
+ EXPECT_EQ((*begin)(1), Just(11));
+ EXPECT_EQ((*begin)(2), Just(23));
+ ++begin;
+ EXPECT_NE(begin, end);
+ EXPECT_EQ((*begin)(1), Just(12));
+ EXPECT_EQ((*begin)(2), Just(22));
+ ++begin;
+ EXPECT_NE(begin, end);
+ EXPECT_EQ((*begin)(1), Just(12));
+ EXPECT_EQ((*begin)(2), Just(23));
+ ++begin;
+ EXPECT_EQ(begin, end);
+ }
+ {
+ typedef std::vector vec;
+ typedef std::map> map;
+ typedef mapping_iterator iterator;
+ vec one{11, 12};
+ vec two{22, 23};
+ vec three{33, 34};
+ map domain_codomain{
+ {1, {one.begin(), one.end()}},
+ {2, {two.begin(), two.end()}},
+ {3, {three.begin(), three.end()}}
+ };
+ auto begin = iterator(domain_codomain.cbegin(), domain_codomain.cend());
+ auto end = iterator();
+ EXPECT_NE(begin, end);
+ EXPECT_EQ(std::distance(begin, end), 2*2*2);
+ for (int i = 0; i <= 1; ++i) {
+ for (int k = 0; k <= 1; ++k) {
+ for (int j = 0; j <= 1; ++j) {
+ EXPECT_NE(begin, end);
+ EXPECT_EQ((*begin)(1).val, Just(11 + i).val);
+ EXPECT_EQ((*begin)(2).val, Just(22 + k).val);
+ EXPECT_EQ((*begin)(3).val, Just(33 + j).val);
+ ++begin;
+ }
+ }
+ }
+ EXPECT_EQ(begin, end);
+ }
+}
+
TEST(IterTest, join_ranges) {
{
typedef std::vector vec;