formatting

RipplB · Apr 30, 2024 · 67adb9c · 67adb9c
1 parent 819bc48
commit 67adb9c
Show file tree

Hide file tree

Showing 2 changed files with 34 additions and 44 deletions.
diff --git a/.../analysis/src/main/java/hu/bme/mit/theta/analysis/multi/builder/StmtMultiBuilderPair.java b/.../analysis/src/main/java/hu/bme/mit/theta/analysis/multi/builder/StmtMultiBuilderPair.java
@@ -27,8 +27,7 @@
 import hu.bme.mit.theta.analysis.multi.stmt.StmtMultiLts;
 import hu.bme.mit.theta.analysis.unit.UnitState;
 
-public final class StmtMultiBuilderPair<LState extends ExprState, LBlank extends ExprState, LAction extends StmtAction, DataState extends ExprState, LPrec extends Prec, LBlankPrec extends Prec,
-		RState extends ExprState, RBlank extends ExprState, RAction extends StmtAction, RPrec extends Prec, RBlankPrec extends Prec> {
+public final class StmtMultiBuilderPair<LState extends ExprState, LBlank extends ExprState, LAction extends StmtAction, DataState extends ExprState, LPrec extends Prec, LBlankPrec extends Prec, RState extends ExprState, RBlank extends ExprState, RAction extends StmtAction, RPrec extends Prec, RBlankPrec extends Prec> {
 
 	private final MultiAnalysisSide<LState, DataState, LBlank, LAction, LPrec, LBlankPrec> leftSide;
 	private final LTS<? super LState, LAction> leftLts;
@@ -42,16 +41,8 @@ public StmtMultiBuilderPair(MultiAnalysisSide<LState, DataState, LBlank, LAction
 		this.rightLts = rightLts;
 	}
 
-	public <DataPrec extends Prec> MultiBuilderResult
-			<LState, RState, DataState, LBlank, RBlank, LAction, RAction,
-					LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec, ExprMultiState<LBlank, RBlank, DataState>, ExprMultiState<LBlank, RBlank, UnitState>,
-					StmtMultiAction<LAction, RAction>,
-					StmtMultiLts<LState, RState, DataState, LBlank, RBlank, LAction, RAction>
-					> build(NextSideFunctions.NextSideFunction<LBlank, RBlank, DataState, ExprMultiState<LBlank, RBlank, DataState>> nextSideFunction,
-							InitFunc<DataState, DataPrec> dataInitFunc) {
-		return MultiBuilderResultKt.multiBuilderResult(
-				StmtMultiAnalysis.of(leftSide, rightSide, nextSideFunction::defineNextSide, dataInitFunc),
-				StmtMultiLts.of(leftLts, (lbs, ds) -> leftSide.getCombineStates().invoke(lbs, ds), rightLts, (rbs, ds) -> rightSide.getCombineStates().invoke(rbs, ds), nextSideFunction::defineNextSide));
+	public <DataPrec extends Prec> MultiBuilderResult<LState, RState, DataState, LBlank, RBlank, LAction, RAction, LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec, ExprMultiState<LBlank, RBlank, DataState>, ExprMultiState<LBlank, RBlank, UnitState>, StmtMultiAction<LAction, RAction>, StmtMultiLts<LState, RState, DataState, LBlank, RBlank, LAction, RAction>> build(NextSideFunctions.NextSideFunction<LBlank, RBlank, DataState, ExprMultiState<LBlank, RBlank, DataState>> nextSideFunction, InitFunc<DataState, DataPrec> dataInitFunc) {
+		return MultiBuilderResultKt.multiBuilderResult(StmtMultiAnalysis.of(leftSide, rightSide, nextSideFunction::defineNextSide, dataInitFunc), StmtMultiLts.of(leftLts, (lbs, ds) -> leftSide.getCombineStates().invoke(lbs, ds), rightLts, (rbs, ds) -> rightSide.getCombineStates().invoke(rbs, ds), nextSideFunction::defineNextSide));
 	}
 
 }
diff --git a/...analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/config/StmtMultiConfigBuilder.kt b/...analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/config/StmtMultiConfigBuilder.kt
@@ -39,13 +39,8 @@ import hu.bme.mit.theta.solver.SolverFactory
 import hu.bme.mit.theta.solver.UCSolver
 import java.util.function.Predicate
 
-sealed class StmtMultiConfigBuilder<
-        LState : ExprState, RState : ExprState, DataState : ExprState, LBlank : ExprState, RBlank : ExprState,
-        LAction : StmtAction, RAction : StmtAction, R : Refutation,
-        LPrec : Prec, RPrec : Prec, DataPrec : Prec, LBlankPrec : Prec, RBlankPrec : Prec>(
-    private val product: MultiBuilderResult<LState, RState, DataState, LBlank, RBlank, LAction, RAction, LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec,
-            ExprMultiState<LBlank, RBlank, DataState>, ExprMultiState<LBlank, RBlank, UnitState>, StmtMultiAction<LAction, RAction>,
-            StmtMultiLts<LState, RState, DataState, LBlank, RBlank, LAction, RAction>>,
+sealed class StmtMultiConfigBuilder<LState : ExprState, RState : ExprState, DataState : ExprState, LBlank : ExprState, RBlank : ExprState, LAction : StmtAction, RAction : StmtAction, R : Refutation, LPrec : Prec, RPrec : Prec, DataPrec : Prec, LBlankPrec : Prec, RBlankPrec : Prec>(
+    private val product: MultiBuilderResult<LState, RState, DataState, LBlank, RBlank, LAction, RAction, LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec, ExprMultiState<LBlank, RBlank, DataState>, ExprMultiState<LBlank, RBlank, UnitState>, StmtMultiAction<LAction, RAction>, StmtMultiLts<LState, RState, DataState, LBlank, RBlank, LAction, RAction>>,
     val prop: Expr<BoolType>,
     val target: Predicate<ExprMultiState<LBlank, RBlank, DataState>>,
     private val lRefToPrec: RefutationToPrec<LPrec, R>,
@@ -73,13 +68,8 @@ sealed class StmtMultiConfigBuilder<
         return MultiConfig(CegarChecker.create(abstractor, refiner), MultiPrec(lInitPrec, rInitPrec, dInitPrec))
     }
 
-    class ItpStmtMultiConfigBuilder<
-            LState : ExprState, RState : ExprState, DataState : ExprState, LBlank : ExprState, RBlank : ExprState,
-            LAction : StmtAction, RAction : StmtAction,
-            LPrec : Prec, RPrec : Prec, DataPrec : Prec, LBlankPrec : Prec, RBlankPrec : Prec>(
-        product: MultiBuilderResult<LState, RState, DataState, LBlank, RBlank, LAction, RAction, LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec,
-                ExprMultiState<LBlank, RBlank, DataState>, ExprMultiState<LBlank, RBlank, UnitState>, StmtMultiAction<LAction, RAction>,
-                StmtMultiLts<LState, RState, DataState, LBlank, RBlank, LAction, RAction>>,
+    class ItpStmtMultiConfigBuilder<LState : ExprState, RState : ExprState, DataState : ExprState, LBlank : ExprState, RBlank : ExprState, LAction : StmtAction, RAction : StmtAction, LPrec : Prec, RPrec : Prec, DataPrec : Prec, LBlankPrec : Prec, RBlankPrec : Prec>(
+        product: MultiBuilderResult<LState, RState, DataState, LBlank, RBlank, LAction, RAction, LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec, ExprMultiState<LBlank, RBlank, DataState>, ExprMultiState<LBlank, RBlank, UnitState>, StmtMultiAction<LAction, RAction>, StmtMultiLts<LState, RState, DataState, LBlank, RBlank, LAction, RAction>>,
         prop: Expr<BoolType>,
         target: Predicate<ExprMultiState<LBlank, RBlank, DataState>>,
         lRefToPrec: RefutationToPrec<LPrec, ItpRefutation>,
@@ -93,7 +83,16 @@ sealed class StmtMultiConfigBuilder<
         pruneStrategy: PruneStrategy = PruneStrategy.FULL,
         private val traceCheckerType: TraceCheckerType = TraceCheckerType.SEQ_ITP
     ) : StmtMultiConfigBuilder<LState, RState, DataState, LBlank, RBlank, LAction, RAction, ItpRefutation, LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec>(
-        product, prop, target, lRefToPrec, rRefToPrec, dRefToPrec, lInitPrec, rInitPrec, dInitPrec, solverFactory,
+        product,
+        prop,
+        target,
+        lRefToPrec,
+        rRefToPrec,
+        dRefToPrec,
+        lInitPrec,
+        rInitPrec,
+        dInitPrec,
+        solverFactory,
         logger,
         pruneStrategy
     ) {
@@ -102,25 +101,18 @@ sealed class StmtMultiConfigBuilder<
             val generator: (init: Expr<BoolType>, target: Expr<BoolType>, solver: ItpSolver) -> ExprTraceChecker<ItpRefutation>
         ) {
 
-            SEQ_ITP(ExprTraceSeqItpChecker::create),
-            FW_BIN(ExprTraceFwBinItpChecker::create),
-            BW_BIN(ExprTraceBwBinItpChecker::create)
+            SEQ_ITP(ExprTraceSeqItpChecker::create), FW_BIN(ExprTraceFwBinItpChecker::create), BW_BIN(
+                ExprTraceBwBinItpChecker::create
+            )
         }
 
         override fun getTraceChecker(): ExprTraceChecker<ItpRefutation> = traceCheckerType.generator(
-            BoolExprs.True(),
-            prop,
-            solverFactory.createItpSolver()
+            BoolExprs.True(), prop, solverFactory.createItpSolver()
         )
     }
 
-    class VarsStmtMultiConfigBuilder<
-            LState : ExprState, RState : ExprState, DataState : ExprState, LBlank : ExprState, RBlank : ExprState,
-            LAction : StmtAction, RAction : StmtAction,
-            LPrec : Prec, RPrec : Prec, DataPrec : Prec, LBlankPrec : Prec, RBlankPrec : Prec>(
-        product: MultiBuilderResult<LState, RState, DataState, LBlank, RBlank, LAction, RAction, LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec,
-                ExprMultiState<LBlank, RBlank, DataState>, ExprMultiState<LBlank, RBlank, UnitState>, StmtMultiAction<LAction, RAction>,
-                StmtMultiLts<LState, RState, DataState, LBlank, RBlank, LAction, RAction>>,
+    class VarsStmtMultiConfigBuilder<LState : ExprState, RState : ExprState, DataState : ExprState, LBlank : ExprState, RBlank : ExprState, LAction : StmtAction, RAction : StmtAction, LPrec : Prec, RPrec : Prec, DataPrec : Prec, LBlankPrec : Prec, RBlankPrec : Prec>(
+        product: MultiBuilderResult<LState, RState, DataState, LBlank, RBlank, LAction, RAction, LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec, ExprMultiState<LBlank, RBlank, DataState>, ExprMultiState<LBlank, RBlank, UnitState>, StmtMultiAction<LAction, RAction>, StmtMultiLts<LState, RState, DataState, LBlank, RBlank, LAction, RAction>>,
         prop: Expr<BoolType>,
         target: Predicate<ExprMultiState<LBlank, RBlank, DataState>>,
         lRefToPrec: RefutationToPrec<LPrec, VarsRefutation>,
@@ -134,7 +126,16 @@ sealed class StmtMultiConfigBuilder<
         pruneStrategy: PruneStrategy = PruneStrategy.FULL,
         private val traceCheckerType: TraceCheckerType = TraceCheckerType.UNSAT_CORE
     ) : StmtMultiConfigBuilder<LState, RState, DataState, LBlank, RBlank, LAction, RAction, VarsRefutation, LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec>(
-        product, prop, target, lRefToPrec, rRefToPrec, dRefToPrec, lInitPrec, rInitPrec, dInitPrec, solverFactory,
+        product,
+        prop,
+        target,
+        lRefToPrec,
+        rRefToPrec,
+        dRefToPrec,
+        lInitPrec,
+        rInitPrec,
+        dInitPrec,
+        solverFactory,
         logger,
         pruneStrategy
     ) {
@@ -147,9 +148,7 @@ sealed class StmtMultiConfigBuilder<
         }
 
         override fun getTraceChecker(): ExprTraceChecker<VarsRefutation> = traceCheckerType.generator(
-            BoolExprs.True(),
-            prop,
-            solverFactory.createUCSolver()
+            BoolExprs.True(), prop, solverFactory.createUCSolver()
         )
     }