Commit 20b88f00 authored by Christian Müller's avatar Christian Müller

saturator

parent 115f9c07
...@@ -4,6 +4,9 @@ version := "0.1" ...@@ -4,6 +4,9 @@ version := "0.1"
scalaVersion := "2.12.8" scalaVersion := "2.12.8"
javaOptions += "-Xmx1G"
javaOptions += "-Xms256m"
// EclipseKeys.withBundledScalaContainers := false // EclipseKeys.withBundledScalaContainers := false
libraryDependencies ++= Seq( libraryDependencies ++= Seq(
......
...@@ -29,7 +29,7 @@ object Saturator extends LazyLogging { ...@@ -29,7 +29,7 @@ object Saturator extends LazyLogging {
} }
if (witheqs != clauses) { if (witheqs != clauses) {
logger.info(s"Saturation introduced equalities in CNF for guard $f") logger.info(s"Saturation introduces equalities for guard $f")
} }
// do not rewrap quantifiers here // do not rewrap quantifiers here
...@@ -51,7 +51,7 @@ object Saturator extends LazyLogging { ...@@ -51,7 +51,7 @@ object Saturator extends LazyLogging {
// val theta = dnfwithineqs.toCNF // val theta = dnfwithineqs.toCNF
val result = if (dnfclauses != withineqs) { val result = if (dnfclauses != withineqs) {
logger.warn(s"Saturation introduces inequalities for guard $f") logger.info(s"Saturation introduces inequalities for guard $f")
dnfwithineqs.toCNF dnfwithineqs.toCNF
} else { } else {
cnfwitheqs cnfwitheqs
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment