diff --git a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/config/ItpStmtMultiConfigBuilder.kt b/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/config/ItpStmtMultiConfigBuilder.kt deleted file mode 100644 index ac1e2d911d..0000000000 --- a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/config/ItpStmtMultiConfigBuilder.kt +++ /dev/null @@ -1,66 +0,0 @@ -/* - * Copyright 2024 Budapest University of Technology and Economics - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ - -package hu.bme.mit.theta.analysis.multi.config - -import hu.bme.mit.theta.analysis.Prec -import hu.bme.mit.theta.analysis.expr.ExprState -import hu.bme.mit.theta.analysis.expr.StmtAction -import hu.bme.mit.theta.analysis.expr.refinement.* -import hu.bme.mit.theta.analysis.multi.MultiBuilder -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.True -import hu.bme.mit.theta.core.type.booltype.BoolType -import hu.bme.mit.theta.solver.ItpSolver -import hu.bme.mit.theta.solver.SolverFactory -import java.util.function.Predicate - -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, MAction : StmtMultiAction>( - product: MultiBuilder.Result, - prop: Expr, - target: Predicate, - lRefToPrec: RefutationToPrec, - rRefToPrec: RefutationToPrec, - dRefToPrec: RefutationToPrec, - lInitPrec: LPrec, - rInitPrec: RPrec, - dInitPrec: DataPrec, - solverFactory: SolverFactory, - logger: Logger, - pruneStrategy: PruneStrategy = PruneStrategy.FULL, - private val traceCheckerType: TraceCheckerType = TraceCheckerType.SEQ_ITP -) : StmtMultiConfigBuilder( - product, prop, target, lRefToPrec, rRefToPrec, dRefToPrec, lInitPrec, rInitPrec, dInitPrec, solverFactory, logger, - pruneStrategy) { - - enum class TraceCheckerType( - val generator: (init: Expr, target: Expr, solver: ItpSolver) -> ExprTraceChecker) { - - SEQ_ITP(ExprTraceSeqItpChecker::create), - FW_BIN(ExprTraceFwBinItpChecker::create), - BW_BIN(ExprTraceBwBinItpChecker::create) - } - - override fun getTraceChecker(): ExprTraceChecker = traceCheckerType.generator(True(), prop, - solverFactory.createItpSolver()) -} \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/config/StmtMultiConfigBuilder.kt b/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/config/StmtMultiConfigBuilder.kt index 8468590ea6..9bfc47a619 100644 --- a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/config/StmtMultiConfigBuilder.kt +++ b/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/config/StmtMultiConfigBuilder.kt @@ -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, @@ -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)) } -} \ No newline at end of file + + 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, MAction : StmtMultiAction>( + product: MultiBuilder.Result, + prop: Expr, + target: Predicate, + lRefToPrec: RefutationToPrec, + rRefToPrec: RefutationToPrec, + dRefToPrec: RefutationToPrec, + lInitPrec: LPrec, + rInitPrec: RPrec, + dInitPrec: DataPrec, + solverFactory: SolverFactory, + logger: Logger, + pruneStrategy: PruneStrategy = PruneStrategy.FULL, + private val traceCheckerType: TraceCheckerType = TraceCheckerType.SEQ_ITP + ) : StmtMultiConfigBuilder( + product, prop, target, lRefToPrec, rRefToPrec, dRefToPrec, lInitPrec, rInitPrec, dInitPrec, solverFactory, + logger, + pruneStrategy) { + + enum class TraceCheckerType( + val generator: (init: Expr, target: Expr, solver: ItpSolver) -> ExprTraceChecker) { + + SEQ_ITP(ExprTraceSeqItpChecker::create), + FW_BIN(ExprTraceFwBinItpChecker::create), + BW_BIN(ExprTraceBwBinItpChecker::create) + } + + override fun getTraceChecker(): ExprTraceChecker = 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, MAction : StmtMultiAction>( + product: MultiBuilder.Result, + prop: Expr, + target: Predicate, + lRefToPrec: RefutationToPrec, + rRefToPrec: RefutationToPrec, + dRefToPrec: RefutationToPrec, + lInitPrec: LPrec, + rInitPrec: RPrec, + dInitPrec: DataPrec, + solverFactory: SolverFactory, + logger: Logger, + pruneStrategy: PruneStrategy = PruneStrategy.FULL, + private val traceCheckerType: TraceCheckerType = TraceCheckerType.UNSAT_CORE + ) : StmtMultiConfigBuilder( + product, prop, target, lRefToPrec, rRefToPrec, dRefToPrec, lInitPrec, rInitPrec, dInitPrec, solverFactory, + logger, + pruneStrategy) { + + enum class TraceCheckerType( + val generator: (init: Expr, target: Expr, solver: UCSolver) -> ExprTraceChecker) { + + UNSAT_CORE(ExprTraceUnsatCoreChecker::create) + } + + override fun getTraceChecker(): ExprTraceChecker = traceCheckerType.generator(BoolExprs.True(), + prop, + solverFactory.createUCSolver()) + } + +} diff --git a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/config/VarsStmtMultiConfigBuilder.kt b/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/config/VarsStmtMultiConfigBuilder.kt deleted file mode 100644 index 86ff077830..0000000000 --- a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/config/VarsStmtMultiConfigBuilder.kt +++ /dev/null @@ -1,64 +0,0 @@ -/* - * Copyright 2024 Budapest University of Technology and Economics - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ - -package hu.bme.mit.theta.analysis.multi.config - -import hu.bme.mit.theta.analysis.Prec -import hu.bme.mit.theta.analysis.expr.ExprState -import hu.bme.mit.theta.analysis.expr.StmtAction -import hu.bme.mit.theta.analysis.expr.refinement.* -import hu.bme.mit.theta.analysis.multi.MultiBuilder -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.True -import hu.bme.mit.theta.core.type.booltype.BoolType -import hu.bme.mit.theta.solver.SolverFactory -import hu.bme.mit.theta.solver.UCSolver -import java.util.function.Predicate - -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, MAction : StmtMultiAction>( - product: MultiBuilder.Result, - prop: Expr, - target: Predicate, - lRefToPrec: RefutationToPrec, - rRefToPrec: RefutationToPrec, - dRefToPrec: RefutationToPrec, - lInitPrec: LPrec, - rInitPrec: RPrec, - dInitPrec: DataPrec, - solverFactory: SolverFactory, - logger: Logger, - pruneStrategy: PruneStrategy = PruneStrategy.FULL, - private val traceCheckerType: TraceCheckerType = TraceCheckerType.UNSAT_CORE -) : StmtMultiConfigBuilder( - product, prop, target, lRefToPrec, rRefToPrec, dRefToPrec, lInitPrec, rInitPrec, dInitPrec, solverFactory, logger, - pruneStrategy) { - - enum class TraceCheckerType( - val generator: (init: Expr, target: Expr, solver: UCSolver) -> ExprTraceChecker) { - - UNSAT_CORE(ExprTraceUnsatCoreChecker::create) - } - - override fun getTraceChecker(): ExprTraceChecker = traceCheckerType.generator(True(), prop, - solverFactory.createUCSolver()) -} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/kotlin/hu/bme/mit/theta/analysis/multi/MultiOfTwoTest.kt b/subprojects/common/analysis/src/test/kotlin/hu/bme/mit/theta/analysis/multi/MultiOfTwoTest.kt index d44686281c..159c77f136 100644 --- a/subprojects/common/analysis/src/test/kotlin/hu/bme/mit/theta/analysis/multi/MultiOfTwoTest.kt +++ b/subprojects/common/analysis/src/test/kotlin/hu/bme/mit/theta/analysis/multi/MultiOfTwoTest.kt @@ -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 @@ -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() @@ -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()