Extending SMT Solvers to Higher-Order Logic.

Satisfiability modulo theories (SMT) solvers have throughout the years been able to cope with increasingly expressive formulas, from ground logics to full first-order logic (FOL) modulo theories. Nevertheless, higher-order logic within SMT is still little explored. We propose a pragmatic extension of SMT solvers to natively support higher-order reasoning without compromising their performance on FOL problems, thus leveraging the extensive research and implementation efforts dedicated to efficient FOL solving. We show how to generalize existing data structures and the ground decision procedure to support partial applications and extensionality, as well as how to reconcile instantiation techniques with functional variables. Our extensions to the SMT solvers cvc4 and veriT are competitive against state-of-the-art HOL provers and are oftentimes better than applying the traditional encoding into FOL.