From b804e23663cf9ff3e3af49a526b2693f8712eb9e Mon Sep 17 00:00:00 2001 From: Oliver Markgraf Date: Fri, 7 Jun 2024 14:01:27 +0200 Subject: [PATCH] =?UTF-8?q?=C3=A2dd=20missing=20flags?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/main/scala/ostrich/OFlags.scala | 3 ++- src/main/scala/ostrich/OstrichMain.scala | 2 +- .../scala/ostrich/OstrichStringTheoryBuilder.scala | 7 ++++++- .../ostrich/proofops/OstrichNielsenSplitter.scala | 2 +- src/test/scala/PropagationTests.scala | 10 ++++------ 5 files changed, 14 insertions(+), 10 deletions(-) diff --git a/src/main/scala/ostrich/OFlags.scala b/src/main/scala/ostrich/OFlags.scala index dd99e1d09f..951e66d7b6 100644 --- a/src/main/scala/ostrich/OFlags.scala +++ b/src/main/scala/ostrich/OFlags.scala @@ -63,7 +63,8 @@ case class OFlags( useParikhConstraints : Boolean = true, minimizeAutomata : Boolean = false, forwardPropagation : Boolean = false, - backwardPropagation : Boolean = false, + backwardPropagation : Boolean = true, + nielsenSplitter : Boolean = true, regexTranslator : OFlags.RegexTranslator.Value = OFlags.RegexTranslator.Hybrid, diff --git a/src/main/scala/ostrich/OstrichMain.scala b/src/main/scala/ostrich/OstrichMain.scala index b037f3d533..0271d5aeed 100644 --- a/src/main/scala/ostrich/OstrichMain.scala +++ b/src/main/scala/ostrich/OstrichMain.scala @@ -96,7 +96,7 @@ object PortfolioSetup { 1000000000, 2000), ParallelFileProver.Configuration( - Param.STRING_THEORY_DESC.set(baseSettings, Param.STRING_THEORY_DESC(baseSettings) + ":+forwardPropagation,+backwardPropagation"), + Param.STRING_THEORY_DESC.set(baseSettings, Param.STRING_THEORY_DESC(baseSettings) + ":+forwardPropagation,+backwardPropagation,-nielsenSplitter"), "-stringSolver=" + Param.STRING_THEORY_DESC(baseSettings) + ":+forwardPropagation,+backwardPropagation", 1000000000, diff --git a/src/main/scala/ostrich/OstrichStringTheoryBuilder.scala b/src/main/scala/ostrich/OstrichStringTheoryBuilder.scala index e2019b7e9a..e18812fea6 100644 --- a/src/main/scala/ostrich/OstrichStringTheoryBuilder.scala +++ b/src/main/scala/ostrich/OstrichStringTheoryBuilder.scala @@ -68,7 +68,9 @@ class OstrichStringTheoryBuilder extends StringTheoryBuilder { def setAlphabetSize(w : Int) : Unit = () - protected var eager, forwardPropagation, backwardPropagation, minimizeAuts, useParikh = false + protected var eager, forwardPropagation, minimizeAuts, useParikh = false + protected var backwardPropagation, nielsenSplitter = true + protected var useLen : OFlags.LengthOptions.Value = OFlags.LengthOptions.Auto protected var regexTrans : OFlags.RegexTranslator.Value = OFlags.RegexTranslator.Hybrid @@ -87,6 +89,8 @@ class OstrichStringTheoryBuilder extends StringTheoryBuilder { forwardPropagation = value case CmdlParser.Opt("backwardPropagation", value) => backwardPropagation = value + case CmdlParser.Opt("nielsenSplitter", value) => + nielsenSplitter = value case CmdlParser.Opt("parikh", value) => useParikh = value case CmdlParser.ValueOpt("regexTranslator", "approx") => @@ -133,6 +137,7 @@ class OstrichStringTheoryBuilder extends StringTheoryBuilder { useParikhConstraints = useParikh, forwardPropagation = forwardPropagation, backwardPropagation = backwardPropagation, + nielsenSplitter = nielsenSplitter, minimizeAutomata = minimizeAuts, regexTranslator = regexTrans)) } diff --git a/src/main/scala/ostrich/proofops/OstrichNielsenSplitter.scala b/src/main/scala/ostrich/proofops/OstrichNielsenSplitter.scala index 3de169a3ee..a1a78cf174 100644 --- a/src/main/scala/ostrich/proofops/OstrichNielsenSplitter.scala +++ b/src/main/scala/ostrich/proofops/OstrichNielsenSplitter.scala @@ -456,7 +456,7 @@ class OstrichNielsenSplitter(goal : Goal, * Apply the Nielsen transformation to some selected equation. */ def splitEquation : Seq[Plugin.Action] = { - if (flags.forwardPropagation || flags.backwardPropagation){ + if (!flags.nielsenSplitter){ return List() } val multiGroups = diff --git a/src/test/scala/PropagationTests.scala b/src/test/scala/PropagationTests.scala index d3b4dad09c..098583421a 100644 --- a/src/test/scala/PropagationTests.scala +++ b/src/test/scala/PropagationTests.scala @@ -45,14 +45,12 @@ object PropagationTests extends Properties("PropagationTests") { } property("noodles-unsat.smt2") = - checkFileOpts("tests/propagation-benchmarks/noodles-unsat.smt2", "unsat", "+forwardPropagation,+backwardPropagation") + checkFileOpts("tests/propagation-benchmarks/noodles-unsat.smt2", "unsat", "+forwardPropagation,+backwardPropagation,-nielsenSplitter") property("noodles-unsat2.smt2") = - checkFileOpts("tests/propagation-benchmarks/noodles-unsat2.smt2", "unsat", "+forwardPropagation,+backwardPropagation") + checkFileOpts("tests/propagation-benchmarks/noodles-unsat2.smt2", "unsat", "+forwardPropagation,+backwardPropagation,-nielsenSplitter") property("noodles-unsat3.smt2") = - checkFileOpts("tests/propagation-benchmarks/noodles-unsat3.smt2", "unsat", "+forwardPropagation,+backwardPropagation") + checkFileOpts("tests/propagation-benchmarks/noodles-unsat3.smt2", "unsat", "+forwardPropagation,+backwardPropagation,-nielsenSplitter") property("noodles-unsat4.smt2") = - checkFileOpts("tests/propagation-benchmarks/noodles-unsat4.smt2", "unsat", "+forwardPropagation,+backwardPropagation") - property("noodles-unsat5.smt2") = - checkFileOpts("tests/propagation-benchmarks/noodles-unsat5.smt2", "unsat", "+forwardPropagation,+backwardPropagation") + checkFileOpts("tests/propagation-benchmarks/noodles-unsat4.smt2", "unsat", "+forwardPropagation,+backwardPropagation,-nielsenSplitter") }