Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Some tweaks to Leon-era propositional logic benchmark #1597

Merged
merged 2 commits into from
Oct 28, 2024
Merged

Some tweaks to Leon-era propositional logic benchmark #1597

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
97fa07c
Some tweaks to propositional logic benchmark
vkuncak Oct 27, 2024
329ea10
More tweaks for termination
vkuncak Oct 28, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
99 changes: 59 additions & 40 deletions frontends/benchmarks/verification/valid/PropositionalLogic.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,66 +1,83 @@
/* Copyright 2009-2021 EPFL, Lausanne */
/* Copyright 2009-2024 EPFL, Lausanne */

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

object PropositionalLogic {
object PropositionalLogic:

sealed abstract class Formula:
def size: BigInt = { // just to be clear what measure we are using
this match
case And(l, r) => l.size + r.size + 1
case Or(l, r) => l.size + r.size + 1
case Not(f) => f.size + 1
case Implies(l, r) => l.size + r.size + 1
case Literal(_) => BigInt(1)
}.ensuring(res => res >= 1)

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: Int) extends Formula

def simplify(f: Formula): Formula = (f match {
case And(lhs, rhs) => And(simplify(lhs), simplify(rhs))
case Or(lhs, rhs) => Or(simplify(lhs), simplify(rhs))
case Implies(lhs, rhs) => Or(Not(simplify(lhs)), simplify(rhs))
case Not(f) => Not(simplify(f))
case Literal(_) => f
}).ensuring(isSimplified(_))
def simplify(f: Formula): Formula = {
decreases(f.size)
f match
case And(lhs, rhs) => And(simplify(lhs), simplify(rhs))
case Or(lhs, rhs) => Or(simplify(lhs), simplify(rhs))
case Implies(lhs, rhs) => Or(Not(simplify(lhs)), simplify(rhs))
case Not(f) => Not(simplify(f))
case Literal(_) => f
}.ensuring(isSimplified(_))

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 isSimplified(f: Formula): Boolean = {
decreases(f.size)
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 nnf(formula: Formula): Formula = (formula match {
case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
case Implies(lhs, rhs) => Implies(nnf(lhs), nnf(rhs))
case Not(And(lhs, rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
case Not(Or(lhs, rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
case Not(Implies(lhs, rhs)) => And(nnf(lhs), nnf(Not(rhs)))
case Not(Not(f)) => nnf(f)
case Not(Literal(_)) => formula
case Literal(_) => formula
}).ensuring(isNNF(_))
def nnf(formula: Formula): Formula = {
require(isSimplified(formula))
decreases(formula.size)
formula match
case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
case Not(And(lhs, rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
case Not(Or(lhs, rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
case Not(Implies(lhs, rhs)) => And(nnf(lhs), nnf(Not(rhs)))
case Not(Not(f)) => nnf(f)
case Not(Literal(_)) => formula
case Literal(_) => formula
}.ensuring(isNNF(_))

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
}
def isNNF(f: Formula): Boolean = {
decreases(f.size)
f match
case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
case Implies(lhs, rhs) => false
case Not(Literal(_)) => true
case Not(_) => false
case Literal(_) => true
}.ensuring(res => !res || isSimplified(f))

def vars(f: Formula): Set[Int] = {
require(isNNF(f))
decreases(f.size)
f match {
case And(lhs, rhs) => vars(lhs) ++ vars(rhs)
case Or(lhs, rhs) => vars(lhs) ++ vars(rhs)
case Implies(lhs, rhs) => vars(lhs) ++ vars(rhs)
case Not(Literal(i)) => Set[Int](i)
case Literal(i) => Set[Int](i)
}
}

def fv(f : Formula) = { vars(nnf(f)) }
def fv(f : Formula) = { vars(nnf(simplify(f))) }

@induct
def nnfIsStable(f: Formula) : Boolean = {
Expand All @@ -73,4 +90,6 @@ object PropositionalLogic {
require(isSimplified(f))
simplify(f) == f
}.holds
}


end PropositionalLogic
Loading