Skip to content

Commit d21d51d

Browse files
SimonGuilloudSimonGuilloud
committed
Add helpers and various improvements.
1 parent ce3bf08 commit d21d51d

12 files changed

Lines changed: 118 additions & 64 deletions

‎build.sbt‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,22 @@
11

22
ThisBuild / version := "0.1.0-SNAPSHOT"
33

4-
ThisBuild / scalaVersion := "3.1.3"
4+
ThisBuild / scalaVersion := "3.7.1"
55

66
lazy val root = (project in file("."))
77
.settings(
88
name := "lattices-algorithms",
99
assembly / mainClass := Some ("Main"),
1010
assembly / assemblyJarName := "lattices.jar",
11-
// https://mvnrepository.com/artifact/com.zaxxer/SparseBitSet
12-
libraryDependencies += "com.zaxxer" % "SparseBitSet" % "1.2"
11+
libraryDependencies += "com.zaxxer" % "SparseBitSet" % "1.2",
12+
libraryDependencies += "com.lihaoyi" %% "sourcecode" % "0.4.1",
1313
)
1414

1515
scalacOptions := Seq("-unchecked", "-deprecation")
16+
scalacOptions ++= Seq(
17+
"-language:implicitConversions",
18+
"-language:experimental.modularity"
19+
)
1620

1721
run / fork := true
1822
run / javaOptions ++= Seq(

‎project/build.properties‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
sbt.version=1.6.2
1+
sbt.version=1.10.2

‎src/main/scala/AigerParser.scala‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
1+
package ortholattices
12
import java.io.{BufferedInputStream, FileInputStream}
2-
import algorithms.Datastructures.*
3+
import ortholattices.algorithms.Datastructures.*
34
import scala.collection.mutable
45

56
object AigerParser {

‎src/main/scala/Benchmark.scala‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
1+
package ortholattices
12
import FormulaGenerator.*
2-
import algorithms.Datastructures.*
3-
import algorithms.{OLAlgorithm, OcbslAlgorithm, Printer}
3+
import ortholattices.algorithms.*
4+
import Datastructures.*
45

56
import java.io.*
67
import java.nio.file.{Files, Paths}

‎src/main/scala/ForkMain.scala‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
1-
import algorithms.Datastructures.*
2-
import algorithms.{OLAlgorithm, OcbslAlgorithm, Printer}
1+
package ortholattices
2+
import ortholattices.algorithms.*
3+
import Datastructures.*
34
import Benchmark.{Algo, Improvement}
45

56
object ForkMain {

‎src/main/scala/FormulaGenerator.scala‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
1-
import algorithms.Datastructures.*
1+
package ortholattices
2+
import ortholattices.algorithms.Datastructures.*
23

34
import scala.util.Random
45

‎src/main/scala/Helpers.scala‎

Lines changed: 80 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,80 @@
1+
2+
package ortholattices
3+
import ortholattices.algorithms.*
4+
import Datastructures.*
5+
6+
object Helpers {
7+
8+
def bot: Formula = Literal(false)
9+
def top: Formula = Literal(true)
10+
def neg(f: Formula): Neg = Neg(f)
11+
def and(args: List[Formula]): And = And(args)
12+
def and(f:Formula*): And = And(f.toList)
13+
def or(args: List[Formula]): Or = Or(args)
14+
def or(f:Formula*): Or = Or(f.toList)
15+
def iff(f: Formula, g: Formula): And = and(implies(f, g), implies(g, f))
16+
def implies(f: Formula, g: Formula): Formula = neg(or(neg(f), g))
17+
18+
19+
val OLAlgo = new OLAlgorithm
20+
val OcbslAlgo = new OcbslAlgorithm
21+
22+
def ¬(f: Formula): Neg = Neg(f)
23+
extension (f: Formula) {
24+
def &(g: Formula): And = and(f, g)
25+
def /\(g: Formula): And = and(f, g)
26+
def |(g: Formula): Or = or(f, g)
27+
def \/(g: Formula): Or = or(f, g)
28+
def unary_! : Neg = Neg(f)
29+
30+
def <->(g: Formula): And = iff(f, g)
31+
def -->(g: Formula): Formula = implies(f, g)
32+
33+
34+
def OLnormalize: Formula = OLAlgo.reducedForm(f)
35+
def OcbslNormalize: Formula = OcbslAlgo.reducedForm(f)
36+
infix def ~(g: Formula): Boolean = OLAlgo.isSame(f, g)
37+
}
38+
39+
def ⊥ : Formula = bot
40+
def ⊤ : Formula = top
41+
42+
given conv_false: Conversion[false, Formula] = _ => bot
43+
given conv_true: Conversion[true, Formula] = _ => top
44+
45+
46+
def Variable(id:Int): Variable = new Variable(id)
47+
48+
val x0 = Variable(0)
49+
val x1 = Variable(1)
50+
val x2 = Variable(2)
51+
val x3 = Variable(3)
52+
val x4 = Variable(4)
53+
val x5 = Variable(5)
54+
val x6 = Variable(6)
55+
val x7 = Variable(7)
56+
val x8 = Variable(8)
57+
val x9 = Variable(9)
58+
val x10 = Variable(10)
59+
val x11 = Variable(11)
60+
val x12 = Variable(12)
61+
val x13 = Variable(13)
62+
val x14 = Variable(14)
63+
val x15 = Variable(15)
64+
val x16 = Variable(16)
65+
val x17 = Variable(17)
66+
val x18 = Variable(18)
67+
val x19 = Variable(19)
68+
val x20 = Variable(20)
69+
val x21 = Variable(21)
70+
val x22 = Variable(22)
71+
val x23 = Variable(23)
72+
val x24 = Variable(24)
73+
val x25 = Variable(25)
74+
val x26 = Variable(26)
75+
val x27 = Variable(27)
76+
val x28 = Variable(28)
77+
val x29 = Variable(29)
78+
val x30 = Variable(30)
79+
80+
}

‎src/main/scala/Main.scala‎

Lines changed: 2 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
import algorithms.Datastructures.*
1+
package ortholattices
2+
import ortholattices.algorithms.Datastructures.*
23
import FormulaGenerator.*
34
import Benchmark.*
45
import FormulaGenerator.*
5-
import algorithms.Datastructures.*
66

77
import scala.concurrent.duration.*
88

@@ -48,34 +48,4 @@ object Main {
4848

4949

5050

51-
val a = Variable(0)
52-
val b = Variable(1)
53-
val c = Variable(2)
54-
val d = Variable(3)
55-
val e = Variable(4)
56-
val f = Variable(5)
57-
58-
val x0 = Variable(0)
59-
val x1 = Variable(1)
60-
val x2 = Variable(2)
61-
val x3 = Variable(3)
62-
val x4 = Variable(4)
63-
val x5 = Variable(5)
64-
65-
66-
def neg(f: Formula): Formula = Neg(f)
67-
68-
def and(args: List[Formula]): Formula = And(args)
69-
70-
def and(f:Formula*): Formula = And(f.toList)
71-
72-
def or(args: List[Formula]): Formula = Or(args)
73-
74-
def or(f:Formula*): Formula = Or(f.toList)
75-
76-
def iff(f: Formula, g: Formula): Formula = and(implies(f, g), implies(g, f))
77-
78-
def implies(f: Formula, g: Formula): Formula = neg(or(neg(f), g))
79-
80-
8151
}

‎src/main/scala/algorithms/Datastructures.scala‎

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,8 @@
1-
package algorithms
1+
package ortholattices.algorithms
22

3-
import algorithms.OLAlgorithm.PolarFormula
4-
import algorithms.OcbslAlgorithm.NoOrFormula
3+
import ortholattices.algorithms.OLAlgorithm.PolarFormula
4+
import ortholattices.algorithms.OcbslAlgorithm.NoOrFormula
5+
import ortholattices.algorithms.Printer
56

67
import scala.collection.mutable
78

@@ -69,11 +70,7 @@ object Datastructures {
6970
def isSame(formula1: Formula, formula2: Formula): Boolean
7071
def reducedForm(formula: Formula): Formula
7172
}
72-
73-
def memoize[I, O](f: I => O): I => O = new mutable.HashMap[I, O]() {
74-
override def apply(key: I): O = getOrElseUpdate(key, f(key))
75-
}
76-
73+
7774
def negationNormalForm(f: Formula, positive: Boolean = true): Formula = f match {
7875
case Variable(id) => if (positive) Variable(id) else Neg(Variable(id))
7976
case Neg(child) => negationNormalForm(child, !positive)

‎src/main/scala/algorithms/OLAlgorithm.scala‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
1-
package algorithms
1+
package ortholattices.algorithms
22

3-
import algorithms.Datastructures.*
4-
import algorithms.OLAlgorithm.*
3+
import Datastructures.*
4+
import ortholattices.algorithms.OLAlgorithm.*
55
import com.zaxxer.sparsebits.SparseBitSet
66

77
import scala.collection.mutable
@@ -112,7 +112,7 @@ class OLAlgorithm extends EquivalenceAndNormalFormAlgorithm {
112112
val a = nPnormalForm(formula1)
113113
val b = nPnormalForm(formula2)
114114
latticesLEQ(a, b) && latticesLEQ(b, a)
115-
override def isSame(formula1: Formula, formula2: Formula): Boolean = false //checkEquivalence(polarize(formula1), polarize(formula2))
115+
override def isSame(formula1: Formula, formula2: Formula): Boolean = checkEquivalence(polarize(formula1), polarize(formula2))
116116

117117

118118
override def reducedForm(formula: Formula): Formula =
@@ -214,7 +214,7 @@ object OLAlgorithm extends EquivalenceAndNormalFormAlgorithm {
214214
f.formulaAIG = Some(r)
215215
r
216216

217-
def toFormula(f:NormalPFormula): Formula = toFormulaAIG(f)
217+
def toFormula(f:NormalPFormula): Formula = toFormulaNNF(f)
218218

219219
//def checkEquivalence(formula1: PolarFormula, formula2: PolarFormula): Boolean = (new OLAlgorithm).checkEquivalence(formula1, formula2)
220220

0 commit comments

Comments
 (0)