This PR add a first prototype version of an engine based on predicate
abstraction + CEGAR.
The idea is similar to LAWI but with important differences in how the
exploration and refinement works. It also supports nonlinear systems
from the start.
The core of the engine is an abstract reachability graph (ARG) that
represents some bounded unrolling of the CHC system.
Each node in the graph represents reachable states of some CHC predicate
(in an overapproximate manner). Several options are possible for the
representation. For this first prototype, we follow standard Cartesian
abstraction over a given set of predicates. The set of predicates is
initially empty and new predicates are added on demand, from
interpolants, computed from the refutation of infeasible unrollings.
This first implementation is extremely naive and can be optimized in
several places. For example, query clauses should be prioritized, and on
refinement, we can refine existing ARG instead of starting from scratch.
Other points is better detection of covered (subsumed) nodes, actually
building ARG instead of tree, and lazy checking of new candidate edges.
This PR add a first prototype version of an engine based on predicate abstraction + CEGAR.
The idea is similar to LAWI but with important differences in how the exploration and refinement works. It also supports nonlinear systems from the start. The core of the engine is an abstract reachability graph (ARG) that represents some bounded unrolling of the CHC system. Each node in the graph represents reachable states of some CHC predicate (in an overapproximate manner). Several options are possible for the representation. For this first prototype, we follow standard Cartesian abstraction over a given set of predicates. The set of predicates is initially empty and new predicates are added on demand, from interpolants, computed from the refutation of infeasible unrollings.
This first implementation is extremely naive and can be optimized in several places. For example, query clauses should be prioritized, and on refinement, we can refine existing ARG instead of starting from scratch. Other points is better detection of covered (subsumed) nodes, actually building ARG instead of tree, and lazy checking of new candidate edges.
The algorithm is based on the general description from the paper Boosting Constrained Horn Solving by Unsat Core Learning (VMCAI '24) https://link.springer.com/chapter/10.1007/978-3-031-50524-9_13