search

shingarov / MachineArithmetic

A mathematical foundation for Smalltalk-25
MIT License
17 stars 6 forks source link

Stray entry in BindEnvironment #198

Closed shingarov closed 9 months ago

shingarov commented 9 months ago

Consider the following Horn query:

(constant adder (func(0, [int;int])))
(define adder(x : int) : int = { 42 })
(constraint 
   (forall ((x int) (Bool true)) 
      (((adder value: x) === 42))))

During the initial solve, SimpC₁'s IBindEnv is {0,1}. These ids point to the following entries in the BE:

  1. x | x∈ℤ
  2. x₁ | x₁∈ℤ

This in itself does not lead to incorrect answers, but blocks working on PLE, because from such IBindEnv, mkCTrie produces the wrong Trie.

This Issue calls to investigate how this "0" entry creeps into the SInfo.

shingarov commented 9 months ago

This is happening because #reduceEnvironments is unimplemented. It is somewhat annoying (we have to read longer constraints) but is not a real problem because there is the --no-environment-reduction flag on the upstream Fixpoint side.