Interpolation: Add implementation for SyGuS interpolation module (final) (#5063)

Add interface for SyGuS Interpolation module. Adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack.

1 files changed, 3 insertions, 0 deletions

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index e95e36c3d..eec17a5f8 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -105,6 +105,7 @@ class Preprocessor;
 class SmtSolver;
 class SygusSolver;
 class AbductionSolver;
+class InterpolationSolver;
 class QuantElimSolver;
 /**
  * Representation of a defined function.  We keep these around in
@@ -1101,6 +1102,8 @@ class CVC4_PUBLIC SmtEngine
 
   /** The solver for abduction queries */
   std::unique_ptr<smt::AbductionSolver> d_abductSolver;
+  /** The solver for interpolation queries */
+  std::unique_ptr<smt::InterpolationSolver> d_interpolSolver;
   /** The solver for quantifier elimination queries */
   std::unique_ptr<smt::QuantElimSolver> d_quantElimSolver;
   /**