From 7aa77d917cdaf221064df3db46f7bcc3d57c793b Mon Sep 17 00:00:00 2001 From: Christoph Schwering Date: Thu, 3 Aug 2017 05:48:05 +1000 Subject: [PATCH] Fixed: Setup::Units::Resize(n) is well-defined for n = 0. This is relevant for the last Grounder::Ply. We create the shallow copy for the setup first and then minimize the setup, which could increase Setup::Units::n_orig_ > 0, whereas ShallowCopy::n_units_ = 0. In general, one should call ShallowCopy::Minimize() instead of Setup::Minimize(), and ShallowCopy::Minimize() doesn't Setup::Units::SealOriginalUnits(). In the special case of a ShallowCopy of an empty setup, however, Setup::Minimize() should be a safe call and now is. --- README.md | 3 ++- examples/sudoku/kb.h | 7 ++++-- src/limbo/grounder.h | 1 + src/limbo/setup.h | 5 +++- src/limbo/solver.h | 35 ---------------------------- tests/kb.cc | 54 ++++++++++++++++++++++---------------------- 6 files changed, 39 insertions(+), 66 deletions(-) diff --git a/README.md b/README.md index 15ecc21..c789abd 100644 --- a/README.md +++ b/README.md @@ -13,7 +13,8 @@ Where to go from here? 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. +* You could also send [me](http://www.cse.unsw.edu.au/~cschwering/) an email: + c.**@unsw.edu.au. ## Features diff --git a/examples/sudoku/kb.h b/examples/sudoku/kb.h index 372a6f5..77f99f6 100644 --- a/examples/sudoku/kb.h +++ b/examples/sudoku/kb.h @@ -95,8 +95,11 @@ class KnowledgeBase { UpdateSolver(); const limbo::internal::Maybe r = solver().Determines(k, val(p)); assert(std::all_of(limbo::internal::int_iterator(1), limbo::internal::int_iterator(9), - [&](size_t i) { return solver()->Entails(k, val(p) == n(i)) == - (r && r.val == n(i)); })); + [&](size_t i) { + return solver().Entails(k, *limbo::Formula::Factory::Atomic( + limbo::Clause{limbo::Literal::Eq(val(p), n(i))})) == + (r && r.val == n(i)); + })); if (r) { assert(!r.val.null()); for (std::size_t i = 1; i <= 9; ++i) { diff --git a/src/limbo/grounder.h b/src/limbo/grounder.h index ebee17c..84947f3 100644 --- a/src/limbo/grounder.h +++ b/src/limbo/grounder.h @@ -1060,6 +1060,7 @@ rescan: } if (minimize) { p->clauses.full_setup->Minimize(); + p->clauses.shallow_setup = p->clauses.full_setup->shallow_copy(); } plies_.erase(plies_.begin(), p); plies_.erase(std::next(p), plies_.end()); diff --git a/src/limbo/setup.h b/src/limbo/setup.h index fa722e3..bdbb901 100644 --- a/src/limbo/setup.h +++ b/src/limbo/setup.h @@ -427,11 +427,14 @@ class Setup { } void Resize(size_t n) { - assert(n >= n_orig_); + assert(n == 0 || n >= n_orig_); for (size_t i = n; i < vec_.size(); ++i) { set_.erase(vec_[i]); } vec_.resize(n); + if (n == 0) { + n_orig_ = 0; + } } void Erase(size_t i) { diff --git a/src/limbo/solver.h b/src/limbo/solver.h index d61d5f8..c829611 100644 --- a/src/limbo/solver.h +++ b/src/limbo/solver.h @@ -151,10 +151,6 @@ class Solver { const Term x = phi.as_not().arg().as_exists().x(); const Formula& psi = phi.as_not().arg().as_exists().arg(); const SortedTermSet& xs = psi.free_vars(); - // XXX TODO Check that this works even if we disable the first if-branch, once the name computation is fixed. - // In test-functions.limbo, the line - // Refute: Fa x Know<1> f(x) == x - // yields an error because the set of names is empty. This error should be fixed by correct name computation. if (xs.all_empty()) { Formula::Ref xi = Formula::Factory::Not(psi.Clone()); return Reduce(*xi); @@ -209,37 +205,6 @@ class Solver { template T Split(int k, GoalPredicate goal, MergeResultPredicate merge, T inconsistent_result, T unsuccessful_result) { - // XXX TODO The statement "the split order [does not matter] for Entails()" - // is wrong: - // - // For Determines(), the split order matters, for Entails() it does not. - // Suppose we have two split terms t1, t2, t3 and two names n1, n2, and - // a query term t and two candidate names n, n' for t. - // - // Let us assume that for all combinations of t1=N*, t3=N**, the reasoner - // finds that t=n. - // - // The reasoner splits t1 at the first level, and after setting t1=n1 it - // descends to the next split level, where it successfully splits t2, which - // obtains t=n' as binding for t. Back at split level one, the reasoner now - // considers the case t1=n2, again descends to the next level, where it - // splits, say, t3, and obtains t=n. - // - // Back at split level one, the reasoner sees that t=n' and t=n are - // incompatible and hence proceeds by splitting t2, which does not succeed. - // In a way, t=n' found with t2 after t1=n1 blocks the real solution. - // - // Again at level one, the reasoner splits t3. If the order does not - // matter, it will not descend to any further split level, since all - // unordered combinations of t1, t2, t3 have been tested already. - // - // If the order does matter, however, it does descend to the next level. - // There it will split t1: even if it picks t2 before t1, t2 will prove - // incompatible with t3 (*). And once it splits t1 at level two, it will - // find t=n, which this time is not blocked by t=n'. - // - // (*) This holds under the assumption that the KB is consistent. - // If the KB is not consistent, could split terms 'block' each other? if (setup().contains_empty_clause()) { return unsuccessful_result; } diff --git a/tests/kb.cc b/tests/kb.cc index e5feff2..cc52b8b 100644 --- a/tests/kb.cc +++ b/tests/kb.cc @@ -46,33 +46,33 @@ TEST(KnowledgeBaseTest, ECAI2016Sound_Guarantee) { EXPECT_TRUE(kb.Entails(*Formula::Factory::Guarantee(Formula::Factory::Bel(1, 1, *(Italian != T), *(Veggie != T))))); } -//TEST(KnowledgeBaseTest, ECAI2016Sound_NoGuarantee) { -// Context ctx; -// KnowledgeBase kb(ctx.sf(), ctx.tf()); -// auto Bool = ctx.CreateSort(); RegisterSort(Bool, ""); -// auto Food = ctx.CreateSort(); RegisterSort(Food, ""); -// auto T = ctx.CreateName(Bool); REGISTER_SYMBOL(T); -// auto Aussie = ctx.CreateFunction(Bool, 0)(); REGISTER_SYMBOL(Aussie); -// auto Italian = ctx.CreateFunction(Bool, 0)(); REGISTER_SYMBOL(Italian); -// auto Eats = ctx.CreateFunction(Bool, 1); REGISTER_SYMBOL(Eats); -// auto Meat = ctx.CreateFunction(Bool, 1); REGISTER_SYMBOL(Meat); -// auto Veggie = ctx.CreateFunction(Bool, 0)(); REGISTER_SYMBOL(Veggie); -// auto roo = ctx.CreateName(Food); REGISTER_SYMBOL(roo); -// auto x = ctx.CreateVariable(Food); REGISTER_SYMBOL(x); -// Formula::belief_level k = 1; -// Formula::belief_level l = 1; -// EXPECT_TRUE(kb.Add(*Formula::Factory::Bel(k, l, *(Aussie == T), *(Italian != T)))); -// EXPECT_TRUE(kb.Add(*Formula::Factory::Bel(k, l, *(Italian == T), *(Aussie != T)))); -// EXPECT_TRUE(kb.Add(*Formula::Factory::Bel(k, l, *(Aussie == T), *(Eats(roo) == T)))); -// EXPECT_TRUE(kb.Add(*Formula::Factory::Bel(k, l, *(T == T), *(Italian == T || Veggie == T)))); -// EXPECT_TRUE(kb.Add(*Formula::Factory::Bel(k, l, *(Italian != T), *(Aussie == T)))); -// EXPECT_TRUE(kb.Add(*Formula::Factory::Bel(k, l, *(Meat(roo) != T), *(T != T)))); -// EXPECT_TRUE(kb.Add(*Formula::Factory::Bel(k, l, *(~Fa(x, (Veggie == T && Meat(x) == T) >> (Eats(x) != T))), *(T != T)))); -// EXPECT_FALSE(kb.Entails(*Formula::Factory::Bel(0, 0, *(Italian != T), *(Veggie != T)))); -// EXPECT_FALSE(kb.Entails(*Formula::Factory::Bel(0, 1, *(Italian != T), *(Veggie != T)))); -// EXPECT_FALSE(kb.Entails(*Formula::Factory::Bel(1, 0, *(Italian != T), *(Veggie != T)))); -// EXPECT_TRUE(kb.Entails(*Formula::Factory::Bel(1, 1, *(Italian != T), *(Veggie != T)))); -//} +TEST(KnowledgeBaseTest, ECAI2016Sound_NoGuarantee) { + Context ctx; + KnowledgeBase kb(ctx.sf(), ctx.tf()); + auto Bool = ctx.CreateSort(); RegisterSort(Bool, ""); + auto Food = ctx.CreateSort(); RegisterSort(Food, ""); + auto T = ctx.CreateName(Bool); REGISTER_SYMBOL(T); + auto Aussie = ctx.CreateFunction(Bool, 0)(); REGISTER_SYMBOL(Aussie); + auto Italian = ctx.CreateFunction(Bool, 0)(); REGISTER_SYMBOL(Italian); + auto Eats = ctx.CreateFunction(Bool, 1); REGISTER_SYMBOL(Eats); + auto Meat = ctx.CreateFunction(Bool, 1); REGISTER_SYMBOL(Meat); + auto Veggie = ctx.CreateFunction(Bool, 0)(); REGISTER_SYMBOL(Veggie); + auto roo = ctx.CreateName(Food); REGISTER_SYMBOL(roo); + auto x = ctx.CreateVariable(Food); REGISTER_SYMBOL(x); + Formula::belief_level k = 1; + Formula::belief_level l = 1; + EXPECT_TRUE(kb.Add(*Formula::Factory::Bel(k, l, *(Aussie == T), *(Italian != T)))); + EXPECT_TRUE(kb.Add(*Formula::Factory::Bel(k, l, *(Italian == T), *(Aussie != T)))); + EXPECT_TRUE(kb.Add(*Formula::Factory::Bel(k, l, *(Aussie == T), *(Eats(roo) == T)))); + EXPECT_TRUE(kb.Add(*Formula::Factory::Bel(k, l, *(T == T), *(Italian == T || Veggie == T)))); + EXPECT_TRUE(kb.Add(*Formula::Factory::Bel(k, l, *(Italian != T), *(Aussie == T)))); + EXPECT_TRUE(kb.Add(*Formula::Factory::Bel(k, l, *(Meat(roo) != T), *(T != T)))); + EXPECT_TRUE(kb.Add(*Formula::Factory::Bel(k, l, *(~Fa(x, (Veggie == T && Meat(x) == T) >> (Eats(x) != T))), *(T != T)))); + EXPECT_FALSE(kb.Entails(*Formula::Factory::Bel(0, 0, *(Italian != T), *(Veggie != T)))); + EXPECT_FALSE(kb.Entails(*Formula::Factory::Bel(0, 1, *(Italian != T), *(Veggie != T)))); + EXPECT_FALSE(kb.Entails(*Formula::Factory::Bel(1, 0, *(Italian != T), *(Veggie != T)))); + EXPECT_TRUE(kb.Entails(*Formula::Factory::Bel(1, 1, *(Italian != T), *(Veggie != T)))); +} } // namespace limbo -- GitLab