src/smt/abduction_solver.h

   1 /*********************                                                        */
   2 /*! \file abduction_solver.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   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 abduction queries
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__SMT__ABDUCTION_SOLVER_H
  18 #define CVC4__SMT__ABDUCTION_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 abduction queries.
  31  *
  32  * This class is responsible for responding to get-abduct commands. It spawns
  33  * a subsolver SmtEngine for a sygus conjecture that captures the abduction
  34  * query, and implements supporting utility methods such as checkAbduct.
  35  */
  36 class AbductionSolver
  37 {
  38  public:
  39   AbductionSolver(SmtEngine* parent);
  40   ~AbductionSolver();
  41   /**
  42    * This method asks this SMT engine to find an abduct with respect to the
  43    * current assertion stack (call it A) and the goal (call it B).
  44    * If this method returns true, then abd is set to a formula C such that
  45    * A ^ C is satisfiable, and A ^ ~B ^ C is unsatisfiable.
  46    *
  47    * @param goal The goal of the abduction problem.
  48    * @param grammarType A sygus datatype type that encodes the syntax
  49    * restrictions on the shape of possible solutions.
  50    * @param abd This argument is updated to contain the solution to the
  51    * abduction problem. Notice that this is a formula whose free symbols
  52    * are contained in goal + the parent's current assertion stack.
  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 getAbduct(const Node& goal, const TypeNode& grammarType, Node& abd);
  58
  59   /**
  60    * Same as above, but without user-provided grammar restrictions. A default
  61    * grammar is chosen internally using the sygus grammar constructor utility.
  62    */
  63   bool getAbduct(const Node& goal, Node& abd);
  64
  65   /**
  66    * Check that a solution to an abduction conjecture is indeed a solution.
  67    *
  68    * The check is made by determining that the assertions conjoined with the
  69    * solution to the abduction problem (a) is SAT, and the assertions conjoined
  70    * with the abduct and the goal is UNSAT. If these criteria are not met, an
  71    * internal error is thrown.
  72    */
  73   void checkAbduct(Node a);
  74
  75  private:
  76   /**
  77    * Get abduct internal.
  78    *
  79    * Get the next abduct from the internal subsolver d_subsolver. If
  80    * successful, this method returns true and sets abd to that abduct.
  81    *
  82    * This method assumes d_subsolver has been initialized to do abduction
  83    * problems.
  84    */
  85   bool getAbductInternal(Node& abd);
  86   /** The parent SMT engine */
  87   SmtEngine* d_parent;
  88   /** The SMT engine subsolver
  89    *
  90    * This is a separate copy of the SMT engine which is used for making
  91    * calls that cannot be answered by this copy of the SMT engine. An example
  92    * of invoking this subsolver is the get-abduct command, where we wish to
  93    * solve a sygus conjecture based on the current assertions. In particular,
  94    * consider the input:
  95    *   (assert A)
  96    *   (get-abduct B)
  97    * In the copy of the SMT engine where these commands are issued, we maintain
  98    * A in the assertion stack. To solve the abduction problem, instead of
  99    * modifying the assertion stack to remove A and add the sygus conjecture
 100    * (exists I. ...), we invoke a fresh copy of the SMT engine and leave the
 101    * assertion stack unchaged. This copy of the SMT engine can be further
 102    * queried for information regarding further solutions.
 103    */
 104   std::unique_ptr<SmtEngine> d_subsolver;
 105   /**
 106    * The conjecture of the current abduction problem. This expression is only
 107    * valid while the parent SmtEngine is in mode SMT_MODE_ABDUCT.
 108    */
 109   Node d_abdConj;
 110   /**
 111    * If applicable, the function-to-synthesize that the subsolver is solving
 112    * for. This is used for the get-abduct command.
 113    */
 114   Node d_sssf;
 115 };
 116
 117 }  // namespace smt
 118 }  // namespace CVC4
 119
 120 #endif /* CVC4__SMT__ABDUCTION_SOLVER_H */