From 3b88e0a39941d5d31a150aa196baebc6f417b4d4 Mon Sep 17 00:00:00 2001 From: Oliver Markgraf Date: Wed, 29 May 2024 16:56:37 +0200 Subject: [PATCH] add RCP to portfolio --- src/main/scala/ostrich/OstrichMain.scala | 80 +++++++++++++----------- 1 file changed, 44 insertions(+), 36 deletions(-) diff --git a/src/main/scala/ostrich/OstrichMain.scala b/src/main/scala/ostrich/OstrichMain.scala index 37e8a4dc71..f47a8d3d13 100644 --- 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(