From ad1b24aac64637b8d252c86e4dca604d8868147d Mon Sep 17 00:00:00 2001 From: Christoph Schwering Date: Wed, 30 Nov 2016 11:23:57 +1100 Subject: [PATCH] Fixed: too few split names were considered (again!). The fix from f46b9745502cc1b9bffad80d93310829c96efee2 was insufficient. One plus name for all splits is not sufficient. For two constants a, b, (a = b) is not valid. To see that on split level 2, at least two names must be considered. So the new fix is a combination of the pre-f46b9745 state and the f46b9745-fix. Another, simpler way to deal with split names is probably to assume that the query only mentions quasi-primitive literals. Any non-quasi-primitive clause could be brought into this normal form by replacing (f(t) = g(t)) by (g(t) != x v f(t) = x) and (f(t) = x) by (t != y v f(y) = x). The solution is simple because it makes - Grounder::Flatten (although we should recycle it in Formula::NF()), - Grounder::PlusSplitNames(), - Solver::ResolveDeterminedTerms() obsolete. As we then drop Solver::ResolveDeterminedTerms(), the reasoner would even preserve soundness (if we keep it, the reasoner would still fall into the (c = d) trap for k >= 2). --- src/lela/format/output.h | 5 +++++ src/lela/grounder.h | 37 +++++++++++++++++++++++++++++++++--- src/lela/solver.h | 4 ++++ tests/grounder.cc | 41 +++++++++++++++++++++------------------- tests/solver.cc | 21 +++++++++++++++++++- 5 files changed, 85 insertions(+), 23 deletions(-) diff --git a/src/lela/format/output.h b/src/lela/format/output.h index 0141b93..d344e81 100644 --- a/src/lela/format/output.h +++ b/src/lela/format/output.h @@ -41,6 +41,11 @@ inline SymbolMap* symbol_map() { return ↦ } +inline void UnregisterAll() { + sort_map()->clear(); + symbol_map()->clear(); +} + inline void RegisterSort(Symbol::Sort s, const std::string& n) { (*sort_map())[s] = n; } diff --git a/src/lela/grounder.h b/src/lela/grounder.h index fb1708a..ef3253f 100644 --- a/src/lela/grounder.h +++ b/src/lela/grounder.h @@ -128,6 +128,7 @@ class Grounder { void PrepareForQuery(size_t k, const Formula::Reader& phi) { names_changed_ |= AddMentionedNames(Mentioned([](Term t) { return t.name(); }, phi)); names_changed_ |= AddPlusNames(PlusNames(phi)); + names_changed_ |= AddPlusNames(PlusSplitNames(k, phi)); AddSplitTerms(SplitTerms(k, phi)); AddAssignLiterals(AssignLiterals(k, phi)); } @@ -367,9 +368,6 @@ class Grounder { // variables in any clause. // PlusNames() computes p for a given clause; it is hence p+1 where p // is the number of variables in that clause. - // This fix also takes care of the right-hand side split name: splitting - // always needs to consider at least one name that does not occur in the KB - // or query, i.e., for every split term there must be at least plus name. PlusMap plus_one; c.Traverse([&plus_one](Term t) { plus_one[t.sort()] = 1; return true; }); return PlusMap::Zip(plus, plus_one, [](size_t lp, size_t rp) { return lp + rp; }); @@ -418,6 +416,39 @@ class Grounder { } } + template + static PlusMap PlusSplitNames(size_t k, const Formula::Reader& phi) { + // When a term t only occurs in the form of literals (t = n), (t = x), or + // their duals and negations, then splitting does not necessitate an + // additional name. However, when t is an argument of another term or when + // it occurs in literals of the form (t = t') or its dual or negation, then + // we might need a name for every split. + // Note that in general we really need k plus names. For instance, + // (c = d) is not valid. To see that for k >= 2, splitting needs to consider + // at least 2 <= k names, not just one. + PlusMap plus; + phi.Traverse([&plus, k](Literal a) { + auto f = [&plus, k](Term t) { + if (t.function()) { + plus[t.sort()] = k; + } + return true; + }; + if (a.lhs().function() && a.rhs().function()) { + f(a.lhs()); + f(a.rhs()); + } + for (Term t : a.lhs().args()) { + t.Traverse(f); + } + for (Term t : a.rhs().args()) { + t.Traverse(f); + } + return true; + }); + return plus; + } + template TermSet SplitTerms(size_t k, const Formula::Reader& phi) { if (k == 0) { diff --git a/src/lela/solver.h b/src/lela/solver.h index e698cf1..784cff7 100644 --- a/src/lela/solver.h +++ b/src/lela/solver.h @@ -94,6 +94,10 @@ class Solver { } private: +#ifdef FRIEND_TEST + FRIEND_TEST(SolverTest, Constants); +#endif + typedef Grounder::TermSet TermSet; typedef Grounder::LiteralSet LiteralSet; typedef Grounder::SortedTermSet SortedTermSet; diff --git a/tests/grounder.cc b/tests/grounder.cc index 92338b2..86bc989 100644 --- a/tests/grounder.cc +++ b/tests/grounder.cc @@ -194,17 +194,20 @@ TEST(GrounderTest, Ground_SplitTerms_Names) { EXPECT_NE(x3.sort(), a.sort()); EXPECT_EQ(names.size(), 2); EXPECT_EQ(names[n1.symbol().sort()].size(), 2); - EXPECT_EQ(names[x3.symbol().sort()].size(), 1); + EXPECT_EQ(names[x3.symbol().sort()].size(), 2); EXPECT_EQ(names[a.sort()].size(), 2); - EXPECT_EQ(names[g.sort()].size(), 1); - EXPECT_EQ(names[h.sort()].size(), 1); - Term nx3 = names[x3.sort()][0]; - Term nSplit = names[a.sort()][ names[a.sort()][0] == n1 ? 1 : 0 ]; - EXPECT_NE(nx3, n1); - EXPECT_NE(nSplit, n1); - EXPECT_NE(nSplit, nx3); + EXPECT_EQ(names[g.sort()].size(), 2); + EXPECT_EQ(names[h.sort()].size(), 2); + Term nx3_1 = names[x3.sort()][0]; + Term nx3_2 = names[x3.sort()][1]; + Term n_Split = names[a.sort()][ names[a.sort()][0] == n1 ? 1 : 0 ]; + EXPECT_NE(nx3_1, n1); + EXPECT_NE(nx3_2, n1); + EXPECT_NE(n_Split, n1); + EXPECT_NE(n_Split, nx3_1); + EXPECT_NE(n_Split, nx3_2); EXPECT_EQ(std::set(terms.begin(), terms.end()), - std::set({tf.CreateTerm(a, {}), tf.CreateTerm(g, {n1}), tf.CreateTerm(g, {nSplit}), tf.CreateTerm(h, {n1, nx3})})); + std::set({tf.CreateTerm(a, {}), tf.CreateTerm(g, {n1}), tf.CreateTerm(g, {n_Split}), tf.CreateTerm(h, {n1, nx3_1}), tf.CreateTerm(h, {n1, nx3_2})})); } { @@ -398,8 +401,8 @@ TEST(GrounderTest, Ground_SplitNames) { g.PrepareForQuery(0, phi.reader()); Grounder::SortedTermSet names = g.Names(); EXPECT_EQ(names[Bool].size(), 1+1);// 2+0); - EXPECT_EQ(names[Human].size(), 1+0); - EXPECT_EQ(names[Animal].size(), 0+0); + EXPECT_EQ(names[Human].size(), 1+1); + EXPECT_EQ(names[Animal].size(), 0+1); Grounder::TermSet terms = g.SplitTerms(); EXPECT_EQ(terms.size(), 0); } @@ -408,7 +411,7 @@ TEST(GrounderTest, Ground_SplitNames) { g.PrepareForQuery(1, phi.reader()); Grounder::SortedTermSet names = g.Names(); EXPECT_EQ(names[Bool].size(), 1+1);// 2+0); - EXPECT_EQ(names[Human].size(), 1+0); + EXPECT_EQ(names[Human].size(), 1+1); EXPECT_EQ(names[Animal].size(), 0+1); Grounder::TermSet terms = g.SplitTerms(); EXPECT_NE(terms.size(), 0); @@ -418,7 +421,7 @@ TEST(GrounderTest, Ground_SplitNames) { g.PrepareForQuery(2, phi.reader()); Grounder::SortedTermSet names = g.Names(); EXPECT_EQ(names[Bool].size(), 1+1);// 2+0); - EXPECT_EQ(names[Human].size(), 1+0); + EXPECT_EQ(names[Human].size(), 1+1); EXPECT_EQ(names[Animal].size(), 0+2); Grounder::TermSet terms = g.SplitTerms(); EXPECT_NE(terms.size(), 0); @@ -428,7 +431,7 @@ TEST(GrounderTest, Ground_SplitNames) { g.PrepareForQuery(3, phi.reader()); Grounder::SortedTermSet names = g.Names(); EXPECT_EQ(names[Bool].size(), 1+1);// 2+0); - EXPECT_EQ(names[Human].size(), 1+0); + EXPECT_EQ(names[Human].size(), 1+1); EXPECT_EQ(names[Animal].size(), 0+3); Grounder::TermSet terms = g.SplitTerms(); EXPECT_NE(terms.size(), 0); @@ -460,8 +463,8 @@ TEST(GrounderTest, Ground_SplitNames_iterated) { g.PrepareForQuery(0, phi.reader()); Grounder::SortedTermSet names = g.Names(); EXPECT_EQ(names[Bool].size(), 1+1);// 2+0); - EXPECT_EQ(names[Human].size(), 1+0); - EXPECT_EQ(names[Animal].size(), 0+0); + EXPECT_EQ(names[Human].size(), 1+1); + EXPECT_EQ(names[Animal].size(), 0+1); Grounder::TermSet terms = g.SplitTerms(); EXPECT_EQ(terms.size(), 0); } @@ -469,7 +472,7 @@ TEST(GrounderTest, Ground_SplitNames_iterated) { g.PrepareForQuery(1, phi.reader()); Grounder::SortedTermSet names = g.Names(); EXPECT_EQ(names[Bool].size(), 1+1);// 2+0); - EXPECT_EQ(names[Human].size(), 1+0); + EXPECT_EQ(names[Human].size(), 1+1); EXPECT_EQ(names[Animal].size(), 0+1); Grounder::TermSet terms = g.SplitTerms(); EXPECT_NE(terms.size(), 0); @@ -478,7 +481,7 @@ TEST(GrounderTest, Ground_SplitNames_iterated) { g.PrepareForQuery(2, phi.reader()); Grounder::SortedTermSet names = g.Names(); EXPECT_EQ(names[Bool].size(), 1+1);// 2+0); - EXPECT_EQ(names[Human].size(), 1+0); + EXPECT_EQ(names[Human].size(), 1+1); EXPECT_EQ(names[Animal].size(), 0+2); Grounder::TermSet terms = g.SplitTerms(); EXPECT_NE(terms.size(), 0); @@ -487,7 +490,7 @@ TEST(GrounderTest, Ground_SplitNames_iterated) { g.PrepareForQuery(3, phi.reader()); Grounder::SortedTermSet names = g.Names(); EXPECT_EQ(names[Bool].size(), 1+1);// 2+0); - EXPECT_EQ(names[Human].size(), 1+0); + EXPECT_EQ(names[Human].size(), 1+1); EXPECT_EQ(names[Animal].size(), 0+3); Grounder::TermSet terms = g.SplitTerms(); EXPECT_NE(terms.size(), 0); diff --git a/tests/solver.cc b/tests/solver.cc index 41f1ad7..729892b 100644 --- a/tests/solver.cc +++ b/tests/solver.cc @@ -192,7 +192,7 @@ TEST(SolverTest, ECAI2016Complete) { EXPECT_TRUE(solver.Consistent(1, Formula::Clause(Clause{Italian == T}).reader())); } -TEST(SetupTest, Bool) { +TEST(SolverTest, Bool) { Solver solver; Context ctx(solver.sf(), solver.tf()); Symbol::Factory sf; @@ -212,5 +212,24 @@ TEST(SetupTest, Bool) { } } +TEST(SolverTest, Constants) { + Solver solver; + UnregisterAll(); + Context ctx(solver.sf(), solver.tf()); + Symbol::Factory sf; + Term::Factory tf; + auto SomeSort = sf.CreateSort(); RegisterSort(SomeSort, ""); + auto a = ctx.NewFun(SomeSort, 0)(); REGISTER_SYMBOL(a); + auto b = ctx.NewFun(SomeSort, 0)(); REGISTER_SYMBOL(b); + { + for (int i = 0; i < 2; ++i) { + for (int k = 0; k <= 3; ++k) { + EXPECT_FALSE(solver.Entails(k, Formula::Clause(Clause{a == b}).reader())); + EXPECT_FALSE(solver.Entails(k, Formula::Clause(Clause{a != b}).reader())); + } + } + } +} + } // namespace lela -- GitLab