From daa2cc7f039dbc67765907907ab5e973a68de140 Mon Sep 17 00:00:00 2001 From: Christoph Schwering Date: Mon, 22 May 2017 11:36:07 +1000 Subject: [PATCH] NF distributes conjunctions over K and disjunctions over M. Previously this was done in Solver during the semantic reduction of formulas. It appears to be much cleaner as an (optional) preprocessing step in the normalization. KnowledgeBase::Entails() has a Boolean `distribute' parameter to control the setting. In the TUI this step can be disabled with "Call: disable_distribute()", which is, for instance, important for the QBF reduction. --- README.md | 10 +- examples/tui/example-rich-father.limbo | 26 ++--- examples/tui/test-functions.limbo | 2 + examples/tui/test-qbf-1.limbo | 1 + examples/tui/test-qbf-10.limbo | 1 + examples/tui/test-qbf-11.limbo | 1 + examples/tui/test-qbf-12.limbo | 1 + examples/tui/test-qbf-13.limbo | 1 + examples/tui/test-qbf-14.limbo | 1 + examples/tui/test-qbf-15.limbo | 1 + examples/tui/test-qbf-16.limbo | 1 + examples/tui/test-qbf-17.limbo | 1 + examples/tui/test-qbf-2.limbo | 1 + examples/tui/test-qbf-3.limbo | 1 + examples/tui/test-qbf-4.limbo | 1 + examples/tui/test-qbf-5.limbo | 1 + examples/tui/test-qbf-6.limbo | 1 + examples/tui/test-qbf-7.limbo | 1 + examples/tui/test-qbf-8.limbo | 1 + examples/tui/test-qbf-9.limbo | 1 + examples/tui/tui-js.cc | 4 + examples/tui/tui-js.html | 26 ++--- examples/tui/tui.cc | 4 + src/limbo/format/pdl/context.h | 6 +- src/limbo/formula.h | 135 +++++++++++++++++++---- src/limbo/kb.h | 7 +- src/limbo/solver.h | 144 ++++++------------------- 27 files changed, 214 insertions(+), 167 deletions(-) diff --git a/README.md b/README.md index 119a0eb..74637df 100644 --- a/README.md +++ b/README.md @@ -89,24 +89,24 @@ $ make test 1. C. Schwering. A Reasoning System for a First-Order Logic of Limited Belief. - In Proc. IJCAI 2017 (to appear). + In *Proc. IJCAI*, 2017 (to appear). [PDF](http://www.cse.unsw.edu.au/~cschwering/ijcai-2017.pdf), [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. + 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. + 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. + 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. + In *Proc. IJCAI*, 2013. [PDF](https://pdfs.semanticscholar.org/387c/951016c68aaf8ce36bb87e5ea4d1ef42405d.pdf) diff --git a/examples/tui/example-rich-father.limbo b/examples/tui/example-rich-father.limbo index 27ca365..fbd16eb 100644 --- a/examples/tui/example-rich-father.limbo +++ b/examples/tui/example-rich-father.limbo @@ -1,32 +1,28 @@ // Are Frank or Fred rich? Sort BOOL, HUMAN +Name T -> BOOL +Name Frank, Fred, Sally -> HUMAN +Fun rich/1 -> BOOL +Fun fatherOf/1 -> HUMAN +Var x -> HUMAN -Function fatherOf/1 -> HUMAN -Function rich/1 -> BOOL - -Name Frank -> HUMAN -Name Fred -> HUMAN -Name Sally -> HUMAN -Name T -> BOOL - -Variable x -> HUMAN - -KB: rich(fatherOf(Sally)) = T +// All we know is that Sally's father is Frank or Fred and that he's rich. KB: fatherOf(Sally) = Frank v fatherOf(Sally) = Fred +KB: rich(fatherOf(Sally)) = T -// It's explicit knowledge that Frank/Fred is the father, then Frank is rich. Same for Fred. +// It's explicit knowledge that Frank/Fred is the father, then Frank is rich. K<0> (fatherOf(Sally) = Frank -> rich(Frank) = T) -// At split level 1, it is believed that that Frank or Fred are rich. +// At belief level 1, it is believed that that Frank or Fred are rich. K<0> (rich(Frank) = T v rich(Fred) = T) K<1> (rich(Frank) = T v rich(Fred) = T) -// At split level 1, it is considered possible that Frank is the father. Same for Fred. +// At belief level 1, it is considered possible that Frank is the father. M<0> (fatherOf(Sally) = Frank) M<1> (fatherOf(Sally) = Frank) -// At split level 1, it is considered possible that Frank is rich. Same for Fred. +// At belief level 1, it is considered possible that Frank is rich. M<0> (rich(Frank) = T) M<1> (rich(Frank) = T) diff --git a/examples/tui/test-functions.limbo b/examples/tui/test-functions.limbo index df41e52..5f14f05 100644 --- a/examples/tui/test-functions.limbo +++ b/examples/tui/test-functions.limbo @@ -22,6 +22,8 @@ Assert: Know<1> (a == n v a != n) Refute: Know<0> Ex x a == x Assert: Know<1> Ex x a == x +Refute: Ex x Know<1> f(x) == x +Refute: Fa x Know<1> f(x) == x Refute: Know<1> Fa x f(x) == x Refute: Know<1> Ex x f(x) != x diff --git a/examples/tui/test-qbf-1.limbo b/examples/tui/test-qbf-1.limbo index 7c18eb4..0d76bca 100644 --- a/examples/tui/test-qbf-1.limbo +++ b/examples/tui/test-qbf-1.limbo @@ -1,4 +1,5 @@ // ex(x1,fa(x2,ex(x3,fa(x4, (x1 v x2)^ (~x2 v x3)^ (x1 v ~x3))))) +Call: disable_distribute() Sort Bool Name T, X -> Bool Fun x1/0, x1'/0 -> Bool diff --git a/examples/tui/test-qbf-10.limbo b/examples/tui/test-qbf-10.limbo index 5ee1284..c4f1d10 100644 --- a/examples/tui/test-qbf-10.limbo +++ b/examples/tui/test-qbf-10.limbo @@ -1,4 +1,5 @@ // ex(x1,ex(x2,ex(x3,ex(x4,x4^ ~x1^ ~x2^ ~x3^ ~x4)))) +Call: disable_distribute() Sort Bool Name T, X -> Bool Fun x1/0, x1'/0 -> Bool diff --git a/examples/tui/test-qbf-11.limbo b/examples/tui/test-qbf-11.limbo index 951de30..af2494d 100644 --- a/examples/tui/test-qbf-11.limbo +++ b/examples/tui/test-qbf-11.limbo @@ -1,4 +1,5 @@ // ex(x1,fa(x2,ex(x3,fa(x4, (~x1 v x2)^ (~x2 v x3)^ (~x1 v ~x3)^ ~x1)))) +Call: disable_distribute() Sort Bool Name T, X -> Bool Fun x1/0, x1'/0 -> Bool diff --git a/examples/tui/test-qbf-12.limbo b/examples/tui/test-qbf-12.limbo index 3470d71..c33806d 100644 --- a/examples/tui/test-qbf-12.limbo +++ b/examples/tui/test-qbf-12.limbo @@ -1,4 +1,5 @@ // ex(x1,ex(x2,ex(x3,ex(x4,x4^ ~x4)))) +Call: disable_distribute() Sort Bool Name T, X -> Bool Fun x1/0, x1'/0 -> Bool diff --git a/examples/tui/test-qbf-13.limbo b/examples/tui/test-qbf-13.limbo index 1ab1532..ab1af52 100644 --- a/examples/tui/test-qbf-13.limbo +++ b/examples/tui/test-qbf-13.limbo @@ -1,4 +1,5 @@ // ex(x1,ex(x2,ex(x3,ex(x4,x1^x2^x3^x4)))) +Call: disable_distribute() Sort Bool Name T, X -> Bool Fun x1/0, x1'/0 -> Bool diff --git a/examples/tui/test-qbf-14.limbo b/examples/tui/test-qbf-14.limbo index aa7c633..afe2fc3 100644 --- a/examples/tui/test-qbf-14.limbo +++ b/examples/tui/test-qbf-14.limbo @@ -1,4 +1,5 @@ // ex(x1,x1) +Call: disable_distribute() Sort Bool Name T, X -> Bool Fun x1/0, x1'/0 -> Bool diff --git a/examples/tui/test-qbf-15.limbo b/examples/tui/test-qbf-15.limbo index c8c0107..7c10a89 100644 --- a/examples/tui/test-qbf-15.limbo +++ b/examples/tui/test-qbf-15.limbo @@ -1,4 +1,5 @@ // fa(x1,x1 v ~x1) +Call: disable_distribute() Sort Bool Name T, X -> Bool Fun x1/0 -> Bool diff --git a/examples/tui/test-qbf-16.limbo b/examples/tui/test-qbf-16.limbo index 241a214..3cb9952 100644 --- a/examples/tui/test-qbf-16.limbo +++ b/examples/tui/test-qbf-16.limbo @@ -1,4 +1,5 @@ // ex(x1,ex(x2,x1^x2)) +Call: disable_distribute() Sort Bool Name T, X -> Bool Fun x1/0, x1'/0 -> Bool diff --git a/examples/tui/test-qbf-17.limbo b/examples/tui/test-qbf-17.limbo index ecf0752..64f0017 100644 --- a/examples/tui/test-qbf-17.limbo +++ b/examples/tui/test-qbf-17.limbo @@ -1,4 +1,5 @@ // fa(x1,fa(x2, (x1 v ~x1)^ (x2 v ~x2))) +Call: disable_distribute() Sort Bool Name T, X -> Bool Fun x1/0 -> Bool diff --git a/examples/tui/test-qbf-2.limbo b/examples/tui/test-qbf-2.limbo index aad606e..daaa65a 100644 --- a/examples/tui/test-qbf-2.limbo +++ b/examples/tui/test-qbf-2.limbo @@ -1,4 +1,5 @@ // ex(x1,fa(x2,ex(x3,fa(x4, (x1 v x2)^ (~x2 v x3)^ (x1 v ~x3)^ (x2 v ~x4))))) +Call: disable_distribute() Sort Bool Name T, X -> Bool Fun x1/0, x1'/0 -> Bool diff --git a/examples/tui/test-qbf-3.limbo b/examples/tui/test-qbf-3.limbo index 188fe6d..09cc3ba 100644 --- a/examples/tui/test-qbf-3.limbo +++ b/examples/tui/test-qbf-3.limbo @@ -1,4 +1,5 @@ // ex(x1,fa(x2,ex(x3,fa(x4, (x1 v x2)^ (~x2 v x3)^ (x1 v ~x3)^ (x2 v ~x3))))) +Call: disable_distribute() Sort Bool Name T, X -> Bool Fun x1/0, x1'/0 -> Bool diff --git a/examples/tui/test-qbf-4.limbo b/examples/tui/test-qbf-4.limbo index ebdc1d6..320bf82 100644 --- a/examples/tui/test-qbf-4.limbo +++ b/examples/tui/test-qbf-4.limbo @@ -1,4 +1,5 @@ // fa(x1,fa(x2,fa(x3,x1^x2^x3 v x1^x2^ ~x3 v x1^ ~x2^x3 v x1^ ~x2^ ~x3 v ~x1^x2^x3 v ~x1^x2^ ~x3 v ~x1^ ~x2^x3 v ~x1^ ~x2^ ~x3))) +Call: disable_distribute() Sort Bool Name T, X -> Bool Fun x1/0 -> Bool diff --git a/examples/tui/test-qbf-5.limbo b/examples/tui/test-qbf-5.limbo index 2eb00bc..7f8bc2a 100644 --- a/examples/tui/test-qbf-5.limbo +++ b/examples/tui/test-qbf-5.limbo @@ -1,4 +1,5 @@ // fa(x1,fa(x2,fa(x3,fa(x4,x4 v ~x4)))) +Call: disable_distribute() Sort Bool Name T, X -> Bool Fun x1/0 -> Bool diff --git a/examples/tui/test-qbf-6.limbo b/examples/tui/test-qbf-6.limbo index 1ab1532..ab1af52 100644 --- a/examples/tui/test-qbf-6.limbo +++ b/examples/tui/test-qbf-6.limbo @@ -1,4 +1,5 @@ // ex(x1,ex(x2,ex(x3,ex(x4,x1^x2^x3^x4)))) +Call: disable_distribute() Sort Bool Name T, X -> Bool Fun x1/0, x1'/0 -> Bool diff --git a/examples/tui/test-qbf-7.limbo b/examples/tui/test-qbf-7.limbo index 4bcd8fe..83b402c 100644 --- a/examples/tui/test-qbf-7.limbo +++ b/examples/tui/test-qbf-7.limbo @@ -1,4 +1,5 @@ // ex(x1,ex(x2,ex(x3,ex(x4,~x1^ ~x2^ ~x3^ ~x4)))) +Call: disable_distribute() Sort Bool Name T, X -> Bool Fun x1/0, x1'/0 -> Bool diff --git a/examples/tui/test-qbf-8.limbo b/examples/tui/test-qbf-8.limbo index 951de30..af2494d 100644 --- a/examples/tui/test-qbf-8.limbo +++ b/examples/tui/test-qbf-8.limbo @@ -1,4 +1,5 @@ // ex(x1,fa(x2,ex(x3,fa(x4, (~x1 v x2)^ (~x2 v x3)^ (~x1 v ~x3)^ ~x1)))) +Call: disable_distribute() Sort Bool Name T, X -> Bool Fun x1/0, x1'/0 -> Bool diff --git a/examples/tui/test-qbf-9.limbo b/examples/tui/test-qbf-9.limbo index a819567..e325d07 100644 --- a/examples/tui/test-qbf-9.limbo +++ b/examples/tui/test-qbf-9.limbo @@ -1,4 +1,5 @@ // ex(x1,ex(x2,ex(x3,ex(x4,x1^ ~x1^ ~x2^ ~x3^ ~x4)))) +Call: disable_distribute() Sort Bool Name T, X -> Bool Fun x1/0, x1'/0 -> Bool diff --git a/examples/tui/tui-js.cc b/examples/tui/tui-js.cc index b6e1a9d..e8e9ccd 100644 --- a/examples/tui/tui-js.cc +++ b/examples/tui/tui-js.cc @@ -83,6 +83,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/examples/tui/tui-js.html b/examples/tui/tui-js.html index 964a5e8..e10de5b 100644 --- a/examples/tui/tui-js.html +++ b/examples/tui/tui-js.html @@ -436,23 +436,23 @@ The following constructs are well-formed formulas:
  • knowledge modality:
    - Know<split-level> formula + Know<belief-level> formula   or   - K<split-level> formula + K<belief-level> formula
  • considering-possible modality:
    - Cons<split-level> formula + Cons<belief-level> formula   or   - M<split-level> formula + M<belief-level> formula
  • conditional belief modality:
    - Bel<split-level1,split-level2> formula1 ==> formula2 + Bel<belief-level1,belief-level2> formula1 ==> formula2   or
    - B<split-level1,split-level2> formula1 ==> formula2 + B<belief-level1,belief-level2> formula1 ==> formula2
  • 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:

    1. formula contains no modal operators and its normal form (≈ prenex-NNF) is a clause without existentially quantified variables;
      2. -
    2. formula is of the form Know<split-level> formula' where formula' satisfies to condition 1 (the split-level is ignored);
      3. -
    3. 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).
      4. +
    4. formula is of the form Know<belief-level> formula' where formula' satisfies to condition 1 (the belief-level is ignored);
      5. +
    5. 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 854a0c0..87196c0 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 e5d4a5a..16da069 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 02b7b8e..2c38a4d 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 bbd9a85..cd130a2 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 72ffd9a..b1bf8e7 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: -- GitLab