src/preprocessing/passes/sygus_inference.h

   1 /*********************                                                        */
   2 /*! \file sygus_inference.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Mathias Preiner
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2021 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 SygusInference
  13  **/
  14
  15 #ifndef CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_
  16 #define CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_
  17
  18 #include <vector>
  19 #include "expr/node.h"
  20
  21 #include "preprocessing/preprocessing_pass.h"
  22
  23 namespace CVC4 {
  24 namespace preprocessing {
  25 namespace passes {
  26
  27 /** SygusInference
  28  *
  29  * A preprocessing utility that turns a set of (quantified) assertions into a
  30  * single SyGuS conjecture. If this is possible, we solve for this single Sygus
  31  * conjecture using a separate copy of the SMT engine. If sygus successfully
  32  * solves the conjecture, we plug the synthesis solutions back into the original
  33  * problem, thus obtaining a set of model substitutions under which the
  34  * assertions should simplify to true.
  35  */
  36 class SygusInference : public PreprocessingPass
  37 {
  38  public:
  39   SygusInference(PreprocessingPassContext* preprocContext);
  40
  41  protected:
  42   /**
  43    * Either replaces all uninterpreted functions in assertions by their
  44    * interpretation in a sygus solution, or leaves the assertions unmodified.
  45    */
  46   PreprocessingPassResult applyInternal(
  47       AssertionPipeline* assertionsToPreprocess) override;
  48   /** solve sygus
  49    *
  50    * Returns true if we can recast the input problem assertions as a sygus
  51    * problem and successfully solve it using a separate call to an SMT engine.
  52    *
  53    * We fail if either a sygus conjecture that corresponds to assertions cannot
  54    * be inferred, or the sygus conjecture we infer is infeasible.
  55    *
  56    * If this function returns true, then we add all uninterpreted symbols s in
  57    * assertions to funs and their corresponding solution to sols.
  58    */
  59   bool solveSygus(const std::vector<Node>& assertions,
  60                   std::vector<Node>& funs,
  61                   std::vector<Node>& sols);
  62 };
  63
  64 }  // namespace passes
  65 }  // namespace preprocessing
  66 }  // namespace CVC4
  67
  68 #endif /* CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ */