diff --git a/README.md b/README.md index 15ecc21a06ff68b0321576764fd62e766d29ee68..c789abd138dc53125dd3d5b69009ca11d8464a35 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 372a6f549b8de7a5b6620aa0e2383c17985f9f11..77f99f6e546b5d4197c57b1f1ed8bbc3e682f4df 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 ebee17c29d49cf828db9f474bacf2d2fe980d0bc..84947f318b9a00caefaf386bed486d028332afff 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 fa722e3fd0bb5471af8ce7a29808d34bc5ee3900..bdbb901e049972c20b34386e64f0276c637fc268 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 d61d5f863902b5b951d1646126a79797397c1025..c829611dc49dc94afdbcbe1ec4751df9e32ef072 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 e5feff2c23f7f28f15058a23d277f48dbb9497c7..cc52b8bf3a4093f15d72f51edf113abb23c778ec 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