## PropositionalLogic.scala [raw]

```/* Copyright 2009-2016 EPFL, Lausanne */

import stainless.lang._
import stainless.annotation._

object PropositionalLogic {

sealed abstract class Formula
case class And(lhs: Formula, rhs: Formula) extends Formula
case class Or(lhs: Formula, rhs: Formula) extends Formula
case class Implies(lhs: Formula, rhs: Formula) extends Formula
case class Not(f: Formula) extends Formula
case class Literal(id: BigInt) extends Formula

def simplify(f: Formula): Formula = (f match {
case Implies(lhs, rhs) => Or(Not(simplify(lhs)), simplify(rhs))
case _ => f
}) ensuring(isSimplified(_))
// Counterexample for postcondition violation in `simplify`:
//   when f is:
//     And(Literal(8), Implies(Literal(7), Literal(6)))

def isSimplified(f: Formula): Boolean = f match {
case And(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
case Or(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
case Implies(_,_) => false
case Not(f) => isSimplified(f)
case Literal(_) => true
}

def isNNF(f: Formula): Boolean = f match {
case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
case Implies(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
case Not(Literal(_)) => true
case Not(_) => false
case Literal(_) => true
}

// @induct
// def wrongCommutative(f: Formula) : Boolean = {
//   nnf(simplify(f)) == simplify(nnf(f))
// }.holds

def simplifyBreaksNNF(f: Formula) : Boolean = {
require(isNNF(f))
isNNF(simplify(f))
}.holds
// Counterexample for postcondition violation in `simplifyBreaksNNF`:
//   when f is:
//     Implies(And(Literal(255), Literal(256)), Literal(267))
}
```

back