Code

Invariant Solver#214

Code

Merged

vkuncak merged 50 commits intoepfl-lara:mainepfl-lara/inox:mainfrom sankalpgambhir:invariant-solversankalpgambhir/inox:invariant-solverCopy head branch name to clipboardSep 25, 2024

+1,308-25

Commits

Commits on Sep 17, 2024

• New Simple Horn Solver reimplementation

  sankalpgambhir

  committed
  b488798

• Add eldarica and z3 relative paths

  sankalpgambhir

  committed
  9685d3e

• Fix multiple symbol declaration

  sankalpgambhir

  committed
  b86d5d0

• Rewrite Constraint Processing

  sankalpgambhir

  committed
  3ace46d

• Ignore semanticdb

  sankalpgambhir

  committed
  875a65d

• Regenerate TIP files

  sankalpgambhir

  committed
  1a1332d

• Reseal Symbols

  sankalpgambhir

  committed
  fd71988

• Better Instructions

  sankalpgambhir

  committed
  d7f8b2c

• Package compiled eldarica

  sankalpgambhir

  committed
  9003408

• Redo many parts; more explicit constraint generation

  sankalpgambhir

  committed
  3858f70

• Make Horn solvers available via SolverFactory

  sankalpgambhir

  committed
  61f9d1d

• Differentiate predicates from HOF in SMTLibTarget

  sankalpgambhir

  committed
  e87d0af

• Add Invariant solvers to factory

  sankalpgambhir

  committed
  bdcc4d1

• Cleanup SimpleSolver

  sankalpgambhir

  committed
  fabe256

• Add Invariant Solver

  sankalpgambhir

  committed
  3a8bb23

• Remove spurious prints

  sankalpgambhir

  committed
  78e7455

• Change constraint accumulation format

  sankalpgambhir

  committed
  5066da4

• Make predicate defs not hide guards

  sankalpgambhir

  committed
  831eebf

• Accumulate top-level assumes as assertions

  sankalpgambhir

  committed
  010bfeb

• More precise handling of disjunction branching

  sankalpgambhir

  committed
  d3149cc

• Generate goal clauses from top-level assertions

  sankalpgambhir

  committed
  5cce5f2

• Change check to match new assertion handling

  sankalpgambhir

  committed
  6fa29af

• Clarify unreachable pattern match error

  sankalpgambhir

  committed
  2494c13

• Rewrite constraint generation to aggressively separate and simplify expressions

  sankalpgambhir

  committed
  1297820

• Remove debug prints

  sankalpgambhir

  committed
  04d60e6

• Extend support for z3 SMTLIB models

  sankalpgambhir

  committed
  bd28265

• Remove SimpleHornSolver

  sankalpgambhir

  committed
  c86347d

• Loosen treatment of guards and nested assertions

  sankalpgambhir

  committed
  d0babac

• More precise transitive guard collection for predicate types

  sankalpgambhir

  committed
  e2257bf

• Explicit node naming

  sankalpgambhir

  committed
  1939385

• Vacuity checking for models

  sankalpgambhir

  committed
  9d1eb30

• Model extraction for predicates

  sankalpgambhir

  committed
  f23da09

• Fix underlying interrupts

  sankalpgambhir

  committed
  9aa5699

• Check that guards are computed transitively

  sankalpgambhir

  committed
  7eeec87

• Assure canonicalization of operator arguments

  sankalpgambhir

  committed
  5e181a7

• Mkae HOF internals private

  sankalpgambhir

  committed
  96723dd

• Disable aggressive model printing

  sankalpgambhir

  committed
  ee68e5f

• Remove non-vacuity checks for models

  sankalpgambhir

  committed
  aff51ea

• Redo uuverifiers dependencies

  sankalpgambhir

  committed
  8f81773

• Removed dangling inductive examples

  sankalpgambhir

  committed
  8db52e3

• Revert require message change

  sankalpgambhir

  committed
  8e7808f

• Revert README about old examples

  sankalpgambhir

  committed
  6eee2dd

• Remove eldarica wrapper

  sankalpgambhir

  committed
  9bd8aa6

• Rename uuverifiers resolver

  sankalpgambhir

  committed
  6b862c5

• Fix solver names

  sankalpgambhir

  committed
  96a02ab

• Remvoe accidental result-flipping in previous change

  sankalpgambhir

  committed
  7e1e98c

• Remove unused method that accesses interpreter internals

  sankalpgambhir

  committed
  d4bb72a

• Add new Eldarica interpreter (without IPC)

  sankalpgambhir

  committed
  9bf9546

Commits on Sep 24, 2024

• Only return a model if the config requests it

  sankalpgambhir

  committed
  b63317e

• Add basic tests

  sankalpgambhir

  committed
  51404e6