change flags

uuverifiers · Jun 4, 2024 · a1be3cd · a1be3cd
1 parent 3b88e0a
commit a1be3cd
Show file tree

Hide file tree

Showing 8 changed files with 19 additions and 41 deletions.
diff --git a/src/main/scala/ostrich/Exploration.scala b/src/main/scala/ostrich/Exploration.scala
@@ -338,18 +338,11 @@ abstract class Exploration(val funApps : Seq[(PreOp, Seq[Term], Term)],
       if (measure("check length consistency") { p.??? } == ProverStatus.Unsat)
         return None
     }
-    if (flags.forwardApprox || flags.forwardOnly || flags.forwardBackward){
+    if (flags.forwardPropagation){
       var result = addForwardConstraints
       if (result.isDefined){
         return None
       }
-      if (flags.forwardOnly){
-        while (result.isEmpty){
-          ap.util.Timeout.check
-          result = addForwardConstraints
-        }
-        return None
-      }
     }
 
 
@@ -645,7 +638,7 @@ abstract class Exploration(val funApps : Seq[(PreOp, Seq[Term], Term)],
                           fwdApps : List[(PreOp, Seq[Term], Term)])
                         : ConflictSet = resConstraints match {
     case List() => {
-      if (!straightLine && flags.forwardBackward){
+      if (!straightLine && flags.forwardPropagation && flags.backwardPropagation){
         var fwdAppsRes : List[(PreOp, Seq[Term], Term)] = fwdApps
         val funAppList = {
           (for ((apps, res) <- sortedFunApps;

diff --git a/src/main/scala/ostrich/OFlags.scala b/src/main/scala/ostrich/OFlags.scala
@@ -61,11 +61,9 @@ case class OFlags(
   useLength               : OFlags.LengthOptions.Value =
                               OFlags.LengthOptions.Auto,
   useParikhConstraints    : Boolean = true,
-  forwardApprox           : Boolean = false,
   minimizeAutomata        : Boolean = false,
-  forwardOnly             : Boolean = false,
-  forwardBackward         : Boolean = false,
-  backwardOnly            : Boolean = false,
+  forwardPropagation      : Boolean = false,
+  backwardPropagation     : Boolean = false,
   regexTranslator         : OFlags.RegexTranslator.Value =
                               OFlags.RegexTranslator.Hybrid,
 

diff --git a/src/main/scala/ostrich/OstrichMain.scala b/src/main/scala/ostrich/OstrichMain.scala
@@ -96,9 +96,9 @@ object PortfolioSetup {
             1000000000,
             2000),
             ParallelFileProver.Configuration(
-          Param.STRING_THEORY_DESC.set(baseSettings, Param.STRING_THEORY_DESC(baseSettings) + ":+forwardBackward"),
+          Param.STRING_THEORY_DESC.set(baseSettings, Param.STRING_THEORY_DESC(baseSettings) + ":+forwardPropagation,+backwardPropagation"),
           "-stringSolver=" +
-            Param.STRING_THEORY_DESC(baseSettings) + ":+forwardBackward",
+            Param.STRING_THEORY_DESC(baseSettings) + ":+forwardPropagation,+backwardPropagation",
           1000000000,
           2000))
       ParallelFileProver(createReader,

diff --git a/src/main/scala/ostrich/OstrichStringTheoryBuilder.scala b/src/main/scala/ostrich/OstrichStringTheoryBuilder.scala
@@ -68,7 +68,7 @@ class OstrichStringTheoryBuilder extends StringTheoryBuilder {
 
   def setAlphabetSize(w : Int) : Unit = ()
 
-  protected var eager, forward, forwardOnly, forwardBackward, backwardOnly, minimizeAuts, useParikh = false
+  protected var eager, forwardPropagation, backwardPropagation, minimizeAuts, useParikh = false
   protected var useLen : OFlags.LengthOptions.Value = OFlags.LengthOptions.Auto
   protected var regexTrans : OFlags.RegexTranslator.Value = OFlags.RegexTranslator.Hybrid
 
@@ -83,14 +83,10 @@ class OstrichStringTheoryBuilder extends StringTheoryBuilder {
       useLen = OFlags.LengthOptions.On
     case CmdlParser.ValueOpt("length", "auto") =>
       useLen = OFlags.LengthOptions.Auto
-    case CmdlParser.Opt("forward", value) =>
-      forward = value
-    case CmdlParser.Opt("forwardOnly", value) =>
-      forwardOnly = value
-    case CmdlParser.Opt("forwardBackward", value) =>
-      forwardBackward = value
-    case CmdlParser.Opt("backwardOnly", value) =>
-      backwardOnly = value
+    case CmdlParser.Opt("forwardPropagation", value) =>
+      forwardPropagation = value
+    case CmdlParser.Opt("backwardPropagation", value) =>
+      backwardPropagation = value
     case CmdlParser.Opt("parikh", value) =>
       useParikh = value
     case CmdlParser.ValueOpt("regexTranslator", "approx") =>
@@ -135,10 +131,8 @@ class OstrichStringTheoryBuilder extends StringTheoryBuilder {
                              OFlags(eagerAutomataOperations = eager,
                                     useLength               = useLen,
                                     useParikhConstraints    = useParikh,
-                                    forwardApprox           = forward,
-                                    forwardOnly             = forwardOnly,
-                                    forwardBackward         = forwardBackward,
-                                    backwardOnly            = backwardOnly,
+                                    forwardPropagation      = forwardPropagation,
+                                    backwardPropagation     = backwardPropagation,
                                     minimizeAutomata        = minimizeAuts,
                                     regexTranslator         = regexTrans))
   }

diff --git a/src/main/scala/ostrich/cesolver/stringtheory/CEStringTheoryBuilder.scala b/src/main/scala/ostrich/cesolver/stringtheory/CEStringTheoryBuilder.scala
@@ -90,7 +90,6 @@ class CEStringTheoryBuilder extends OstrichStringTheoryBuilder {
         eagerAutomataOperations = eager,
         useLength               = useLen,
         useParikhConstraints    = useParikh,
-        forwardApprox           = forward,
         minimizeAutomata        = minimizeAuts,
         regexTranslator         = regexTrans,
         ceaBackend              = backend,

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.forwardOnly || flags.forwardBackward || flags.backwardOnly){
+    if (flags.forwardPropagation || flags.backwardPropagation){
       return List()
     }
     val multiGroups =

diff --git a/src/test/scala/PropagationTests.scala b/src/test/scala/PropagationTests.scala
@@ -45,18 +45,14 @@ object PropagationTests extends Properties("PropagationTests") {
     }
 
     property("noodles-unsat.smt2") =
-      checkFileOpts("tests/propagation-benchmarks/noodles-unsat.smt2", "unknown", "", "-timeout=3000")
-    property("noodles-unsat.smt2") =
-      checkFileOpts("tests/propagation-benchmarks/noodles-unsat.smt2", "unknown", "+forward", "-timeout=3000")
-    property("noodles-unsat.smt2") =
-      checkFileOpts("tests/propagation-benchmarks/noodles-unsat.smt2", "unsat", "+forwardBackward")
+      checkFileOpts("tests/propagation-benchmarks/noodles-unsat.smt2", "unsat", "+forwardPropagation,+backwardPropagation")
     property("noodles-unsat2.smt2") =
-      checkFileOpts("tests/propagation-benchmarks/noodles-unsat2.smt2", "unsat", "+forwardBackward")
+      checkFileOpts("tests/propagation-benchmarks/noodles-unsat2.smt2", "unsat", "+forwardPropagation,+backwardPropagation")
     property("noodles-unsat3.smt2") =
-      checkFileOpts("tests/propagation-benchmarks/noodles-unsat3.smt2", "unsat", "+forwardBackward")
+      checkFileOpts("tests/propagation-benchmarks/noodles-unsat3.smt2", "unsat", "+forwardPropagation,+backwardPropagation")
     property("noodles-unsat4.smt2") =
-      checkFileOpts("tests/propagation-benchmarks/noodles-unsat4.smt2", "unsat", "+forwardBackward")
+      checkFileOpts("tests/propagation-benchmarks/noodles-unsat4.smt2", "unsat", "+forwardPropagation,+backwardPropagation")
     property("noodles-unsat5.smt2") =
-      checkFileOpts("tests/propagation-benchmarks/noodles-unsat5.smt2", "unsat", "+forwardBackward")
+      checkFileOpts("tests/propagation-benchmarks/noodles-unsat5.smt2", "unsat", "+forwardPropagation,+backwardPropagation")
 
 }
diff --git a/src/test/scala/SMTLIBTests.scala b/src/test/scala/SMTLIBTests.scala
@@ -107,8 +107,6 @@ object SMTLIBTests extends Properties("SMTLIBTests") {
     checkFileOpts("tests/null-problem.smt2", "sat", "", "+model")
   property("failedProp.smt2") =
     checkFileOpts("tests/failedProp.smt2", "unknown", "", s"-timeout=$shortTimeout")
-  property("failedProp.smt2 +forward") =
-    checkFileOpts("tests/failedProp.smt2", "unsat", "+forward", s"-timeout=$shortTimeout")
 
   property("propagation.smt2") =
     checkFileOpts("tests/propagation.smt2", "sat", "", "+model")