src/preprocessing/passes/sygus_abduct.h

   1 /*********************                                                        */
   2 /*! \file sygus_abduct.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-2019 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 Sygus abduction preprocessing pass, which transforms an arbitrary
  13  ** input into an abduction problem.
  14  **/
  15
  16 #ifndef CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H
  17 #define CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H
  18
  19 #include "preprocessing/preprocessing_pass.h"
  20 #include "preprocessing/preprocessing_pass_context.h"
  21
  22 namespace CVC4 {
  23 namespace preprocessing {
  24 namespace passes {
  25
  26 /** SygusAbduct
  27  *
  28  * A preprocessing utility that turns a set of quantifier-free assertions into
  29  * a sygus conjecture that encodes an abduction problem. In detail, if our
  30  * input formula is F( x ) for free symbols x, then we construct the sygus
  31  * conjecture:
  32  *
  33  * exists A. forall x. ( A( x ) => ~F( x ) )
  34  *
  35  * where A( x ) is a predicate over the free symbols of our input. In other
  36  * words, A( x ) is a sufficient condition for showing ~F( x ).
  37  *
  38  * Another way to view this is A( x ) is any condition such that A( x ) ^ F( x )
  39  * is unsatisfiable.
  40  *
  41  * A common use case is to find the weakest such A that meets the above
  42  * specification. We do this by streaming solutions (sygus-stream) for A
  43  * while filtering stronger solutions (sygus-filter-sol=strong). These options
  44  * are enabled by default when this preprocessing class is used (sygus-abduct).
  45  *
  46  * If the input F( x ) is partitioned into axioms Fa and negated conjecture Fc
  47  * Fa( x ) ^ Fc( x ), then the sygus conjecture we construct is:
  48  *
  49  * exists A. ( exists y. A( y ) ^ Fa( y ) ) ^ forall x. ( A( x ) => ~F( x ) )
  50  *
  51  * In other words, A( y ) must be consistent with our axioms Fa and imply
  52  * ~F( x ). We encode this conjecture using SygusSideConditionAttribute.
  53  */
  54 class SygusAbduct : public PreprocessingPass
  55 {
  56  public:
  57   SygusAbduct(PreprocessingPassContext* preprocContext);
  58
  59   /**
  60    * Returns the sygus conjecture corresponding to the abduction problem for
  61    * input problem (F above) given by asserts, and axioms (Fa above) given by
  62    * axioms. Note that axioms is expected to be a subset of asserts.
  63    *
  64    * The type abdGType (if non-null) is a sygus datatype type that encodes the
  65    * grammar that should be used for solutions of the abduction conjecture.
  66    */
  67   static Node mkAbductionConjecture(const std::vector<Node>& asserts,
  68                                     const std::vector<Node>& axioms,
  69                                     TypeNode abdGType);
  70
  71  protected:
  72   /**
  73    * Replaces the set of assertions by an abduction sygus problem described
  74    * above.
  75    */
  76   PreprocessingPassResult applyInternal(
  77       AssertionPipeline* assertionsToPreprocess) override;
  78 };
  79
  80 }  // namespace passes
  81 }  // namespace preprocessing
  82 }  // namespace CVC4
  83
  84 #endif /* CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H_ */