Inclusion Constraints over Non-Empty Sets of Trees
Author: Joachim Niehren and Martin Müller and Andreas
Podelski
Editor: Max Dauchet
We present a new constraint system called Ines. Its
constraints are
conjunctions of inclusions $t_1\subseteq t_2$
between first-order terms
(without set operators) which are interpreted over non-empty sets of
trees. The existing systems of set constraints can express Ines
constraints only if they include negation. Their satisfiability
problem is NEXPTIME-complete. We present an incremental
algorithm that solves the satisfiability problem of Ines
constraints in cubic time. We intend to apply Ines constraints for
type analysis for a concurrent constraint programming language.
|