Code

Fix infinite recursion in isRVarApp#264

Code

Draft

shingarov wants to merge 133 commits intopure-z3shingarov/MachineArithmetic:pure-z3from issue-255shingarov/MachineArithmetic:issue-255Copy head branch name to clipboard

+4,249-313

Commits

Commits on Mar 21, 2024

• [PreSmalltalks] Temporarily replace Benoît's Trie with an experiment

  shingarov

  committed
  dd3a049

• [PLE] Initialize HornInfo's axioms

  shingarov

  committed
  c911cbb

• [PLE] Add AxiomEnv>>#isPleCstr:sid:

  shingarov

  committed
  645007e

• [PLE] Add #strengthenSortedReft:

  shingarov

  committed
  c39cd70

• [PLE] First stab at #doPLE:

  shingarov

  committed
  59e8f33

• [PLE] No longer skip testPLE0

  shingarov

  committed
  943b76d

• [PLE] Add PLE package

  shingarov

  committed
  58cb75b

• [PLE] Add class ICtx

  shingarov

  committed
  1d65107

• [PLE] Start implementing Normalizable typeclass

  shingarov

  committed
  e9eaa6e

• [PLE] Towards a somewhat-sensible #doPLE:

  shingarov

  committed
  a6d9327

• [PLE] Fake some bogus InstRes. NEVER MERGE THIS IN.

  shingarov

  committed
  058ed43

• [PLE] On UNSAFE, attempt to lazy-PLE

  shingarov

  committed
  4bcf9f4

• [PLE] Start implementing ICtx

  shingarov

  committed
  e88bed5

• [PLE] Add class EvAccum

  shingarov

  committed
  dc9fa6b

• [PLE] Temporary experiments with refinement reflection

  Show description for 0cda6a4
  shingarov

  committed
  0cda6a4

• [PLE] Add HornPosPleTest>>test42, even simple than ple0

  shingarov

  committed
  e2d803e

• [PLE] Introduce class EvalEnvPLE

  shingarov

  committed
  6b28299

• [PLE] Move loopB out of PreSmalltalks

  Show description for fff7dc7
  shingarov

  committed
  fff7dc7

• [PLE] Implement BlockClosure>>withCtx:

  shingarov

  committed
  0f64a21

• [PLE] Improve comment

  shingarov

  committed
  4558a68

• [PLE] Move SInfo>>instantiate: to PLE

  shingarov

  committed
  b854fc8

• [PLE] More experiments with Equation

  shingarov

  committed
  14749b3

• [PLE] Experiment with SymEnv

  shingarov

  committed
  9bb7965

• [PLE] Add SimpC>>cBinds (internal to mkCTrie)

  shingarov

  committed
  0766e60

• [PLE] Pass z3 (Solver) argument to SInfo>>instEnv:

  shingarov

  committed
  c0b7ad4

• [PLE] Experiment with Knowledge

  shingarov

  committed
  b3884e6

• [PLE] Experiment with InstEnv

  shingarov

  committed
  70a7181

• [PLE] Experiment with ICtx

  shingarov

  committed
  ed410c5

• [PLE] Improve comment in EvAccum

  shingarov

  committed
  bc6ae5f

• [PLE] Add ECon>>shortcut:

  shingarov

  committed
  76fe1b5

• [PLE] Refactor mkCTrie: through cBinds

  shingarov

  committed
  08b8448

• [PLE] Experiment with fastEval

  shingarov

  committed
  5c430b0

• [PLE] Experiment with #pleTrie:

  shingarov

  committed
  85049be

• [PLE] Move PLE to src/PLE following the new convention

  shingarov

  committed
  a3ef77e

• [PLE] Move PLE-specific methods in Equation to PLE

  Show description for 89a0604
  shingarov

  committed
  89a0604

• [PLE] Add class ConstMap

  shingarov

  committed
  3b03623

• [PLE] Improve comment in SInfo>>doPLE:

  shingarov

  committed
  6811f7b

• [PLE] Move SymEnv>>makeContextWithSEnv to PLE

  shingarov

  committed
  756a10a

• [PLE] Add class SMTContext

  shingarov

  committed
  3517f1d

• [PLE] Fix interpretation of <$> in #loopB

  shingarov

  committed
  9b9d7f8

• [PLE] Implement Set>>equalitiesPred

  shingarov

  committed
  7fabda9

• [PLE] Fix rebase of reflect5

  shingarov

  committed
  201b08c

• [PLE] Remove some debug #shouldBeImplemented so passing PLE tests are green

  shingarov

  committed
  c2a1b26

• [PLE] Add L8PosTest>>test_42

  shingarov

  committed
  a6618c0

• [PLE] Introduce (just the selector of) CGInfo>>addReflectVar:

  shingarov

  committed
  3db22da

• [PLE] begin working on notGuardedApps, squash later

  shingarov

  committed
  a59eab3

• [PLE] towards a real updCtx

  shingarov

  committed
  4ef2666

• [PLE] Use bogus equation name for now

  Show description for 881c896
  shingarov

  committed
  881c896

• [PLE] For now short-circuit deciding whether the equation is recursive

  shingarov

  committed
  cd13e41

• [PLE] Move PLE-specific Equation>>substEq:es: to PLE package

  shingarov

  committed
  b3feb75

• [PLE] Move goFastEval to Z3Node from F.Expr

  shingarov

  committed
  8a6c5e0

• [PLE] Actually evaluate the equation body

  shingarov

  committed
  8643d3c

• [PLE] Implement Z3Node>>notGuardedApps

  shingarov

  committed
  abe61e5

• [PLE] Actually wire the equation's body all the way to strengthen

  shingarov

  committed
  37c99df

• [PLE] Prefer self-consistent capitalization of name 'testPLE0'

  shingarov

  committed
  908e915

• [PLE] Add testPleInc

  shingarov

  committed
  ed0afb7

• [PLE] Actually implement EvalEnv of the Equation's args

  shingarov

  committed
  b0cd1bb

• [PLE] Towards a more realistic fastEval

  shingarov

  committed
  0f4dee4

• [PLE] Remove irrelevant and insert relevant halts

  Show description for 1445454
  shingarov

  committed
  1445454

• [PLE] Implement more meat in fastEval

  shingarov

  committed
  37d0a07

• [PLE] Implement reasoning about (EEq (EVar x) c) in findConstants

  shingarov

  committed
  dbbace2

• [PLE] Actually implement Equation>>normalize

  shingarov

  committed
  c9c8ee3

• [PLE] Implement enough for testPleInc to work

  shingarov

  committed
  68e193a

• [PLE] Add testPleSimpleIf

  Show description for bb8a7a5
  shingarov

  committed
  bb8a7a5

• [PLE] Fix polymorphic component instantiation

  shingarov

  committed
  4895e5d

• [PLE] Allow recursive application of eqName inside eqBody

  Show description for 6e230b0
  shingarov

  committed
  6e230b0

• [PLE] Fix some obvious problems in notGuardedApps

  shingarov

  committed
  ff4b233

• [PLE] Gauss' example of 1+...+100 works, too

  shingarov

  committed
  9e33199

• [PLE] Towards implementing the |branches|>1 case in loopT

  shingarov

  committed
  9d0af89

• [PLE] Add testPleGauss

  shingarov

  committed
  6d9ed6c

• [PLE] More cases in notGuardedApps

  shingarov

  committed
  a75a173

• [PLE] First experiments with ITE

  shingarov

  committed
  d737d5f

• [PLE] Pass the Z3 solver into the constructor of Knowledge

  shingarov

  committed
  5f84873

• [PLE] Implement isConstant relative to set of data constructors

  shingarov

  committed
  9c4e33e

• [PLE] Implement more cases in goFastEval

  shingarov

  committed
  8367ee5

• [PLE] Recursively pass the ICtx, not the Z3 solver, into fastEval

  shingarov

  committed
  17fd6c7

• [PLE] Implement the ITE case in notGuardedApps

  shingarov

  committed
  6bf5c24

• [PLE] Towards working Gauss example

  shingarov

  committed
  d5a895b

• [PLE] Somewhat more-understandable testPleGauss

  shingarov

  committed
  3c1d92b

• [PLE] Actually implement goFastEval(PAtom)

  shingarov

  committed
  9793da5

• [PLE] Actually implement evalCandsLoop

  shingarov

  committed
  bc470ac

• [PLE] Add L₈ test_sumGauss

  shingarov

  committed
  314e6f4

• [PLE] Implement addReflectVar

  Show description for 6a0ff0b
  shingarov

  committed
  6a0ff0b

• [PLE] Implement Pierce–Dunfield bidi-checking for Refl annotations

  shingarov

  committed
  2b5754a

• [PLE] Add cgiDefs and gciConsts to the HornQuery, and set the --rewrite flag

  shingarov

  committed
  c0c95c0

• [PLE] Add L8PosTest >> test_42b and L8PosTest >> test_PleInc

  

  janvrany

  authored and

  shingarov

  committed
  11cfa86

• [PLE] Add L₈ tests adder, poly, sum100

  shingarov

  committed
  4f14f92

• [PLE] Add L₈ test_IncInc

  shingarov

  committed
  a59c9d9

• [PLE] Add L₈ test_trid_01, test_trid_02, test_tradd2_01, test_tradd2_02

  

  janvrany

  authored and

  shingarov

  committed
  3690fd2

• [PLE] Add L₈ test_42_chain, showing a simple chain of two reflects

  shingarov

  committed
  5e4552f

• [PLE] Add test_adder_chain, distilling the uncurrying problem to its simplest form

  Show description for 85c0c36
  shingarov

  committed
  85c0c36

• [PLE] Implement "e found in acc" path in fastEval

  shingarov

  committed
  527a60b

• [PLE] A supermonkey-programmer implementation of EIte

  shingarov

  committed
  c7797a4

• [PLE] Implement fastEval(PNot)

  shingarov

  committed
  3630ef9

• [PLE] Implement fastEval(EBin)

  shingarov

  committed
  8b0f695

• [PLE] Refactor order of arguments to #simplify:in: (expr is now self)

  shingarov

  committed
  6f81f26

• [PLE] Add L₈ test_trabs_02, showing a simple TR-style control flow

  

  janvrany

  authored and

  shingarov

  committed
  f45e136

• [PLE] Add L₈ test_addorsub, a simplified test for TR-style control flow

  

  janvrany

  authored and

  shingarov

  committed
  022821b

• [PLE] Add L₈ test_static_assert_eq to test reflect on polymorphic types

  

  janvrany

  authored and

  shingarov

  committed
  fba43e6

• [PLE] Add L₈ test_abs_01 and test_abs_02

  

  janvrany

  authored and

  shingarov

  committed
  f13e55d

• [PLE] Initial rudiments of Z3Node>>simplify:in:

  shingarov

  committed
  c223bca

• [PLE] First prototype of inlining

  shingarov

  committed
  83f4931

• [PLE] Implement #normalizeLetOnLet

  Show description for bce5791
  shingarov

  committed
  bce5791

• [PLE tests] Don't use /[zero] for non-recursive reflects

  shingarov

  committed
  177ccdb

• [PLE] Some progress on inlining

  shingarov

  committed
  edbb248

• [PLE inlining] Add test_42b_chain_longer demoing the α-rename problem

  Show description for 4dbe8e4
  shingarov

  committed
  4dbe8e4

• [PLE inlining] Kill misleading comment

  shingarov

  committed
  05dc248

• [PLE inlining] normalizeLetOnLet recursively, not just one level

  shingarov

  committed
  904fa7f

• [PLE inlining] Add l8Neg test_IncInc

  shingarov

  committed
  7f8e8b0

• [PLE tests] Remove /0 termination metric from test_abs_*

  shingarov

  committed
  5bff0a0

• [PLE inlining] First step towards inlining EIf

  shingarov

  committed
  b189ff7

• Fix bug in type renaming w.r.t termination metric

  Show description for 927785b
  

  janvrany

  authored and

  shingarov

  committed
  927785b

• Uniquify all Sprite preterms before elaboration +++what

  shingarov

  committed
  3493278

• Implement String >> #uniq via (new) #uniqueVariableNameFor:

  

  janvrany

  authored and

  shingarov

  committed
  406097e

• [PLE inlining] Swap branches in normalizeLetOnLet, anticipating adding tail elimination of EIf

  shingarov

  committed
  b3aa68a

• [PLE tests] Remove rec keyword in test_abs_02

  shingarov

  committed
  f23cecb

• [PLE inlining] Tail-eliminate EIf

  Show description for 6801f15
  shingarov

  committed
  6801f15

• [PLE tests] Remove rec in trabs_02

  shingarov

  committed
  fabb5f4

• ...and tradd

  shingarov

  committed
  fa8f787

• [PLE] Fix L₈ test test_sumGauss

  Show description for d22f378
  

  janvrany

  authored and

  shingarov

  committed
  d22f378

• [PLE] Add L₈ test_abs_03, test_abs_04 and bunch of test_pos_XX

  Show description for e64d2ec
  

  janvrany

  authored and

  shingarov

  committed
  e64d2ec

• [PLE] add PLE to the baseline

  

  janvrany

  authored and

  shingarov

  committed
  3018d53

• [PLE] Remove nonsensical L₈ test_poly

  Show description for 815ade9
  shingarov

  committed
  815ade9

• [PLE] Groom L₈ tests

  shingarov

  committed
  6dd59a6

• [PLE] Move abs bitvector tests to Neg side

  Show description for f7ffe6b
  shingarov

  committed
  f7ffe6b

• [PLE] Add test_42pos, demonstrating how PLE strengthens a weaker explicit refinement

  shingarov

  committed
  4add01e

• [PLE] Add L₈>>test_Gauss′

  shingarov

  committed
  d89e719

• [PLE] Fix glaringly obvious typo (must be ictx, not Z3 ctx)

  shingarov

  committed
  798f4c7

• [Temporary Trie] Fix idiotic typo

  shingarov

  committed
  ff8a586

• Add bitvector version of L₈ test_sum_Gauss

  shingarov

  committed
  9b2db83

• [PLE] Don't simplify Z3Nodes waiting for feedback on Z3Prover/z3#7179

  shingarov

  committed
  fcfd25a

• add first test_poly; NB missing test_bool

  shingarov

  committed
  31aeeb2

Commits on Apr 3, 2024

• [PLE] Add neg Gauss corresponding to upstream Sprite

  Show description for 439ba60
  shingarov

  committed
  439ba60