Issues

• Build time grows exponentially for ?: chains with exclusive guards and for flat || conditions

  bug
  IDNI/tau-lang#203 · Filter by author andrei-idni opened on Oct 5, 2026
  5

• Reuse translated bit-vector expressions across concrete VM steps

  IDNI/tau-lang#199 · Filter by author TheDarkLightX opened on Sep 30, 2026
  3

  

• Bounded BDD decision reduces time on quantified bit-vector examples

  IDNI/tau-lang#184 · Filter by author TheDarkLightX opened on Sep 27, 2026
  

• Use graph propagation for closed modular bit-vector sum equations

  IDNI/tau-lang#182 · Filter by author TheDarkLightX opened on Sep 27, 2026
  

• Reuse existing miniscoping before public API quantifier elimination

  IDNI/tau-lang#180 · Filter by author TheDarkLightX opened on Sep 26, 2026
  

• A specification of functional shape is solved at every step although its outputs are determined by the values it reads

  IDNI/tau-lang#178 · Filter by author taumorrow opened on Sep 26, 2026
  

• Opening the full shape of #124 with the positions as streams is spent in the warm-up, which eliminates a quantified rest the definitions already settle

  IDNI/tau-lang#176 · Filter by author taumorrow opened on Sep 26, 2026
  

• A specification carrying its state in lookback streams pays the whole telescope at the fixpoint check of the unbounded continuation

  IDNI/tau-lang#174 · Filter by author taumorrow opened on Sep 26, 2026
  

• Every REPL line and every step of a run re-seeds the type resolver with every stream the session has seen

  IDNI/tau-lang#172 · Filter by author taumorrow opened on Sep 25, 2026
  

• A constant that accumulates clauses has no way to drop one: removing a conjunct means rebuilding the constant from the remaining clauses

  IDNI/tau-lang#169 · Filter by author taumorrow opened on Sep 24, 2026
  

• factored_tau_sat groups the units of a conjunction by pairwise list comparison, quadratic in the clause count

  IDNI/tau-lang#167 · Filter by author taumorrow opened on Sep 24, 2026
  

• The Boolean operators of a tau constant renormalize the temporal layer of a fresh normal form on every step

  IDNI/tau-lang#165 · Filter by author taumorrow opened on Sep 24, 2026
  

• sat of an always-conjunction over streams decides the whole formula although its components are independent

  IDNI/tau-lang#163 · Filter by author taumorrow opened on Sep 24, 2026
  

• The step of an accumulating :tau run normalizes the whole constant twice: once to build it and once more to decide it

  IDNI/tau-lang#159 · Filter by author taumorrow opened on Sep 24, 2026
  

• Every step decides the solver's fresh splitter <:splitN> != 0 through the full temporal pipeline

  IDNI/tau-lang#157 · Filter by author taumorrow opened on Sep 24, 2026
  

• syntactic_variable_simplification canonicalizes the substituted terms and thereby decides every tau constant they carry

  IDNI/tau-lang#155 · Filter by author taumorrow opened on Sep 24, 2026
  

• A complemented :tau constant is decided monolithically on every step of an accumulating run: its sometimes normal form falls out of the per-component factoring

  IDNI/tau-lang#153 · Filter by author taumorrow opened on Sep 24, 2026
  2

  

• Fold same-type disequation alternatives before CQE distribution

  IDNI/tau-lang#152 · Filter by author TheDarkLightX opened on Sep 24, 2026
  

• Prune contradictory clauses during quantifier-elimination distribution

  IDNI/tau-lang#151 · Filter by author TheDarkLightX opened on Sep 24, 2026
  

• REPL silently stops evaluating after a mixed-algebra ternary inside a conjunction (piped scripts die quietly)

  IDNI/tau-lang#102 · Filter by author taumorrow opened on Sep 2, 2026
  2