add RCP to portfolio

uuverifiers · May 29, 2024 · 3b88e0a · 3b88e0a
1 parent 9be99d4
commit 3b88e0a
Showing 1 changed file with 44 additions and 36 deletions.
diff --git a/src/main/scala/ostrich/OstrichMain.scala b/src/main/scala/ostrich/OstrichMain.scala
@@ -67,44 +67,52 @@ object PortfolioSetup {
   private val ceaStringTheory =
     "ostrich.cesolver.stringtheory.CEStringTheory"
 
-  // Run the BW, ADT, and CEA solvers
+  // Run the BW, ADT, CEA and RCP solvers
   ParallelFileProver.addPortfolio(
     "strings", arguments => {
-                 import arguments._
-                 val strategies =
-                   List(ParallelFileProver.Configuration(
-                          baseSettings,
-                          "-stringSolver=" +
-                            Param.STRING_THEORY_DESC(baseSettings),
-                          1000000000,
-                          2000),
-                        ParallelFileProver.Configuration(
-                          Param.STRING_THEORY_DESC.set(
-                                  baseSettings,
-                                  Param.STRING_THEORY_DESC.defau),
-                          "-stringSolver=" +
-                            Param.STRING_THEORY_DESC.defau,
-                          1000000000,
-                          2000),
-                        ParallelFileProver.Configuration(
-                          Param.STRING_THEORY_DESC.set(
-                                  baseSettings,
-                                  ceaStringTheory),
-                          "-stringSolver=" +
-                            ceaStringTheory,
-                          1000000000,
-                          2000))
-                 ParallelFileProver(createReader,
-                                    timeout,
-                                    true,
-                                    userDefStoppingCond(),
-                                    strategies,
-                                    1,
-                                    3,
-                                    runUntilProof,
-                                    prelResultPrinter,
-                                    threadNum)
-               })
+      import arguments._
+      val strategies =
+        List(
+          ParallelFileProver.Configuration(
+          baseSettings,
+          "-stringSolver=" +
+            Param.STRING_THEORY_DESC(baseSettings),
+          1000000000,
+          2000),
+          ParallelFileProver.Configuration(
+            Param.STRING_THEORY_DESC.set(
+              baseSettings,
+              Param.STRING_THEORY_DESC.defau),
+            "-stringSolver=" +
+              Param.STRING_THEORY_DESC.defau,
+            1000000000,
+            2000),
+          ParallelFileProver.Configuration(
+            Param.STRING_THEORY_DESC.set(
+              baseSettings,
+              ceaStringTheory),
+            "-stringSolver=" +
+              ceaStringTheory,
+            1000000000,
+            2000),
+            ParallelFileProver.Configuration(
+          Param.STRING_THEORY_DESC.set(baseSettings, Param.STRING_THEORY_DESC(baseSettings) + ":+forwardBackward"),
+          "-stringSolver=" +
+            Param.STRING_THEORY_DESC(baseSettings) + ":+forwardBackward",
+          1000000000,
+          2000))
+      ParallelFileProver(createReader,
+        timeout,
+        true,
+        userDefStoppingCond(),
+        strategies,
+        1,
+        4,
+        runUntilProof,
+        prelResultPrinter,
+        threadNum)
+    })
+
 
   // Run the BW and ADT solvers
   ParallelFileProver.addPortfolio(