-
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 #99 from ftsrg/xsts-dev
xsts-dev
- Loading branch information
Showing
35 changed files
with
36,882 additions
and
107 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
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
77 changes: 77 additions & 0 deletions
77
...ava/hu/bme/mit/theta/analysis/prod2/prod2explpred/AutomaticItpRefToProd2ExplPredPrec.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,77 @@ | ||
| package hu.bme.mit.theta.analysis.prod2.prod2explpred; | ||
|
|
||
| import hu.bme.mit.theta.analysis.expl.ExplPrec; | ||
| import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation; | ||
| import hu.bme.mit.theta.analysis.expr.refinement.RefutationToPrec; | ||
| import hu.bme.mit.theta.analysis.pred.ExprSplitters.ExprSplitter; | ||
| import hu.bme.mit.theta.analysis.pred.PredPrec; | ||
| import hu.bme.mit.theta.analysis.prod2.Prod2Prec; | ||
| import hu.bme.mit.theta.core.decl.VarDecl; | ||
| 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; | ||
|
|
||
| import java.util.*; | ||
|
|
||
| import static com.google.common.base.Preconditions.checkArgument; | ||
| import static com.google.common.base.Preconditions.checkNotNull; | ||
|
|
||
| public final class AutomaticItpRefToProd2ExplPredPrec implements RefutationToPrec<Prod2Prec<ExplPrec, PredPrec>, ItpRefutation> { | ||
|
|
||
| private final Set<VarDecl<?>> explPreferredVars; | ||
| private final Map<VarDecl<?>, Integer> predCount; | ||
| private final ExprSplitter exprSplitter; | ||
| private final int maxPredCount; | ||
|
|
||
| private AutomaticItpRefToProd2ExplPredPrec(final Set<VarDecl<?>> explPreferredVars, final ExprSplitter exprSplitter, final int maxPredCount) { | ||
| this.explPreferredVars = checkNotNull(explPreferredVars); | ||
| this.exprSplitter = checkNotNull(exprSplitter); | ||
| this.maxPredCount = maxPredCount; | ||
|
|
||
| this.predCount = new HashMap<>(); | ||
| } | ||
|
|
||
| public static AutomaticItpRefToProd2ExplPredPrec create(final Set<VarDecl<?>> explPreferredVars, final ExprSplitter exprSplitter, final int maxPredCount) { | ||
| checkArgument(maxPredCount >= 0, "MaxPredCount must be non-negative."); | ||
| return new AutomaticItpRefToProd2ExplPredPrec(explPreferredVars, exprSplitter, maxPredCount); | ||
| } | ||
|
|
||
| @Override | ||
| public Prod2Prec<ExplPrec, PredPrec> toPrec(ItpRefutation refutation, int index) { | ||
| final Collection<Expr<BoolType>> exprs = exprSplitter.apply(refutation.get(index)); | ||
| Set<VarDecl<?>> explSelectedVars = new HashSet<>(); | ||
| Set<Expr<BoolType>> predSelectedExprs = new HashSet<>(); | ||
| for (var expr : exprs) { | ||
| final Set<VarDecl<?>> containedVars = ExprUtils.getVars(expr); | ||
| boolean allExpl = true; | ||
| for (var decl : containedVars) { | ||
| if(maxPredCount>=0){ | ||
| if (!predCount.containsKey(decl)) { | ||
| predCount.put(decl, 1); | ||
| } | ||
| if(predCount.get(decl)>=maxPredCount){ | ||
| explPreferredVars.add(decl); | ||
| } else { | ||
| predCount.put(decl, predCount.get(decl) + 1); | ||
| } | ||
| } | ||
| if (explPreferredVars.contains(decl)) { | ||
| explSelectedVars.add(decl); | ||
| } else allExpl = false; | ||
| } | ||
| if (!allExpl) predSelectedExprs.add(expr); | ||
| } | ||
| return Prod2Prec.of(ExplPrec.of(explSelectedVars), PredPrec.of(predSelectedExprs)); | ||
|
|
||
| } | ||
|
|
||
| @Override | ||
| public Prod2Prec<ExplPrec, PredPrec> join(Prod2Prec<ExplPrec, PredPrec> prec1, Prod2Prec<ExplPrec, PredPrec> prec2) { | ||
| return Prod2Prec.of(prec1.getPrec1().join(prec2.getPrec1()), prec1.getPrec2().join(prec2.getPrec2())); | ||
| } | ||
|
|
||
| @Override | ||
| public String toString() { | ||
| return getClass().getSimpleName(); | ||
| } | ||
| } |
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
65 changes: 65 additions & 0 deletions
65
subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/StmtCounterVisitor.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,65 @@ | ||
| package hu.bme.mit.theta.core.utils; | ||
|
|
||
| import hu.bme.mit.theta.core.stmt.*; | ||
| import hu.bme.mit.theta.core.type.Type; | ||
|
|
||
| public class StmtCounterVisitor implements StmtVisitor<Void, Integer> { | ||
|
|
||
| private static final class LazyHolder { | ||
| private final static StmtCounterVisitor INSTANCE = new StmtCounterVisitor(); | ||
| } | ||
|
|
||
| private StmtCounterVisitor() { | ||
| } | ||
|
|
||
| public static StmtCounterVisitor getInstance() { | ||
| return StmtCounterVisitor.LazyHolder.INSTANCE; | ||
| } | ||
|
|
||
| @Override | ||
| public Integer visit(SkipStmt stmt, Void param) { | ||
| return 1; | ||
| } | ||
|
|
||
| @Override | ||
| public Integer visit(AssumeStmt stmt, Void param) { | ||
| return 1; | ||
| } | ||
|
|
||
| @Override | ||
| public <DeclType extends Type> Integer visit(AssignStmt<DeclType> stmt, Void param) { | ||
| return 1; | ||
| } | ||
|
|
||
| @Override | ||
| public <DeclType extends Type> Integer visit(HavocStmt<DeclType> stmt, Void param) { | ||
| return 1; | ||
| } | ||
|
|
||
| @Override | ||
| public Integer visit(SequenceStmt stmt, Void param) { | ||
| int count = 0; | ||
| for (var subStmt: stmt.getStmts()){ | ||
| count+=subStmt.accept(this,null); | ||
| } | ||
| return count+1; | ||
| } | ||
|
|
||
| @Override | ||
| public Integer visit(NonDetStmt stmt, Void param) { | ||
| int count = 0; | ||
| for (var subStmt: stmt.getStmts()){ | ||
| count+=subStmt.accept(this,null); | ||
| } | ||
| return count+1; | ||
| } | ||
|
|
||
| @Override | ||
| public Integer visit(OrtStmt stmt, Void param) { | ||
| int count = 0; | ||
| for (var subStmt: stmt.getStmts()){ | ||
| count+=subStmt.accept(this,null); | ||
| } | ||
| return count+1; | ||
| } | ||
| } |
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
Oops, something went wrong.