lib/logic/lexpr.nit

   1 # This file is part of NIT ( http://www.nitlanguage.org ).
   2 #
   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
   6 #
   7 #     http://www.apache.org/licenses/LICENSE-2.0
   8 #
   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.
  14
  15 # Logical expression.
  16 #
  17 # This module provides a simple data structure for first order logic.
  18 # Basic logical operators and algorithms are provided.
  19 #
  20 # ~~~
  21 # var a = new LVar("a")
  22 # var b = new LVar("b")
  23 # var c = new LVar("c")
  24 #
  25 # assert a.to_s == "a"
  26 # assert (a|b).to_s == "(a | b)"
  27 # assert (~(a|b)).to_s == "~(a | b)"
  28 # ~~~
  29 #
  30 # Compute a negative normal form:
  31 #
  32 # ~~~
  33 # var ex = a | (b & c)
  34 # var nex = ~ex
  35 # assert ex.nnf.to_s == "(a | (b & c))"
  36 # assert nex.nnf.to_s == "(~a & (~b | ~c))"
  37 # ~~~
  38 #
  39 # Compute a conjunctive normal form:
  40 #
  41 # ~~~
  42 # assert ex.cnf.simplify.to_s == "(a|b) & (a|c)"
  43 # assert nex.cnf.simplify.to_s == "(~a) & (~b|~c)"
  44 # ~~~
  45 module lexpr
  46
  47 # A logical expression
  48 #
  49 # The basic (primitive) operators are: `&` (and), `|` (or) and `~` (not).
  50 # Composed operators are `impl` and `^`, they implemented using the basic operators.
  51 class LExpr
  52         # It the logical expression `ltrue`?
  53         #
  54         # ~~~
  55         # assert     ltrue.is_t
  56         # assert not lfalse.is_t
  57         # assert not (new LVar("a")).is_t
  58         # ~~~
  59         fun is_t: Bool do return false
  60
  61         # It the logical expression `lfalse`?
  62         #
  63         # ~~~
  64         # assert     lfalse.is_f
  65         # assert not ltrue.is_f
  66         # assert not (new LVar("a")).is_f
  67         # ~~~
  68         fun is_f: Bool do return false
  69
  70         # The negation of `self`
  71         #
  72         # ~~~
  73         # var a = new LVar("a")
  74         # assert (~a).to_s == "~a"
  75         # assert (~~a).to_s == "a"
  76         # ~~~
  77         fun ~:LExpr do return lnot
  78
  79         private var lnot: LExpr is lazy do return new LNot(self)
  80
  81         # Disjunction with `e` (and).
  82         #
  83         # ~~~
  84         # var a = new LVar("a")
  85         # var b = new LVar("b")
  86         # assert (a|b).to_s == "(a | b)"
  87         # ~~~
  88         #
  89         # `true` and `false` operands are optimized.
  90         #
  91         # ~~~
  92         # assert (a|ltrue).is_t
  93         # assert (a|lfalse) == a
  94         # ~~~
  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)
 101         end
 102
 103         # Conjunction with `e` (or).
 104         #
 105         # ~~~
 106         # var a = new LVar("a")
 107         # var b = new LVar("b")
 108         # assert (a&b).to_s == "(a & b)"
 109         # ~~~
 110         #
 111         # `true` and `false` operands are optimized.
 112         #
 113         # ~~~
 114         # assert (a&ltrue) == a
 115         # assert (a&lfalse).is_f
 116         # ~~~
 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)
 123         end
 124
 125         # Implication with `e` (implies).
 126         #
 127         # Note: it is transformed with conjunctions and disjunctions.
 128         #
 129         # ~~~
 130         # var a = new LVar("a")
 131         # var b = new LVar("b")
 132         # assert a.imp(b).to_s == "(~a | b)"
 133         # ~~~
 134         fun imp(e: LExpr): LExpr
 135         do
 136                 return (~self) | e
 137         end
 138
 139         # Exclusive disjunction with `e` (xor).
 140         #
 141         # Note: it is transformed with conjunctions and disjunctions.
 142         #
 143         # ~~~
 144         # var a = new LVar("a")
 145         # var b = new LVar("b")
 146         # assert (a^b).to_s == "((a & ~b) | (~a & b))"
 147         # ~~~
 148         fun ^(e: LExpr): LExpr
 149         do
 150                 return (self & ~e) | (~self & e)
 151         end
 152
 153         # The negation normal form (NNF).
 154         #
 155         # In NNF, the negation operator is only applied to variables.
 156         #
 157         # ~~~
 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)"
 162         # ~~~
 163         #
 164         # Subclasses implement it recursively.
 165         fun nnf: LExpr do return self
 166
 167         # The negative negation normal form (NNF).
 168         #
 169         # This method is used to implement `nnf`.
 170         # Basically, it returns the NNF of `~self`.
 171         #
 172         # ~~~
 173         # var a = new LVar("a")
 174         # var b = new LVar("b")
 175         # assert (a&b).nnnf.to_s == "(~a | ~b)"
 176         # ~~~
 177         #
 178         # Subclasses implements it by using De Morgan's laws to push negation inwards.
 179         fun nnnf: LExpr do return ~self
 180
 181         # Compute a conjunctive normal form.
 182         #
 183         # By default, a unique *equivalent* formula is computed (but its size might be exponential).
 184         #
 185         # ~~~
 186         # var a = new LVar("a")
 187         # var b = new LVar("b")
 188         # var c = new LVar("c")
 189         #
 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)"
 193         # ~~~
 194         #
 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
 198                 var ss = new CNF
 199                 var s = new Set[LExpr]
 200                 ss.data.add s
 201                 s.add self
 202                 return ss
 203         end
 204
 205         # The size of the logical expression.
 206         fun size: Int do return 1
 207 end
 208
 209 # A logical conjunction operation
 210 class LAnd
 211         super LExpr
 212
 213         # The first operand
 214         var e1: LExpr
 215
 216         # The second operand
 217         var e2: LExpr
 218
 219         redef fun to_s do return "({e1} & {e2})"
 220
 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)
 224
 225         redef fun size do return e1.size + e2.size + 1
 226 end
 227
 228 # A logical disjunction operation
 229 class LOr
 230         super LExpr
 231
 232         # The first operand
 233         var e1: LExpr
 234
 235         # The second operand
 236         var e2: LExpr
 237
 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
 241
 242         redef fun cnf(v) do
 243                 var c1 = e1.cnf(v)
 244                 var c2 = e2.cnf(v)
 245
 246                 if c1.data.length > 1 and c2.data.length > 1 and v != null then
 247                         var z = new LVar("zz{v.length}")
 248                         v.add z
 249                         var nz = ~z
 250
 251                         var res = new CNF
 252                         for c in c1.data do
 253                                 var set = c.clone
 254                                 set.add z
 255                                 res.data.add(set)
 256                         end
 257                         for c in c2.data do
 258                                 var set = c.clone
 259                                 set.add nz
 260                                 res.data.add(set)
 261                         end
 262
 263                         return res
 264                 end
 265
 266                 var res = new CNF
 267                 for i in c1.data do for j in c2.data do
 268                         res.data.add i.union(j)
 269                 end
 270                 return res
 271         end
 272
 273         redef fun size do return e1.size + e2.size + 1
 274 end
 275
 276 # A logical negation operation
 277 class LNot
 278         super LExpr
 279
 280         # The argument
 281         var e: LExpr
 282
 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
 287         redef fun cnf(v) do
 288                 if e isa LVar then return super
 289                 return e.nnnf.cnf(v)
 290         end
 291         redef fun size do return e.size + 1
 292 end
 293
 294 # The logical *true* variable.
 295 fun ltrue: LTrue do return once new LTrue
 296
 297 # The class of the singleton `ltrue`
 298 class LTrue
 299         super LExpr
 300         redef fun is_t do return true
 301         redef fun ~ do return lfalse
 302         redef fun to_s do return "true"
 303 end
 304
 305 # The logical *false* variable.
 306 fun lfalse: LFalse do return once new LFalse
 307
 308 # The class of the singleton `lfalse`
 309 class LFalse
 310         super LExpr
 311         redef fun is_f do return true
 312         redef fun ~ do return ltrue
 313         redef fun to_s do return "false"
 314 end
 315
 316
 317 # A variable of a logical expression.
 318 class LVar
 319         super LExpr
 320
 321         # The name of the variable (used for representation)
 322         #
 323         # Internally, two variables with the same name are not merged
 324         var name: String
 325
 326         redef fun to_s do return name
 327 end
 328
 329 # A conjunctive normal form of a logical expression.
 330 class CNF
 331         # The conjunction of disjunction of units.
 332         var data = new Set[Set[LExpr]]
 333
 334         # Simplify `self` by removing some useless clauses.
 335         #
 336         # * trivially clauses (with both a variable and its negation)
 337         # * subsumed clauses
 338         fun simplify: CNF
 339         do
 340                 var cs2 = new Set[Set[LExpr]]
 341
 342                 # First pass to remove clauses with a variable and its negation.
 343                 # These clauses become trivially `true`, thus useless in the conjunction.
 344                 for c in data do
 345                         for i in c do
 346                                 var nn = ~i
 347                                 if c.has(nn) then continue label
 348                         end
 349                         cs2.add c
 350                 end label
 351
 352                 # Second pass to remove clauses subsumed by an other one.
 353                 var cs3 = new Set[Set[LExpr]]
 354                 for c in cs2 do
 355                         for c2 in cs2 do
 356                                 if c2 != c and c2.has_all(c) then continue label
 357                         end
 358                         cs3.add c
 359                 end label
 360
 361                 var res = new CNF
 362                 res.data = cs3
 363                 return res
 364         end
 365
 366         # Merge two CNF
 367         fun &(o: CNF): CNF
 368         do
 369                 var res = new CNF
 370                 res.data.add_all self.data
 371                 res.data.add_all o.data
 372                 return res
 373         end
 374
 375         redef fun to_s do return [for c in data do "(" + c.join("|") + ")"].join(" & ")
 376
 377         redef fun ==(o) do return o isa CNF and data == o.data
 378         redef fun hash do return data.hash
 379 end