Code

Limited functions#54

Code

Open

ole-thoeb wants to merge 45 commits intomoves-rwth:mainmoves-rwth/caesar:mainfrom ole-thoeb:limitedole-thoeb/caesar:limitedCopy head branch name to clipboard

+2,071-327

Commits

Commits on Jan 3, 2025

• ignore .idea

  ole-thoeb

  committed
  6a0eb63

  Copy full SHA for 6a0eb63

• generation working?

  ole-thoeb

  committed
  86636f0

  Copy full SHA for 86636f0

• stop z3 from being too smart.

  Show description for edea5f6
  ole-thoeb

  committed
  edea5f6

  Copy full SHA for edea5f6

• Always add the "fuel synonym axiom" for function that have a fuel parameter

  ole-thoeb

  committed
  f32b61f

  Copy full SHA for f32b61f

• Cleanup fuel code

  Show description for 694edfd
  ole-thoeb

  committed
  694edfd

  Copy full SHA for 694edfd

• Use OnceCell<T> over RefCell<Option<T>> for lazy initialisation

  ole-thoeb

  committed
  e049f54

  Copy full SHA for e049f54

• Lit-wrap constants without propagation

  ole-thoeb

  committed
  722f145

  Copy full SHA for 722f145

• rustfmt

  ole-thoeb

  committed
  180403d

  Copy full SHA for 180403d

• clippy

  ole-thoeb

  committed
  ac29f5a

  Copy full SHA for ac29f5a

• bundle flags for SmtCtx in SmtCtxOptions struct

  ole-thoeb

  committed
  fc14dca

  Copy full SHA for fc14dca

• Address most of the PR feedback

  ole-thoeb

  committed
  40cb672

  Copy full SHA for 40cb672

• propagate const information and cleanup axiom generation

  ole-thoeb

  committed
  ea7b6c9

  Copy full SHA for ea7b6c9

• Correctly construct SmtCtx in test

  ole-thoeb

  committed
  5ea3ba3

  Copy full SHA for 5ea3ba3

• Change quantifier translation a bit, again

  Show description for 0858fa1
  ole-thoeb

  committed
  0858fa1

  Copy full SHA for 0858fa1

• update/improve comments

  ole-thoeb

  committed
  710cdb8

  Copy full SHA for 710cdb8

• Redo parts of code generation for fuel encoding + more examples

  Show description for 634df49
  ole-thoeb

  committed
  634df49

  Copy full SHA for 634df49

• All caps TODO breaks test runner??!

  ole-thoeb

  committed
  fe24531

  Copy full SHA for fe24531

• Fix run command

  ole-thoeb

  committed
  79a853f

  Copy full SHA for 79a853f

• don't try to compile example type given in docs

  ole-thoeb

  committed
  1df7670

  Copy full SHA for 1df7670

• Make rust type provided for intuition actually compile

  ole-thoeb

  committed
  63bfd4e

  Copy full SHA for 63bfd4e

• Ensure new types/function can not clash with user defined code

  ole-thoeb

  committed
  9bed56d

  Copy full SHA for 9bed56d

• Only encode non-zero fuel condition in trigger

  Show description for 6ec2096
  ole-thoeb

  committed
  6ec2096

  Copy full SHA for 6ec2096

• More examples

  ole-thoeb

  committed
  09dc2c3

  Copy full SHA for 09dc2c3

• Closely mimic encoding from paper

  ole-thoeb

  committed
  9b701c6

  Copy full SHA for 9b701c6

• Revert back to the Dafny way of fuel.

  Show description for d0e7b15
  ole-thoeb

  committed
  d0e7b15

  Copy full SHA for d0e7b15

• Fix lit wrapping

  Show description for e807772
  ole-thoeb

  committed
  e807772

  Copy full SHA for e807772

• Add quantifier ids and weight to foralls

  ole-thoeb

  committed
  0c16039

  Copy full SHA for 0c16039

• Adjust integration tests

  Show description for 6f8b365
  ole-thoeb

  committed
  6f8b365

  Copy full SHA for 6f8b365

• rust fmt

  ole-thoeb

  committed
  4a82860

  Copy full SHA for 4a82860

• Consider less function calls as constant

  Show description for 0a53472
  ole-thoeb

  committed
  0a53472

  Copy full SHA for 0a53472

• Make test less flaky by adding @trigger

  ole-thoeb

  committed
  1f0fe09

  Copy full SHA for 1f0fe09

• Enable datatype specific lit wrapping

  Show description for def8c85
  ole-thoeb

  committed
  def8c85

  Copy full SHA for def8c85

• Fixes after rebasing

  ole-thoeb

  committed
  fc6d452

  Copy full SHA for fc6d452

• Rename ConstantExpr... to LiteralExpr... and use builder style for collector

  ole-thoeb

  committed
  8ba5a71

  Copy full SHA for 8ba5a71

• Add tracing to literal value collecting

  ole-thoeb

  committed
  631b728

  Copy full SHA for 631b728

• Do not lit-wrap if we can not profit from it

  ole-thoeb

  committed
  f944bea

  Copy full SHA for f944bea

Commits on Jan 9, 2025

• clone prover when slicing instead of using push/pop

  Show description for 971fdfd
  ole-thoeb

  committed
  971fdfd

  Copy full SHA for 971fdfd

Commits on Jan 11, 2025

• Fighting in vain with z3 params

  ole-thoeb

  committed
  669d70c

  Copy full SHA for 669d70c

Commits on Jan 31, 2025

• Revert "Fighting in vain with z3 params"

  Show description for 5b8fdaa
  ole-thoeb

  committed
  5b8fdaa

  Copy full SHA for 5b8fdaa

• set parameters via set_global_param

  Show description for de430c5
  ole-thoeb

  committed
  de430c5

  Copy full SHA for de430c5

Commits on Feb 6, 2025

• Removed superfluous parameter setting

  ole-thoeb

  committed
  932eedb

  Copy full SHA for 932eedb

Commits on Feb 9, 2025

• Add plain version of fuel, not using datatype

  ole-thoeb

  committed
  68c1680

  Copy full SHA for 68c1680

Commits on Feb 10, 2025

• Add --static-fuel flag

  Show description for 5ffd375
  ole-thoeb

  committed
  5ffd375

  Copy full SHA for 5ffd375

Commits on Feb 11, 2025

• Also generate computation axioms for static fuel

  ole-thoeb

  committed
  0d7232e

  Copy full SHA for 0d7232e

• Rename different encodings and consolidate fuel encodings

  ole-thoeb

  committed
  d3ed935

  Copy full SHA for d3ed935