diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/AbstractMonolithicExpr.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/AbstractMonolithicExpr.kt new file mode 100644 index 0000000000..04427ecfac --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/AbstractMonolithicExpr.kt @@ -0,0 +1,84 @@ +/* + * 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.algorithm.bounded + +import hu.bme.mit.theta.analysis.pred.PredPrec +import hu.bme.mit.theta.analysis.pred.PredState +import hu.bme.mit.theta.core.decl.Decl +import hu.bme.mit.theta.core.decl.Decls +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.model.Valuation +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.anytype.Exprs +import hu.bme.mit.theta.core.type.booltype.BoolExprs +import hu.bme.mit.theta.core.type.booltype.BoolLitExpr +import hu.bme.mit.theta.core.type.booltype.BoolType +import hu.bme.mit.theta.core.type.booltype.IffExpr +import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.And +import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.Not +import hu.bme.mit.theta.core.utils.ExprUtils +import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory +import java.util.HashMap + +fun MonolithicExpr.createAbstract(prec: PredPrec): MonolithicExpr { + // TODO: handle initOffsetIndex in abstract initExpr + val lambdaList = ArrayList() + val lambdaPrimeList = ArrayList() + val activationLiterals = ArrayList>() + val literalToPred = HashMap, Expr>() + + prec.preds.forEachIndexed { index, expr -> + run { + val v = Decls.Var("v$index", BoolType.getInstance()) + activationLiterals.add(v) + literalToPred[v] = expr + lambdaList.add(IffExpr.of(v.ref, expr)) + lambdaPrimeList.add( + BoolExprs.Iff(Exprs.Prime(v.ref), ExprUtils.applyPrimes(expr, this.transOffsetIndex)) + ) + } + } + + var indexingBuilder = VarIndexingFactory.indexingBuilder(1) + this.vars./*filter { it !in ctrlVars }.*/ forEach { decl -> + repeat(transOffsetIndex.get(decl)) { indexingBuilder = indexingBuilder.inc(decl) } + } + + return MonolithicExpr( + initExpr = And(And(lambdaList), initExpr), + transExpr = And(And(lambdaList), And(lambdaPrimeList), transExpr), + propExpr = Not(And(And(lambdaList), Not(propExpr))), + transOffsetIndex = indexingBuilder.build(), + initOffsetIndex = VarIndexingFactory.indexing(0), + vars = activationLiterals /* + ctrlVars*/, + valToState = { valuation: Valuation -> + PredState.of( + valuation + .toMap() + .entries + .stream() + .map { + when ((it.value as BoolLitExpr).value) { + true -> literalToPred[it.key] + false -> Not(literalToPred[it.key]) + } + } + .toList() + ) + }, + biValToAction = this.biValToAction, + ) +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExpr.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExpr.kt index e87e1b3c13..f1f9146cd2 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExpr.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExpr.kt @@ -15,14 +15,20 @@ */ package hu.bme.mit.theta.analysis.algorithm.bounded +import hu.bme.mit.theta.analysis.expl.ExplState +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.model.Valuation import hu.bme.mit.theta.core.type.Expr import hu.bme.mit.theta.core.type.booltype.BoolType import hu.bme.mit.theta.core.utils.ExprUtils.getVars import hu.bme.mit.theta.core.utils.indexings.VarIndexing import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory -data class MonolithicExpr( +data class MonolithicExpr +@JvmOverloads +constructor( val initExpr: Expr, val transExpr: Expr, val propExpr: Expr, @@ -30,4 +36,13 @@ data class MonolithicExpr( val initOffsetIndex: VarIndexing = VarIndexingFactory.indexing(0), val vars: List> = (getVars(initExpr) union getVars(transExpr) union getVars(propExpr)).toList(), + val valToState: (Valuation) -> ExprState = ExplState::of, + val biValToAction: (Valuation, Valuation) -> ExprAction = { _: Valuation, _: Valuation -> + object : ExprAction { + override fun toExpr(): Expr = transExpr + + override fun nextIndexing(): VarIndexing = transOffsetIndex + } + }, + val ctrlVars: Collection> = listOf(), ) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExprCegarChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExprCegarChecker.java new file mode 100644 index 0000000000..385a5e572e --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExprCegarChecker.java @@ -0,0 +1,137 @@ +/* + * 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.algorithm.bounded; + +import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.Not; + +import com.google.common.base.Preconditions; +import hu.bme.mit.theta.analysis.*; +import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; +import hu.bme.mit.theta.analysis.algorithm.SafetyResult; +import hu.bme.mit.theta.analysis.algorithm.Witness; +import hu.bme.mit.theta.analysis.expr.ExprAction; +import hu.bme.mit.theta.analysis.expr.ExprState; +import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceChecker; +import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceFwBinItpChecker; +import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceStatus; +import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation; +import hu.bme.mit.theta.analysis.pred.PredPrec; +import hu.bme.mit.theta.analysis.unit.UnitPrec; +import hu.bme.mit.theta.common.logging.Logger; +import hu.bme.mit.theta.core.model.Valuation; +import hu.bme.mit.theta.solver.SolverFactory; +import java.util.ArrayList; +import java.util.List; +import java.util.function.BiFunction; +import java.util.function.Function; + +public class MonolithicExprCegarChecker< + W extends Witness, S extends ExprState, A extends ExprAction, P extends Prec> + implements SafetyChecker, PredPrec> { + private final MonolithicExpr model; + private final Function< + MonolithicExpr, + SafetyChecker< + W, + ? extends Trace, + UnitPrec>> + checkerFactory; + + private final Function valToState; + private final BiFunction biValToAction; + + private final SolverFactory solverFactory; + + private final Logger logger; + + public MonolithicExprCegarChecker( + MonolithicExpr model, + Function< + MonolithicExpr, + SafetyChecker< + W, + ? extends Trace, + UnitPrec>> + checkerFactory, + Function valToState, + BiFunction biValToAction, + Logger logger, + SolverFactory solverFactory) { + this.model = model; + this.checkerFactory = checkerFactory; + this.valToState = valToState; + this.biValToAction = biValToAction; + this.logger = logger; + this.solverFactory = solverFactory; + } + + public SafetyResult> check(PredPrec initPrec) { + var predPrec = + initPrec == null + ? PredPrec.of(List.of(model.getInitExpr(), model.getPropExpr())) + : initPrec; + + while (true) { + final var abstractMonolithicExpr = + AbstractMonolithicExprKt.createAbstract(model, predPrec); + final var checker = checkerFactory.apply(abstractMonolithicExpr); + + final var result = checker.check(); + if (result.isSafe()) { + logger.write(Logger.Level.INFO, "Model is safe, stopping CEGAR"); + return SafetyResult.safe(result.getWitness()); + } else { + Preconditions.checkState(result.isUnsafe()); + final Trace trace = + result.asUnsafe().getCex(); + + final ExprTraceChecker exprTraceFwBinItpChecker = + ExprTraceFwBinItpChecker.create( + model.getInitExpr(), + Not(model.getPropExpr()), + solverFactory.createItpSolver()); + + if (trace != null) { + final ExprTraceStatus concretizationResult = + exprTraceFwBinItpChecker.check(trace); + if (concretizationResult.isFeasible()) { + logger.write(Logger.Level.INFO, "Model is unsafe, stopping CEGAR"); + + final var valTrace = concretizationResult.asFeasible().getValuations(); + Valuation lastValuation = null; + final ArrayList states = new ArrayList<>(); + final ArrayList actions = new ArrayList<>(); + for (var val : valTrace.getStates()) { + states.add(valToState.apply(val)); + if (lastValuation != null) { + actions.add(biValToAction.apply(lastValuation, val)); + } + lastValuation = val; + } + + return SafetyResult.unsafe(Trace.of(states, actions), result.getWitness()); + } else { + final var ref = concretizationResult.asInfeasible().getRefutation(); + final var newPred = ref.get(ref.getPruneIndex()); + final var newPrec = PredPrec.of(newPred); + predPrec = predPrec.join(newPrec); + logger.write(Logger.Level.INFO, "Added new predicate " + newPrec); + } + } + } + } + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/ReversedMonolithicExpr.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/ReversedMonolithicExpr.kt new file mode 100644 index 0000000000..6e8481e55e --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/ReversedMonolithicExpr.kt @@ -0,0 +1,31 @@ +/* + * 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.algorithm.bounded + +import hu.bme.mit.theta.core.type.booltype.BoolExprs.Not +import hu.bme.mit.theta.core.utils.ExprUtils +import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory + +fun MonolithicExpr.createReversed(): MonolithicExpr { + return MonolithicExpr( + initExpr = Not(propExpr), + transExpr = ExprUtils.reverse(transExpr, transOffsetIndex), + propExpr = Not(initExpr), + transOffsetIndex = transOffsetIndex, + initOffsetIndex = VarIndexingFactory.indexing(0), + vars = vars, + ) +} diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/anytype/Exprs.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/anytype/Exprs.java index 4a55648279..04df53164b 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/anytype/Exprs.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/anytype/Exprs.java @@ -15,25 +15,23 @@ */ package hu.bme.mit.theta.core.type.anytype; +import static com.google.common.base.Preconditions.checkArgument; + import hu.bme.mit.theta.core.decl.Decl; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.Type; import hu.bme.mit.theta.core.type.booltype.BoolType; -import static com.google.common.base.Preconditions.checkArgument; - public final class Exprs { - private Exprs() { - } + private Exprs() {} public static RefExpr Ref(final Decl decl) { return RefExpr.of(decl); } - public static IteExpr Ite(final Expr cond, - final Expr then, - final Expr elze) { + public static IteExpr Ite( + final Expr cond, final Expr then, final Expr elze) { return IteExpr.of(cond, then, elze); } @@ -42,12 +40,13 @@ public static PrimeExpr Prime(final Expr - Dereference Dereference(final Expr arr, final Expr offset, final ExprType type) { + Dereference Dereference( + final Expr arr, final Expr offset, final ExprType type) { return Dereference.of(arr, offset, type); } public static - Reference Reference(final Expr expr, final ArrType type) { + Reference Reference(final Expr expr, final ArrType type) { return Reference.of(expr, type); } @@ -55,14 +54,15 @@ Reference Reference(final Expr expr, final ArrType * Convenience methods */ - public static PrimeExpr Prime(final Expr op, - final int i) { - checkArgument(i > 0); - if (i == 1) { + public static Expr Prime( + final Expr op, final int i) { + checkArgument(i >= 0); + if (i == 0) { + return op; + } else if (i == 1) { return Prime(op); } else { return Prime(Prime(op, i - 1)); } } - } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprReverser.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprReverser.java new file mode 100644 index 0000000000..d69449e845 --- /dev/null +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprReverser.java @@ -0,0 +1,135 @@ +/* + * 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.core.utils; + +import static com.google.common.base.Preconditions.checkArgument; +import static hu.bme.mit.theta.core.type.anytype.Exprs.Prime; + +import hu.bme.mit.theta.common.DispatchTable; +import hu.bme.mit.theta.common.DispatchTable2; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.Type; +import hu.bme.mit.theta.core.type.anytype.PrimeExpr; +import hu.bme.mit.theta.core.type.anytype.RefExpr; +import hu.bme.mit.theta.core.utils.indexings.VarIndexing; + +public class ExprReverser { + + private final VarIndexing indexing; + + private final DispatchTable> TABLE = + DispatchTable.>builder() + .addCase(RefExpr.class, this::reverseRef) + .addCase(PrimeExpr.class, this::reversePrime) + + // Default + + .addDefault( + (o) -> { + final Expr expr = (Expr) o; + return expr.map(e -> reverseInner(e)); + }) + .build(); + + public ExprReverser(VarIndexing indexing) { + this.indexing = indexing; + } + + public Expr reverse(final Expr expr) { + final var transformed = PrimeToLeaves.transform(expr); + return (Expr) TABLE.dispatch(transformed); + } + + @SuppressWarnings("unchecked") + private Expr reverseInner(final Expr expr) { + return (Expr) TABLE.dispatch(expr); + } + + /* + * General + */ + + private Expr reverseRef(final RefExpr expr) { + final VarDecl varDecl = extractVarDecl(expr); + return reverse(varDecl, 0); + } + + private Expr reversePrime(final PrimeExpr expr) { + final int primeDepth = primeDepth(expr); + final VarDecl varDecl = extractVarDecl(expr); + return reverse(varDecl, primeDepth); + } + + private Expr reverse(final VarDecl decl, int primeDepth) { + checkArgument(primeDepth >= 0 && primeDepth <= indexing.get(decl)); + return Prime(decl.getRef(), indexing.get(decl) - primeDepth); + } + + private static int primeDepth(final Expr expr) { + if (expr instanceof PrimeExpr) { + return 1 + primeDepth(((PrimeExpr) expr).getOp()); + } else { + return 0; + } + } + + private static VarDecl extractVarDecl(final Expr expr) { + if (expr instanceof RefExpr refExpr) { + checkArgument(refExpr.getDecl() instanceof VarDecl); + return (VarDecl) refExpr.getDecl(); + } else if (expr instanceof PrimeExpr primeExpr) { + return extractVarDecl(primeExpr.getOp()); + } else { + throw new IllegalArgumentException( + "Cannot extract variable declaration from expression: " + expr); + } + } + + private static class PrimeToLeaves { + + private static final DispatchTable2> TABLE = + DispatchTable2.>builder() + .addCase(RefExpr.class, PrimeToLeaves::transformRef) + .addCase(PrimeExpr.class, PrimeToLeaves::transformPrime) + + // Default + + .addDefault( + (o, primeDepth) -> { + final Expr expr = (Expr) o; + return expr.map(e -> transform(e, primeDepth)); + }) + .build(); + + public static Expr transform(final Expr expr) { + return transform(expr, 0); + } + + @SuppressWarnings("unchecked") + private static Expr transform(final Expr expr, int primeDepth) { + return (Expr) TABLE.dispatch(expr, primeDepth); + } + + private static Expr transformRef(final Expr expr, Integer primeDepth) { + return Prime(expr, primeDepth); + } + + private static Expr transformPrime(final Expr expr, Integer primeDepth) { + return transform(((PrimeExpr) expr).getOp(), primeDepth + 1); + } + } +} diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprUtils.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprUtils.java index 6873033f60..e429afb05e 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprUtils.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprUtils.java @@ -15,6 +15,9 @@ */ package hu.bme.mit.theta.core.utils; +import static com.google.common.base.Preconditions.checkNotNull; +import static hu.bme.mit.theta.core.utils.TypeUtils.cast; + import com.google.common.collect.ImmutableList; import hu.bme.mit.theta.common.Tuple2; import hu.bme.mit.theta.common.container.Containers; @@ -36,7 +39,7 @@ import hu.bme.mit.theta.core.type.functype.FuncAppExpr; import hu.bme.mit.theta.core.utils.IndexedVars.Builder; import hu.bme.mit.theta.core.utils.indexings.VarIndexing; - +import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; import java.util.ArrayList; import java.util.Collection; import java.util.Collections; @@ -48,26 +51,21 @@ import java.util.Set; import java.util.stream.Collectors; -import static com.google.common.base.Preconditions.checkNotNull; -import static hu.bme.mit.theta.core.utils.TypeUtils.cast; - -/** - * Utility functions related to expressions. - */ +/** Utility functions related to expressions. */ public final class ExprUtils { private static final ExprSimplifier exprSimplifier = ExprSimplifier.create(); - private ExprUtils() { - } + private ExprUtils() {} /** * Collect atoms from a Boolean expression into a given collection. * - * @param expr Expression + * @param expr Expression * @param collectTo Collection where the atoms should be put */ - public static void collectAtoms(final Expr expr, final Collection> collectTo) { + public static void collectAtoms( + final Expr expr, final Collection> collectTo) { ExprAtomCollector.collectAtoms(expr, collectTo); } @@ -114,7 +112,9 @@ public static Collection> getConjuncts(final Expr expr) if (expr instanceof AndExpr) { final AndExpr andExpr = (AndExpr) expr; - return andExpr.getOps().stream().map(ExprUtils::getConjuncts).flatMap(Collection::stream) + return andExpr.getOps().stream() + .map(ExprUtils::getConjuncts) + .flatMap(Collection::stream) .collect(Collectors.toSet()); } else { return Collections.singleton(expr); @@ -124,7 +124,7 @@ public static Collection> getConjuncts(final Expr expr) /** * Collect params of an expression into a given collection. * - * @param expr Expression + * @param expr Expression * @param collectTo Collection where the params should be put */ public static void collectParams(final Expr expr, final Collection> collectTo) { @@ -152,10 +152,11 @@ public static void collectParams(final Expr expr, final Collection> exprs, final Collection> collectTo) { + public static void collectParams( + final Iterable> exprs, final Collection> collectTo) { exprs.forEach(e -> collectParams(e, collectTo)); } @@ -183,11 +184,10 @@ public static Set> getParams(final Iterable> expr return vars; } - /** * Collect variables of an expression into a given collection. * - * @param expr Expression + * @param expr Expression * @param collectTo Collection where the variables should be put */ public static void collectVars(final Expr expr, final Collection> collectTo) { @@ -206,10 +206,11 @@ public static void collectVars(final Expr expr, final Collection> /** * Collect variables from expressions into a given collection. * - * @param exprs Expressions + * @param exprs Expressions * @param collectTo Collection where the variables should be put */ - public static void collectVars(final Iterable> exprs, final Collection> collectTo) { + public static void collectVars( + final Iterable> exprs, final Collection> collectTo) { exprs.forEach(e -> collectVars(e, collectTo)); } @@ -240,10 +241,11 @@ public static Set> getVars(final Iterable> exprs) { /** * Collect indexed constants of an expression into a given collection. * - * @param expr Expression + * @param expr Expression * @param collectTo Collection where the constants should be put */ - public static void collectIndexedConstants(final Expr expr, final Collection> collectTo) { + public static void collectIndexedConstants( + final Expr expr, final Collection> collectTo) { if (expr instanceof RefExpr) { final RefExpr refExpr = (RefExpr) expr; final Decl decl = refExpr.getDecl(); @@ -259,10 +261,12 @@ public static void collectIndexedConstants(final Expr expr, final Collection< /** * Collect indexed constants from expressions into a given collection. * - * @param exprs Expressions + * @param exprs Expressions * @param collectTo Collection where the constants should be put */ - public static void collectIndexedConstants(final Iterable> exprs, final Collection> collectTo) { + public static void collectIndexedConstants( + final Iterable> exprs, + final Collection> collectTo) { exprs.forEach(e -> collectIndexedConstants(e, collectTo)); } @@ -284,7 +288,8 @@ public static Set> getIndexedConstants(final Expr expr) { * @param exprs Expressions * @return Set of constants appearing in the expressions */ - public static Set> getIndexedConstants(final Iterable> exprs) { + public static Set> getIndexedConstants( + final Iterable> exprs) { final Set> consts = new HashSet<>(); collectIndexedConstants(exprs, consts); return consts; @@ -293,10 +298,11 @@ public static Set> getIndexedConstants(final Iterable expr, final Collection> collectTo) { + public static void collectConstants( + final Expr expr, final Collection> collectTo) { if (expr instanceof RefExpr) { final RefExpr refExpr = (RefExpr) expr; final Decl decl = refExpr.getDecl(); @@ -312,10 +318,11 @@ public static void collectConstants(final Expr expr, final Collection> exprs, final Collection> collectTo) { + public static void collectConstants( + final Iterable> exprs, final Collection> collectTo) { exprs.forEach(e -> collectConstants(e, collectTo)); } @@ -368,8 +375,7 @@ public static IndexedVars getVarsIndexed(final Iterable> exprs } /** - * Transform expression into an equivalent new expression without - * if-then-else constructs. + * Transform expression into an equivalent new expression without if-then-else constructs. * * @param expr Original expression * @return Transformed expression @@ -382,10 +388,11 @@ public static Expr eliminateIte(final Expr expr) { * Simplify expression and substitute the valuation. * * @param expr Original expression - * @param val Valuation + * @param val Valuation * @return Simplified expression */ - public static Expr simplify(final Expr expr, final Valuation val) { + public static Expr simplify( + final Expr expr, final Valuation val) { return exprSimplifier.simplify(expr, val); } @@ -439,6 +446,29 @@ public static List> canonizeAll(final List> exprs) { return canonizedArgs; } + /** + * Reverses the given expression (swaps primed variables with unprimed variables and + * vice-versa). Also works if variables can have multiple primes. + * + * @param expr Original expression + * @return Reversed form + */ + public static Expr reverse( + final Expr expr, final VarIndexing indexing) { + return new ExprReverser(indexing).reverse(expr); + } + + /** + * Reverses the given expression (swaps primed variables with unprimed variables and + * vice-versa). + * + * @param expr Original expression + * @return Reversed form + */ + public static Expr reverse(final Expr expr) { + return new ExprReverser(VarIndexingFactory.indexing(1)).reverse(expr); + } + /** * Transform an expression into a ponated one. * @@ -457,29 +487,29 @@ public static Expr ponate(final Expr expr) { /** * Transform an expression by universally quantifying certain variables. * - * @param expr Original expression + * @param expr Original expression * @param mapping Quantifying * @return Transformed expression */ - public static Expr close(final Expr expr, final Map, ParamDecl> mapping) { + public static Expr close( + final Expr expr, final Map, ParamDecl> mapping) { return ExprCloser.close(expr, mapping); } /** - * Transform an expression by applying primes to an expression based on an - * indexing. + * Transform an expression by applying primes to an expression based on an indexing. * - * @param expr Original expression + * @param expr Original expression * @param indexing Indexing * @return Transformed expression */ - public static Expr applyPrimes(final Expr expr, final VarIndexing indexing) { + public static Expr applyPrimes( + final Expr expr, final VarIndexing indexing) { return ExprPrimeApplier.applyPrimes(expr, indexing); } /** - * Get the size of an expression by counting the nodes in its tree - * representation. + * Get the size of an expression by counting the nodes in its tree representation. * * @param expr Expression * @return Node count @@ -491,11 +521,12 @@ public static int nodeCountSize(final Expr expr) { /** * Change fixed subexpressions using a lookup * - * @param expr the expr to change subexpressions in + * @param expr the expr to change subexpressions in * @param lookup the lookup mapping subexpression to replacements * @return the changed expression */ - public static Expr changeSubexpr(Expr expr, Map, Expr> lookup) { + public static Expr changeSubexpr( + Expr expr, Map, Expr> lookup) { if (lookup.containsKey(expr)) { return cast(lookup.get(expr), expr.getType()); } else { @@ -503,13 +534,16 @@ public static Expr changeSubexpr(Expr expr, Map, } } - public static Expr changeDecls(Expr expr, Map, ? extends Decl> lookup) { - return changeSubexpr(expr, lookup.entrySet().stream().map(entry -> Map.entry(entry.getKey().getRef(), entry.getValue().getRef())).collect(Collectors.toMap(Entry::getKey, Entry::getValue))); + public static Expr changeDecls( + Expr expr, Map, ? extends Decl> lookup) { + return changeSubexpr( + expr, + lookup.entrySet().stream() + .map(entry -> Map.entry(entry.getKey().getRef(), entry.getValue().getRef())) + .collect(Collectors.toMap(Entry::getKey, Entry::getValue))); } - /** - * Extracts function and its arguments from a nested expression - */ + /** Extracts function and its arguments from a nested expression */ public static Tuple2, List>> extractFuncAndArgs(final FuncAppExpr expr) { final Expr func = expr.getFunc(); final Expr arg = expr.getParam(); @@ -518,8 +552,8 @@ public static Tuple2, List>> extractFuncAndArgs(final FuncAppExp final Tuple2, List>> funcAndArgs = extractFuncAndArgs(funcApp); final Expr resFunc = funcAndArgs.get1(); final List> args = funcAndArgs.get2(); - final List> resArgs = ImmutableList.>builder().addAll(args).add(arg) - .build(); + final List> resArgs = + ImmutableList.>builder().addAll(args).add(arg).build(); return Tuple2.of(resFunc, resArgs); } else { return Tuple2.of(func, ImmutableList.of(arg));