-
Notifications
You must be signed in to change notification settings - Fork 43
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #118 from ftsrg/xsts-loops
Combined prod domain
- Loading branch information
Showing
25 changed files
with
1,825 additions
and
94 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
18 changes: 18 additions & 0 deletions
18
...n/java/hu/bme/mit/theta/analysis/expr/refinement/maxatomcount/IndividualMaxAtomCount.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,18 @@ | ||
| package hu.bme.mit.theta.analysis.expr.refinement.maxatomcount; | ||
|
|
||
| import hu.bme.mit.theta.core.decl.VarDecl; | ||
|
|
||
| import java.util.Map; | ||
|
|
||
| public class IndividualMaxAtomCount implements MaxAtomCount{ | ||
| private Map<VarDecl<?>,Integer> declToCount; | ||
|
|
||
| public IndividualMaxAtomCount(final Map<VarDecl<?>,Integer> declToCount){ | ||
| this.declToCount = declToCount; | ||
| } | ||
|
|
||
| @Override | ||
| public int get(VarDecl<?> decl) { | ||
| return declToCount.get(decl); | ||
| } | ||
| } |
9 changes: 9 additions & 0 deletions
9
...is/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/maxatomcount/MaxAtomCount.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,9 @@ | ||
| package hu.bme.mit.theta.analysis.expr.refinement.maxatomcount; | ||
|
|
||
| import hu.bme.mit.theta.core.decl.VarDecl; | ||
|
|
||
| public interface MaxAtomCount { | ||
|
|
||
| int get(final VarDecl<?> decl); | ||
|
|
||
| } |
17 changes: 17 additions & 0 deletions
17
...s/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/maxatomcount/NMaxAtomCount.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,17 @@ | ||
| package hu.bme.mit.theta.analysis.expr.refinement.maxatomcount; | ||
|
|
||
| import hu.bme.mit.theta.core.decl.VarDecl; | ||
|
|
||
| public class NMaxAtomCount implements MaxAtomCount{ | ||
|
|
||
| private final int n; | ||
|
|
||
| public NMaxAtomCount(final int n){ | ||
| this.n=n; | ||
| } | ||
|
|
||
| @Override | ||
| public int get(VarDecl<?> decl) { | ||
| return n; | ||
| } | ||
| } |
12 changes: 12 additions & 0 deletions
12
...in/java/hu/bme/mit/theta/analysis/expr/refinement/maxatomcount/UnlimitedMaxAtomCount.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,12 @@ | ||
| package hu.bme.mit.theta.analysis.expr.refinement.maxatomcount; | ||
|
|
||
| import hu.bme.mit.theta.core.decl.VarDecl; | ||
|
|
||
| public class UnlimitedMaxAtomCount implements MaxAtomCount { | ||
|
|
||
| @Override | ||
| public int get(VarDecl<?> decl) { | ||
| return 0; | ||
| } | ||
|
|
||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
125 changes: 125 additions & 0 deletions
125
...src/main/java/hu/bme/mit/theta/analysis/prod2/prod2explpred/Prod2ExplPredAbstractors.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,125 @@ | ||
| package hu.bme.mit.theta.analysis.prod2.prod2explpred; | ||
|
|
||
| import com.google.common.collect.ImmutableSet; | ||
| import hu.bme.mit.theta.analysis.expl.ExplPrec; | ||
| import hu.bme.mit.theta.analysis.expl.ExplState; | ||
| import hu.bme.mit.theta.analysis.pred.PredPrec; | ||
| import hu.bme.mit.theta.analysis.pred.PredState; | ||
| import hu.bme.mit.theta.analysis.prod2.Prod2Prec; | ||
| import hu.bme.mit.theta.analysis.prod2.Prod2State; | ||
| import hu.bme.mit.theta.common.container.Containers; | ||
| import hu.bme.mit.theta.core.decl.ConstDecl; | ||
| import hu.bme.mit.theta.core.decl.Decls; | ||
| import hu.bme.mit.theta.core.model.Valuation; | ||
| import hu.bme.mit.theta.core.type.Expr; | ||
| import hu.bme.mit.theta.core.type.LitExpr; | ||
| import hu.bme.mit.theta.core.type.booltype.BoolExprs; | ||
| import hu.bme.mit.theta.core.type.booltype.BoolType; | ||
| import hu.bme.mit.theta.core.utils.ExprUtils; | ||
| import hu.bme.mit.theta.core.utils.PathUtils; | ||
| import hu.bme.mit.theta.core.utils.VarIndexing; | ||
| import hu.bme.mit.theta.solver.Solver; | ||
| import hu.bme.mit.theta.solver.utils.WithPushPop; | ||
|
|
||
| import java.util.*; | ||
| import java.util.function.Function; | ||
| import java.util.stream.Collectors; | ||
|
|
||
| import static com.google.common.base.Preconditions.checkNotNull; | ||
| import static hu.bme.mit.theta.core.type.booltype.BoolExprs.*; | ||
|
|
||
| public class Prod2ExplPredAbstractors { | ||
|
|
||
| private Prod2ExplPredAbstractors() {} | ||
|
|
||
| public interface Prod2ExplPredAbstractor { | ||
|
|
||
| Collection<Prod2State<ExplState, PredState>> createStatesForExpr(final Expr<BoolType> expr, final VarIndexing exprIndexing, | ||
| final Prod2Prec<ExplPrec,PredPrec> prec, final VarIndexing precIndexing, | ||
| final Function<? super Valuation, ? extends ExplState> valuationToState, final int limit); | ||
|
|
||
| } | ||
|
|
||
| public static BooleanAbstractor booleanAbstractor(final Solver solver){ | ||
| return new BooleanAbstractor(solver, false); | ||
| } | ||
|
|
||
| private static final class BooleanAbstractor implements Prod2ExplPredAbstractor{ | ||
|
|
||
| private final Solver solver; | ||
| private final List<ConstDecl<BoolType>> actLits; | ||
| private final String litPrefix; | ||
| private static int instanceCounter = 0; | ||
| private final boolean split; | ||
|
|
||
| public BooleanAbstractor(final Solver solver, final boolean split) { | ||
| this.solver = checkNotNull(solver); | ||
| this.actLits = new ArrayList<>(); | ||
| this.litPrefix = "__Prod2ExplPred" + getClass().getSimpleName() + "_" + instanceCounter + "_"; | ||
| instanceCounter++; | ||
| this.split = split; | ||
| } | ||
|
|
||
| @Override | ||
| public Collection<Prod2State<ExplState, PredState>> createStatesForExpr(final Expr<BoolType> expr, final VarIndexing exprIndexing, | ||
| final Prod2Prec<ExplPrec, PredPrec> prec, final VarIndexing stateIndexing, | ||
| final Function<? super Valuation, ? extends ExplState> valuationToState, final int limit) { | ||
| checkNotNull(expr); | ||
| checkNotNull(exprIndexing); | ||
| checkNotNull(prec); | ||
| checkNotNull(stateIndexing); | ||
|
|
||
| final List<Expr<BoolType>> preds = new ArrayList<>(prec.getPrec2().getPreds()); | ||
| generateActivationLiterals(preds.size()); | ||
|
|
||
| assert actLits.size() >= preds.size(); | ||
|
|
||
| final List<Prod2State<ExplState,PredState>> states = new LinkedList<>(); | ||
| try (WithPushPop wp = new WithPushPop(solver)) { | ||
| solver.add(PathUtils.unfold(expr, exprIndexing)); | ||
| for (int i = 0; i < preds.size(); ++i) { | ||
| solver.add(Iff(actLits.get(i).getRef(), PathUtils.unfold(preds.get(i), stateIndexing))); | ||
| } | ||
| while (solver.check().isSat() && (limit == 0 || states.size() < limit)) { | ||
| final Valuation model = solver.getModel(); | ||
|
|
||
| final Valuation valuation = PathUtils.extractValuation(model, stateIndexing); | ||
| final ExplState explState = valuationToState.apply(valuation); | ||
|
|
||
| final Set<Expr<BoolType>> newStatePreds = Containers.createSet(); | ||
| final List<Expr<BoolType>> feedback = new LinkedList<>(); | ||
| feedback.add(True()); | ||
| for (int i = 0; i < preds.size(); ++i) { | ||
| final ConstDecl<BoolType> lit = actLits.get(i); | ||
| final Expr<BoolType> pred = preds.get(i); | ||
| final Optional<LitExpr<BoolType>> eval = model.eval(lit); | ||
| if (eval.isPresent()) { | ||
| if (eval.get().equals(True())) { | ||
| newStatePreds.add(pred); | ||
| feedback.add(lit.getRef()); | ||
| } else { | ||
| newStatePreds.add(prec.getPrec2().negate(pred)); | ||
| feedback.add(Not(lit.getRef())); | ||
| } | ||
| } | ||
| } | ||
| final Set<Expr<BoolType>> simplfiedNewStatePreds = newStatePreds.stream().map(pred -> ExprUtils.simplify(pred,explState)).collect(Collectors.toSet()); | ||
| final PredState predState = PredState.of(simplfiedNewStatePreds); | ||
|
|
||
| final Prod2State<ExplState,PredState> prod2ExplPredState = Prod2State.of(explState,predState); | ||
| states.add(prod2ExplPredState); | ||
| solver.add(Not(And(PathUtils.unfold(explState.toExpr(), stateIndexing),And(feedback)))); | ||
| } | ||
|
|
||
| } | ||
| return states; | ||
| } | ||
|
|
||
| private void generateActivationLiterals(final int n) { | ||
| while (actLits.size() < n) { | ||
| actLits.add(Decls.Const(litPrefix + actLits.size(), BoolExprs.Bool())); | ||
| } | ||
| } | ||
| } | ||
|
|
||
| } |
73 changes: 73 additions & 0 deletions
73
...is/src/main/java/hu/bme/mit/theta/analysis/prod2/prod2explpred/Prod2ExplPredAnalysis.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,73 @@ | ||
| /* | ||
| * Copyright 2017 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.prod2.prod2explpred; | ||
|
|
||
| import static com.google.common.base.Preconditions.checkNotNull; | ||
|
|
||
| import hu.bme.mit.theta.analysis.Action; | ||
| import hu.bme.mit.theta.analysis.Analysis; | ||
| import hu.bme.mit.theta.analysis.InitFunc; | ||
| import hu.bme.mit.theta.analysis.PartialOrd; | ||
| import hu.bme.mit.theta.analysis.TransFunc; | ||
| import hu.bme.mit.theta.analysis.expl.ExplPrec; | ||
| import hu.bme.mit.theta.analysis.expl.ExplState; | ||
| import hu.bme.mit.theta.analysis.expr.ExprAction; | ||
| import hu.bme.mit.theta.analysis.pred.PredPrec; | ||
| import hu.bme.mit.theta.analysis.pred.PredState; | ||
| import hu.bme.mit.theta.analysis.prod2.*; | ||
| import hu.bme.mit.theta.analysis.prod2.prod2explpred.Prod2ExplPredAbstractors.Prod2ExplPredAbstractor; | ||
| import hu.bme.mit.theta.analysis.prod2.prod2explpred.Prod2ExplPredDedicatedTransFunc; | ||
|
|
||
| public final class Prod2ExplPredAnalysis<A extends ExprAction> | ||
| implements Analysis<Prod2State<ExplState, PredState>, A, Prod2Prec<ExplPrec, PredPrec>> { | ||
|
|
||
| private final PartialOrd<Prod2State<ExplState, PredState>> partialOrd; | ||
| private final InitFunc<Prod2State<ExplState, PredState>, Prod2Prec<ExplPrec, PredPrec>> initFunc; | ||
| private final TransFunc<Prod2State<ExplState, PredState>, A, Prod2Prec<ExplPrec, PredPrec>> transFunc; | ||
|
|
||
| private Prod2ExplPredAnalysis(final Analysis<ExplState, ? super A, ExplPrec> analysis1, final Analysis<PredState, ? super A, PredPrec> analysis2, | ||
| final StrengtheningOperator<ExplState, PredState, ExplPrec, PredPrec> strenghteningOperator, | ||
| final Prod2ExplPredAbstractor prod2ExplPredAbstractor) { | ||
| checkNotNull(analysis1); | ||
| checkNotNull(analysis2); | ||
| partialOrd = Prod2Ord.create(analysis1.getPartialOrd(), analysis2.getPartialOrd()); | ||
| initFunc = Prod2InitFunc.create(analysis1.getInitFunc(), analysis2.getInitFunc(), strenghteningOperator); | ||
| transFunc = Prod2ExplPredDedicatedTransFunc.create(prod2ExplPredAbstractor); | ||
| } | ||
|
|
||
| public static <A extends ExprAction> Prod2ExplPredAnalysis<A> create( | ||
| final Analysis<ExplState, ? super A, ExplPrec> analysis1, final Analysis<PredState, ? super A, PredPrec> analysis2, | ||
| final StrengtheningOperator<ExplState, PredState, ExplPrec, PredPrec> strenghteningOperator, | ||
| final Prod2ExplPredAbstractor prod2ExplPredAbstractor) { | ||
| return new Prod2ExplPredAnalysis<A>(analysis1, analysis2, strenghteningOperator, prod2ExplPredAbstractor); | ||
| } | ||
|
|
||
| @Override | ||
| public PartialOrd<Prod2State<ExplState, PredState>> getPartialOrd() { | ||
| return partialOrd; | ||
| } | ||
|
|
||
| @Override | ||
| public InitFunc<Prod2State<ExplState, PredState>, Prod2Prec<ExplPrec, PredPrec>> getInitFunc() { | ||
| return initFunc; | ||
| } | ||
|
|
||
| @Override | ||
| public TransFunc<Prod2State<ExplState, PredState>, A, Prod2Prec<ExplPrec, PredPrec>> getTransFunc() { | ||
| return transFunc; | ||
| } | ||
|
|
||
| } |
Oops, something went wrong.