From 46a66aa3f0a3391f33b6213c8bbe3871e17ef0cd Mon Sep 17 00:00:00 2001 From: mondokm Date: Wed, 19 Feb 2025 16:05:35 +0100 Subject: [PATCH] Move L2S --- .../theta/analysis/{l2s => algorithm/bounded}/MonolithicL2S.kt | 3 +-- .../bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt | 3 +-- .../hu/bme/mit/theta/xsts/cli/XstsCliMonolithicBaseCommand.kt | 2 +- 3 files changed, 3 insertions(+), 5 deletions(-) rename subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/{l2s => algorithm/bounded}/MonolithicL2S.kt (96%) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/l2s/MonolithicL2S.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicL2S.kt similarity index 96% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/l2s/MonolithicL2S.kt rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicL2S.kt index ff703ebeb1..06ad8e0a90 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/l2s/MonolithicL2S.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicL2S.kt @@ -13,9 +13,8 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package hu.bme.mit.theta.analysis.l2s +package hu.bme.mit.theta.analysis.algorithm.bounded -import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr import hu.bme.mit.theta.common.container.Containers import hu.bme.mit.theta.core.decl.Decls import hu.bme.mit.theta.core.decl.VarDecl diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt index 0e8ac433e7..eb69cfb781 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt @@ -20,7 +20,7 @@ import hu.bme.mit.theta.analysis.algorithm.EmptyProof import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.algorithm.bounded.* -import hu.bme.mit.theta.analysis.l2s.createMonolithicL2S +import hu.bme.mit.theta.analysis.algorithm.bounded.createMonolithicL2S import hu.bme.mit.theta.analysis.pred.PredPrec import hu.bme.mit.theta.analysis.pred.PredState import hu.bme.mit.theta.analysis.ptr.PtrPrec @@ -35,7 +35,6 @@ import hu.bme.mit.theta.xcfa.cli.params.BoundedConfig import hu.bme.mit.theta.xcfa.cli.params.XcfaConfig import hu.bme.mit.theta.xcfa.cli.utils.getSolver import hu.bme.mit.theta.xcfa.model.XCFA -import java.util.* fun getBoundedChecker( xcfa: XCFA, diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMonolithicBaseCommand.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMonolithicBaseCommand.kt index f11f526c79..4e73a05413 100644 --- a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMonolithicBaseCommand.kt +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMonolithicBaseCommand.kt @@ -20,7 +20,7 @@ import com.github.ajalt.clikt.parameters.options.option import com.github.ajalt.clikt.parameters.types.boolean import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr import hu.bme.mit.theta.analysis.algorithm.bounded.createReversed -import hu.bme.mit.theta.analysis.l2s.createMonolithicL2S +import hu.bme.mit.theta.analysis.algorithm.bounded.createMonolithicL2S import hu.bme.mit.theta.xsts.XSTS import hu.bme.mit.theta.xsts.analysis.hu.bme.mit.theta.xsts.analysis.toMonolithicExpr