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 and http://smtlib.cs.uiowa.edu/language.shtml
• 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)

Details of components

Input format/Parsing

Using special SMTLib2 files with the following constraints:

• filename ends with .smt2
• set-logic command is "(set-logic HORN)"
• Syntax of assert statements as in https://github.com/sosy-lab/sv-benchmarks/tree/master/clauses
• no push/pop
• only one (check-sat) at the end of the file)

We use SMTInterpol's parser (with a special Script) to convert such a file into a Hypergraph in one shot (not like SMTInterpol, which interleaves parsing with solver activity).