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

• Convert Horn clause file format to Horn Clause Graph
  • file format possibly: smtlib2 with set-theory HORN as described in https://github.com/sosy-lab/sv-benchmarks/tree/master/clauses
• Convert 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
  • Build a formula (something like SSA) from a ground derivation
• 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)