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

  Copy full SHA for 13ffb90

• add function for litexpr creation

  mondokm

  committed
  b3724dd

  Copy full SHA for b3724dd

• add new tests

  mondokm

  committed
  d6f4e7b

  Copy full SHA for d6f4e7b

• use interpreter in relprod

  mondokm

  committed
  d4c0fa5

  Copy full SHA for d4c0fa5

• Fix for when the constraint is terminal 1

  mondokm

  committed
  af55d09

  Copy full SHA for af55d09

• Add level skip for unbounded domain

  mondokm

  committed
  f288371

  Copy full SHA for f288371

• Update delta jar

  mondokm

  committed
  94c17d1

  Copy full SHA for 94c17d1

• Add toString

  mondokm

  committed
  d470b4b

  Copy full SHA for d470b4b

• Reenable tests

  mondokm

  committed
  8f33a93

  Copy full SHA for 8f33a93

• Use nodeInterpreter for level skips in finite domains

  mondokm

  committed
  a31f8ce

  Copy full SHA for a31f8ce

• Reformat files

  mondokm

  committed
  c80a182

  Copy full SHA for c80a182

Commits on Aug 15, 2024

• Add new test cases

  mondokm

  committed
  5497271

  Copy full SHA for 5497271

• Simplify case when lhs is level-skip

  mondokm

  committed
  d265f9a

  Copy full SHA for d265f9a

• Simplify lhs level-skip and fix statespaceinfo

  mondokm

  committed
  302b8ce

  Copy full SHA for 302b8ce

• Add constrained cursor tests

  mondokm

  committed
  18595f8

  Copy full SHA for 18595f8

• Add new test case

  mondokm

  committed
  b91fb99

  Copy full SHA for b91fb99

• Add statespaceinfo tests

  mondokm

  committed
  fee5a29

  Copy full SHA for fee5a29

• Handle level skips in bounds collection

  mondokm

  committed
  81d9b20

  Copy full SHA for 81d9b20

• Disable not supported tests

  mondokm

  committed
  29ed1b7

  Copy full SHA for 29ed1b7

• Improve caching of valuation

  mondokm

  committed
  d903eb4

  Copy full SHA for d903eb4

• Use unbounded domains for now

  mondokm

  committed
  84e37c2

  Copy full SHA for 84e37c2

• Don't include tmp vars

  mondokm

  committed
  fbc035d

  Copy full SHA for fbc035d

• Add state vars and temp vars to XSTS

  mondokm

  committed
  91a582e

  Copy full SHA for 91a582e

• Reformat files

  mondokm

  committed
  07353cc

  Copy full SHA for 07353cc

• Rename temp vars to local

  mondokm

  committed
  08963dd

  Copy full SHA for 08963dd

• Use default nodeToString

  mondokm

  committed
  5ce63e9

  Copy full SHA for 5ce63e9

• Change Preconditions check to assertion

  mondokm

  committed
  ea0d2b2

  Copy full SHA for ea0d2b2

Commits on Nov 5, 2024

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

  mondokm

  committed
  f7bf171

  Copy full SHA for f7bf171

• Merged mdd-dev

  leventeBajczi

  committed
  763b2fe

  Copy full SHA for 763b2fe

• Added MDD backend to XCFA frontend

  leventeBajczi

  committed
  880cf8b

  Copy full SHA for 880cf8b

• Fixed some bugs

  leventeBajczi

  committed
  5ed25cc

  Copy full SHA for 5ed25cc

• Version bump

  leventeBajczi

  committed
  adb190b

  Copy full SHA for adb190b

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

  leventeBajczi

  committed
  fe44378

  Copy full SHA for fe44378

• re-added failing tests

  leventeBajczi

  committed
  a626d21

  Copy full SHA for a626d21

• Add default values to CfaToMonolithicExpr.kt

  mondokm

  committed
  98b7473

  Copy full SHA for 98b7473

• Add var ordering for cfa and xcfa

  mondokm

  committed
  ef9654b

  Copy full SHA for ef9654b

• Fix formatting

  mondokm

  committed
  48fc830

  Copy full SHA for 48fc830

Commits on Nov 6, 2024

• fixed vars for mdd

  leventeBajczi

  committed
  13c6069

  Copy full SHA for 13c6069

• Merged some files from kszi2/ic3-update

  

  dantpu

  authored and

  leventeBajczi

  committed
  ef3de32

  Copy full SHA for ef3de32

• Fixed Witness->Proof

  leventeBajczi

  committed
  09d16e2

  Copy full SHA for 09d16e2

• Change var ordering

  mondokm

  committed
  c5e2fec

  Copy full SHA for c5e2fec

• Use var ordering properly

  mondokm

  committed
  a2af700

  Copy full SHA for a2af700

• Fixed stateToAction

  leventeBajczi

  committed
  8256648

  Copy full SHA for 8256648

• var -> globalVar

  leventeBajczi

  committed
  c362fd6

  Copy full SHA for c362fd6

• Instead of keeping metadata, combine it with meaningful edges

  leventeBajczi

  committed
  8cad4c5

  Copy full SHA for 8cad4c5

Commits on Nov 7, 2024

• Removed infinite state spaces from mdd test

  leventeBajczi

  committed
  2bbba4d

  Copy full SHA for 2bbba4d

• Add input validation to MddChecker

  mondokm

  committed
  612fc4c

  Copy full SHA for 612fc4c

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

  leventeBajczi

  committed
  c6039f8

  Copy full SHA for c6039f8

• Fix MddNodeInitializer caching

  mondokm

  committed
  b56d417

  Copy full SHA for b56d417

• Added reversed and abstract checkers

  leventeBajczi

  committed
  f155e8b

  Copy full SHA for f155e8b

• Add identityexprs to transRel

  mondokm

  committed
  f5cb264

  Copy full SHA for f5cb264

• Add semantic equals to MddExpressionRepresentation

  mondokm

  committed
  deae12f

  Copy full SHA for deae12f

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

  mondokm

  committed
  6b0aff3

  Copy full SHA for 6b0aff3

• Remove edge and loc vars from defaultvalues

  mondokm

  committed
  6c56d77

  Copy full SHA for 6c56d77

• Add FORCE var ordering

  mondokm

  committed
  36083c3

  Copy full SHA for 36083c3

• Add XSTS var ordering

  mondokm

  committed
  8a0dfb7

  Copy full SHA for 8a0dfb7

• Remove collect

  mondokm

  committed
  a23046d

  Copy full SHA for a23046d

Commits on Nov 11, 2024

• Reformat and MDD notsolvable

  leventeBajczi

  committed
  eb64b77

  Copy full SHA for eb64b77

• removed erroneous test

  leventeBajczi

  committed
  9518942

  Copy full SHA for 9518942

• Merge branch 'master' into emergent-2025

  leventeBajczi

  authored
  161935b

  Copy full SHA for 161935b

• Comment out test takng too long

  leventeBajczi

  committed
  dd8bdea

  Copy full SHA for dd8bdea

• Better task timing for testing

  leventeBajczi

  committed
  c498938

  Copy full SHA for c498938

• Using labels instead of edges for variable ordering

  leventeBajczi

  committed
  37b4d14

  Copy full SHA for 37b4d14

• Merge branch 'master' into emergent-2025

  leventeBajczi

  authored
  87475ef

  Copy full SHA for 87475ef