tracking: datatypes

[c-cube]

• 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)
  • need corresponding TKBO with 2 levels
    (just replace KBO with it anyway, and build weight fun
    from constant classification)
  • 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…