Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

EmergenTheta Update #314

Draft
wants to merge 57 commits into
base: master
Choose a base branch
from
Draft

EmergenTheta Update #314

wants to merge 57 commits into from

Conversation

leventeBajczi
Copy link
Contributor

@leventeBajczi leventeBajczi commented Nov 5, 2024

This PR updates the Emergent portfolio for EmergenTheta.

  • MddChecker updates (by @mondokm)
  • Add binding for MddChecker for XcfaCli
  • Add reverse BMC, KIND, IMC
  • Assemble Portfolio

Comment on lines +151 to 160
// VarDecl<IntType> tempVar = VarPoolUtil.requestInt();
for (Stmt stmt : nonDetStmt.getStmts()) {
final Expr<BoolType> tempExpr = Eq(
ExprUtils.applyPrimes(tempVar.getRef(), indexing), Int(count++));
final StmtUnfoldResult result = toExpr(stmt, indexing.inc(tempVar));
choices.add(And(tempExpr, And(result.exprs)));
// final Expr<BoolType> tempExpr = Eq(
// ExprUtils.applyPrimes(tempVar.getRef(), indexing),
// Int(count++));
final StmtUnfoldResult result = toExpr(stmt, indexing /*.inc(tempVar)*/);
choices.add(/*And(tempExpr, */ And(result.exprs) /*)*/);
indexings.add(result.indexing);
jointIndexing = jointIndexing.join(result.indexing);
}
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this OK?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, this is intentional, comments can even be removed

Copy link

github-actions bot commented Nov 7, 2024

❗ Please run ./gradlew spotlessApply on your branch to fix formatting.

Copy link

github-actions bot commented Nov 7, 2024

Benchexec test report for a selection of SV-Benchmarks (correct / incorrect / all):

task set BOUNDED CEGAR HORN
Arrays ✅ (1 / 0 / 82) HTML/CSV ❓ (0 / 0 / 4) HTML/CSV ✅ (1 / 0 / 49) HTML/CSV
BitVectors ✅ (4 / 0 / 22) HTML/CSV ✅ (4 / 0 / 29) HTML/CSV ✅ (2 / 0 / 29) HTML/CSV
Combinations ❓ (0 / 0 / 39) HTML/CSV ❓ (0 / 0 / 39) HTML/CSV ❓ (0 / 0 / 39) HTML/CSV
Concurrency ❓ (0 / 0 / 124) HTML/CSV ✅ (14 / 0 / 42) HTML/CSV ❓ (0 / 0 / 125) HTML/CSV
ConcurrencySafety-NoOverflows ❓ (0 / 0 / 116) HTML/CSV ✅ (15 / 0 / 43) HTML/CSV ❓ (0 / 0 / 121) HTML/CSV
ControlFlow ✅ (2 / 0 / 30) HTML/CSV ✅ (4 / 0 / 59) HTML/CSV ❗ (31 / 17 / 66) HTML/CSV
ECA ❓ (0 / 0 / 32) HTML/CSV ❓ (0 / 0 / 31) HTML/CSV ❓ (0 / 0 / 32) HTML/CSV
Floats ❓ (0 / 0 / 17) HTML/CSV ✅ (7 / 0 / 22) HTML/CSV ❓ (0 / 0 / 34) HTML/CSV
Hardware ❓ (0 / 0 / 29) HTML/CSV ✅ (1 / 0 / 17) HTML/CSV ❓ (0 / 0 / 29) HTML/CSV
Heap ✅ (9 / 0 / 112) HTML/CSV ❗ (41 / 1 / 98) HTML/CSV ❗ (9 / 1 / 112) HTML/CSV
Loops ✅ (12 / 0 / 50) HTML/CSV ✅ (1 / 0 / 7) HTML/CSV ✅ (24 / 0 / 67) HTML/CSV
NoDataRace ❓ (0 / 0 / 127) HTML/CSV ❗ (36 / 3 / 58) HTML/CSV ❓ (0 / 0 / 129) HTML/CSV
ProductLines ❓ (0 / 0 / 329) HTML/CSV ❓ (0 / 0 / 336) HTML/CSV ❓ (0 / 0 / 334) HTML/CSV
Recursive ❓ (0 / 0 / 153) HTML/CSV ❗ (10 / 11 / 41) HTML/CSV ❓ (0 / 0 / 153) HTML/CSV
Sequentialized ✅ (2 / 0 / 35) HTML/CSV ✅ (3 / 0 / 37) HTML/CSV ✅ (4 / 0 / 36) HTML/CSV
XCSP ✅ (18 / 0 / 37) HTML/CSV ✅ (17 / 0 / 39) HTML/CSV ✅ (6 / 0 / 35) HTML/CSV

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants