logic :: LExpr :: defaultinit
# 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
lib/logic/lexpr.nit:47,1--207,3