Skip to content

Commit

Permalink
MultiConfigBuilder as sealed and move implementations under it
Browse files Browse the repository at this point in the history
  • Loading branch information
RipplB committed Apr 16, 2024
1 parent fc1e1fe commit bdd55d8
Show file tree
Hide file tree
Showing 4 changed files with 81 additions and 135 deletions.
66 changes: 0 additions & 66 deletions ...lysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/config/ItpStmtMultiConfigBuilder.kt
View file

This file was deleted.

78 changes: 76 additions & 2 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 @@ -30,11 +30,14 @@ import hu.bme.mit.theta.analysis.multi.stmt.ExprMultiState
import hu.bme.mit.theta.analysis.multi.stmt.StmtMultiAction
import hu.bme.mit.theta.common.logging.Logger
import hu.bme.mit.theta.core.type.Expr
import hu.bme.mit.theta.core.type.booltype.BoolExprs
import hu.bme.mit.theta.core.type.booltype.BoolType
import hu.bme.mit.theta.solver.ItpSolver
import hu.bme.mit.theta.solver.SolverFactory
import hu.bme.mit.theta.solver.UCSolver
import java.util.function.Predicate

abstract class StmtMultiConfigBuilder<
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,
Expand Down Expand Up @@ -66,4 +69,75 @@ abstract class StmtMultiConfigBuilder<
val refiner = SingleExprTraceRefiner.create(traceChecker, precRefiner, pruneStrategy, logger)
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,
MState : ExprMultiState<LBlank, RBlank, DataState>, MAction : StmtMultiAction<LAction, RAction>>(
product: MultiBuilder.Result<LState, RState, DataState, LBlank, RBlank, LAction, RAction, LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec, MState, MAction>,
prop: Expr<BoolType>,
target: Predicate<MState>,
lRefToPrec: RefutationToPrec<LPrec, ItpRefutation>,
rRefToPrec: RefutationToPrec<RPrec, ItpRefutation>,
dRefToPrec: RefutationToPrec<DataPrec, ItpRefutation>,
lInitPrec: LPrec,
rInitPrec: RPrec,
dInitPrec: DataPrec,
solverFactory: SolverFactory,
logger: Logger,
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, MState, MAction>(
product, prop, target, lRefToPrec, rRefToPrec, dRefToPrec, lInitPrec, rInitPrec, dInitPrec, solverFactory,
logger,
pruneStrategy) {

enum class TraceCheckerType(
val generator: (init: Expr<BoolType>, target: Expr<BoolType>, solver: ItpSolver) -> ExprTraceChecker<ItpRefutation>) {

SEQ_ITP(ExprTraceSeqItpChecker::create),
FW_BIN(ExprTraceFwBinItpChecker::create),
BW_BIN(ExprTraceBwBinItpChecker::create)
}

override fun getTraceChecker(): ExprTraceChecker<ItpRefutation> = traceCheckerType.generator(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,
MState : ExprMultiState<LBlank, RBlank, DataState>, MAction : StmtMultiAction<LAction, RAction>>(
product: MultiBuilder.Result<LState, RState, DataState, LBlank, RBlank, LAction, RAction, LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec, MState, MAction>,
prop: Expr<BoolType>,
target: Predicate<MState>,
lRefToPrec: RefutationToPrec<LPrec, VarsRefutation>,
rRefToPrec: RefutationToPrec<RPrec, VarsRefutation>,
dRefToPrec: RefutationToPrec<DataPrec, VarsRefutation>,
lInitPrec: LPrec,
rInitPrec: RPrec,
dInitPrec: DataPrec,
solverFactory: SolverFactory,
logger: Logger,
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, MState, MAction>(
product, prop, target, lRefToPrec, rRefToPrec, dRefToPrec, lInitPrec, rInitPrec, dInitPrec, solverFactory,
logger,
pruneStrategy) {

enum class TraceCheckerType(
val generator: (init: Expr<BoolType>, target: Expr<BoolType>, solver: UCSolver) -> ExprTraceChecker<VarsRefutation>) {

UNSAT_CORE(ExprTraceUnsatCoreChecker::create)
}

override fun getTraceChecker(): ExprTraceChecker<VarsRefutation> = traceCheckerType.generator(BoolExprs.True(),
prop,
solverFactory.createUCSolver())
}

}
64 changes: 0 additions & 64 deletions ...ysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/config/VarsStmtMultiConfigBuilder.kt
View file

This file was deleted.

8 changes: 5 additions & 3 deletions ...rojects/common/analysis/src/test/kotlin/hu/bme/mit/theta/analysis/multi/MultiOfTwoTest.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ import hu.bme.mit.theta.analysis.expl.ExplState
import hu.bme.mit.theta.analysis.expl.ExplStatePredicate
import hu.bme.mit.theta.analysis.expl.ItpRefToExplPrec
import hu.bme.mit.theta.analysis.expr.ExprStatePredicate
import hu.bme.mit.theta.analysis.multi.config.ItpStmtMultiConfigBuilder
import hu.bme.mit.theta.analysis.multi.config.StmtMultiConfigBuilder
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.StmtMultiAnalysis
Expand Down Expand Up @@ -108,7 +108,8 @@ class MultiOfTwoTest {
{ llts, cls, rlts, crs, dns -> StmtMultiLts.of(llts, cls, rlts, crs, dns) })
val prop = Not(xsts.prop)
val dataPredicate = ExplStatePredicate(prop, solver)
val multiConfigBuilder = ItpStmtMultiConfigBuilder(product, prop, { s -> dataPredicate.test(s.dataState) },
val multiConfigBuilder = StmtMultiConfigBuilder.ItpStmtMultiConfigBuilder(product, prop,
{ s -> dataPredicate.test(s.dataState) },
cfaRefToPrec, ItpRefToExplPrec(), ItpRefToExplPrec(), cfaInitPrec,
dataInitPrec, dataInitPrec, Z3SolverFactory.getInstance(), logger)
val result = multiConfigBuilder.build().check()
Expand Down Expand Up @@ -165,7 +166,8 @@ class MultiOfTwoTest {
val prop = Not(xsts.prop)
val dataPredicate = ExprStatePredicate(prop, solver)

val multiConfigBuilder = ItpStmtMultiConfigBuilder(product, prop, { s -> dataPredicate.test(s.dataState) },
val multiConfigBuilder = StmtMultiConfigBuilder.ItpStmtMultiConfigBuilder(product, prop,
{ s -> dataPredicate.test(s.dataState) },
cfaRefToPrec, ItpRefToPredPrec(ExprSplitters.atoms()), ItpRefToPredPrec(ExprSplitters.atoms()), cfaInitPrec,
dataInitPrec, dataInitPrec, Z3SolverFactory.getInstance(), logger)
val result = multiConfigBuilder.build().check()
Expand Down

0 comments on commit bdd55d8

Please sign in to comment.