tracking: datatypes

[c-cube]

• [x] inference for acyclicity (not just simplification): given C ∨ s = t, look for σ such that sσ = tσ is absurd by acyclicity. Then infer Cσ from that. E.g. s (f x) = s (s (f a)) would give σ={x→a} (do anti-unification with cstors only, then try to unify cstor-prefixed subterms on one side with the root on the other side)
• [ ] remove some specialized rules (positive injectivity) and instead, generate rewrite rules during preprocessing
• [ ] hierarchic superposition for datatypes (with defined functions being part of the background)
  • [x] need corresponding TKBO with 2 levels (just replace KBO with it anyway, and build weight fun from constant classification)
  • [x] with TKBO implemented, removed the code that forces rpo6 to be used when induction is enabled, as well as constraint disabling
  • narrowing with defined symbols would ± correspond to E-unification on pure background literals
  • [ ] add purification inference (read carefully!) → do we want weak abstraction? would need 2 kinds of vars then
  • [ ] add "case split" rule for t != u where they are of a datatype. use a table for caching split for a given ground t. split looks like t = cstor1(…) | … | t=cstor_k(…) where each … is a list of fresh parameters (i.e. possibly inductive skolems). → avatar should fire on that! Do not do case split on α != β where both are parameters of a recursive datatype (always possible to pick distinct values). For non-recursive datatypes we need to do it. → check on examples/data/unit_… problems
  • need a theory solver (msat + small SMT?) that deals with parameters → parameters are the way of dealing with exhaustiveness
• [ ] look into "superposition for fixed domains" more seriously (ask Weidenbach for more details?)

• rule similar to fool_param for for datatypes: C[t] where t:nat (strict subterm) is not a cstor term nor a variable would become C[S x] ∨ t ≠ S x and C[0] ∨ t ≠ 0
  • should be terminating (reduces the number of such strict subterms) but careful that with reduction you might find the same clause again, this must be an inference and not a simplification
  • is sound, and might be decreasing (check!). It does seem to work for fool.
  • enables more reductions…