Code

EmergenTheta Update#314

Code

Merged

leventeBajczi merged 64 commits intomasterftsrg/theta:masterfrom emergent-2025ftsrg/theta:emergent-2025Copy head branch name to clipboardNov 11, 2024

+4,723-2,538

Commits

Commits on Aug 12, 2024

• use domainsize in MddChecker

  mondokm

  committed
  13ffb90

• add function for litexpr creation

  mondokm

  committed
  b3724dd

• add new tests

  mondokm

  committed
  d6f4e7b

• use interpreter in relprod

  mondokm

  committed
  d4c0fa5

• Fix for when the constraint is terminal 1

  mondokm

  committed
  af55d09

• Add level skip for unbounded domain

  mondokm

  committed
  f288371

• Update delta jar

  mondokm

  committed
  94c17d1

• Add toString

  mondokm

  committed
  d470b4b

• Reenable tests

  mondokm

  committed
  8f33a93

• Use nodeInterpreter for level skips in finite domains

  mondokm

  committed
  a31f8ce

• Reformat files

  mondokm

  committed
  c80a182

Commits on Aug 15, 2024

• Add new test cases

  mondokm

  committed
  5497271

• Simplify case when lhs is level-skip

  mondokm

  committed
  d265f9a

• Simplify lhs level-skip and fix statespaceinfo

  mondokm

  committed
  302b8ce

• Add constrained cursor tests

  mondokm

  committed
  18595f8

• Add new test case

  mondokm

  committed
  b91fb99

• Add statespaceinfo tests

  mondokm

  committed
  fee5a29

• Handle level skips in bounds collection

  mondokm

  committed
  81d9b20

• Disable not supported tests

  mondokm

  committed
  29ed1b7

• Improve caching of valuation

  mondokm

  committed
  d903eb4

• Use unbounded domains for now

  mondokm

  committed
  84e37c2

• Don't include tmp vars

  mondokm

  committed
  fbc035d

• Add state vars and temp vars to XSTS

  mondokm

  committed
  91a582e

• Reformat files

  mondokm

  committed
  07353cc

• Rename temp vars to local

  mondokm

  committed
  08963dd

• Use default nodeToString

  mondokm

  committed
  5ce63e9

• Change Preconditions check to assertion

  mondokm

  committed
  ea0d2b2

Commits on Nov 5, 2024

• Add default values to CFA monolithic, fix division by zero in simplify, add CfaMddCheckerTest

  mondokm

  committed
  f7bf171

• Merged mdd-dev

  leventeBajczi

  committed
  763b2fe

• Added MDD backend to XCFA frontend

  leventeBajczi

  committed
  880cf8b

• Fixed some bugs

  leventeBajczi

  committed
  5ed25cc

• Version bump

  leventeBajczi

  committed
  adb190b

• Added xcfa tests, modified cfa tests, removed offending stmttoexpr tests

  leventeBajczi

  committed
  fe44378

• re-added failing tests

  leventeBajczi

  committed
  a626d21

• Add default values to CfaToMonolithicExpr.kt

  mondokm

  committed
  98b7473

• Add var ordering for cfa and xcfa

  mondokm

  committed
  ef9654b

• Fix formatting

  mondokm

  committed
  48fc830

Commits on Nov 6, 2024

• fixed vars for mdd

  leventeBajczi

  committed
  13c6069

• Merged some files from kszi2/ic3-update

  

  dantpu

  authored and

  leventeBajczi

  committed
  ef3de32

• Fixed Witness->Proof

  leventeBajczi

  committed
  09d16e2

• Change var ordering

  mondokm

  committed
  c5e2fec

• Use var ordering properly

  mondokm

  committed
  a2af700

• Fixed stateToAction

  leventeBajczi

  committed
  8256648

• var -> globalVar

  leventeBajczi

  committed
  c362fd6

• Instead of keeping metadata, combine it with meaningful edges

  leventeBajczi

  committed
  8cad4c5

Commits on Nov 7, 2024

• Removed infinite state spaces from mdd test

  leventeBajczi

  committed
  2bbba4d

• Add input validation to MddChecker

  mondokm

  committed
  612fc4c

• Fixed bug relating to multi-variable definitions in a single statement

  leventeBajczi

  committed
  c6039f8

• Fix MddNodeInitializer caching

  mondokm

  committed
  b56d417

• Added reversed and abstract checkers

  leventeBajczi

  committed
  f155e8b

• Add identityexprs to transRel

  mondokm

  committed
  f5cb264

• Add semantic equals to MddExpressionRepresentation

  mondokm

  committed
  deae12f

• Merge remote-tracking branch 'origin/emergent-2025' into emergent-2025

  mondokm

  committed
  6b0aff3

• Remove edge and loc vars from defaultvalues

  mondokm

  committed
  6c56d77

• Add FORCE var ordering

  mondokm

  committed
  36083c3

• Add XSTS var ordering

  mondokm

  committed
  8a0dfb7

• Remove collect

  mondokm

  committed
  a23046d

Commits on Nov 11, 2024

• Reformat and MDD notsolvable

  leventeBajczi

  committed
  eb64b77

• removed erroneous test

  leventeBajczi

  committed
  9518942

• Merge branch 'master' into emergent-2025

  leventeBajczi

  authored
  161935b

• Comment out test takng too long

  leventeBajczi

  committed
  dd8bdea

• Better task timing for testing

  leventeBajczi

  committed
  c498938

• Using labels instead of edges for variable ordering

  leventeBajczi

  committed
  37b4d14

• Merge branch 'master' into emergent-2025

  leventeBajczi

  authored
  87475ef