âdd missing flags

uuverifiers · Jun 7, 2024 · b804e23 · b804e23
1 parent 266d40d
commit b804e23
Show file tree

Hide file tree

Showing 5 changed files with 14 additions and 10 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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")
 
 }