src/smt/interpolation_solver.h

   1 /*********************                                                        */
   2 /*! \file interpolation_solver.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Ying Sheng, Andrew Reynolds, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief The solver for interpolation queries
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__SMT__INTERPOLATION_SOLVER_H
  18 #define CVC4__SMT__INTERPOLATION_SOLVER_H
  19
  20 #include "expr/node.h"
  21 #include "expr/type_node.h"
  22
  23 namespace CVC4 {
  24
  25 class SmtEngine;
  26
  27 namespace smt {
  28
  29 /**
  30  * A solver for interpolation queries.
  31  *
  32  * This class is responsible for responding to get-interpol commands. It spawns
  33  * a subsolver SmtEngine for a sygus conjecture that captures the interpolation
  34  * query, and implements supporting utility methods such as checkInterpol.
  35  */
  36 class InterpolationSolver
  37 {
  38  public:
  39   InterpolationSolver(SmtEngine* parent);
  40   ~InterpolationSolver();
  41
  42   /**
  43    * This method asks this SMT engine to find an interpolant with respect to
  44    * the current assertion stack (call it A) and the conjecture (call it B). If
  45    * this method returns true, then interpolant is set to a formula I such that
  46    * A ^ ~I and I ^ ~B are both unsatisfiable.
  47    *
  48    * @param conj The conjecture of the interpolation problem.
  49    * @param grammarType A sygus datatype type that encodes the syntax
  50    * restrictions on the shape of possible solutions.
  51    * @param interpol This argument is updated to contain the solution to the
  52    * interpolation problem.
  53    *
  54    * This method invokes a separate copy of the SMT engine for solving the
  55    * corresponding sygus problem for generating such a solution.
  56    */
  57   bool getInterpol(const Node& conj,
  58                    const TypeNode& grammarType,
  59                    Node& interpol);
  60
  61   /**
  62    * Same as above, but without user-provided grammar restrictions. A default
  63    * grammar is chosen internally using the sygus grammar constructor utility.
  64    */
  65   bool getInterpol(const Node& conj, Node& interpol);
  66
  67   /**
  68    * Check that a solution to an interpolation problem is indeed a solution.
  69    *
  70    * The check is made by determining that the assertions imply the solution of
  71    * the interpolation problem (interpol), and the solution implies the goal
  72    * (conj). If these criteria are not met, an internal error is thrown.
  73    */
  74   void checkInterpol(Node interpol,
  75                      const std::vector<Node>& easserts,
  76                      const Node& conj);
  77
  78  private:
  79   /** The parent SMT engine */
  80   SmtEngine* d_parent;
  81 };
  82
  83 }  // namespace smt
  84 }  // namespace CVC4
  85
  86 #endif /* CVC4__SMT__INTERPOLATION_SOLVER_H */