1 # This file is part of NIT ( http://www.nitlanguage.org ).
3 # Licensed under the Apache License, Version 2.0 (the "License");
4 # you may not use this file except in compliance with the License.
5 # You may obtain a copy of the License at
7 # http://www.apache.org/licenses/LICENSE-2.0
9 # Unless required by applicable law or agreed to in writing, software
10 # distributed under the License is distributed on an "AS IS" BASIS,
11 # WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
12 # See the License for the specific language governing permissions and
13 # limitations under the License.
17 # This module provides a simple data structure for first order logic.
18 # Basic logical operators and algorithms are provided.
21 # var a = new LVar("a")
22 # var b = new LVar("b")
23 # var c = new LVar("c")
25 # assert a.to_s == "a"
26 # assert (a|b).to_s == "(a | b)"
27 # assert (~(a|b)).to_s == "~(a | b)"
30 # Compute a negative normal form:
33 # var ex = a | (b & c)
35 # assert ex.nnf.to_s == "(a | (b & c))"
36 # assert nex.nnf.to_s == "(~a & (~b | ~c))"
39 # Compute a conjunctive normal form:
42 # assert ex.cnf.simplify.to_s == "(a|b) & (a|c)"
43 # assert nex.cnf.simplify.to_s == "(~a) & (~b|~c)"
47 # A logical expression
49 # The basic (primitive) operators are: `&` (and), `|` (or) and `~` (not).
50 # Composed operators are `impl` and `^`, they implemented using the basic operators.
52 # It the logical expression `ltrue`?
56 # assert not lfalse.is_t
57 # assert not (new LVar("a")).is_t
59 fun is_t
: Bool do return false
61 # It the logical expression `lfalse`?
65 # assert not ltrue.is_f
66 # assert not (new LVar("a")).is_f
68 fun is_f
: Bool do return false
70 # The negation of `self`
73 # var a = new LVar("a")
74 # assert (~a).to_s == "~a"
75 # assert (~~a).to_s == "a"
77 fun ~
:LExpr do return lnot
79 private var lnot
: LExpr is lazy
do return new LNot(self)
81 # Disjunction with `e` (and).
84 # var a = new LVar("a")
85 # var b = new LVar("b")
86 # assert (a|b).to_s == "(a | b)"
89 # `true` and `false` operands are optimized.
92 # assert (a|ltrue).is_t
93 # assert (a|lfalse) == a
95 fun |(e
: LExpr): LExpr do
96 if self.is_f
then return e
97 if self.is_t
then return ltrue
98 if e
.is_f
then return self
99 if e
.is_t
then return ltrue
100 return new LOr(self, e
)
103 # Conjunction with `e` (or).
106 # var a = new LVar("a")
107 # var b = new LVar("b")
108 # assert (a&b).to_s == "(a & b)"
111 # `true` and `false` operands are optimized.
114 # assert (a<rue) == a
115 # assert (a&lfalse).is_f
117 fun &(e
: LExpr): LExpr do
118 if self.is_f
then return lfalse
119 if self.is_t
then return e
120 if e
.is_f
then return lfalse
121 if e
.is_t
then return self
122 return new LAnd(self, e
)
125 # Implication with `e` (implies).
127 # Note: it is transformed with conjunctions and disjunctions.
130 # var a = new LVar("a")
131 # var b = new LVar("b")
132 # assert a.imp(b).to_s == "(~a | b)"
134 fun imp
(e
: LExpr): LExpr
139 # Exclusive disjunction with `e` (xor).
141 # Note: it is transformed with conjunctions and disjunctions.
144 # var a = new LVar("a")
145 # var b = new LVar("b")
146 # assert (a^b).to_s == "((a & ~b) | (~a & b))"
148 fun ^
(e
: LExpr): LExpr
150 return (self & ~e
) | (~
self & e
)
153 # The negation normal form (NNF).
155 # In NNF, the negation operator is only applied to variables.
158 # var a = new LVar("a")
159 # var b = new LVar("b")
160 # assert (a&b).nnf.to_s == "(a & b)"
161 # assert (~(a&b)).nnf.to_s == "(~a | ~b)"
164 # Subclasses implement it recursively.
165 fun nnf
: LExpr do return self
167 # The negative negation normal form (NNF).
169 # This method is used to implement `nnf`.
170 # Basically, it returns the NNF of `~self`.
173 # var a = new LVar("a")
174 # var b = new LVar("b")
175 # assert (a&b).nnnf.to_s == "(~a | ~b)"
178 # Subclasses implements it by using De Morgan's laws to push negation inwards.
179 fun nnnf
: LExpr do return ~
self
181 # Compute a conjunctive normal form.
183 # By default, a unique *equivalent* formula is computed (but its size might be exponential).
186 # var a = new LVar("a")
187 # var b = new LVar("b")
188 # var c = new LVar("c")
190 # var ex = a | (b & c)
191 # assert ex.cnf.to_s == "(a|b) & (a|c)"
192 # assert (~ex).cnf.to_s == "(~a) & (~b|~c)"
195 # If a parameter `vars` is given, an *equisatisfiable* formula is computed.
196 # Additional variables, named `zzsomething`, are created by the transformation and stored in `vars`.
197 fun cnf
(vars
: nullable Array[LVar]): CNF do
199 var s
= new Set[LExpr]
205 # The size of the logical expression.
206 fun size
: Int do return 1
209 # A logical conjunction operation
219 redef fun to_s
do return "({e1} & {e2})"
221 redef fun nnf
do return e1
.nnf
& e2
.nnf
222 redef fun nnnf
do return e1
.nnnf
| e2
.nnnf
223 redef fun cnf
(v
) do return e1
.cnf
(v
) & e2
.cnf
(v
)
225 redef fun size
do return e1
.size
+ e2
.size
+ 1
228 # A logical disjunction operation
238 redef fun to_s
do return "({e1} | {e2})"
239 redef fun nnf
do return e1
.nnf
| e2
.nnf
240 redef fun nnnf
do return e1
.nnnf
& e2
.nnnf
246 if c1
.data
.length
> 1 and c2
.data
.length
> 1 and v
!= null then
247 var z
= new LVar("zz{v.length}")
267 for i
in c1
.data
do for j
in c2
.data
do
268 res
.data
.add i
.union
(j
)
273 redef fun size
do return e1
.size
+ e2
.size
+ 1
276 # A logical negation operation
283 redef fun ~
do return e
284 redef fun to_s
do return "~{e}"
285 redef fun nnf
do return e
.nnnf
286 redef fun nnnf
do return e
.nnf
288 if e
isa LVar then return super
291 redef fun size
do return e
.size
+ 1
294 # The logical *true* variable.
295 fun ltrue
: LTrue do return once
new LTrue
297 # The class of the singleton `ltrue`
300 redef fun is_t
do return true
301 redef fun ~
do return lfalse
302 redef fun to_s
do return "true"
305 # The logical *false* variable.
306 fun lfalse
: LFalse do return once
new LFalse
308 # The class of the singleton `lfalse`
311 redef fun is_f
do return true
312 redef fun ~
do return ltrue
313 redef fun to_s
do return "false"
317 # A variable of a logical expression.
321 # The name of the variable (used for representation)
323 # Internally, two variables with the same name are not merged
326 redef fun to_s
do return name
329 # A conjunctive normal form of a logical expression.
331 # The conjunction of disjunction of units.
332 var data
= new Set[Set[LExpr]]
334 # Simplify `self` by removing some useless clauses.
336 # * trivially clauses (with both a variable and its negation)
340 var cs2
= new Set[Set[LExpr]]
342 # First pass to remove clauses with a variable and its negation.
343 # These clauses become trivially `true`, thus useless in the conjunction.
347 if c
.has
(nn
) then continue label
352 # Second pass to remove clauses subsumed by an other one.
353 var cs3
= new Set[Set[LExpr]]
356 if c2
!= c
and c2
.has_all
(c
) then continue label
370 res
.data
.add_all
self.data
371 res
.data
.add_all o
.data
375 redef fun to_s
do return [for c
in data
do "(" + c
.join
("|") + ")"].join
(" & ")
377 redef fun ==(o
) do return o
isa CNF and data
== o
.data
378 redef fun hash
do return data
.hash