--- /dev/null
+# This file is part of NIT ( http://www.nitlanguage.org ).
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+# http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+# Logical expression.
+#
+# This module provides a simple data structure for first order logic.
+# Basic logical operators and algorithms are provided.
+#
+# ~~~
+# var a = new LVar("a")
+# var b = new LVar("b")
+# var c = new LVar("c")
+#
+# assert a.to_s == "a"
+# assert (a|b).to_s == "(a | b)"
+# assert (~(a|b)).to_s == "~(a | b)"
+# ~~~
+#
+# Compute a negative normal form:
+#
+# ~~~
+# var ex = a | (b & c)
+# var nex = ~ex
+# assert ex.nnf.to_s == "(a | (b & c))"
+# assert nex.nnf.to_s == "(~a & (~b | ~c))"
+# ~~~
+#
+# Compute a conjunctive normal form:
+#
+# ~~~
+# assert ex.cnf.simplify.to_s == "(a|b) & (a|c)"
+# assert nex.cnf.simplify.to_s == "(~a) & (~b|~c)"
+# ~~~
+module lexpr
+
+# A logical expression
+#
+# The basic (primitive) operators are: `&` (and), `|` (or) and `~` (not).
+# Composed operators are `impl` and `^`, they implemented using the basic operators.
+class LExpr
+ # It the logical expression `ltrue`?
+ #
+ # ~~~
+ # assert ltrue.is_t
+ # assert not lfalse.is_t
+ # assert not (new LVar("a")).is_t
+ # ~~~
+ fun is_t: Bool do return false
+
+ # It the logical expression `lfalse`?
+ #
+ # ~~~
+ # assert lfalse.is_f
+ # assert not ltrue.is_f
+ # assert not (new LVar("a")).is_f
+ # ~~~
+ fun is_f: Bool do return false
+
+ # The negation of `self`
+ #
+ # ~~~
+ # var a = new LVar("a")
+ # assert (~a).to_s == "~a"
+ # assert (~~a).to_s == "a"
+ # ~~~
+ fun ~:LExpr do return lnot
+
+ private var lnot: LExpr is lazy do return new LNot(self)
+
+ # Disjunction with `e` (and).
+ #
+ # ~~~
+ # var a = new LVar("a")
+ # var b = new LVar("b")
+ # assert (a|b).to_s == "(a | b)"
+ # ~~~
+ #
+ # `true` and `false` operands are optimized.
+ #
+ # ~~~
+ # assert (a|ltrue).is_t
+ # assert (a|lfalse) == a
+ # ~~~
+ fun |(e: LExpr): LExpr do
+ if self.is_f then return e
+ if self.is_t then return ltrue
+ if e.is_f then return self
+ if e.is_t then return ltrue
+ return new LOr(self, e)
+ end
+
+ # Conjunction with `e` (or).
+ #
+ # ~~~
+ # var a = new LVar("a")
+ # var b = new LVar("b")
+ # assert (a&b).to_s == "(a & b)"
+ # ~~~
+ #
+ # `true` and `false` operands are optimized.
+ #
+ # ~~~
+ # assert (a<rue) == a
+ # assert (a&lfalse).is_f
+ # ~~~
+ fun &(e: LExpr): LExpr do
+ if self.is_f then return lfalse
+ if self.is_t then return e
+ if e.is_f then return lfalse
+ if e.is_t then return self
+ return new LAnd(self, e)
+ end
+
+ # Implication with `e` (implies).
+ #
+ # Note: it is transformed with conjunctions and disjunctions.
+ #
+ # ~~~
+ # var a = new LVar("a")
+ # var b = new LVar("b")
+ # assert a.imp(b).to_s == "(~a | b)"
+ # ~~~
+ fun imp(e: LExpr): LExpr
+ do
+ return (~self) | e
+ end
+
+ # Exclusive disjunction with `e` (xor).
+ #
+ # Note: it is transformed with conjunctions and disjunctions.
+ #
+ # ~~~
+ # var a = new LVar("a")
+ # var b = new LVar("b")
+ # assert (a^b).to_s == "((a & ~b) | (~a & b))"
+ # ~~~
+ fun ^(e: LExpr): LExpr
+ do
+ return (self & ~e) | (~self & e)
+ end
+
+ # The negation normal form (NNF).
+ #
+ # In NNF, the negation operator is only applied to variables.
+ #
+ # ~~~
+ # var a = new LVar("a")
+ # var b = new LVar("b")
+ # assert (a&b).nnf.to_s == "(a & b)"
+ # assert (~(a&b)).nnf.to_s == "(~a | ~b)"
+ # ~~~
+ #
+ # Subclasses implement it recursively.
+ fun nnf: LExpr do return self
+
+ # The negative negation normal form (NNF).
+ #
+ # This method is used to implement `nnf`.
+ # Basically, it returns the NNF of `~self`.
+ #
+ # ~~~
+ # var a = new LVar("a")
+ # var b = new LVar("b")
+ # assert (a&b).nnnf.to_s == "(~a | ~b)"
+ # ~~~
+ #
+ # Subclasses implements it by using De Morgan's laws to push negation inwards.
+ fun nnnf: LExpr do return ~self
+
+ # Compute a conjunctive normal form.
+ #
+ # By default, a unique *equivalent* formula is computed (but its size might be exponential).
+ #
+ # ~~~
+ # var a = new LVar("a")
+ # var b = new LVar("b")
+ # var c = new LVar("c")
+ #
+ # var ex = a | (b & c)
+ # assert ex.cnf.to_s == "(a|b) & (a|c)"
+ # assert (~ex).cnf.to_s == "(~a) & (~b|~c)"
+ # ~~~
+ #
+ # If a parameter `vars` is given, an *equisatisfiable* formula is computed.
+ # Additional variables, named `zzsomething`, are created by the transformation and stored in `vars`.
+ fun cnf(vars: nullable Array[LVar]): CNF do
+ var ss = new CNF
+ var s = new Set[LExpr]
+ ss.data.add s
+ s.add self
+ return ss
+ end
+
+ # The size of the logical expression.
+ fun size: Int do return 1
+end
+
+# A logical conjunction operation
+class LAnd
+ super LExpr
+
+ # The first operand
+ var e1: LExpr
+
+ # The second operand
+ var e2: LExpr
+
+ redef fun to_s do return "({e1} & {e2})"
+
+ redef fun nnf do return e1.nnf & e2.nnf
+ redef fun nnnf do return e1.nnnf | e2.nnnf
+ redef fun cnf(v) do return e1.cnf(v) & e2.cnf(v)
+
+ redef fun size do return e1.size + e2.size + 1
+end
+
+# A logical disjunction operation
+class LOr
+ super LExpr
+
+ # The first operand
+ var e1: LExpr
+
+ # The second operand
+ var e2: LExpr
+
+ redef fun to_s do return "({e1} | {e2})"
+ redef fun nnf do return e1.nnf | e2.nnf
+ redef fun nnnf do return e1.nnnf & e2.nnnf
+
+ redef fun cnf(v) do
+ var c1 = e1.cnf(v)
+ var c2 = e2.cnf(v)
+
+ if c1.data.length > 1 and c2.data.length > 1 and v != null then
+ var z = new LVar("zz{v.length}")
+ v.add z
+ var nz = ~z
+
+ var res = new CNF
+ for c in c1.data do
+ var set = c.clone
+ set.add z
+ res.data.add(set)
+ end
+ for c in c2.data do
+ var set = c.clone
+ set.add nz
+ res.data.add(set)
+ end
+
+ return res
+ end
+
+ var res = new CNF
+ for i in c1.data do for j in c2.data do
+ res.data.add i.union(j)
+ end
+ return res
+ end
+
+ redef fun size do return e1.size + e2.size + 1
+end
+
+# A logical negation operation
+class LNot
+ super LExpr
+
+ # The argument
+ var e: LExpr
+
+ redef fun ~ do return e
+ redef fun to_s do return "~{e}"
+ redef fun nnf do return e.nnnf
+ redef fun nnnf do return e.nnf
+ redef fun cnf(v) do
+ if e isa LVar then return super
+ return e.nnnf.cnf(v)
+ end
+ redef fun size do return e.size + 1
+end
+
+# The logical *true* variable.
+fun ltrue: LTrue do return once new LTrue
+
+# The class of the singleton `ltrue`
+class LTrue
+ super LExpr
+ redef fun is_t do return true
+ redef fun ~ do return lfalse
+ redef fun to_s do return "true"
+end
+
+# The logical *false* variable.
+fun lfalse: LFalse do return once new LFalse
+
+# The class of the singleton `lfalse`
+class LFalse
+ super LExpr
+ redef fun is_f do return true
+ redef fun ~ do return ltrue
+ redef fun to_s do return "false"
+end
+
+
+# A variable of a logical expression.
+class LVar
+ super LExpr
+
+ # The name of the variable (used for representation)
+ #
+ # Internally, two variables with the same name are not merged
+ var name: String
+
+ redef fun to_s do return name
+end
+
+# A conjunctive normal form of a logical expression.
+class CNF
+ # The conjunction of disjunction of units.
+ var data = new Set[Set[LExpr]]
+
+ # Simplify `self` by removing some useless clauses.
+ #
+ # * trivially clauses (with both a variable and its negation)
+ # * subsumed clauses
+ fun simplify: CNF
+ do
+ var cs2 = new Set[Set[LExpr]]
+
+ # First pass to remove clauses with a variable and its negation.
+ # These clauses become trivially `true`, thus useless in the conjunction.
+ for c in data do
+ for i in c do
+ var nn = ~i
+ if c.has(nn) then continue label
+ end
+ cs2.add c
+ end label
+
+ # Second pass to remove clauses subsumed by an other one.
+ var cs3 = new Set[Set[LExpr]]
+ for c in cs2 do
+ for c2 in cs2 do
+ if c2 != c and c2.has_all(c) then continue label
+ end
+ cs3.add c
+ end label
+
+ var res = new CNF
+ res.data = cs3
+ return res
+ end
+
+ # Merge two CNF
+ fun &(o: CNF): CNF
+ do
+ var res = new CNF
+ res.data.add_all self.data
+ res.data.add_all o.data
+ return res
+ end
+
+ redef fun to_s do return [for c in data do "(" + c.join("|") + ")"].join(" & ")
+
+ redef fun ==(o) do return o isa CNF and data == o.data
+ redef fun hash do return data.hash
+end
nitlanguage / nit.git / commitdiff