guarantee-consistency modality:
@@ -498,13 +498,13 @@ When f is a constant symbol (that is, has arit
Variables in the KB are implicitly universally quantified.
-A split-level is a natural number ≥ 0 that indicates how much reasoning effort the reasoner can spend on proving the formula in the modality.
+A belief-level is a natural number ≥ 0 that indicates how much reasoning effort the reasoner can spend on proving the formula in the modality.
The modal operator Know is the usual knowledge modality, Cons means a formula is considered possible (that is, its negation is not known), and Bel is conditional belief.
All three operators are sound but incomplete with respect to the unlimited logic of only-knowing/believing.
-The split-level can have two different meanings.
+The belief-level can have two different meanings.
The one within Know and the first parameter of Bel specify how many terms may be split.
A split means to select a term f(n1,...,nl) and consider all possible denotations of that term; that is, the reasoner tests all (relevant) assignments for these terms.
-The split-level in Cons and the second parameter of Bel, on the other hand, specify how many terms can be freely assigned a value, which means to select a (possibly non-ground) term f(t1,...,tl) and fix its denotation.
+The belief-level in Cons and the second parameter of Bel, on the other hand, specify how many terms can be freely assigned a value, which means to select a (possibly non-ground) term f(t1,...,tl) and fix its denotation.
Within the scope of the Guarantee modality the reasoner is allowed to assume the knowledge base is consistent, which may improve performance because it limits the splitting search space.
@@ -514,8 +514,8 @@ Operator precedence is as follows:
equivalence < implication < disjunction < conjunction < negation, quantifiers, modalities < brackets.
Note the maximal precedence of quantifiers and modalities.
Use brackets to expand the scope of a quantifier or a modal operator.
-For example, to say that formula1 || formula2 is known, write Know<split-level> (formula1 || formula2).
-The formula Know<split-level> formula1 || formula2 by contrast says that either formula1 is known or formula2 is true.
+For example, to say that formula1 || formula2 is known, write Know<belief-level> (formula1 || formula2).
+The formula Know<belief-level> formula1 || formula2 by contrast says that either formula1 is known or formula2 is true.
@@ -540,8 +540,8 @@ where one of the following syntactic conditions must be satisfied:
- formula contains no modal operators and its normal form (≈ prenex-NNF) is a clause without existentially quantified variables;
- - formula is of the form Know<split-level> formula' where formula' satisfies to condition 1 (the split-level is ignored);
- - formula is of the form Bel<split-level1,split-level2> formula1 ==> formula2 where !formula1 || formula2 satisfies to condition 1 (the split-levels affect how faithful the induced system of spheres is to the unlimited logic).
+ - formula is of the form Know<belief-level> formula' where formula' satisfies to condition 1 (the belief-level is ignored);
+ - formula is of the form Bel<belief-level1,belief-level2> formula1 ==> formula2 where !formula1 || formula2 satisfies to condition 1 (the belief-levels affect how faithful the induced system of spheres is to the unlimited logic).
Free variables in formula in KB definitions are implicitly universally quantified.
diff --git a/examples/tui/tui.cc b/examples/tui/tui.cc
index 854a0c0f226254f5de620520971779fcdfb44ee6..87196c0ecfe6e62c7803c273ce59b137b0c74838 100644
--- a/examples/tui/tui.cc
+++ b/examples/tui/tui.cc
@@ -124,6 +124,10 @@ struct Callback : public limbo::format::pdl::DefaultCallback {
ctx->logger()->print_queries = true;
} else if (proc == "disable_query_logging") {
ctx->logger()->print_queries = false;
+ } else if (proc == "enable_distribute") {
+ ctx->set_distribute(true);
+ } else if (proc == "disable_distribute") {
+ ctx->set_distribute(false);
} else if (bs_(ctx, proc, args)) {
// it's a call for Battleship
} else if (su_(ctx, proc, args)) {
diff --git a/src/limbo/format/pdl/context.h b/src/limbo/format/pdl/context.h
index e5d4a5aef282718fb71245e7ba9a6f7c55a5e91b..16da0698908223cf5ec546348575f3184cd51246 100644
--- a/src/limbo/format/pdl/context.h
+++ b/src/limbo/format/pdl/context.h
@@ -187,6 +187,9 @@ class Context {
logger_(DefaultLogger::UnregisterMetaVariableData(id));
}
+ void set_distribute(bool b) { distribute_ = b; }
+ bool distribute() const { return distribute_; }
+
bool AddToKb(const Formula& alpha) {
const bool ok = kb_.Add(alpha);
logger_(DefaultLogger::AddToKbData(alpha, ok));
@@ -194,7 +197,7 @@ class Context {
}
bool Query(const Formula& alpha) {
- const bool yes = kb_.Entails(alpha);
+ const bool yes = kb_.Entails(alpha, distribute_);
logger_(DefaultLogger::QueryData(kb_, alpha, yes));
return yes;
}
@@ -233,6 +236,7 @@ class Context {
Registry meta_vars_;
Registry formulas_;
KnowledgeBase kb_;
+ bool distribute_ = true;
};
} // namespace pdl
diff --git a/src/limbo/formula.h b/src/limbo/formula.h
index 02b7b8e4cf0c0d1d5c962b9c114d5b9001f6af6e..2c38a4d6fa2fd9d0eb275bf5b6d543c3ad474ad6 100644
--- a/src/limbo/formula.h
+++ b/src/limbo/formula.h
@@ -120,10 +120,10 @@ class Formula {
ITraverse(Traversal(f));
}
- Ref NF(Symbol::Factory* sf, Term::Factory* tf) const {
+ Ref NF(Symbol::Factory* sf, Term::Factory* tf, bool distribute = true) const {
Formula::Ref c = Clone();
c->Rectify(sf, tf);
- c = c->Normalize();
+ c = c->Normalize(distribute);
c = c->Flatten(0, sf, tf);
return Ref(std::move(c));
}
@@ -204,7 +204,7 @@ class Formula {
virtual std::pair quantifier_prefix() const = 0;
- virtual Ref Normalize() const = 0;
+ virtual Ref Normalize(bool distribute) const = 0;
virtual Ref Flatten(size_t nots, Symbol::Factory* sf, Term::Factory* tf) const = 0;
@@ -272,7 +272,7 @@ class Formula::Atomic : public Formula {
return std::make_pair(QuantifierPrefix(), this);
}
- Ref Normalize() const override { return Clone(); }
+ Ref Normalize(bool distribute) const override { return Clone(); }
Ref Flatten(size_t nots, Symbol::Factory* sf, Term::Factory* tf) const override {
// The following two expressions are equivalent provided that x1 ... xN do
@@ -417,9 +417,9 @@ class Formula::Or : public Formula {
return std::make_pair(QuantifierPrefix(), this);
}
- Ref Normalize() const override {
- Ref l = alpha_->Normalize();
- Ref r = beta_->Normalize();
+ Ref Normalize(bool distribute) const override {
+ Ref l = alpha_->Normalize(distribute);
+ Ref r = beta_->Normalize(distribute);
QuantifierPrefix lp;
QuantifierPrefix rp;
const Formula* ls;
@@ -518,7 +518,15 @@ class Formula::Exists : public Formula {
return p;
}
- Ref Normalize() const override { return Factory::Exists(x_, alpha_->Normalize()); }
+ Ref Normalize(bool distribute) const override {
+ const TermSet& ts = alpha_->free_vars();
+ Ref alpha = alpha_->Normalize(distribute);
+ if (ts.find(x_) != ts.end()) {
+ return Factory::Exists(x_, std::move(alpha));
+ } else {
+ return alpha;
+ }
+ }
Ref Flatten(size_t nots, Symbol::Factory* sf, Term::Factory* tf) const override {
return Factory::Exists(x_, alpha_->Flatten(nots, sf, tf));
@@ -571,7 +579,7 @@ class Formula::Not : public Formula {
return p;
}
- Ref Normalize() const override {
+ Ref Normalize(bool distribute) const override {
switch (alpha_->type()) {
case kAtomic: {
const Clause& c = arg().as_atomic().arg();
@@ -582,19 +590,19 @@ class Formula::Not : public Formula {
}
}
case kNot:
- return arg().as_not().arg().Normalize();
+ return arg().as_not().arg().Normalize(distribute);
case kOr:
- return Factory::Not(arg().Normalize());
+ return Factory::Not(arg().Normalize(distribute));
case kExists: {
Term x = arg().as_exists().x();
const Formula& alpha = arg().as_exists().arg();
- return Factory::Not(Factory::Exists(x, alpha.Normalize()));
+ return Factory::Not(Factory::Exists(x, alpha.Normalize(distribute)));
}
case kKnow:
case kCons:
case kBel:
case kGuarantee: {
- return Factory::Not(arg().Normalize());
+ return Factory::Not(arg().Normalize(distribute));
}
}
throw;
@@ -646,7 +654,14 @@ class Formula::Know : public Formula {
return std::make_pair(QuantifierPrefix(), this);
}
- Ref Normalize() const override { return Factory::Know(k_, alpha_->Normalize()); }
+ Ref Normalize(bool distribute) const override {
+ Ref alpha = alpha_->Normalize(distribute);
+ if (distribute) {
+ return DistK(k_, std::move(alpha));
+ } else {
+ return Factory::Know(k_, std::move(alpha));
+ }
+ }
Ref Flatten(size_t nots, Symbol::Factory* sf, Term::Factory* tf) const override {
Formula::Ref alpha = alpha_->Flatten(0, sf, tf);
@@ -656,6 +671,47 @@ class Formula::Know : public Formula {
internal::Maybe AsUnivClause(size_t nots) const override { return internal::Nothing; }
private:
+ static Ref DistK(split_level k, Ref alpha) {
+ if (alpha->type() == kNot) {
+ const Formula& beta = alpha->as_not().arg();
+ switch (beta.type()) {
+ case kAtomic: {
+ const Clause& c = beta.as_atomic().arg();
+ if (c.size() == 1) {
+ return Factory::Know(k, Factory::Atomic(Clause{c[0].flip()}));
+ } else if (c.size() >= 2) {
+ Ref gamma;
+ for (Literal a : c) {
+ Ref delta = Factory::Know(k, Factory::Atomic(Clause{a.flip()}));
+ if (!gamma) {
+ gamma = std::move(std::move(delta));
+ } else {
+ gamma = Factory::Or(std::move(gamma), std::move(delta));
+ }
+ }
+ gamma = Factory::Not(std::move(gamma));
+ return gamma;
+ }
+ break;
+ }
+ case kNot:
+ return DistK(k, beta.as_not().arg().Clone());
+ case kOr:
+ return Factory::Not(Factory::Or(Factory::Not(DistK(k, Factory::Not(beta.as_or().lhs().Clone()))),
+ Factory::Not(DistK(k, Factory::Not(beta.as_or().rhs().Clone())))));
+ case kExists:
+ return Factory::Not(Factory::Exists(beta.as_exists().x(),
+ Factory::Not(DistK(k, Factory::Not(beta.as_exists().arg().Clone())))));
+ case kKnow:
+ case kCons:
+ case kBel:
+ case kGuarantee:
+ break;
+ }
+ }
+ return Factory::Know(k, std::move(alpha));
+ }
+
split_level k_;
Ref alpha_;
};
@@ -694,7 +750,14 @@ class Formula::Cons : public Formula {
return std::make_pair(QuantifierPrefix(), this);
}
- Ref Normalize() const override { return Factory::Cons(k_, alpha_->Normalize()); }
+ Ref Normalize(bool distribute) const override {
+ Ref alpha = alpha_->Normalize(distribute);
+ if (distribute) {
+ return DistM(k_, std::move(alpha));
+ } else {
+ return Factory::Cons(k_, std::move(alpha));
+ }
+ }
Ref Flatten(size_t nots, Symbol::Factory* sf, Term::Factory* tf) const override {
Formula::Ref alpha = alpha_->Flatten(0, sf, tf);
@@ -704,6 +767,40 @@ class Formula::Cons : public Formula {
internal::Maybe AsUnivClause(size_t nots) const override { return internal::Nothing; }
private:
+ static Ref DistM(split_level k, Ref alpha) {
+ switch (alpha->type()) {
+ case kAtomic: {
+ const Clause& c = alpha->as_atomic().arg();
+ if (c.size() >= 2) {
+ Ref gamma;
+ for (Literal a : c) {
+ Ref delta = Factory::Know(k, Factory::Atomic(Clause{a.flip()}));
+ if (!gamma) {
+ gamma = std::move(std::move(delta));
+ } else {
+ gamma = Factory::Or(std::move(gamma), std::move(delta));
+ }
+ }
+ return gamma;
+ }
+ break;
+ }
+ case kNot:
+ break;
+ case kOr:
+ return Factory::Or(DistM(k, alpha->as_or().lhs().Clone()),
+ DistM(k, alpha->as_or().rhs().Clone()));
+ case kExists:
+ return Factory::Exists(alpha->as_exists().x(), DistM(k, alpha->as_exists().arg().Clone()));
+ case kKnow:
+ case kCons:
+ case kBel:
+ case kGuarantee:
+ break;
+ }
+ return Factory::Cons(k, std::move(alpha));
+ }
+
split_level k_;
Ref alpha_;
};
@@ -763,8 +860,10 @@ class Formula::Bel : public Formula {
return std::make_pair(QuantifierPrefix(), this);
}
- Ref Normalize() const override { return Factory::Bel(k_, l_, antecedent_->Normalize(), consequent_->Normalize(),
- not_antecedent_or_consequent_->Normalize()); }
+ Ref Normalize(bool distribute) const override {
+ return Factory::Bel(k_, l_, antecedent_->Normalize(distribute), consequent_->Normalize(distribute),
+ not_antecedent_or_consequent_->Normalize(distribute));
+ }
Ref Flatten(size_t nots, Symbol::Factory* sf, Term::Factory* tf) const override {
Formula::Ref ante = antecedent_->Flatten(0, sf, tf);
@@ -826,7 +925,7 @@ class Formula::Guarantee : public Formula {
return std::make_pair(QuantifierPrefix(), this);
}
- Ref Normalize() const override { return Factory::Guarantee(alpha_->Normalize()); }
+ Ref Normalize(bool distribute) const override { return Factory::Guarantee(alpha_->Normalize(distribute)); }
Ref Flatten(size_t nots, Symbol::Factory* sf, Term::Factory* tf) const override {
return Factory::Guarantee(alpha_->Flatten(nots, sf, tf));
diff --git a/src/limbo/kb.h b/src/limbo/kb.h
index bbd9a8542c094759303e0600f10dc1c14ae3d2d4..cd130a2fb05d47e16596cc1229f7717e1568bdb5 100644
--- a/src/limbo/kb.h
+++ b/src/limbo/kb.h
@@ -67,7 +67,7 @@ class KnowledgeBase {
}
bool Add(const Formula& alpha) {
- Formula::Ref beta = alpha.NF(sf_, tf_);
+ Formula::Ref beta = alpha.NF(sf_, tf_, false);
bool assume_consistent = false;
if (beta->type() == Formula::kGuarantee) {
beta = beta->as_guarantee().arg().Clone();
@@ -92,15 +92,14 @@ class KnowledgeBase {
return false;
}
- bool Entails(const Formula& sigma) {
+ bool Entails(const Formula& sigma, bool distribute = true) {
assert(sigma.subjective());
assert(sigma.free_vars().empty());
if (spheres_changed_) {
BuildSpheres();
spheres_changed_ = false;
}
- Formula::Ref sigma_nf = sigma.NF(sf_, tf_);
- Formula::Ref phi = ReduceModalities(*sigma_nf, false);
+ Formula::Ref phi = ReduceModalities(*sigma.NF(sf_, tf_, distribute), false);
assert(phi->objective());
return objective_.Entails(0, *phi, Solver::kNoConsistencyGuarantee);
}
diff --git a/src/limbo/solver.h b/src/limbo/solver.h
index 72ffd9ac20f8a830664a2fb98c71b4c9653cd739..b1bf8e7ebe183738c4c298ab6d52d7a6b41f73ee 100644
--- a/src/limbo/solver.h
+++ b/src/limbo/solver.h
@@ -91,7 +91,11 @@ class Solver {
assume_consistent ? grounder_.RelevantSplitTerms(phi) :
grounder_.SplitTerms();
const SortedTermSet& names = grounder_.Names();
- return s.Subsumes(Clause{}) || ReduceConjunctions(s, split_terms, names, k, phi);
+ return s.Subsumes(Clause{}) || phi.trivially_valid() ||
+ Split(s, split_terms, names, k,
+ [this, &names, &phi](const Setup& s) { return Reduce(s, names, phi); },
+ [](bool r1, bool r2) { return r1 && r2; },
+ true, false);
}
internal::Maybe Determines(int k, Term lhs, bool assume_consistent) {
@@ -136,7 +140,7 @@ class Solver {
assume_consistent ? grounder_.RelevantSplitTerms(phi) :
TermSet();
const SortedTermSet& names = grounder_.Names();
- return ReduceDisjunctions(s, assign_lits, names, k, phi, assume_consistent, relevant_terms);
+ return !phi.trivially_invalid() && Assign(s, assign_lits, names, k, phi, assume_consistent, relevant_terms);
}
private:
@@ -149,105 +153,6 @@ class Solver {
typedef Grounder::LiteralAssignmentSet LiteralAssignmentSet;
typedef Grounder::SortedTermSet SortedTermSet;
- bool ReduceConjunctions(const Setup& s,
- const TermSet& split_terms,
- const SortedTermSet& names,
- int k,
- const Formula& phi) {
- assert(phi.objective());
- switch (phi.type()) {
- case Formula::kNot: {
- switch (phi.as_not().arg().type()) {
- case Formula::kAtomic: {
- const Clause c = phi.as_not().arg().as_atomic().arg();
- return std::all_of(c.begin(), c.end(), [&, this](Literal a) {
- a = a.flip();
- Formula::Ref psi = Formula::Factory::Atomic(Clause{a});
- return ReduceConjunctions(s, split_terms, names, k, *psi);
- });
- }
- case Formula::kNot: {
- return ReduceConjunctions(s, split_terms, names, k, phi.as_not().arg().as_not().arg());
- }
- case Formula::kOr: {
- Formula::Ref left = Formula::Factory::Not(phi.as_not().arg().as_or().lhs().Clone());
- Formula::Ref right = Formula::Factory::Not(phi.as_not().arg().as_or().rhs().Clone());
- return ReduceConjunctions(s, split_terms, names, k, *left) &&
- ReduceConjunctions(s, split_terms, names, k, *right);
- }
- case Formula::kExists: {
- const Term x = phi.as_not().arg().as_exists().x();
- const Formula& psi = phi.as_not().arg().as_exists().arg();
- const TermSet& ns = names[x.sort()];
- return std::all_of(ns.begin(), ns.end(), [&, this](const Term n) {
- Formula::Ref xi = Formula::Factory::Not(psi.Clone());
- xi->SubstituteFree(Term::Substitution(x, n), tf_);
- return ReduceConjunctions(s, split_terms, names, k, *xi);
- });
- }
- default:
- break;
- }
- }
- default: {
- if (phi.trivially_valid()) {
- return true;
- }
- return Split(s, split_terms, names, k,
- [this, &names, &phi](const Setup& s) { return Reduce(s, names, phi); },
- [](bool r1, bool r2) { return r1 && r2; },
- true, false);
- }
- }
- throw;
- }
-
- bool ReduceDisjunctions(const Setup& s,
- const LiteralAssignmentSet& assign_lits,
- const SortedTermSet& names,
- int k,
- const Formula& phi,
- bool assume_consistent,
- const TermSet& relevant_terms) {
- assert(phi.objective());
- switch (phi.type()) {
- case Formula::kAtomic: {
- return Assign(s, assign_lits, names, k, phi, assume_consistent, relevant_terms);
- }
- case Formula::kOr: {
- const Formula& left = phi.as_or().lhs();
- const Formula& right = phi.as_or().rhs();
- return ReduceDisjunctions(s, assign_lits, names, k, left, assume_consistent, relevant_terms) ||
- ReduceDisjunctions(s, assign_lits, names, k, right, assume_consistent, relevant_terms);
- }
- case Formula::kExists: {
- const Term x = phi.as_exists().x();
- const TermSet& ns = names[x.sort()];
- return std::any_of(ns.begin(), ns.end(), [&, this](const Term n) {
- Formula::Ref psi = phi.as_exists().arg().Clone();
- psi->SubstituteFree(Term::Substitution(x, n), tf_);
- return ReduceDisjunctions(s, assign_lits, names, k, *psi, assume_consistent, relevant_terms);
- });
- }
- case Formula::kNot: {
- switch (phi.as_not().arg().type()) {
- case Formula::kNot:
- return ReduceDisjunctions(s, assign_lits, names, k, phi.as_not().arg().as_not().arg(), assume_consistent,
- relevant_terms);
- default:
- return !phi.trivially_invalid() && Assign(s, assign_lits, names, k, phi, assume_consistent, relevant_terms);
- }
- }
- case Formula::kKnow:
- case Formula::kCons:
- case Formula::kBel:
- case Formula::kGuarantee:
- assert(false);
- return false;
- }
- throw;
- }
-
bool Reduce(const Setup& s, const SortedTermSet& names, const Formula& phi) {
assert(phi.objective());
switch (phi.type()) {
@@ -278,12 +183,23 @@ class Solver {
case Formula::kExists: {
const Term x = phi.as_not().arg().as_exists().x();
const Formula& psi = phi.as_not().arg().as_exists().arg();
- const TermSet& ns = names[x.sort()];
- return std::all_of(ns.begin(), ns.end(), [this, &s, &names, &psi, x](const Term n) {
+ const TermSet& 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.find(x) == xs.end()) {
Formula::Ref xi = Formula::Factory::Not(psi.Clone());
- xi->SubstituteFree(Term::Substitution(x, n), tf_);
return Reduce(s, names, *xi);
- });
+ } else {
+ const TermSet& ns = names[x.sort()];
+ assert(!ns.empty());
+ return std::all_of(ns.begin(), ns.end(), [this, &s, &names, &psi, x](const Term n) {
+ Formula::Ref xi = Formula::Factory::Not(psi.Clone());
+ xi->SubstituteFree(Term::Substitution(x, n), tf_);
+ return Reduce(s, names, *xi);
+ });
+ }
}
case Formula::kKnow:
case Formula::kCons:
@@ -302,12 +218,18 @@ class Solver {
case Formula::kExists: {
const Term x = phi.as_exists().x();
const Formula& psi = phi.as_exists().arg();
- const TermSet& ns = names[x.sort()];
- return std::any_of(ns.begin(), ns.end(), [this, &s, &names, &psi, x](const Term n) {
- Formula::Ref xi = psi.Clone();
- xi->SubstituteFree(Term::Substitution(x, n), tf_);
- return Reduce(s, names, *xi);
- });
+ const TermSet& xs = psi.free_vars();
+ if (xs.find(x) == xs.end()) {
+ return Reduce(s, names, psi);
+ } else {
+ const TermSet& ns = names[x.sort()];
+ assert(!ns.empty());
+ return std::any_of(ns.begin(), ns.end(), [this, &s, &names, &psi, x](const Term n) {
+ Formula::Ref xi = psi.Clone();
+ xi->SubstituteFree(Term::Substitution(x, n), tf_);
+ return Reduce(s, names, *xi);
+ });
+ }
}
case Formula::kKnow:
case Formula::kCons: