Skip to content

Commit

Permalink
Clear air around MultiBuilderResult
Browse files Browse the repository at this point in the history
  • Loading branch information
@RipplB
RipplB committed May 20, 2024
1 parent df13bf8 commit 5be9f68
Show file tree
Hide file tree
Showing 4 changed files with 27 additions and 39 deletions.
4 changes: 2 additions & 2 deletions ...sis/multi/builder/MultiBuilderResult.java → ...multi/builder/MultiBuilderResultPOJO.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@
import hu.bme.mit.theta.analysis.unit.UnitPrec;
import hu.bme.mit.theta.analysis.unit.UnitState;

public class MultiBuilderResult<
public class MultiBuilderResultPOJO<
LState extends State, RState extends State, DataState extends State, LBlank extends State, RBlank extends State,
LAction extends Action, RAction extends Action,
LPrec extends Prec, RPrec extends Prec, DataPrec extends Prec, LBlankPrec extends Prec, RBlankPrec extends Prec,
Expand All @@ -35,7 +35,7 @@ public class MultiBuilderResult<
private final MultiAnalysisSide<MState, DataState, MBlankState, MAction, MultiPrec<LPrec, RPrec, DataPrec>, MultiPrec<LBlankPrec, RBlankPrec, UnitPrec>> side;
private final MLts lts;

public MultiBuilderResult(MultiAnalysisSide<MState, DataState, MBlankState, MAction, MultiPrec<LPrec, RPrec, DataPrec>, MultiPrec<LBlankPrec, RBlankPrec, UnitPrec>> side, MLts lts) {
public MultiBuilderResultPOJO(MultiAnalysisSide<MState, DataState, MBlankState, MAction, MultiPrec<LPrec, RPrec, DataPrec>, MultiPrec<LBlankPrec, RBlankPrec, UnitPrec>> side, MLts lts) {
this.side = side;
this.lts = lts;
}
Expand Down
4 changes: 2 additions & 2 deletions ...ysis/src/main/java/hu/bme/mit/theta/analysis/multi/builder/stmt/StmtMultiBuilderPair.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@
import hu.bme.mit.theta.analysis.expr.StmtAction;
import hu.bme.mit.theta.analysis.multi.MultiAnalysisSide;
import hu.bme.mit.theta.analysis.multi.NextSideFunctions;
import hu.bme.mit.theta.analysis.multi.builder.MultiBuilderResult;
import hu.bme.mit.theta.analysis.multi.builder.MultiBuilderResultPOJO;
import hu.bme.mit.theta.analysis.multi.builder.MultiBuilderResultKt;
import hu.bme.mit.theta.analysis.multi.stmt.ExprMultiState;
import hu.bme.mit.theta.analysis.multi.stmt.StmtMultiAction;
Expand All @@ -43,7 +43,7 @@ public final class StmtMultiBuilderPair<LState extends ExprState, LBlank extends
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) {
public <DataPrec extends Prec> MultiBuilderResultPOJO<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));
}

Expand Down
50 changes: 19 additions & 31 deletions ...on/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/builder/MultiBuilderResult.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,37 +23,25 @@ import hu.bme.mit.theta.analysis.multi.*
import hu.bme.mit.theta.analysis.unit.UnitPrec
import hu.bme.mit.theta.analysis.unit.UnitState

// The commented class in this file would be the appropriate solution, however, with
//IntelliJ IDEA 2024.1 (Ultimate Edition)
//Build #IU-241.14494.240, built on March 28, 2024
//Runtime version: 17.0.10+8-b1207.12 amd64
//VM: OpenJDK 64-Bit Server VM by JetBrains s.r.o.
//Windows 10.0
//GC: G1 Young Generation, G1 Old Generation
//Memory: 12288M
//Cores: 12
//Registry:
//debugger.new.tool.window.layout=true
//ide.experimental.ui=true
//Non-Bundled Plugins:
//com.github.lonre.gruvbox-intellij-theme (0.6.2)
//Kotlin: 241.14494.240-IJ
// the usage of this class, or any other solution in this file causes the kotlin plugin to crash, maybe even crashing
// The following class in this file should be used, however, with
// IntelliJ IDEA 2024.1 (Ultimate Edition)
// Build #IU-241.14494.240, built on March 28, 2024
// Kotlin: 241.14494.240-IJ
// the usage of this class causes the kotlin plugin to crash, maybe even crashing
// the whole IDE. For this reason, a POJO has to be used instead

//data class MultiBuilderResult
//<
// LState : State, RState : State, DataState : State, LBlank : State, RBlank : State,
// LAction : Action, RAction : Action,
// LPrec : Prec, RPrec : Prec, DataPrec : Prec, LBlankPrec : Prec, RBlankPrec : Prec,
// MState : MultiState<LBlank, RBlank, DataState>, MBlankState : MultiState<LBlank, RBlank, UnitState>, MAction : MultiAction<LAction, RAction>,
// MAnalysis : MultiAnalysis<LState, RState, DataState, LBlank, RBlank, LAction, RAction, LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec, MState, MBlankState, MAction>,
// MLts : MultiLts<LState, RState, DataState, LBlank, RBlank, LAction, RAction, MState, MAction>
// >
// (
// val side: MultiAnalysisSide<MState, DataState, MBlankState, MAction, MultiPrec<LPrec, RPrec, DataPrec>, MultiPrec<LBlankPrec, RBlankPrec, UnitPrec>>,
// val lts: MLts
//)
data class MultiBuilderResult
<
LState : State, RState : State, DataState : State, LBlank : State, RBlank : State,
LAction : Action, RAction : Action,
LPrec : Prec, RPrec : Prec, DataPrec : Prec, LBlankPrec : Prec, RBlankPrec : Prec,
MState : MultiState<LBlank, RBlank, DataState>, MBlankState : MultiState<LBlank, RBlank, UnitState>, MAction : MultiAction<LAction, RAction>,
MLts : MultiLts<LState, RState, DataState, LBlank, RBlank, LAction, RAction, MState, MAction>
>
(
val side: MultiAnalysisSide<MState, DataState, MBlankState, MAction, MultiPrec<LPrec, RPrec, DataPrec>, MultiPrec<LBlankPrec, RBlankPrec, UnitPrec>>,
val lts: MLts
)

internal fun <
LState : State, RState : State, DataState : State, LBlank : State, RBlank : State,
Expand All @@ -63,7 +51,7 @@ internal fun <
MAnalysis : MultiAnalysis<LState, RState, DataState, LBlank, RBlank, LAction, RAction, LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec, MState, MBlankState, MAction>,
MLts : MultiLts<LState, RState, DataState, LBlank, RBlank, LAction, RAction, MState, MAction>
> multiBuilderResult(analysis: MAnalysis, lts: MLts):
MultiBuilderResult<LState, RState, DataState, LBlank, RBlank, LAction, RAction, LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec, MState, MBlankState, MAction, MLts> {
MultiBuilderResultPOJO<LState, RState, DataState, LBlank, RBlank, LAction, RAction, LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec, MState, MBlankState, MAction, MLts> {
val side =
MultiAnalysisSide<MState, DataState, MBlankState, MAction, MultiPrec<LPrec, RPrec, DataPrec>, MultiPrec<LBlankPrec, RBlankPrec, UnitPrec>>(
analysis,
Expand All @@ -84,5 +72,5 @@ internal fun <
)
}
)
return MultiBuilderResult(side, lts)
return MultiBuilderResultPOJO(side, lts)
}
8 changes: 4 additions & 4 deletions ...analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/config/StmtMultiConfigBuilder.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ import hu.bme.mit.theta.analysis.expr.StmtAction
import hu.bme.mit.theta.analysis.expr.refinement.*
import hu.bme.mit.theta.analysis.multi.MultiPrec
import hu.bme.mit.theta.analysis.multi.RefToMultiPrec
import hu.bme.mit.theta.analysis.multi.builder.MultiBuilderResult
import hu.bme.mit.theta.analysis.multi.builder.MultiBuilderResultPOJO
import hu.bme.mit.theta.analysis.multi.stmt.ExprMultiState
import hu.bme.mit.theta.analysis.multi.stmt.StmtMultiAction
import hu.bme.mit.theta.analysis.multi.stmt.StmtMultiLts
Expand All @@ -40,7 +40,7 @@ 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>>,
private val product: MultiBuilderResultPOJO<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>,
Expand Down Expand Up @@ -69,7 +69,7 @@ sealed class StmtMultiConfigBuilder<LState : ExprState, RState : ExprState, Data
}

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>>,
product: MultiBuilderResultPOJO<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>,
Expand Down Expand Up @@ -112,7 +112,7 @@ sealed class StmtMultiConfigBuilder<LState : ExprState, RState : ExprState, Data
}

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>>,
product: MultiBuilderResultPOJO<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>,
Expand Down

0 comments on commit 5be9f68

Please sign in to comment.