Tree Automizer

Goals

• Construct an "Automizer for Trees"
  • i.e. working on Tree Automata instead of NWAs
• possible applications
  • Horn clause solving
  • Data flow proofs

Components

• Horn clause file format to Horn Clause Graph
  • Convert Horn clauses (in some text format) to a graph stucture (let's call it HornClauseGraph, HCG)
• Horn clause graph to Program Tree Automaton
  • Convert the Horn Clause Graph to a Tree Automaton, analogous to the "Program Automaton" in Automizer
• Adapt CegarLoop from Automizer
  • Currently it works on Nested Word Automata, we want a version that works on Tree Automata
• Ground derivation to Interpolant Tree Automaton
  • Construct a Tree Automaton from a Horn clause ground derivation, analogous to the "Interpolant Automaton" or "Data Automaton"
• Adapt TraceChecker for trees
  • have a Tree Object or so
  • Build something like SSA from it
• Basic data structures
  • Graph Node and Edge for Horn Clause Graph
  • Label for Horn Clause Graph edges
    • similar to IAction?
    • carries a TransitionFormula, and what else?
    • needs a connection to the source nodes/edge components for variable tracking
  • Tree
    • the Trees that the tree automata operate on
    • represents a ground derivation (in the Horn clause case)